A Lean-Congruence Format for EP-Bisimilarity

TL;DR

This paper introduces a new format for defining ep-bisimilarity, a refined form of strong bisimilarity that preserves safety and liveness, by extending the De Simone format to handle concurrency relations.

Contribution

It extends the De Simone format to incorporate successor relations for ep-bisimilarity, proving it as a congruence and lean congruence across enriched languages.

Findings

Ep-bisimilarity is a congruence for enriched De Simone languages.

The new format effectively captures concurrency in bisimilarity.

Ep-bisimilarity preserves safety and liveness properties.

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.