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

TL;DR

This paper provides a concise proof of correctness for a recently proposed quasi-polynomial time algorithm solving parity games, enhancing understanding of its reliability and theoretical foundation.

Contribution

It introduces a short, clear proof of correctness for the quasi-polynomial algorithm for parity games, simplifying validation of its correctness.

Findings

Proof confirms the algorithm's correctness

Simplifies understanding of the algorithm's validity

Supports the algorithm's theoretical soundness

Abstract

Recently Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li and Frank Stephan proposed a quasi-polynomial time algorithm for parity games. This paper proposes a short proof of correctness of their algorithm.

Equations

$$f:0\dots k\to 1\dots m.$$

$$\mathrm{bin}(f)=\sum _{j\in \mathrm{do}{\mathrm{m}}_{\text{even}}(f)}{2}^j.$$

$$\mathcal{O}\left(m(M+1{)}^{\lceil \log (n+1)\rceil }\right)\le \mathcal{O}\left(m{M}^{1+\log (n)}\right).$$

$$O(m|S_{k-1,M}|)=O\left(m\sum _{i=0}^k\left(\genfrac{}{}{0ex}{}{k}{i}\right)\cdot \left(\genfrac{}{}{0ex}{}{i+M-1}{i}\right)\right).$$

$$O\left(\min \left(m{n}^2{2}^M/\sqrt{M\log n},m{n}^{\mathrm{2.4427...}}{n}^{\log (1+\frac{M}{\log n})}\cdot \left(1+\frac{M}{\log n}\right)\right)\right).$$

$$g(k)$$

$$g(i)=\frac{k!}{i!(k-i)!}\cdot \frac{(i-1+M)!}{i!(M-1)!}=\frac{(k-i)(i-1+M)}{i^2}\cdot g(i-1).$$

$$g(k)$$

$$=1/2e^{k\ln (k+M-1)-(k+1/2)\ln k+k}=1/2e^{k(1-\ln k+\ln (k+M-1))-(\ln k)/2}$$

$$=1/2e^{k\ln ((e(k+M-1))/k)-(\ln k)/2}=k^{-1/2}\cdot (e(k+M-1)/k{)}^k$$

$$=k^{-1/2}\cdot (2(n+1){)}^{\log e+\log (1+(M-1)/k)}=O(k^{-1/2}\cdot n^{\mathrm{1.4427...}}{n}^{\log (1+\frac{M-1}{\log n})}\cdot (1+\frac{M-1}{\log n}))$$

$$O(m|S_{k-1,M}|)$$

$$=O\left(m\cdot 2^k/\sqrt{k}\left(\genfrac{}{}{0ex}{}{k-1+M}{\min (\frac{k-1+M}{2},k)}\right)\right)$$

$$=O\left(\min \left(m{n}^2{2}^M/\sqrt{M\log n},m{n}^{\mathrm{2.4427...}}{n}^{\log (1+\frac{M-1}{\log n})}\cdot (1+\frac{M-1}{\log n})\right)\right).$$

$$1\ge g(i_{\ast })/g(i_{\ast }-1)\iff 1\ge \frac{(k-i_{\ast })(i_{\ast }+M-1)}{i_{\ast }^2}$$

$$\iff$$

$$O(m\cdot \sum _{i=0}^{k}g(i))=O(m\cdot kg(i_{\ast })).$$

$$m\cdot kg(i_{\ast })$$

$$=m\cdot k\cdot \frac{k!}{i_{\ast }!(k-i_{\ast })!}\frac{(k+i_{\ast })!}{i_{\ast }!k!}=m\cdot k\cdot \frac{(k+i_{\ast })!}{(i_{\ast }!{)}^2(k-i_{\ast })!}$$

$$<m\cdot k\cdot e^{(k+i_{\ast }+1/2)\ln (k+i_{\ast })-(k+i_{\ast })-2((i_{\ast }+1/2)\ln (i_{\ast })-i_{\ast })-((k-i_{\ast }+1/2)\ln (k-i_{\ast })-(k-i_{\ast }))},$$

