Parity game

From Wikipedia, the free encyclopedia

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.

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[1]. Games related to parity games were implicitly used in Rabin's proof of decidability of second order theory of n successors, where determinacy of such games was proven[2]. Knaster-Tarski theorem leads to a relatively simple proof of determinacy of parity games[3].

Moreover, parity games are history-free determined[3][4], 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.

[edit] 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 V0, such that the resulting subgraph has the property that in each cycle the largest occurring color is even.

[edit] 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 there is a choice function selecting a single out-going edge from each vertex of V0, 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 2\cdot i, and no node with color 2\cdot i-1.

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

[edit] References

  1. ^ D. A. Martin: Borel determinacy, The Annals of Mathematics, Vol 102 No. 2 pp. 363-371 (1975)
  2. ^ Rabin, MO (1969). "Decidability of second order theories and automata on infinite trees". Trans. AMS 141: 1–35. doi:10.2307/1995086. 
  3. ^ a b E. 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
  4. ^ A. Mostowski: Games with forbidden positions, University of Gdansk, Tech. Report 78 (1991)
Languages