Enabling Preserving Bisimulation Equivalence

TL;DR

The paper introduces enabling preserving bisimilarity, a new semantic equivalence that maintains justness in process verification, addressing limitations of classical bisimilarity in liveness property analysis.

Contribution

It proposes enabling preserving bisimilarity, a finer equivalence that preserves justness and is a congruence for standard process operators.

Findings

Enabling preserving bisimilarity is justness-preserving.

It is a congruence for all standard operators, including parallel composition.

Addresses limitations of classical bisimilarity in liveness verification.

Abstract

Most fairness assumptions used for verifying liveness properties are criticised for being too strong or unrealistic. On the other hand, justness, arguably the minimal fairness assumption required for the verification of liveness properties, is not preserved by classical semantic equivalences, such as strong bisimilarity. To overcome this deficiency, we introduce a finer alternative to strong bisimilarity, called enabling preserving bisimilarity. We prove that this equivalence is justness-preserving and a congruence for all standard operators, including parallel composition.