Parity Game Reductions
S. Cranen, J.J.A. Keiren, T.A.C. Willemse

TL;DR
This paper explores equivalence relations like bisimulation and stuttering bisimulation to reduce the size of parity games, which are crucial in model checking but computationally expensive to solve.
Contribution
It provides detailed proofs that these relations are true equivalences, have unique quotients, and effectively approximate winning regions, along with game-based characterizations and a lattice of equivalences.
Findings
Bisimulation and stuttering bisimulation are proven to be equivalences.
These relations have unique quotients and approximate winning regions.
A lattice of equivalences for parity games is established.
Abstract
Parity games play a central role in model checking and satisfiability checking. Solving parity games is computationally expensive, among others due to the size of the games, which, for model checking problems, can easily contain vertices or beyond. Equivalence relations can be used to reduce the size of a parity game, thereby potentially alleviating part of the computational burden. We reconsider (governed) bisimulation and (governed) stuttering bisimulation, and we give detailed proofs that these relations are equivalences, have unique quotients and they approximate the winning regions of parity games. Furthermore, we present game-based characterisations of these relations. Using these characterisations our equivalences are compared to relations for parity games that can be found in the literature, such as direct simulation equivalence and delayed simulation equivalence. To…
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.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Logic, Reasoning, and Knowledge
