A parity game is played on a colored directed graph, where each node has been colored by a priority – one of (usually) finitely many natural numbers. Two players, 0 and 1, move a (single, shared) token along the edges of the graph. The owner of the node that the token falls on selects the successor node (does the next move). The players keep moving the token, resulting in a (possibly infinite) path, called a play. The winner of a finite play is the player whose opponent is unable to move. The winner of an infinite play is determined by the priorities appearing in the play. Typically, player 0 wins an infinite play if the largest priority that occurs infinitely often in the play is even. Player 1 wins otherwise. This explains the word "parity" in the title. Parity games lie in the third level of the Borel hierarchy, and are consequently determined. Games related to parity games were implicitly used in Rabin's proof of decidability of the monadic second-order theory of n successors (S2S for n = 2), where determinacy of such games was proven. The Knaster–Tarski theorem leads to a relatively simple proof of determinacy of parity games. Moreover, parity games are history-free determined. This means that if a player has a winning strategy then that player has a winning strategy that depends only on the current board position, and not on the history of the play.
Solving a game
Solving a parity game played on a finite graph means deciding, for a given starting position, which of the two players has a winning strategy. It has been shown that this problem is in NP and co-NP, more precisely UP and co-UP, as well as in QP (quasipolynomial time). It remains an open question whether this decision problem is solvable in PTime. Given that parity games are history-free determined, solving a given parity game is equivalent to solving the following simple looking graph-theoretic problem. Given a finite colored directed bipartite graph with n vertices V = V 0 ∪ V 1 {\displaystyle 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 {\displaystyle V_{0}} , such that the resulting subgraph has the property that in each cycle the largest occurring color is even.
Recursive algorithm for solving parity games Zielonka outlined a recursive algorithm that solves parity games. Let G = ( V , V 0 , V 1 , E , Ω ) {\displaystyle G=(V,V_{0},V_{1},E,\Omega )} be a parity game, where V 0 {\displaystyle V_{0}} resp. V 1 {\displaystyle V_{1}} are the sets of nodes belonging to player 0 resp. 1, V = V 0 ∪ V 1 {\displaystyle V=V_{0}\cup V_{1}} is the set of all nodes, E ⊆ V × V {\displaystyle E\subseteq V\times V} is the total set of edges, and Ω : V → N {\displaystyle \Omega :V\rightarrow \mathbb {N} } is the priority assignment function. Zielonka's algorithm is based on the notation of attractors. Let U ⊆ V {\displaystyle U\subseteq V} be a set of nodes and i = 0 , 1 {\displaystyle i=0,1} be a player. The i-attractor of U is the least set of nodes A t t r i ( U ) {\displaystyle Attr_{i}(U)} containing U such that i can force a visit to U from every node in A t t r i ( U ) {\displaystyle Attr_{i}(U)} . It can be defined by a fix-point computation:
… excerpt ends here. Continue reading the full article.
