A Lean-Congruence Format for EP-Bisimilarity

TL;DR

This paper introduces a new format for defining ep-bisimilarity in process algebras, ensuring it is a congruence and suitable for recursive definitions, thus advancing the formal verification of concurrent systems.

Contribution

It extends the De Simone format to incorporate successor relations, establishing ep-bisimilarity as a congruence and a lean congruence for recursion in enriched languages.

Findings

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

The new format supports inductive definitions of successor relations.

Ep-bisimilarity is a lean congruence for recursion.

Abstract

Enabling preserving bisimilarity is a refinement of strong bisimilarity, which 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.