$$(k+i_{\ast }+1/2)\ln (k+i_{\ast })-(k+i_{\ast })-2((i_{\ast }+1/2)\ln (i_{\ast })-i_{\ast })$$

$$-((k-i_{\ast }+1/2)\ln (k-i_{\ast })-(k-i_{\ast }))$$

$$=$$

$$+1/2(\ln (k+i_{\ast })-2\ln (i_{\ast })-\ln (k-i_{\ast }))$$

$$=$$

$$O\left(m\cdot k\cdot e^{k(\ln (\frac{1+1/\sqrt{2}}{1-1/\sqrt{2}}))+1/2(\ln (\frac{1+1/\sqrt{2}}{k^2(1-1/\sqrt{2})}))}\right)$$

$$=O\left(m{n}^{\log \frac{\sqrt{2}+1}{\sqrt{2}-1}}\right)=O(m{n}^{\mathrm{2.5431...}})$$

Full text

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 [3] 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

[TABLE]

The integer $k$ is chosen such that $2^{k}$ is strictly larger than twice the number of vertices. The domain of $f$ is denoted $\operatorname{dom}(f)$ and its image $\operatorname{im}(f)$. We also let $\operatorname{dom_{\text{even}}}(f)=\{f(i)\text{ is even}|i\in\operatorname{im}(f)\}$. Statistics are assumed to be increasing, i.e. $\forall i,j\in\operatorname{dom}(f),(i\leq j\implies f(i)\leq f(j))\enspace$. A statistic $f$ can be modified by inserting a priority $c$ at an index $\ell$, which results in removing all pairs of index $\leq\ell$ from $f$ and adding the pair $(\ell,c)$.

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 [2].

1 Correctness of the algorithm

Theorem 1.1** (Calude et al).**

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

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

Lemma 1.2**.**

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

Proof 1.3**.**

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.

An easy case is when the sequence of statistics is ultimately constant equal to some $f$ then $f\to_{c}f$ thus $c$ is odd because an update by an even priority always performs an insertion. In the opposite case define $(\ell,d)$ the maximal pair (for the dichotomic order) inserted infinitely often. Since $d$ is inserted infinitely often then $d\leq\limsup_{t}c_{t}=c$. And $d\geq c$ otherwise $c$ would be inserted infinitely often at an index $\geq\ell$ which would contradict the maximality of $(\ell,d)$. Since $(\ell,c)$ is inserted infinitely often then it is removed infinitely often, let $(\ell^{\prime},c^{\prime})$ be a pair used infinitely often to remove $(\ell,c)$. Since $(\ell,c)$ is removed by the insertion of $(\ell^{\prime},c^{\prime})$ then $\ell\leq\ell^{\prime}$ hence $\ell=\ell^{\prime}$ by maximality of $\ell$. Since $(\ell^{\prime},c^{\prime})=(\ell,c^{\prime})\neq(\ell,c)$ then $c^{\prime}<c$ by maximality of $c$. Since $(\ell,c)$ is removed by the insertion of $(\ell^{\prime},c^{\prime})$ and $c^{\prime}<c$ then this insertion is necessarily performed by a type I update and since $\ell=\ell^{\prime}$ then $c$ is odd otherwise the insertion would occur at a higher index.

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

Definition 1.4** (Counter value).**

With every statistic $f$ is associated its counter value

[TABLE]

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.

Lemma 1.5**.**

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})$

Proof 1.6**.**

Let $\ell$ be the entry of the insertion in update $f_{N}\rightarrow_{c_{N}}f_{N+1}$. Then, $f_{N}(\ell)$ cannot be defined and even, because otherwise $\ell+1$ could also be chosen. Also, $f_{N+1}(\ell)$ is $c_{N}$ and thus even. On the other hand, since $f_{N}\rightarrow_{c_{N}}f_{N+1}$ is a type 1 update, we have for $j<\ell$ that $f_{N}(j)$ is defined and even and $f_{N+1}(j)$ is not defined. No index $>\ell$ changes on an insertion on index $\ell$. Hence, $\operatorname{bin}(f_{N+1})-\operatorname{bin}(f_{N+1})=2^{\ell}-(1+2+4+\dots+2^{\ell-1})=1$.

Next, the lemma about type 2 updates.

