Parity 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,^[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 ${\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 ${\displaystyle V_{0}}$, 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. Let ${\displaystyle G=(V,V_{0},V_{1},E,\Omega )}$ be a parity game, where ${\displaystyle V_{0}}$ resp. ${\displaystyle V_{1}}$ are the sets of nodes belonging to player 0 resp. 1, ${\displaystyle V=V_{0}\cup V_{1}}$ is the set of all nodes, ${\displaystyle E\subseteq V\times V}$ is the total set of edges, and ${\displaystyle \Omega :V\rightarrow \mathbb {N} }$ is the priority assignment function.

Zielonka's algorithm is based on the notation of attractors. Let ${\displaystyle U\subseteq V}$ be a set of nodes and ${\displaystyle i=0,1}$ be a player. The i-attractor of U is the least set of nodes ${\displaystyle Attr_{i}(U)}$ containing U such that i can force a visit to U from every node in ${\displaystyle Attr_{i}(U)}$. It can be defined by a fix-point computation:

${\displaystyle {\begin{aligned}Attr_{i}(U)^{0}&:=U\\Attr_{i}(U)^{j+1}&:=Attr_{i}(U)^{j}\cup \{v\in V_{i}\mid \exists (v,w)\in E:w\in Attr_{i}(U)^{j}\}\cup \{v\in V_{1-i}\mid \forall (v,w)\in E:w\in Attr_{i}(U)^{j}\}\\Attr_{i}(U)&:=\bigcup _{j=0}^{\infty }Attr_{i}(U)^{j}\end{aligned}}}$

In other words, one starts with the initial set U. Then, for each step (${\displaystyle Attr_{i}(U)^{j+1}}$) one adds all nodes belonging to player 0 that can reach the previous set (${\displaystyle Attr_{i}(U)^{j}}$) with a single edge and all nodes belonging to player 1 that must reach the previous set (${\displaystyle Attr_{i}(U)^{j}}$) 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 p be the largest one and let ${\displaystyle i=p{\bmod {2}}}$ be the player associated with the priority. Let ${\displaystyle U=\{v\mid \Omega (v)=p\}}$ be the set of nodes with priority p and let ${\displaystyle A=Attr_{i}(U)}$ be the corresponding attractor of player i. Player i can now ensure that every play that visits A infinitely often is won by player i.

Consider the game ${\displaystyle G'=G\setminus A}$ in which all nodes and affected edges of A are removed. We can now solve the smaller game ${\displaystyle G'}$ by recursion and obtain a pair of winning sets ${\displaystyle W'_{i},W'_{1-i}}$. If ${\displaystyle W'_{1-i}}$ is empty, then so is ${\displaystyle W_{1-i}}$ for the game G, because player ${\displaystyle 1-i}$ can only decide to escape from ${\displaystyle W_{i}'}$ to A which also results in a win for player i.

Otherwise, if ${\displaystyle W'_{1-i}}$ is not empty, we only know for sure that player ${\displaystyle 1-i}$ can win on ${\displaystyle W'_{1-i}}$ as player i cannot escape from ${\displaystyle W'_{1-i}}$ to A (since A is an i-attractor). We therefore compute the attractor ${\displaystyle B=Attr_{1-i}(W'_{1-i})}$ and remove it from G to obtain the smaller game ${\displaystyle G''=G\setminus B}$. We again solve it by recursion and obtain a pair of winning sets ${\displaystyle W''_{i},W''_{1-i}}$. It follows that ${\displaystyle W_{i}=W''_{i}}$ and ${\displaystyle W_{1-i}=W''_{1-i}\cup B}$.

In simple pseudocode, the algorithm might be expressed as this:

function ${\displaystyle solve(G)}$
    p := maximal priority in G
    if ${\displaystyle p=0}$
        return ${\displaystyle W_{0},W_{1}:=V,\{\}}$
    else
        U := nodes in G with priority p
        ${\displaystyle i:=p{\bmod {2}}}$
        ${\displaystyle A:=Attr_{i}(U)}$
        ${\displaystyle W_{0}',W_{1}':=solve(G\setminus A)}$
        if ${\displaystyle W_{1-i}'=\{\}}$
            return ${\displaystyle W_{i},W_{1-i}:=V,\{\}}$
        ${\displaystyle B:=Attr_{1-i}(W_{1-i}')}$
        ${\displaystyle W_{0}'',W_{1}'':=solve(G\setminus B)}$
        return ${\displaystyle W_{i},W_{1-i}:=W_{i}'',W_{1-i}''\cup B}$

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, and thus every vertex is colored by a set of colors instead of a single color. Accordingly, we say a vertex v has color j if the color j belongs to the color set of v. An infinite play is winning for player 0 if there exists i such that infinitely many vertices in the play have color 2i, yet finitely many have color 2i+1.

Note that as opposed to parity games, this game is no longer symmetric with respect to players 0 and 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.