TL;DR
This paper introduces a finite game characterization for contrasimilarity, enabling its use in verification and equivalence checking, supported by formalization in Isabelle/HOL.
Contribution
It provides the first finite game-based characterization of contrasimilarity and a formal Isabelle/HOL implementation for verification purposes.
Findings
Finite game characterization for contrasimilarity.
Enables practical equivalence checking for finite-state processes.
Formal proof in Isabelle/HOL supports correctness and future use.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
