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 complete the overview we develop coinductive characterisations of direct- and delayed simulation equivalence and we establish a lattice of equivalences for parity games.
Recommendations
- Solving parity games by a reduction to SAT
- Solving parity games in practice
- Generalized Parity Games
- A reduction from parity games to simple stochastic games
- A brief excursion to parity games
- Algorithms for Parity Games
- Algorithms for solving parity games
- Parameterized Algorithms for Parity Games
- scientific article; zbMATH DE number 3062454
- Solving parity games in big steps
Cites work
- scientific article; zbMATH DE number 1670778 (Why is no real title available?)
- scientific article; zbMATH DE number 177845 (Why is no real title available?)
- scientific article; zbMATH DE number 1954381 (Why is no real title available?)
- scientific article; zbMATH DE number 1962853 (Why is no real title available?)
- scientific article; zbMATH DE number 1500523 (Why is no real title available?)
- A cure for stuttering parity games
- A deterministic subexponential algorithm for solving parity games
- A randomized subexponential algorithm for parity games
- Abstraction in fixpoint logic
- Advanced automata minimization
- An \(\mathcal O(m\log n)\) algorithm for computing stuttering equivalence and branching bisimulation
- Automata, logics, and infinite games. A guide to current research
- Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking
- Bisimulation, modal logic and model checking games
- Branching bisimilarity checking for PRS
- Branching bisimilarity is an equivalence indeed!
- Branching bisimulation games
- Büchi automata can have smaller quotients
- Characterizing finite Kripke structures in propositional temporal logic
- Combinatorial structure and randomized subexponential algorithms for infinite games
- Consistent consequence for Boolean equation systems
- Consistent correlations for parameterised Boolean equation systems with applications in correctness proofs for manipulations
- Deciding the unguarded modal \(\mu\)-calculus
- Deciding the winner in parity games is in \(\mathrm{UP}\cap\mathrm{co-UP}\)
- Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata
- Fatal Attractors in Parity Games
- Games for synthesis of controllers with partial observation.
- Infinite games on finitely coloured graphs with applications to automata on infinite trees
- Infinite games played on finite graphs
- Invariants for parameterised Boolean equation systems
- Liveness analysis for parameterised Boolean equation systems
- Nondeterministic controllers of nondeterministic processes
- On model checking for the \(\mu\)-calculus and its fragments
- On parity game preorders and the logic of matching plays
- On the Ehrenfeucht-Fraïssé game in theoretical computer science (extended abstract)
- Simulation Relations for Alternating Parity Automata and Parity Games
- Simulation-based minimization
- Solving Parity Games in Big Steps
- Solving parity games in practice
- Static Analysis Techniques for Parameterised Boolean Equation Systems
- Static analysis of parity games: alternating reachability under parity
Cited in
(10)- Dual reduction and elementary games
- Solving parity games by a reduction to SAT
- Generalized Parity Games
- A reduction from parity games to simple stochastic games
- Partial-order reduction for parity games with an application on parameterised Boolean equation systems
- Coalgebraic satisfiability checking for arithmetic \(\mu\)-calculi
- Parity to safety in polynomial time for pushdown and collapsible pushdown systems
- A cure for stuttering parity games
- On parity game preorders and the logic of matching plays
- scientific article; zbMATH DE number 5734580 (Why is no real title available?)
This page was built for publication: Parity game reductions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1656552)
