Email Gateway (Oct 11 2023 at 05:40): Email Gateway (Oct 11 2023 at 05:40):From: Gerwin Klein <cl-isabelle-users@lists.cam.ac.uk>
Coupled Similarity and Contrasimilarity, and How to Compute Them
by Benjamin Bisping and Luisa Montanari
We survey and extend characterizations of coupled similarity and contrasimilarityand prove properties relevant for algorithms computing their simulation preorders and equivalences.
Coupled similarity and contrasimilarity are two weak forms of bisimilarity for systems with internal behavior. They have outstanding applications in contexts where internal choices must transparently be distributed in time or space, for example, in process calculi encodings or in action refinements.
Our key contribution is to characterize the coupled simulation and contrasimulation preorders by reachability games. We also show how preexisting definitions coincide and that they can be reformulated using coupled delay simulations. We moreover verify a polynomial-time coinductive fixed-point algorithm computing the coupled simulation preorder. Through reduction proofs, we establish that deciding coupled similarity is at least as complex as computing weak similarity; and that contrasimilarity checking is at least as hard as trace inclusion checking.
https://www.isa-afp.org/entries/Coupledsim_Contrasim.html
Enjoy!
Gerwin
Last updated: Apr 28 2024 at 16:17 UTC