A Game Characterization for Contrasimilarity
Computer Science and Game Theory
2021-08-25 v1 Logic in Computer Science
Abstract
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.
Cite
@article{arxiv.2108.10492,
title = {A Game Characterization for Contrasimilarity},
author = {Benjamin Bisping and Luisa Montanari},
journal= {arXiv preprint arXiv:2108.10492},
year = {2021}
}
Comments
In Proceedings EXPRESS/SOS 2021, arXiv:2108.09624