A Game Characterization for Contrasimilarity

Benjamin Bisping
(Technische Universität Berlin)
Luisa Montanari
(Technische Universität Berlin)

We present the first game characterization of contrasimilarity, the weakest form of bisimilarity. The game is finite for finite-state processes and can thus be used for contrasimulation equivalence checking, of which no tool has been capable to date. A machine-checked Isabelle/HOL formalization backs our work and enables further use of contrasimilarity in verification contexts.

In Ornela Dardha and Valentina Castiglioni: Proceedings Combined 28th International Workshop on Expressiveness in Concurrency and 18th Workshop on Structural Operational Semantics (EXPRESS/SOS 2021), Paris, France (online event), 23rd August 2021, Electronic Proceedings in Theoretical Computer Science 339, pp. 27–42.
Published: 23rd August 2021.

ArXived at: https://dx.doi.org/10.4204/EPTCS.339.5 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org