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 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.
Parity games lie in the third level of the Borel hierarchy, and are consequently determined.
[2] The Knaster–Tarski theorem leads to a relatively simple proof of determinacy of parity games.
[3][4][5] 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 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,[6] as well as in QP (quasipolynomial time).
[7] 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
, such that the resulting subgraph has the property that in each cycle the largest occurring color is even.
Zielonka outlined a recursive algorithm that solves parity games.
are the sets of nodes belonging to player 0 resp.
Zielonka's algorithm is based on the notation of attractors.
It can be defined by a fix-point computation: In other words, one starts with the initial set U.
) one adds all nodes belonging to player 0 that can reach the previous set (
) with a single edge and all nodes belonging to player 1 that must reach the previous set (
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).
by recursion and obtain a pair of winning sets
We again solve it by recursion and obtain a pair of winning sets
In simple pseudocode, the algorithm might be expressed as this: A slight modification of the above game, and the related graph-theoretic problem, makes solving the game NP-hard.
Parity is the special case where every vertex has a single color.
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 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 2i, and no node with color 2i + 1...
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.
Two state-of-the-art parity game solving toolsets are the following:
