A short proof of correctness of the quasi-polynomial time algorithm for parity games

Parity games

A parity game is given by a directed graph $(V,E)$, a starting node $s\in V$, a function which attaches to each $v\in V$ a priority $\operatorname{pty}(v)$ from a set $\{1,2,...,m\}$; the main parameter of the game is $n$, the number of nodes, and the second parameter is $m$. Two players Anke and Boris move alternately in the graph with Anke moving first. A move from a node $v$ to another node $w$ is valid if $(v,w)$ is an edge in the graph; furthermore, it is required that from every node one can make at least one valid move. The alternate moves by Anke and Boris define an infinite sequence of nodes which is called a play. Anke wins a play through nodes $v_{0},v_{1},\cdots$ iff $\limsup_{t}\operatorname{pty}(v_{t})$ is even, otherwise Boris wins the play.

We say that a player wins the parity game if she has a strategy which guarantees the play to be winning for her. Parity games are determined thus either Anke or Boris wins the parity game.

Statistics

The core of the algorithm of Calude et al. is to keep track of statistics about the game, in the form of partial functions

The initial statistic is the empty statistic $f_{0}=\emptyset$, which is updated successively by all the priorities visited during the play, thus producing a sequence of statistics. The update of a statistic $f$ by a priority $c$ is performed by applying successively the following two rules.

Type I update: If $c$ is even then it is inserted at the highest index $j\in 0\cdots k$ such that $f$ is defined and even on $0\ldots j-1$.

Type II update: If $\operatorname{im}(f)$ contains at least one value $<c$ then $c$ is inserted at the highest index $j\in\operatorname{dom}(f)$ such that $f(j)<c$.

Applying both rules in succession ensures that the update of an increasing statistic is increasing. If rule II triggers an insertion then we say the update is a type II update. Notice that in this case, applying or not rule I in the first place does not change the result. If rule I triggers an insertion but rule II does not then we say the update is a type I update.

Anke (resp. Boris) wins the statistics game if she (resp. he) has a strategy to enforce (resp. to avoid) a visit to a statistic whose domain contains $k$. Similarly to the game of chess, statistics games are determined: either Anke or Boris has a winning strategy .

Correctness of the algorithm

Anke wins the parity game iff she wins the statistics games.

Since statistics games are determined, the direct implication follows from:

If Boris wins the statistics games, he wins the parity game.

Every play won by Boris in the statistics game is won by Boris in the parity game because $c=\limsup_{t}c_{t}$ is odd in every sequence of statistics updates $f_{0}\to_{c_{0}}f_{1}\to_{c_{1}}\ldots$ such that $\forall t\geq 0,k\not\in\operatorname{dom}(f_{t})$, the proof of which follows.

The converse implication (Corollary 1.13) relies on several crucial properties of statistics.

With every statistic $f$ is associated its counter value

In the sequel we fix a sequence $f_{0}\to_{c_{0}}f_{1}\ldots\to_{c_{N}}f_{N+1}$ of statistics updates. We will first give two lemmas that gives information on what can be said when an update of type 1 and 2, respectively, is used on a date.

For all $N$ if $f_{N}\rightarrow_{c_{N}}f_{N+1}$ is a type 1 update, then $\operatorname{bin}(f_{N})+1=\operatorname{bin}(f_{N+1})$

Fix a number $i>0$. Consider the smallest date $T$ such that $\operatorname{bin}(f_{T+1})\geq i$. Then the update on date $T$ is of type 1 and $\operatorname{bin}(f_{T+1})=i$

By minimality of $T$ we get that $\operatorname{bin}(f_{T})<i$ (because $\operatorname{bin}(f_{0})=0$). By Lemma 1.7, the update on date $T$ has type 1. By Lemma 1.5, we thus get that $\operatorname{bin}(f_{T+1})=i$.

Next, we define even factorization and then show that a long even factorization implies that Anke wins the parity game.

An even factorization of length $j$ is a sequence $0\leq t_{0}<\ldots<t_{j}$ such that for every $i\in 0\ldots j-1$, the maximum of $c_{t_{i}},c_{t_{i}+1},\ldots,c_{t_{i+1}-1}$ is even.

We next show that long even sequences exists.

For all $N$, there is an even factorization of length at least $\operatorname{bin}(f_{N})$.

If Anke wins the statistics game then she wins the parity game.

By definition of the statistics game, Anke can enforce the play to reach a statistic $f_{N+1}$ such that $k\in\operatorname{dom}(f_{N+1})$.

If $N$ is chosen minimal then $f_{N}\to_{c_{N}}f_{N+1}$ is an update of type 1 by Corollary 1.9 on entry $k$. Hence, $f_{N+1}$ is defined on $k$ and $f_{N+1}(k)$ is even. This implies that $\operatorname{bin}(f_{N+1})\geq 2^{k}$. According to Lemma 1.12, such a play has an even factorization $t_{0}<t_{1}<\ldots<t_{j}$ of length $\operatorname{bin}(f_{N+1})\geq 2^{k}$. Since $2^{k}$ is $>$ than twice the number of vertices, the play loops on the same vertex at some dates $t_{i}$ and $t_{i^{\prime}}$, while having the same current player, with $0\leq i<i^{\prime}\leq j$. By definition of even factorizations, the maximal priority on this loop is even. Thus Boris has no positional winning strategy in the parity game (because if he had followed it, no loop can have even maximal priority), and since parity games are positional , Boris has no winning strategy at all in the parity game.

Consider a fixed $N$. Let $x=\operatorname{bin}(f_{N})$. We will show that the following sequence $t_{1},\dots,t_{x}$ is an even factorization.

For ease of notation, let $t_{x+1}=N+1$ (note that $t_{x+1}$ is not part of the even factorization). For all $j\leq x$, let $t_{j}<t_{j+1}$ be the last date $T$ using rule 1 such that $\operatorname{bin}(f_{T+1})=j$.

Sequence is well-defined. This sequence is well-defined because (1) on the first date $T$ where $\operatorname{bin}(f_{T+1})\geq j$ we use rule 1 and $\operatorname{bin}(f_{T+1})=j$, by Corollary 1.9; and (2) $\operatorname{bin}(f_{t_{j+1}})=j$ (and hence a date $T<t_{j+1}$ exists where $\operatorname{bin}(f_{T+1})\geq j$), which is true for $j=x$ by definition of $t_{x+1}$ and otherwise follows from Lemma 1.5 because we use rule 1 on date $t_{j+1}$ for $j<x$.

Let $T^{\prime}\in\{T,\dots,t_{i+1}-1\}$ be the first date such that $\operatorname{bin}(f_{T^{\prime}+1})\geq i$. This is well-defined because we have that $\operatorname{bin}(f_{t_{i+1}})=i$ by Lemma 1.5 (since we use rule 1 on date $t_{i+1}$). Clearly $T^{\prime}>T$ since $\operatorname{bin}(f_{T+1})<i$ by Claim 1. This also implies that $\operatorname{bin}(f_{T^{\prime}})<i$. We must thus make an update on date $T^{\prime}$. We cannot make an update of type 1 on date $T^{\prime}$, because $\operatorname{bin}(f_{T^{\prime}})<i\leq\operatorname{bin}(f_{T^{\prime}+1})$ would then imply that $\operatorname{bin}(f_{T^{\prime}+1})=i$ by Lemma 1.5, which contradicts the choice of $t_{i}$ (since $t_{i}<T<T^{\prime}<t_{i+1}$ as noted). We next argue that the update on date $T^{\prime}$ cannot be of type 2 either which contradicts that an update have either type 1 or 2, shows that $c$ must be even and thus completes the proof of the lemma.

The update on date $T^{\prime}$ is not of type 2

Time complexity of solving statistics games

A reachability game $G$ is a tuple $(V,E,\top)$, where $V$ is a set of $n$ vertices and $E\subseteq V\times V$ is a set of $m$ edges. The vertex $\top\in V$ is a the target vertex. The play starts in some initial vertex $s$, player 1 and 2 alternatively select a vertex $u\in\{u\mid(v,u)\in E\}$. The play then continues to $u$. If the play is ever in $w$, the game ends and player 1 wins, otherwise player 2 wins.

If player $1$ has a strategy to ensure a win from some vertex $s$, then $s$ is called a winning vertex. The classical algorithm for reachability games $G$ is called backward induction and computes in time $O(m)$ the set of winning vertices.

Statistics game as a reachability game

Given a parity game $G=(V,E)$, with $M$ priorities, $n$ vertices and $m$ edges, let $k=\lceil\log(n+1)\rceil$ be the maximum index in the corresponding statistics game. Denote $S_{i,M}$ the set of statistics with $M$ priorities and $i$ being the highest possible index.

The corresponding statistics game is the reachability game with vertices $V\times S_{k-1,M}\cup\{\top\}$. For every edge $(v,u)\in E$ and statistic update $f\rightarrow_{\operatorname{pty}(u)}f^{\prime}$ with $k\not\in\operatorname{dom}(f)$, there is an edge from $(v,f)$ to $(u,f^{\prime})$ if $k\not\in\operatorname{dom}(f^{\prime})$ or to $w$ if $k\in\operatorname{dom}(f^{\prime})$.

A naïve upper complexity bound

According to Theorem 1.1, a vertex $s$ is winning in the parity game if and only if the vertex $(s,\emptyset)$ is winning in the statistics game.

The statistics game has $\leq n|S_{k-1,M}|+1$ vertices and $\leq m|S_{k-1,M}|$ edges and there is a naïve $(M+1)^{\lceil\log(n+1)\rceil}$ upper bound on $|S_{k-1,M}|$. This gives a first straightforward upper bound on the complexity of solving parity games:

Tighter upper complexity bounds

