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. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.339.5 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |