A parity game is played on a colored
directed graph
In mathematics, and more specifically in graph theory, a directed graph (or digraph) is a graph that is made up of a set of vertices connected by directed edges, often called arcs.
Definition
In formal terms, a directed graph is an ordered pa ...
, where each node has been colored by a priority – one of (usually) finitely many
natural numbers
In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and ordering (as in "this is the ''third'' largest city in the country").
Numbers used for counting are called ''cardinal n ...
. 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
A path is a route for physical travel – see Trail.
Path or PATH may also refer to:
Physical paths of different types
* Bicycle path
* Bridle path, used by people on horseback
* Course (navigation), the intended path of a vehicle
* Desire p ...
, 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 In mathematical logic, the Borel hierarchy is a stratification of the Borel algebra generated by the open subsets of a Polish space; elements of this algebra are called Borel sets. Each Borel set is assigned a unique countable ordinal number called ...
, and are consequently
determined.
Games related to parity games were implicitly used in
Rabin
Rabin is a List of Jewish surnames, Hebrew surname. It originates from the Hebrew word ''rav'' meaning Rabbi, or from the name of the specific Rabbi Abin I, Abin. The most well known bearer of the name was Yitzhak Rabin, prime minister of Israel ...
's
proof of
decidability of the
monadic second-order theory of ''n'' successors (
S2S for ''n'' = 2), where
determinacy
Determinacy is a subfield of set theory, a branch of mathematics, that examines the conditions under which one or the other player of a game has a winning strategy, and the consequences of the existence of such strategies. Alternatively and sim ...
of such games was
proven. The
Knaster–Tarski theorem leads to a relatively simple proof of determinacy of parity games.
[ E. A. Emerson and C. S. Jutla: Tree Automata, Mu-Calculus and Determinacy, IEEE Proc. Foundations of Computer Science, pp 368–377 (1991), ]
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
In computational complexity theory, co-NP is a complexity class. A decision problem X is a member of co-NP if and only if its complement is in the complexity class NP. The class can be defined as follows: a decision problem is in co-NP precisely ...
, 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
In computational complexity theory, P, also known as PTIME or DTIME(''n''O(1)), is a fundamental complexity class. It contains all decision problems that can be solved by a deterministic Turing machine using a polynomial amount of computation time ...
.
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
In the mathematical field of graph theory, a bipartite graph (or bigraph) is a graph whose vertices can be divided into two disjoint and independent sets U and V, that is every edge connects a vertex in U to one in V. Vertex sets U and V are ...
with ''n'' vertices , and ''V'' colored with colors from ''1'' to ''m'', is there a choice function selecting a single out-going edge from each vertex of , 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 be a parity game, where resp. are the sets of nodes belonging to player 0 resp. 1, is the set of all nodes, is the total set of edges, and is the priority assignment function.
Zielonka's algorithm is based on the notation of attractors. Let be a set of nodes and be a player. The -attractor of is the least set of nodes containing such that can force a visit to from every node in . It can be defined by a fix-point computation:
:
In other words, one starts with the initial set . Then, for each step () 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 () 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 be the player associated with the priority. Let be the set of nodes with priority and let be the corresponding attractor of player .
Player can now ensure that every play that visits infinitely often is won by player .
Consider the game in which all nodes and affected edges of are removed. We can now solve the smaller game by recursion and obtain a pair of winning sets . If is empty, then so is for the game , because player can only decide to escape from to which also results in a win for player .
Otherwise, if is not empty, we only know for sure that player can win on as player cannot escape from to (since is an -attractor). We therefore compute the attractor and remove it from to obtain the smaller game . We again solve it by recursion and obtain a pair of winning sets . It follows that and .
In simple pseudocode
In computer science, pseudocode is a plain language description of the steps in an algorithm or another system. Pseudocode often uses structural conventions of a normal programming language, but is intended for human reading rather than machine re ...
, the algorithm might be expressed as this:
function
:= maximal priority in
if
return
else
:= nodes in with priority
if
return
return
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
In computational complexity theory, NP-hardness ( non-deterministic polynomial-time hardness) is the defining property of a class of problems that are informally "at least as hard as the hardest problems in NP". A simple example of an NP-hard pr ...
. 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
In the mathematical theory of directed graphs, a graph is said to be strongly connected if every vertex is reachable from every other vertex. The strongly connected components of an arbitrary directed graph form a partition into subgraphs that a ...
) 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
In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software systems ...
problem for the modal μ-calculus In theoretical computer science, the modal μ-calculus (Lμ, Lμ, sometimes just μ-calculus, although this can have a more general meaning) is an extension of propositional modal logic (with many modalities) by adding the least fixed point opera ...
for instance is known to be equivalent to parity game solving. Also, decision problems like validity or satisfiability for modal logic
Modal logic is a collection of formal systems developed to represent statements about necessity and possibility. It plays a major role in philosophy of language, epistemology, metaphysics, and natural language semantics. Modal logics extend other ...
s can be reduced to parity game solving.
References
*
Further reading
* E. Grädel, W. Thomas, T. Wilke (Eds.) : ''Automata, Logics, and Infinite Games'', Springer LNCS 2500 (2003), {{ISBN, 3-540-00388-6
* W. Zielonka : ''Infinite games on finitely coloured graphs with applications to automata on infinite tree'', TCS, 200(1-2):135-183, 1998
External links
Two state-of-the-art parity game solving toolsets are the following:
PGSolver Collection
Oink
Game theory game classes
Finite model theory