We give tighter upper complexity bounds, starting with some bounds on $|S_{i,M}|$ for all $i,M$.

Each increasing function $f:\{1,\dots,x\}\rightarrow\{1,\dots,y\}$ has a 1-to-1 correspondence with subsets of size $x$ of $\{1,\dots,x+y-1\}$ as follows: Let $S_{f}$ be the set $\{f(1),f(2)+1,\dots,f(x)+x-1\}$. Observe that since $f$ is increasing, $f(i)+i<f(i+1)+i+1$ for all $i$. Thus $S_{f}$ has exactly $x$ elements. On the other hand, every set $S=\{1\leq j_{0}<\dots<j_{x}\}$ corresponds to the function $f_{S}(z)=j_{z}-z+1$. The function $f_{S}$ is increasing because $j_{i}>j_{i-1}$ for all $i$. There are ${{x+y-1}\choose{x}}$ subsets of size $x$ of $\{1,\dots,x+y-1\}$.

A partial increasing function is a increasing function in its domain. For a fixed $i$, there are ${{x+1}\choose{i}}$ domains of size $i$. Since each domain of size $i$ corresponds to the domain $\{1,\dots,i\}$ we can apply Lemma 2.1 and see that there are ${{i+y-1}\choose{i}}$ increasing functions for a fixed domain of size $i$. Thus, there are $\sum_{i=0}^{x+1}{{x+1}\choose{i}}\cdot{{i+y-1}\choose{i}}$ increasing partial functions $f:\{0,\dots,x\}\rightarrow\{1,\dots,y\}$ in total.

Hence, the time complexity of backwards induction on the statistics game is

Given a parity game with $n$ vertices, $m$ actions and max priority $M$, the winner of each initial vertex can be found in time

Especially, for $M\geq\epsilon\log^{2}n$, for some constant $\epsilon>0$, the winner can be found in $O(m\cdot n^{1.4427...}n^{\log(1+\frac{M}{\log n})}\cdot(1+\frac{M}{\log n}))$ time.

For $M=\log n$, the winner can be found in time $O\left(mn^{\log\frac{\sqrt{2}+1}{\sqrt{2}-1}}\right)=O(mn^{2.5431...})$.

We will give an upper bound on $O\left(m\sum_{i=0}^{k}{{k}\choose{i}}\cdot{{i+M-1}\choose{i}}\right)$.

Let $g(i)={{k}\choose{i}}\cdot{{i+M-1}\choose{i}}$. For $i=k$ we have that

Observe that $2^{k}=2^{\lceil{\log(n+1)}\rceil}<2^{\log(n+1)+1}=2(n+1)$.

A trivial bound on ${{y}\choose{x}}$ for all $x,y$ is $y^{x}/x!$. We thus get using Stirling’s approximation that

We first consider the case where $M\geq\epsilon k^{2}$ for some constant $\epsilon>0$. Observe that $g(k)$ is a factor $\epsilon$ of $g(k-1)$ for this choice of $M$. Also, for $0<i<k$ we have that $g(i)/g(i-1)>(k-i)\epsilon$. Thus, $g(i)$ is decreasing geometrically (with a constant factor of at most $1/\epsilon$) for $k-1/\epsilon>i$ and increasing below that. But, $1/\epsilon$ is a constant and thus, $\sum_{i=0}^{k}g(i)$ is $O(g(k))=O({{k-1+M}\choose{k}})=O(k^{-1/2}\cdot n^{\log e+\log(1+(M-1)/k)}\cdot(1+\frac{M-1}{\log n}))$. Hence, the time complexity is $O(m\log^{-1/2}n\cdot n^{1.4427...}n^{\log(1+\frac{M-1}{\log n})}\cdot(1+\frac{M-1}{\log n}))$ in this case.

Next we consider smaller values of $M\geq k+1$. Note that ${{y}\choose{x}}$ is geometrically increasing for a fixed $y$ for $x<y/2$ and geometrically decreasing for $x>y/2$. Also, ${{y}\choose{y/2}}\approx 2^{y}/\sqrt{y}$.

Note that the above argument basically finds the maximum of ${{k}\choose{i}}$ and ${{i-1+M}\choose{i}}$ independently, i.e. without using that it is the same $i$. Thus, one can give better bounds for especially specific values of $M$ as a function of $k$. We see that $g(i)$ keeps increasing until $g(i)/g(i-1)\leq 1$. Let $i_{*}$ be the smallest such $i$.

We then get an upper bound on $O(m|S_{k-1,M}|)$ of

This bound is accurate upto a factor of $k=O(\log n)$.

Thus, for instance, for $M=k+1$, we have that $i_{*}=\frac{k}{\sqrt{2}}$. Inserting this into $O(m\cdot kg(i_{*}))$ we get that

where we used Stirling’s approximation for the inequality. We next consider the exponent of $e$.

Inserting it back into the earlier expression, we get that the time complexity is

References