A Lean-Congruence Format for EP-Bisimilarity

Abstract

Enabling preserving bisimilarity is a refinement of strong bisimilarity that preserves safety as well as liveness properties. To define it properly, labelled transition systems needed to be upgraded with a successor relation, capturing concurrency between transitions enabled in the same state. We enrich the well-known De Simone format to handle inductive definitions of this successor relation. We then establish that ep-bisimilarity is a congruence for the operators, as well as lean congruence for recursion, for all (enriched) De Simone languages.

In Proceedings EXPRESS/SOS2023, arXiv:2309.05788. A full version of this paper, enriched with two appendices, is available at arXiv:2308.16350

References in corpus (3)

• Analysing Mutual Exclusion using Process Algebra with Signals
• Progress, Fairness and Justness in Process Algebra
• A Lean-Congruence Format for EP-Bisimilarity

Cited by in corpus (1)

• A Lean-Congruence Format for EP-Bisimilarity