A Lean-Congruence Format for EP-Bisimilarity
Logic in Computer Science
2023-09-18 v1
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.
Keywords
Cite
@article{arxiv.2309.07933,
title = {A Lean-Congruence Format for EP-Bisimilarity},
author = {Rob van Glabbeek and Peter Höfner and Weiyou Wang},
journal= {arXiv preprint arXiv:2309.07933},
year = {2023}
}
Comments
In Proceedings EXPRESS/SOS2023, arXiv:2309.05788. A full version of this paper, enriched with two appendices, is available at arXiv:2308.16350