Lemma 1.7**.**

For all $N$ if there is an update of type 2 on $(\ell,c)$ at date $N$, then there is a $t<N$ such that

the update on date $t$ is of type 1 2. 2.

the statistics $f_{t+1}$ is equal to $f_{N+1}$ except that $f_{t+1}(\ell)\neq f_{N+1}(\ell)$ and $f_{t+1}(\ell)$ is even (implying that $\operatorname{bin}(f_{t+1})=\operatorname{bin}(f_{N+1})$ if $c$ is even and $\operatorname{bin}(f_{t+1})>\operatorname{bin}(f_{N+1})$ if $c$ is odd) 3. 3.

there are no insertions at index $\ell^{\prime}$ for any $\ell^{\prime}>\ell$ between date $t$ and $N$.

Also, $t<N$ is the last date such that there is a type 1 update at that date on index $\ell$.

Proof 1.8**.**

Let $t<N$ be the largest date such that there is a type 1 update at that date on index $\ell$. This is well-defined, since initially, $f_{0}=\emptyset$ and for the smallest $t^{\prime}$, such that $\ell\in f_{t^{\prime}+1}$, we must have that the update at date $t^{\prime}$ is a type 1 update (by definition). We see that both $f_{N+1}(i)$ and $f_{t+1}(i)$ are undefined for $i<\ell$ because of the updates on date $N$ and $t$ respectively. Also, for all $i>\ell$ such that $f_{t+1}(i)$ or $f_{N+1}(i)$ is defined, we have that both are defined and $f_{t+1}(i)=f_{N+1}(i)$. This is because, if an insertion $(\ell^{\prime},d)$ is performed for $\ell^{\prime}>\ell$ on a date $t^{\prime}$ between $t+1$ and $N$, we have that $f_{t^{\prime}+1}(\ell)$ becomes undefined and hence, there must be a date $>t^{\prime}$ such that $\ell$ is inserted again, which would use rule 1 and thus contradict the choice of $t$. Thus, the statistics match except that $f_{t+1}(\ell)<f_{N+1}(\ell)$ (because each later time we change index $\ell$ we use rule 2 and the entry thus increases). Also, $f_{t+1}(\ell)$ is even because the update on date $t$ is of type 1.

We also give a corollary.

Corollary 1.9**.**

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$

Proof 1.10**.**

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.

Definition 1.11** (Even factorizations).**

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.

Lemma 1.12**.**

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

Corollary 1.13**.**

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

Proof 1.14**.**

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 [3], Boris has no winning strategy at all in the parity game.

Proof 1.15** (Proof of Lemma 1.12).**

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$.*

Sequence is an even factorization.* Consider some fixed $i<x$. We will argue that the maximum priority $c$ in $c_{t_{i}},c_{t_{i}+1},\ldots,c_{t_{i+1}-1}$ is even. We will do so using contradiction, so assume that $c$ is odd. Let $T\in\{t_{i},t_{i}+1,\dots,t_{i+1}-1\}$ be the smallest date such that $c$ is seen on that date and let $\ell$ be the index changed on that date. Note that $T>t_{i}$, since we use rule 1 on date $t_{i}$ which requires an even number.*

Claim 1**.**

The number $\ell$ is well-defined and $\operatorname{bin}(f_{T+1})<i=\operatorname{bin}(f_{t_{i}+1})$.

Proof 1.16**.**

Let $\ell^{\prime}$ be the index inserted at date $t_{i}$. Let $\ell^{\prime\prime}$ be the largest index inserted at a date in $t_{i},\dots,T-1$. By definition of $\ell^{\prime\prime}$, we have that $f_{T}(\ell^{\prime\prime})$ is defined and by definition of $T$ and $c$ we have that $f_{T}(\ell^{\prime\prime})<c$. Thus, we can perform a type 2 insertion of $c$ at $\ell^{\prime\prime}$ and hence $\ell$ is well-defined. Thus, $f_{T+1}(i)$ is odd or undefined for $i\leq\ell$, and $\operatorname{dom_{\text{even}}}(f_{T+1})\cap\ell+1\dots k=\operatorname{dom_{\text{even}}}(f_{t_{i}+1})\cap\ell+1\dots k$ because no such entry has changed between those two dates. On the other hand $f_{t_{i}+1}(\ell^{\prime})$ is even since a rule 1 update was used on that index on that date.

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.

