Parity game reductions
From MaRDI portal
Publication:1656552
DOI10.1007/S00236-017-0301-XzbMATH Open1398.68337arXiv1603.06422OpenAlexW2311027344WikidataQ59514724 ScholiaQ59514724MaRDI QIDQ1656552FDOQ1656552
Authors: Sjoerd Cranen, Jeroen J. A. Keiren, T. A. C. Willemse 
Publication date: 10 August 2018
Published in: Acta Informatica (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1603.06422
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
Specification and verification (program logics, model checking, etc.) (68Q60) Games involving topology, set theory, or logic (91A44)
Cites Work
- Solving parity games in practice
- Characterizing finite Kripke structures in propositional temporal logic
- Automata, logics, and infinite games. A guide to current research
- Title not available (Why is that?)
- Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking
- Deciding the winner in parity games is in \(\mathrm{UP}\cap\mathrm{co-UP}\)
- On model checking for the \(\mu\)-calculus and its fragments
- Infinite games on finitely coloured graphs with applications to automata on infinite trees
- Infinite games played on finite graphs
- Title not available (Why is that?)
- Title not available (Why is that?)
- Solving Parity Games in Big Steps
- A randomized subexponential algorithm for parity games
- A deterministic subexponential algorithm for solving parity games
- Games for synthesis of controllers with partial observation.
- Branching bisimilarity is an equivalence indeed!
- Bisimulation, modal logic and model checking games
- Title not available (Why is that?)
- Nondeterministic controllers of nondeterministic processes
- Combinatorial structure and randomized subexponential algorithms for infinite games
- Simulation Relations for Alternating Parity Automata and Parity Games
- Title not available (Why is that?)
- Advanced automata minimization
- On the Ehrenfeucht-Fraïssé game in theoretical computer science (extended abstract)
- Static Analysis Techniques for Parameterised Boolean Equation Systems
- Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata
- Simulation-based minimization
- An \(\mathcal O(m\log n)\) algorithm for computing stuttering equivalence and branching bisimulation
- Fatal Attractors in Parity Games
- Branching bisimilarity checking for PRS
- Invariants for parameterised Boolean equation systems
- On parity game preorders and the logic of matching plays
- Static analysis of parity games: alternating reachability under parity
- Branching bisimulation games
- Consistent consequence for Boolean equation systems
- A cure for stuttering parity games
- Büchi automata can have smaller quotients
- Liveness analysis for parameterised Boolean equation systems
- Consistent correlations for parameterised Boolean equation systems with applications in correctness proofs for manipulations
- Deciding the unguarded modal \(\mu\)-calculus
- Abstraction in fixpoint logic
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
- Title not available (Why is that?)
Uses Software
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)
