Parity game

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, resulting in a (possibly infinite) path, called the 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 formula_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 formula_2, 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 formula_3 be a parity game, where formula_2 resp. formula_5 are the sets of nodes belonging to player 0 resp. 1, formula_1 is the set of all nodes, formula_7 is the total set of edges, and formula_8 is the priority assignment function.
Zielonka's algorithm is based on the notation of attractors. Let formula_9 be a set of nodes and formula_10 be a player. The -attractor of is the least set of nodes formula_11 containing such that can force a visit to from every node in formula_11. It can be defined by a fix-point computation:
In other words, one starts with the initial set . Then, for each step (formula_14) one adds all nodes belonging to player 0 that can reach the previous set (formula_15) with a single edge and all nodes belonging to player 1 that must reach the previous set (formula_15) no matter which edge player 1 takes.
Zielonka's algorithm is based on a recursive descent on the number of priorities. If the maximal priority is 0, it is immediate to see that player 0 wins the whole game (with an arbitrary strategy). Otherwise, let be the largest one and let formula_17 be the player associated with the priority. Let formula_18 be the set of nodes with priority and let formula_19 be the corresponding attractor of player .
Player can now ensure that every play that visits infinitely often is won by player .
Consider the game formula_20 in which all nodes and affected edges of are removed. We can now solve the smaller game formula_21 by recursion and obtain a pair of winning sets formula_22. If formula_23 is empty, then so is formula_24 for the game , because player formula_25 can only decide to escape from formula_26 to which also results in a win for player .
Otherwise, if formula_23 is not empty, we only know for sure that player formula_25 can win on formula_23 as player cannot escape from formula_23 to (since is an -attractor). We therefore compute the attractor formula_31 and remove it from to obtain the smaller game formula_32. We again solve it by recursion and obtain a pair of winning sets formula_33. It follows that formula_34 and formula_35.
In simple pseudocode, the algorithm might be expressed as this:
 function formula_36
 := maximal priority in 
 if formula_37
 return formula_38
 else
 := nodes in with priority 
 formula_39
 formula_40
 formula_41
 if formula_42
 return formula_43
 formula_44
 formula_45
 return formula_46
Related games and their decision problems.
A slight modification of the above game, and the related graph-theoretic problem, makes solving the game NP-hard. The modified game has the Rabin acceptance condition.
Specifically, in the above bipartite graph scenario, the problem now is to determine if there
is 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 2"i", and no node with color 2"i" + 1...
Note that as opposed to parity games, this game is no longer symmetric with respect to players 0 and 1.
Relation with logic and automata theory.
Despite its interesting complexity theoretic status, parity game solving can be seen as the algorithmic backend to problems in automated verification and controller synthesis. The model-checking problem for the modal μ-calculus for instance is known to be equivalent to parity game solving. Also, decision problems like validity or satisfiability for modal logics can be reduced to parity game solving.
External links.
Two state-of-the-art parity game solving toolsets are the following:
Graph visualisation tool that can model and solve parity games: