Consistent correlations for parameterised Boolean equation systems with applications in correctness proofs for manipulations

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

8 Citations (Scopus)
1 Downloads (Pure)

Abstract

We introduce the concept of consistent correlations for parameterised Boolean equation systems (PBESs), motivated largely by the laborious proofs of correctness required for most manipulations in this setting. Consistent correlations focus on relating the equations that occur in PBESs, rather than their solutions. For a fragment of PBESs, consistent correlations are shown to coincide with a recently introduced form of bisimulation. Finally, we show that bisimilarity on processes induces consistent correlations on PBESs encoding model checking problems. We apply our theory to two example manipulations from the literature.
Original languageEnglish
Title of host publicationCONCUR 2010 - Concurrency Theory (21st International Conference, Paris, France, August 31-September 3, 2010. Proceedings)
EditorsP. Gastin, F. Laroussinie
Place of PublicationBerlin
PublisherSpringer
Pages584-598
ISBN (Print)978-3-642-15374-7
DOIs
Publication statusPublished - 2010

Publication series

NameLecture Notes in Computer Science
Volume6269
ISSN (Print)0302-9743

Fingerprint

Dive into the research topics of 'Consistent correlations for parameterised Boolean equation systems with applications in correctness proofs for manipulations'. Together they form a unique fingerprint.

Cite this