Parity game

Parity Games are (possibly) infinite games played on a graph by two players, 0 and 1. In such games, game positions are assigned priorities, i.e. natural numbers.

A play in a parity game is a maximal sequence of nodes following the transition relation. The winner of a finite play of a parity game is the player whose opponent is unable to move. The outcome of an infinite play is determined by the priorities of the occurring positions. Typically, player 0 wins an infinite play if the highest infinitely often occurring priority is even. Player 1 wins otherwise. Whence the name "parity".

Parity games lie in the third level of the borel hierarchy and are as such determined [D. A. Martin: Borel determinacy, The Annals of Mathematics, Vol 102 No. 2 pp. 363-371 (1975)] . Games related to parity games were implicitly used in Rabin'sproof of decidability of second order theory of n successors, where determinacy of such games was proven [cite journal|last = Rabin|first = MO|title= Decidability of second order theories and automata on infinite trees|journal = Trans. AMS|year=1969|pages=1–35|volume=141|doi= 10.2307/1995086] . Knaster-Tarski theorem leads to a relatively simple proof of determinacy of parity gamesE. A. Emerson and C. S. Jutla: Tree Automata, Mu-Calculus and Determinacy, IEEE Proc. Foundations of Computer Science, pp 368-377 (1991), ISBN 0-8186-2445-0] .

Moreover, parity games are history-free determined [A. Mostowski: Games with forbidden positions, University of Gdansk, Tech. Report 78 (1991)] , so that if a player has a winning strategy then she has a winning strategy which depends only on the board position, and not on the history of the play.

Decision Problem

The "decision problem" of a parity game played on a finite graph consists of deciding the winner of a play from a given position. It has been shown that this problem is in NP and Co-NP, as well as UP and co-UP. It remains an open question whether for any parity game the decision problem is solvable in PTime.

Given that parity games are history free determined, the decision problem can be seen as the following rather simple looking graph theory problem. Given a finite colored directed bipartite graph with "n" vertices $V\; =\; V\_0\; cup\; V\_1$, and "V" colored with colors from "1" to "m", is there a choice function selecting a single out-going edge from each vertex of $V\_0$, such that the resulting subgraph has the property that in each cycle the largest occurring color is even.

Related Games and Their Decision Problems

A slight modification of the above game, and the related graph-theoretic problem, makes the decision problem NP-hard. The modified game has the Rabin acceptance condition.Specifically, in the above bipartite graph decision problem, the problem now is to determine if thereis a choice function selecting a single out-going edge from each vertex of $V\_0$, such that the resulting subgraph has the property that in each cycle (and hence each strongly connected component) it is the case that there exists an "i" and a node with color $2cdot\; i$, and no node with color $2cdot\; i-1$.

Note that as opposed to parity games, this game is no more symmetric with respect to players 0 and 1.

References

* E. Grädel, W. Thomas, T. Wilke (Eds.) : [http://www-mgi.informatik.rwth-aachen.de/Misc/LNCS2500/ Automata, Logics, and Infinite Games] , Springer LNCS 2500 (2003), ISBN 3540003886
* Complexity Zoo: [http://qwiki.caltech.edu/wiki/Complexity_Zoo#np NP]

External links

Parity Game Solvers:
* [http://www.tcs.ifi.lmu.de/~mlange/pgsolver/ PGSolver Collection]