Claim 2**.**

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

Proof 1.17**.**

Assuming towards contradiction that rule 2 is used on date $T^{\prime}$. Let $(\ell^{\prime},c^{\prime})$ be the update performed on date $T^{\prime}$. Since $\operatorname{bin}(f_{T^{\prime}})<i\leq\operatorname{bin}(f_{T^{\prime}+1})$, we have that $c^{\prime}$ is even. We will argue that there can be no such $\ell^{\prime}$. Let $\ell^{\prime\prime}$ be the largest index changed between date $T$ and date $T^{\prime}$, both included. We thus have that $\ell^{\prime\prime}\geq\ell,\ell^{\prime}$. We can apply Lemma 1.7 and see that there is $t$ such that $t<T^{\prime}$ and such that $\operatorname{bin}(f_{j+1})=\operatorname{bin}(f_{T^{\prime}+1})$, because $c^{\prime}$ is even. We thus just need to argue that $t\geq T$ to contradict that $T^{\prime}$ is the first date in $\{T,\dots,t_{i+1}-1\}$ where $\operatorname{bin}(f_{T^{\prime}+1})\geq i$.

If $\bm{\ell^{\prime\prime}>\ell^{\prime}}$.* Note that this is especially the case if $\ell>\ell^{\prime}$. We see that $t\geq T$ because there is no insertion between date $t$ and $T^{\prime}$ at a higher index than $\ell^{\prime}$ by Lemma 1.7. This contradicts the choice of $T^{\prime}$.*

Otherwise, if $\bm{\ell^{\prime\prime}=\ell^{\prime}\geq\ell}$.* In this case $f_{T+1}(\ell^{\prime})$ is either not defined or at least $c$. This is because if $f_{T}(\ell^{\prime})$ was defined and smaller than $c$, then it would be changed on date $T$. We have that $f_{T^{\prime}}(\ell^{\prime})$ is defined and $<c^{\prime}\leq c$ because otherwise we could not use rule 2 on date $T^{\prime}$ and insert into $\ell^{\prime}$. Consider the first date $t^{\prime}\geq T$ such that $f_{t+1}(\ell^{\prime})$ is defined and $<c$. Hence $t^{\prime}\leq T^{\prime}$. To lower an entry or make it defined we must use rule 1 on that entry and thus, we use rule 1 on date $t^{\prime}$ on entry $\ell^{\prime}$. Hence $t^{\prime}\neq T^{\prime}$ (because we use rule 2 on date $T^{\prime}$) and thus $t^{\prime}<T^{\prime}$. But then $t\geq t^{\prime}\geq T$ because $t<T^{\prime}$ is the last date on which rule 1 was used on index $\ell^{\prime}$ by Lemma 1.7. This contradicts the choice of $T^{\prime}$.*

2 Time complexity of solving statistics games

Reachability 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:

[TABLE]

Tighter upper complexity bounds

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

Lemma 2.1**.**

Let $x,y\in\mathbb{Z}$. The number of increasing functions $f:\{1,\dots,x\}\rightarrow\{1,\dots,y\}$ is ${{x+y-1}\choose{x}}$

Proof 2.2**.**

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\}$.

Lemma 2.3**.**

Let $x,y\in\mathbb{Z}$. The number of increasing, partial functions $f:\{0,\dots,x\}\rightarrow\{1,\dots,y\}$ is $\sum_{i=0}^{x+1}{{x+1}\choose{i}}\cdot{{i+y-1}\choose{i}}$

Proof 2.4**.**

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

[TABLE]

Theorem 2.5**.**

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

[TABLE]

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...})$.

Proof 2.6**.**

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

[TABLE]

For $0<i<k$ we have that

[TABLE]

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

[TABLE]

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}$.

Thus, the time complexity is

[TABLE]

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$.

[TABLE]

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

[TABLE]

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

[TABLE]

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

[TABLE]

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

[TABLE]