Graph operations on parity games and polynomial-time algorithms
From MaRDI portal
Abstract: Parity games are games that are played on directed graphs whose vertices are labeled by natural numbers, called priorities. The players push a token along the edges of the digraph. The winner is determined by the parity of the greatest priority occurring infinitely often in this infinite play. A motivation for studying parity games comes from the area of formal verification of systems by model checking. Deciding the winner in a parity game is polynomial time equivalent to the model checking problem of the modal mu-calculus. Another strong motivation lies in the fact that the exact complexity of solving parity games is a long-standing open problem, the currently best known algorithm being subexponential. It is known that the problem is in the complexity classes UP and coUP. In this paper we identify restricted classes of digraphs where the problem is solvable in polynomial time, following an approach from structural graph theory. We consider three standard graph operations: the join of two graphs, repeated pasting along vertices, and the addition of a vertex. Given a class C of digraphs on which we can solve parity games in polynomial time, we show that the same holds for the class obtained from C by applying once any of these three operations to its elements. These results provide, in particular, polynomial time algorithms for parity games whose underlying graph is an orientation of a complete graph, a complete bipartite graph, a block graph, or a block-cactus graph. These are classes where the problem was not known to be efficiently solvable. Previous results concerning restricted classes of parity games which are solvable in polynomial time include classes of bounded tree-width, bounded DAG-width, and bounded clique-width. We also prove that recognising the winning regions of a parity game is not easier than computing them from scratch.
Recommendations
Cites work
- A deterministic subexponential algorithm for solving parity games
- Automata, logics, and infinite games. A guide to current research
- Clique-Width and Parity Games
- Computing crossing numbers in quadratic time
- DAG-Width and Parity Games
- Deciding the winner in parity games is in \(\mathrm{UP}\cap\mathrm{co-UP}\)
- Fast mu-calculus model checking when tree-width is bounded.
- Graph Classes: A Survey
- Graph minors XXIII. Nash-Williams' immersion conjecture
- Graph minors. XIII: The disjoint paths problem
- scientific article; zbMATH DE number 1670778 (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?)
- scientific article; zbMATH DE number 5585443 (Why is no real title available?)
- Infinite games on finitely coloured graphs with applications to automata on infinite trees
- Infinite games played on finite graphs
- Logic for Programming, Artificial Intelligence, and Reasoning
- Solving parity games in practice
- Strategy construction for parity games with imperfect information
- Time and parallelizability results for parity games with bounded treewidth
Cited in
(8)- The theory of universal graphs for games: past and future
- Parameterized Algorithms for Parity Games
- Parity Games on Graphs with Medium Tree-Width
- Parity in graph sharing games
- Parity games on undirected graphs
- Partial solvers for parity games: effective polynomial-time composition
- Deciding Parity Games in Quasi-polynomial Time
- A note on Lights-Out-puzzle: parity-state graphs
This page was built for publication: Graph operations on parity games and polynomial-time algorithms
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q906273)
