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.
|Title of host publication||CONCUR 2010 - Concurrency Theory (21st International Conference, Paris, France, August 31-September 3, 2010. Proceedings)|
|Editors||P. Gastin, F. Laroussinie|
|Place of Publication||Berlin|
|Publication status||Published - 2010|
|Name||Lecture Notes in Computer Science|