Solving parity games using an automata-based algorithm
From MaRDI portal
Abstract: Parity games are abstract infinite-round games that take an important role in formal verification. In the basic setting, these games are two-player, turn-based, and played under perfect information on directed graphs, whose nodes are labeled with priorities. The winner of a play is determined according to the parities (even or odd) of the minimal priority occurring infinitely often in that play. The problem of finding a winning strategy in parity games is known to be in UPTime CoUPTime and deciding whether a polynomial time solution exists is a long-standing open question. In the last two decades, a variety of algorithms have been proposed. Many of them have been also implemented in a platform named PGSolver. This has enabled an empirical evaluation of these algorithms and a better understanding of their relative merits. In this paper, we further contribute to this subject by implementing, for the first time, an algorithm based on alternating automata. More precisely, we consider an algorithm introduced by Kupferman and Vardi that solves a parity game by solving the emptiness problem of a corresponding alternating parity automaton. Our empirical evaluation demonstrates that this algorithm outperforms other algorithms when the game has a a small number of priorities relative to the size of the game. In many concrete applications, we do indeed end up with parity games where the number of priorities is relatively small. This makes the new algorithm quite useful in practice.
Recommendations
Cites work
- A Deterministic Subexponential Algorithm for Solving Parity Games
- Admissibility in Infinite Games
- Alternating tree automata, parity games, and modal -calculus
- An Accelerated Algorithm for 3-Color Parity Games with an Application to Timed Games
- An automata-theoretic approach to branching-time model checking
- An Optimal Strategy Improvement Algorithm for Solving Parity and Payoff Games
- Deciding the winner in parity games is in \(\mathrm{UP}\cap\mathrm{co-UP}\)
- Facets of Synthesis: Revisiting Church’s Problem
- Generalized mean-payoff and energy games
- scientific article; zbMATH DE number 1670778 (Why is no real title available?)
- scientific article; zbMATH DE number 3870578 (Why is no real title available?)
- scientific article; zbMATH DE number 3757688 (Why is no real title available?)
- scientific article; zbMATH DE number 1500523 (Why is no real title available?)
- scientific article; zbMATH DE number 1775458 (Why is no real title available?)
- Improved model checking of hierarchical systems
- Infinite games on finitely coloured graphs with applications to automata on infinite trees
- Module checking
- On promptness in parity games
- Polynomial-time under-approximation of winning regions in parity games
- Quantitative stochastic parity games
- Results on the propositional \(\mu\)-calculus
- Solving parity games by a reduction to SAT
- Solving Parity Games in Big Steps
- Solving parity games in practice
Cited in
(23)- Solving parity games via priority promotion
- A delayed promotion policy for parity games
- Improving parity games in practice
- Solving the parity problem in one-dimensional cellular automata
- Games for verification: Algorithmic issues
- Static analysis of parity games: alternating reachability under parity
- Algorithms for solving parity games
- A comparison of BDD-based parity game solvers
- A CSP-Based Approach for Solving Parity Game
- Simulation Relations for Alternating Parity Automata and Parity Games
- Solving parity games in practice
- Solving parity games by a reduction to SAT
- Algorithms for Parity Games
- scientific article; zbMATH DE number 1773090 (Why is no real title available?)
- Solving parity games via priority promotion
- A parity game tale of two counters
- Simple fixpoint iteration to solve parity games
- scientific article; zbMATH DE number 7455738 (Why is no real title available?)
- Deciding Parity Games in Quasi-polynomial Time
- On the Way to Alternating Weak Automata
- Register games
- Justifications and a reconstruction of parity game solving algorithms
- New algorithms for combinations of objectives using separating automata
This page was built for publication: Solving parity games using an automata-based algorithm
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2830208)
