An Ordered Approach to Solving Parity Games in Quasi Polynomial Time and Quasi Linear Space

Introduction

Parity games are two-player zero-sum games played on a finite graph. The two players, named even and odd, move a token around the graph until a cycle is formed. Each vertex is labelled with an integer colour, and the winner is determined by the parity of the largest colour that appears on the cycle: player even wins if it is an even colour, and player odd wins otherwise.

Parity games have been the focus of intense study , in part due to their practical applications. Solving parity games is the central and most expensive step in many model checking , satisfiability checking , and synthesis algorithms.

Parity games have also attracted attention due to their unusual complexity status. The problem of determining the winner of a parity game is known to lie in UP $\cap$ co-UP , so the problem is very unlikely to be NP-complete. However, despite much effort, no polynomial time algorithm has been devised for the problem. Determining the exact complexity of solving a parity game is a major open problem.

Three main classes of algorithms have been developed for solving parity games in practice. The recursive algorithm , which despite being one of the oldest algorithms has been found to be quite competitive in practice . Strategy improvement algorithms use a local search technique , similar to the simplex method for linear programming and policy iteration algorithms for solving Markov decision processes. Progress measure algorithms define a measure that captures the winner of the game, and then use value iteration techniques to find it . Each of these algorithms has inspired lines of further research, all of which have contributed to our understanding of parity games. Unfortunately, all of them are known to have exponential worst case complexity.

Recently, Calude et al. have provided a quasi-polynomial time algorithm for solving parity games that runs in time $O(n^{\lceil\log(c)+6\rceil})$, where $c$ denotes the number of priorities used in the game. Previously, the best known algorithm for parity games was a deterministic sub-exponential algorithm , which could solve parity games in $n^{O(\sqrt{n})}$ time, so this new result represents a significant advance in our understanding of parity games.

Their approach is to provide a compact witness that can be used to decide whether player even wins a play. Traditionally, one must store the entire history of a play, so that when the players construct a cycle, we can easily find the largest priority on that cycle. The key observation of Calude et al. is that a witness of poly-logarithmic size can be used instead. This allows them to simulate a parity game on an alternating Turing machine that uses poly-logarithmic space, which leads to a deterministic algorithm that uses quasi-polynomial time and space.

This new result has already inspired follow-up work. Jurdziński and Lazić have developed an adaptation of the classical small-progress measures algorithm that runs in quasi-polynomial time. Their approach is to provide a succinct encoding of a small-progress measure, which is very different from the succinct encoding developed by Calude et al. . The key advantage of using progress measures as a base for the algorithm is that it avoids the quasi-polynomial space requirement of the algorithm of Calude et al., instead providing an algorithm that runs in quasi-polynomial time and near linear space.

In this paper, we develop a progress-measure based algorithm for solving parity games that uses the succinct witnesses of Calude et al. . These witnesses were designed to be used in a forward manner, which means that they are updated as we move along a play of the game. Our key contribution is to show that these witnesses can also be used in a backwards manner, by processing the play backwards from a certain point. This allows us to formulate a value iteration algorithm that uses (backwards versions of) the witnesses of Calude et al. directly.

The outcome of this is to provide a second algorithm for parity games that runs in quasi-polynomial time and near linear space. We provide a comprehensive complexity analysis of this algorithm, which is more detailed than the one given Calude et al. for the original algorithm. In particular, we show that our algorithm provides

a quasi bi-linear running time for a fixed number of colours, $O(mn\log(n)^{c-1})$;

a quasi bi-linear FPT bound, e.g. $O(mn\mathfrak{a}(n)^{\log\log n})$, where any other quasi-constant function can be used to replace the inverse Ackermann function $\mathfrak{a}$; and

an improved upper bound for a high number of colours, $O(m\cdot h\cdot n^{c_{1.45}+\log_{2}(h)})$

for parity games with $m$ edges, $n$ vertices, and $c$ colours, where $h=\lceil 1+c/\log(n)\rceil$ and the constant $c_{1.45}=\log_{2}\mathsf{e}<1.45$. We also provide an argument that parity games with $O(\log n)$ colours can be solved in polynomial time.

The complexity bounds (1) of our algorithm only match the bounds for the algorithm of Jurdziński and Lazić , while (2) and (3) are new. Moreover, we believe that it is interesting that the witnesses of Calude et al. can be used in this way. The history of research into parity games has shown that ideas from the varying algorithms for parity games can often spur on further research. Our result and the work of Jurdziński and Lazić show that there are two very different ways of succinctly encoding the information that is needed to decide the winner in a parity game, and that both of them can be applied in value iteration algorithms. Moreover, implementing our progress measure is easier, as standard representations of the colours can be used. We have implemented our algorithm, and we provide some experimental results in the last section.

Finally, we present a lower bound for our algorithm, and for the algorithm of Calude et al. . We derive a family of examples upon which both of the algorithms achieve their worst case—quasi-polynomial—running time. These are simple single player games.

Preliminaries

A play $\langle v_{0},v_{1},\ldots\rangle$ is won by player even if $\limsup_{i\rightarrow\infty}\phi(v_{i})$ is even, by player odd if $\limsup_{i\rightarrow\infty}\phi(v_{i})$ is odd.

A strategy for player even is a function $\sigma:V^{*}V_{e}\rightarrow V$ such that \big{(}v,\sigma(\rho,v)\big{)}\in E for all $\rho\in V^{*}$ and $v\in V_{e}$. A strategy $\sigma$ is called memoryless if $\sigma$ only depends on the last state ($\sigma(\rho,v)=\sigma(\rho^{\prime},v)$ for all $\rho,\rho^{\prime}\in V^{*}$ and $v\in V_{e}$). A play $\langle v_{0},v_{1},\ldots\rangle$ is consistent with $\sigma$ if, for every initial sequence $\rho_{n}=v_{0},v_{1},\ldots,v_{n}$ of the play that ends in a state of player even ($v_{n}\in V_{e}$), $\sigma(\rho_{n})=v_{n+1}$ holds.

It is well known that the following conditions are equivalent: Player even wins the game starting at $v_{0}$ if she has a strategy $\sigma$ that satisfies that

all plays $\langle v_{0},v_{1},\ldots\rangle$ consistent with $\sigma$ satisfy $\limsup_{i\rightarrow\infty}\phi(v_{i})$ (i.e. the highest colour that occurs infinitely often in the play) is even;

all plays $\langle v_{0},v_{1},\ldots\rangle$ consistent with $\sigma$ contain a winning loop $v_{i},v_{i+1},\ldots,v_{i+k}$, that satisfies $v_{i}=v_{i+k}$ and $\phi(v_{i})\geq\phi(v_{i+j})$ for all natural numbers $j\leq k$;

as (1), and $\sigma$ must be memoryless; or

We use different criteria in the technical part, choosing the one that is most convenient.

QP Algorithms

We discuss a variation of the algorithm of Calude et al. .

In a nutshell, the algorithm keeps a data structure, the witnesses, that encodes the existence of sequences of “good” events. This intuitively qualifies witnesses as a measure of progress in the construction of a winning cycle. This intuition does not fully hold, as winning cycles are not normally identified immediately, but it gives a good intuition of the guarantees the data structure provides.

In , witnesses are used to track information in an alternating machine. As they are quite succinct (they have only logarithmically many entries in the number of vertices of the game, and each entry only requires logarithmic space in the number of colours), this entails the quasi-polynomial complexity.

We have made this data structure accessible for value iteration, using it in a similar way as classical progress measures. This requires a—simple—argument that witnesses can be used in a backward analysis of a run just as well as in a forward analysis. This, in turn, requires a twist in the updating rule that allows for rational decisions. For this, we equip the data structure with an order, and show that the same game is still won by the same player if the antagonist can increase the value in every step.

Let $\rho=v_{1},v_{2},\dots,v_{m}$ be a prefix of a play of the parity game. An $i$-witness is a sequence of (not necessarily consecutive) positions of $\rho$

of length exactly $2^{i}$, that satisfies the following properties:

Position: Each $p_{j}$ specifies a position in the play $\rho$, so each $p_{j}$ is an integer that satisfies $1\leq p_{j}\leq m$.

Order: The positions are ordered. So we have $p_{j}<p_{j+1}$ for all $j<2^{i}$.

Evenness: All positions other than the final one are even. Formally, for all $j<2^{i}$ the colour $\phi(v_{p_{j}})$ of the vertex in position $p_{j}$ is even.

Inner domination: The colour of every vertex between $p_{j}$ and $p_{j+1}$ is dominated by the colour of $p_{j}$, or the colour of $p_{j+1}$. Formally, for all $j<2^{i}$, the largest colour of any vertex in the subsequence $v_{p_{j}},v_{(p_{j})+1},\ldots,v_{p_{(j+1)}}$ is less than or equal to \max\big{\{}\phi(v_{p_{j}}),\phi(v_{p_{j+1}})\big{\}}.

Outer domination: The colour of $p_{2^{i}}$ is greater than or equal to the colour of every vertex that appears after $p_{2^{i}}$ in $\rho$. Formally, for all $k$ in the range $p_{2^{i}}<k\leq m$, we have that $\phi(v_{k})\leq\phi(v_{p_{2^{i}}})$.

Witnesses

We define $C_{\_}=C\cup\{\_\}$ to be the set of colours augmented with the $\_$ symbol. A witness is a sequence

of length $k+1$—we will later see that $k=\lfloor\log_{2}(e)\rfloor$ is big enough, where $e$ is the number of vertices with an even colour—where each element $b_{i}\in C_{\_}$, and that satisfies the following properties.

Witnessing. There exists a family of $i$-witnesses, one for each element $b_{i}$ with $b_{i}\neq\_$. We refer to such an $i$-witness in the run $\rho$. We will refer to this witness as

Dominating colour. For each $b_{j}\neq\_$, we have that $b_{j}=\phi(v_{p_{i,2^{i}}})$. In other words, $b_{j}$ is the outer domination colour of the $i$-witness.

Ordered sequences. The $i$-witness associated with $b_{i}$ starts after $j$-witness associated with $b_{j}$ whenever $i<j$. Formally, for all $i$ and $j$ with $i<j$, if $b_{i}\neq\_$ and $b_{j}\neq\_$, then $p_{j,2^{j}}<p_{i,1}$.

It should be noted that the $i$-witnesses associated with each position $b_{i}$ are not stored in the witness, but in order for a sequence to be a witness, the corresponding $i$-witnesses must exist.

Observe that the dominating colour property combined with the ordered sequences property imply that the colours in a witness are monotonically increasing, since each colour $b_{j}$ (weakly) dominates all colours that appear afterwards in $\rho$.

Forwards and backwards witnesses.

So far, we have described forwards witnesses, which were introduced in . In this paper, we introduce the concept of a backwards witnesses, and an ordering over these witnesses, which will be used in our main result. For each play $\rho=v_{1},v_{2},\dots,v_{m}$, we define the reverse play $\overleftarrow{\rho}=v_{m},v_{m-1},\dots,v_{1}$. A backwards witness is a witness for $\overleftarrow{\rho}$, or for an initial sequence of it.

Order on witnesses.

We first introduce an order $\succeq$ over the set $C_{\_}$ that captures the following requirements: even numbers are better than odd numbers, and all numbers are better than $\_$. Among the even numbers, higher numbers are better than smaller ones, while among the odd numbers, smaller numbers are better than higher numbers. Formally, $b\succeq c$ if either $c=\_\,$; or if $c$ is odd and $b$ is either odd and $b\leq c$ holds, or $b$ is even; or $c$ is even and $b$ is even and $b\geq c$ holds.

Then, we define an order $\sqsupseteq$ over witnesses. This order compares two witnesses lexicographically, starting from $b_{k}$ and working downwards, and for each individual position the entries are compared using $\succeq$. We also define a special witness $\mathsf{won}$ which is $\sqsupseteq$ than any other witness.

The value of a witness.

An even chain of length $m$ is a sequence of positions $p_{1}<p_{2}<p_{3}<\ldots<p_{m}$ (with $0\leq p_{0}$ and $p_{m}\leq n$) in $\rho$ that has the following properties:

for all $j\leq m$, we have that $\phi(v_{p_{j}})$ is even, and

for all $j<m$ the colours in the subsequence defined by $p_{j}$ and $p_{j+1}$ are less than or equal to $\phi(p_{j})$ or $\phi(p_{j+1})$. More formally, we have that all colours $\phi(v_{p_{j}}),\phi(v_{(p_{j})+1}),\ldots,\phi(v_{p_{(j+1)}})$ are less than or equal to \max\big{\{}\phi(v_{p_{j}}),\phi(v_{p_{j+1}})\big{\}}.

For each witness $\mathbf{b}=b_{k},b_{k-1},\ldots,b_{0}$, we define the function $\mathsf{even}(\mathbf{b},i)=1$ if $b_{i}\neq\_$ and $b_{i}$ is even. Then we define the value of the witness $\mathbf{b}$ to be $\mathsf{value}(\mathbf{b})=\sum_{i=0}^{k}2^{i}\cdot\mathsf{even}(\mathbf{b},i)$. We can show that the value $\mathbf{b}$ corresponds to the length of an even chain in $\rho$ that is witnessed by $\mathbf{b}$.

If $\mathbf{b}$ is a (forward or backward) witness of $\rho$, then there is an even chain of length $\mathsf{value}(\mathbf{b})$ in $\rho$.

Let $i$ be an index such that $\mathsf{even}(\mathbf{b},i)=1$. By definition, the $i$-witness $p_{i,1},p_{i,2},\dots,p_{i,2^{i}}$ is an even chain of length $2^{i}$ in $\rho$. This holds irrespective of whether $\mathbf{b}$ is a forward or backward witness.

Then, given an index $j>i$ such that $\mathsf{even}(\mathbf{b},j)=1$, observe that the outer domination property ensures that $\phi(p_{i,2^{i}})\geq\phi(v_{l})$ for all $l$ in the range $p_{i,2^{i}}\leq l\leq p_{j,1}$. So, when we concatenate the $i$-witness with the $j$-witness we still obtain an even chain. Thus, $\rho$ must contain an even chain of length $\mathsf{value}(\mathbf{b})$.

Let $e=|\{v\in V\;:\;\phi(v)\text{ is even }\}|$ be the number of vertices with even colours in the game. Observe that, if we have an even chain whose length is strictly greater than $e$, then $\rho$ must contain a cycle, since there must be a vertex with even colour that has been visited twice. Moreover, the largest priority on this cycle must be even, so this is a winning cycle for player even. Thus, for player even to win the parity game, it is sufficient for him to force a play that has a witness whose value is strictly greater than $e$.

If, from an initial state $v_{0}$, player even can force the game to run through a sequence $\rho$, such that $\rho$ has a (forwards or backwards) witness $\mathbf{b}$ such that $\mathsf{value}(\mathbf{b})$ is greater than the number of vertices with even colour, then player even wins the parity game starting at $v_{0}$.

1 Updating forward witnesses

We now show how forward witnesses can be constructed incrementally by processing the play one vertex at a time. Throughout this subsection, we will suppose that we have a play $\rho=v_{0},v_{1},\dots,v_{m}$, and a new vertex $v_{m+1}$ that we would like to append to $\rho$ to create $\rho^{\prime}$. We will use $d=\phi(v_{m+1})$ to denote the colour of this new vertex. We will suppose that $\mathbf{b}=b_{k},b_{k-1},\ldots,b_{1},b_{0}$ is a witness for $\rho$, and we will construct a witness $\mathbf{c}=c_{k},c_{k-1},\ldots,c_{1},c_{0}$ for $\rho^{\prime}$.

We present three lemmas that allow us to perform this task.

Suppose that there exists an index $j$ such that $b_{i}$ is even for all $i<j$, and that $b_{i}\geq d$ or $b_{i}=\_$ for all $i>j$. If we set $c_{i}=b_{i}$ for all $i>j$, $c_{j}=d$, and $c_{i}=\_$ for all $i<j$, then $\mathbf{c}$ is a witness for $\rho^{\prime}$.

For the indices $i>j$, observe that since $b_{i}\geq d$, the outer domination of the corresponding $i$-witnesses continues to hold. For the indices $i<j$, since we set $c_{i}=\_$ there are no conditions that need to be satisfied.

To complete the proof, we must argue that there is a $j$-witness that corresponds to $c_{j}$. This witness is obtained by concatenating the $i$-witnesses corresponding to the numbers $b_{i}$ for $i<j$, and then adding the vertex $v_{m+1}$ as the final position. This produces a sequence of length $1+\sum_{i=0}^{j-1}2^{i}=2^{j}$ as required. Since all $b_{i}$ with $i<j$ were even, the evenness condition is satisfied. For inner domination, observe that the outer domination of each $i$-witness ensures that the gaps between the concatenated sequences are inner dominated, and the fact that $b_{0}$ dominates sequence $v_{p_{0,1}},\ldots,v_{m}$ ensures that the final subsequence is also dominated by $b_{0}$ or $d$. Outer domination is trivial, since $v_{m+1}$ is the last vertex in $\rho^{\prime}$. So, we have constructed a $j$-witness for $\rho^{\prime}$, and we have shown that $\mathbf{c}$ is a witness for $\rho^{\prime}$.

Note that, differently from Calude et al. , we also allow this operation to be performed in the case where $d$ is odd.

Suppose that there exists an index $j$ such that $b_{j}\neq\_$, $d>b_{j}$, and, for all $i>j$, either $b_{i}=\_$ or $b_{i}\geq d$ hold. Then setting $c_{i}=b_{i}$ for all $i>j$, setting $c_{j}=d$, and setting $c_{i}=\_$ for all $i<j$ yields a witness for $\rho^{\prime}$.

For all $i>j$, we set $c_{i}=b_{i}$. Observe that this is valid, since $b_{i}\geq d$, and so the outer domination property continues to hold for the $i$-witness associated with $b_{i}$. For all $i<j$, we set $c_{i}=\_$, and this is trivially valid, since this imposes no requirements upon $\rho^{\prime}$.

To complete the proof, we must argue that setting $c_{j}=d$ is valid. Observe that in $\rho$, the $j$-witness associated with $b_{j}$ ends at a certain position $p=p_{j,2^{j}}$. We can create a new $j$-witness for $\rho^{\prime}$ by instead setting $p_{j,2^{j}}=m+1$, that is, we change the last position of the $j$-witness to point to the newly added vertex. Note that inner domination continues to hold, since $d>b_{j}=\phi(v_{p})$ and since $v_{p}$ outer dominated $\rho$. All other properties trivially hold, and so $\mathbf{c}$ is a witness for $\rho^{\prime}$.

Suppose that for all $j\leq k$ either $b_{j}=\_$ or $b_{j}\geq d$. If we set $c_{i}=b_{i}$ for all $i\leq k$, then $\mathbf{c}$ is a witness for $\rho^{\prime}$.

Since $d\leq b_{j}$ for all $j$, the outer domination of every $i$-witness implied by $\mathbf{b}$ is not changed. Moreover, no other property of a witness is changed by the inclusion of $v_{m+1}$, so by setting $\mathbf{c}=\mathbf{b}$ we obtain a witness for $\rho^{\prime}$.

When we want to update a witness upon scanning another state $v_{m+1}$, we find the largest witness that (according to $\sqsubseteq$) can be obtained by applying Lemmas 3 through 5. The largest such witness is quite easy to find: first, there are at most $3k$ to check, but the rule is simply to update the leftmost position in a witness that can be updated.

For a given witness $\mathbf{b}$ and a vertex $v_{m+1}$, we denote with

$\mathsf{ru}(\mathbf{b},v_{m+1})$ the raw update of the witness to $\mathbf{c}$, as obtained by the update rules described above.

$\mathsf{up}(\mathbf{b},v_{m+1})$ is either $\mathsf{ru}(\mathbf{b},v_{m+1})$ if \mathsf{value}\big{(}\mathsf{ru}(\mathbf{b},v_{m+1})\big{)}\leq e (where $e$ is the number of vertices with even colour), or $\mathsf{up}(\mathbf{b},v_{m+1})=\mathsf{won}$ otherwise.

Basic Update Game

With these update rules, we define a forward and a backward basic update game. The game is played between player even and player odd. In this game, player even and player odd produce a play of the game as usual: if the pebble is on a position of player even, then player even selects a successor, and if the pebble is on a position of player odd, then player odd selects a successor.

Player even can stop any time she likes and evaluate the game using $\mathbf{b}_{0}=\_,\ldots,\_$ as a starting point and the update rule $\mathbf{b}_{i+1}=\mathsf{up}(\mathbf{b}_{i},v_{i})$. For a forward game, she would process the partial play $\rho^{+}=v_{0},v_{1},v_{2},\ldots,v_{n}$ from left to right, and for the backwards game she would process the partial play $\rho^{-}=v_{n},v_{n-1},\ldots,v_{0}$. In both cases, she has won if $\mathbf{b}_{n+1}=\mathsf{won}$.

If player even has a strategy to win the (forward or backward) basic update game, then she has a strategy to win the parity game.

By definition, we can only have $\mathbf{b}_{n+1}=\mathsf{won}$ if at some point we created a witness whose value was more than the total number of even colours in the game. As we have argued, such a witness implies that a cycle has been created, and that the largest priority on the cycle is even. Since player even can achieve this no matter what player odd does, this implies that player even has a winning strategy for the parity game.

The Data-structure for the Progress Measure

Recall that there are two obstacles in implementing the algorithm of Calude et al. as a value iteration algorithm. The first (and minor) obstacle is that it uses forward witnesses, while value iteration naturally uses backward witnesses. We have already addressed this point by introducing the same measure for a backward analysis.

The second obstacle is the lack of an order over witnesses that is compatible with value iteration. While we have introduced an order in the previous sections, this order is not a natural order. In particular, it is not preserved under update, nor does it agree with the order over values. As a simple example consider the following two sequences:

While $\mathsf{value}(\mathbf{b})=3>\mathsf{value}(\mathbf{c})=2$, $\mathbf{c}\sqsupset\mathbf{b}$. In particular, $c_{2}\succ b_{2}$ and $c_{1}\succ b_{1}$ hold. Yet, when using the update rules when traversing a state with colour $6$, $\mathbf{b}$ is updated to $\mathbf{b}^{\prime}=6,\_,\_,$, while $\mathbf{c}$ is updated to $\mathbf{c}^{\prime}=9,8,6$. While $\mathbf{c}\sqsupset\mathbf{b}$ held prior to the update, $\mathbf{b}^{\prime}\sqsupset\mathbf{c}^{\prime}$ holds after the update. Value iteration, however, needs a natural order that will allow us to choose the successor with the higher value.

We overcome this problem by allowing the antagonist in our game, player odd, an extra move: prior to executing the update rule for a value $\mathbf{b}$, player odd may increase the witness $\mathbf{b}$ in the $\sqsubseteq$ ordering. The corresponding antagonistic update is defined as follows.

Obtaining $\mathsf{au}(\mathbf{b},v)$ is quite simple: $\mathsf{au}(\mathbf{b},v)$ is either $\mathsf{up}(\mathbf{b},v)$ or it is $\mathsf{up}(\mathbf{d},v)$ where $\mathbf{d}$ is

Observe that if $\mathbf{b}\sqsubseteq\mathbf{b}^{\prime}$ then $\mathsf{au}(\mathbf{b},v)\sqsubseteq\mathsf{au}(\mathbf{b}^{\prime},v)$, because the minimum used in $\mathsf{au}(\mathbf{b}^{\prime},v)$ ranges over a smaller set.

Antagonistic Update Game

The antagonistic update game is played like the basic update game, but uses the antagonistic update rule. I.e. player even and odd play out a play of the game as usual: if the pebble is on a position of player even, then player even selects a successor, and if the pebble is on a position of player odd, then player odd selects a successor.

Player even can stop any time she likes and evaluate the game using $\mathbf{b}_{0}=\_,\ldots,\_$ as a starting point and the update rule $\mathbf{b}_{i+1}=\mathsf{au}(\mathbf{b}_{i},v_{i})$. For a forward game, she would process the partial play $\rho^{+}=v_{0},v_{1},v_{2},\ldots,v_{n}$ from left to right, and for the backwards game she would process the partial play $\rho^{-}=v_{n},v_{n-1},\ldots,v_{0}$. In both cases, she has won if $\mathbf{b}_{n+1}=\mathsf{won}$.

If player even has a strategy to win the (forward or backward) antagonistic update game, then she has a strategy to win the parity game.

We first look at the evaluation of a play $\rho^{+}=v_{0},v_{1},v_{2},\ldots,v_{n}$ or $\rho^{-}=v_{n},v_{n-1},\ldots,v_{0}$ in a forward or backwards game, respectively. In an antagonistic game, this will lead to a sequence $\mathbf{a}_{0},\mathbf{a}_{1},\ldots,\mathbf{a}_{n+1}$, while it leads to a sequence $\mathbf{b}_{0},\mathbf{b}_{1},\ldots,\mathbf{b}_{n+1}$ when using the basic update rule. We show by induction that $\mathbf{b}_{i}\sqsupseteq\mathbf{a}_{i}$ holds.

For an induction basis, $\mathbf{b}_{0}=\mathbf{a}_{0}=\_,\ldots,\_$.

For the induction step, if $\mathbf{b}_{i}\sqsupseteq\mathbf{a}_{i}$, then

Thus, when player even wins the (forward or backward) antagonistic update game, then she wins the (forward or backward) basic update game using the same strategy.

It remains to show that, if player even has a strategy to win the parity games, then she has a strategy to win the antagonistic update game. For this, we will use the fact that she can, in this case, make sure that the highest number that occurs infinitely often on a run is even. We exploit this in two steps. We first introduce a $\downarrow_{x}$ operator, for every even number $x$, that removes all but possibly one entry with numbers smaller than $x$, and adjust the one that possibly remains to $x-1$. We then argue that, when there are no higher numbers than $x$, this value of the witnesses obtained after this operator are non-decreasing w.r.t. $\sqsupseteq$, and increase strictly with every occurrence of $x$.

Formally we define, for a witness $\mathbf{b}=b_{k},b_{k-1},\ldots,b_{0}$ and an even number $x$, the following.

$\mathbf{b}\downarrow_{x}$ to be $\mathbf{b}$ if, for all $i\leq k$, $b_{i}=\_$ or $b_{i}\geq x$ holds.

Otherwise, let $i=\max\{s\leq k\mid b_{s}\neq\_$ and $b_{s}<x\}$. We define $\mathbf{b}\downarrow_{x}=b_{k}^{\prime},b_{k-1}^{\prime},\ldots,b_{0}^{\prime}$ with $b_{j}^{\prime}=b_{j}$ for all $j>i$, $b_{i}^{\prime}=x-1$, and $b_{j}^{\prime}=\_$ for all $j<i$.

The $\downarrow_{x}$ operator provides the following guarantees:

$\mathbf{b}\sqsupset\mathbf{a}\;\Rightarrow\;\mathbf{b}\downarrow_{x}\sqsupseteq\mathbf{a}\downarrow_{x}$

$\phi(v)<x\;\Rightarrow\;\mathsf{up}(\mathbf{b},v)\downarrow_{x}\sqsupseteq\mathbf{b}\downarrow_{x}$

$\phi(v)<x\;\Rightarrow\;\mathsf{au}(\mathbf{b},v)\downarrow_{x}\sqsupseteq\mathbf{b}\downarrow_{x}$

$\phi(v)=x\;\Rightarrow\;\mathsf{up}(\mathbf{b},v)\downarrow_{x}\sqsupset\mathbf{b}\downarrow_{x}$

$\phi(v)=x\;\Rightarrow\;\mathsf{au}(\mathbf{b},v)\downarrow_{x}\sqsupset\mathbf{b}\downarrow_{x}$

For (1), let $i\leq k$ be the highest position with $b_{i}\neq a_{i}$, and thus with $b_{i}\succ a_{i}$ (as $\mathbf{b}\sqsupset\mathbf{a}$). If $b_{i}\succeq x$ or $x+1\succeq a_{i}$, the claim follows immediately (and we have $\mathbf{b}\downarrow_{x}\sqsupset\mathbf{a}\downarrow_{x}$). For the case $x\succ b_{i}\succ a_{i}\succ x+1$, this position would be replaced by $x-1$ and all smaller positions by $\_$ by the $\downarrow_{x}$ operator (and we have $\mathbf{b}\downarrow_{x}=\mathbf{a}\downarrow_{x}$).

For (2), the highest position $i\leq k$ for which $\mathbf{a}=\mathsf{up}(\mathbf{b},v)$ and $\mathbf{b}$ differ (if any) satisfies $a_{i}<x$ and $b_{i}\prec x$ (the latter holds because otherwise $v$ does not overwrite position $i$ by this update rule). If $b_{i}\prec x+1$, then we get $\mathsf{up}(\mathbf{b},v)\downarrow_{x}\sqsupset\mathbf{b}\downarrow_{x}$; otherwise we get $\mathsf{up}(\mathbf{b},v)\downarrow_{x}=\mathbf{b}\downarrow_{x}$.

For (4), $\mathbf{a}=\mathsf{up}(\mathbf{b},v)$ and $\mathbf{b}$ differ in some highest position $i\leq k$, and for that position, $x=a_{i}\succ b_{i}$ holds. Thus, $\mathsf{up}(\mathbf{b},v)\downarrow_{x}\sqsupset\mathbf{b}\downarrow_{x}$.

This almost immediately implies the correctness.

If player even can win the parity game from a position $v$, then she can win the (forward and backward) antagonistic update game from $v$.

Player even can play such that the highest colour that occurs in a run infinitely many times is even. She can thus in particular play to make sure that, at some point in the run, an even colour $x$ has occurred more often that the size of the image of $\downarrow_{x}$ after the last occurrence of a priority higher than $x$. By Lemma 6, evaluating the forward or backward antagonistic update game at this point will lead to a win of player even.

These results directly provide the correctness of all four games described.

Player even can win the forward and backward antagonistic and basic update game from a position $v$ if, and only if, she can win the parity game from $v$.

Value Iteration

Let $\mathbf{b}_{v}=\max_{\sqsubseteq}\{\mathsf{au}(\iota(s),v)\mid(v,s)\in E\}$ for $v\in V_{e}$ and $\mathbf{b}_{v}=\min_{\sqsubseteq}\{\mathsf{au}(\iota(s),v)\mid(v,s)\in E\}$ for $v\in V_{o}$. We say that $\iota$ can be lifted at $v$ if $\iota(v)\sqsubset\mathbf{b}_{v}$. When $\iota$ is liftable at $v$, we define by $\mathsf{lift}(\iota,v)$ the function $\iota^{\prime}$ with $\iota^{\prime}(v)=\mathbf{b}_{v}$ and $\iota^{\prime}(v^{\prime})=\iota(v^{\prime})$ for all $v^{\prime}\neq v$. We extend the lift operation to every non-empty set $V^{\prime}\subseteq V$ of liftable positions, where $\iota^{\prime}=\mathsf{lift}(\iota,V^{\prime})$ updates all values $v\in V^{\prime}$ concurrently.

A progress measure is called consistent if it cannot be lifted at any vertex $v\in V$. The minimal consistent progress measure $\iota_{\min}$ is the smallest (w.r.t. the partial order in the natural lattice defined by pointwise comparison) progress measure that satisfies

for all $v\in V_{e}$ that $\iota(v)\sqsupseteq\max_{\sqsubseteq}\{\mathsf{au}(\iota(s),v)\mid(v,s)\in E\}$, and

for all $v\in V_{o}$ that $\iota(v)\sqsupseteq\min_{\sqsubseteq}\{\mathsf{au}(\iota(s),v)\mid(v,s)\in E\}$.

As $\mathsf{au}(\mathbf{b},v)$ is monotone in $\mathbf{b}$ by definition and the state space is finite, we get the following.

The minimal consistent progress measure $\iota_{\min}$ is well defined.

First, a consistent progress measure always exists: the function that maps all states to $\mathsf{won}$ is a consistent progress measure.

Second if we have two consistent progress measures $\iota$ and $\iota^{\prime}$, then the pointwise minimum $\iota^{\prime\prime}:v\mapsto\min_{\sqsubseteq}\{\iota(v),\iota^{\prime}(v)\}$ is a consistent progress measure. To see this, we assume w.l.o.g. that $\iota(v)\sqsubseteq\iota^{\prime}(v)$.

For $v\in V_{e}$ we get $\iota^{\prime\prime}(v)=\iota(v)\sqsupseteq\max_{\sqsubseteq}\{\mathsf{au}(\iota(s),v)\mid(v,s)\in E\}\sqsupseteq\max_{\sqsubseteq}\{\mathsf{au}(\iota^{\prime\prime}(s),v)\mid(v,s)\in E\}$, using that $\iota^{\prime\prime}(s)\sqsubseteq\iota(s)$ holds for all $s\in V$.

Likewise, we get for $v\in V_{o}$ that $\iota^{\prime\prime}(v)=\iota(v)\sqsupseteq\min_{\sqsubseteq}\{\mathsf{au}(\iota(s),v)\mid(v,s)\in E\}\sqsupseteq\min_{\sqsubseteq}\{\mathsf{au}(\iota^{\prime\prime}(s),v)\mid(v,s)\in E\}$, using again that $\iota^{\prime\prime}(s)\sqsubseteq\iota(s)$ holds for all $s\in V$.

As the state space is finite, we get the minimal consistent progress measure as a pointwise minimum of all consistent progress measures.

Moreover, we can compute the minimal consistent progress measure by starting with the initial progress measure $\iota_{0}$, which maps all vertices to the minimal witness $\_,\ldots,\_$, and iteratively lifting.

The minimal consistent progress measure $\iota_{\min}$ can be obtained by any sequence of lift operations on liftable positions, starting from $\iota_{0}$.

We show that, for any sequence $\iota_{0},\iota_{1},\ldots,\iota_{n}$ of progress measures constructed by a sequence of lift operations, for all $v\in V$, and for all $i\leq n$, $\iota_{i}(v)\sqsubseteq\iota_{\min}(v)$ holds.

For the induction basis, $\iota_{0}(v)$ is the minimal element for all $v\in V$, such that $\iota_{0}(v)\sqsubseteq\iota_{\min}(v)$ holds trivially. For the induction step, let $V_{i}\subseteq V$ be a set of liftable position for $\iota_{i}$ and $\iota_{i+1}=\mathsf{lift}(\iota_{i},V_{i})$. We now make the following case distinction.

For $v\in V_{i}\cap V_{e}$, we have $\iota_{i+1}(v)=\max_{\sqsubseteq}\{\mathsf{au}(\iota(s),v)\mid(v,s)\in E\}\sqsubseteq_{IH}\max_{\sqsubseteq}\{\mathsf{au}(\iota_{\min}(s),v)\mid(v,s)\in E\}\sqsubseteq\iota_{\min}(v)$.

For $v\in V_{i}\cap V_{o}$, we have $\iota_{i+1}(v)=\min_{\sqsubseteq}\{\mathsf{au}(\iota(s),v)\mid(v,s)\in E\}\sqsubseteq_{IH}\min_{\sqsubseteq}\{\mathsf{au}(\iota_{\min}(s),v)\mid(v,s)\in E\}\sqsubseteq\iota_{\min}(v)$.

For $v\notin V_{i}$, we have $\iota_{i+1}(v)=\iota_{i}(v)\sqsubseteq_{IH}\iota_{\min}(v)$.

While we have proven that the value of the progress measures cannot surpass the value of $\iota_{\min}$ at any vertex, each liftable progress measure $\iota_{i}$ is succeeded by a progress measure $\iota_{i+1}$, which is nowhere smaller, and strictly increasing for some vertices. Thus, this sequence terminates eventually by reaching a non-liftable progress measure. But non-liftable progress measures are consistent.

Thus, we eventually reach a consistent progress measure $\iota_{n}$ which is pointwise no larger than $\iota_{\min}$; i.e. we eventually reach $\iota_{\min}$.

It is simple to get from establishing that $\iota_{\min}(v)=\mathsf{won}$ holds to a winning strategy of player even in the antagonistic update game.

If $\iota_{\min}(v)=\mathsf{won}$, then player even has a strategy to win the antagonistic update game when starting from $v$.

We can construct the strategy in the following way: starting in state $v_{n}=v$, where $n$ is the length of the play we will create, player even selects for a state $v_{i}\in V_{e}$ with $i>0$ a successor $v_{i-1}$ such that $\iota_{i}(v_{i})\sqsubseteq\mathsf{au}(\iota_{i-1}(v_{i-1}),v_{i})$. Note that such a successor must always exist. Note also that, if $v_{i}\in V_{o}$ with $i>0$, then $\iota_{i}(v_{i})\sqsubseteq\mathsf{au}(\iota_{i-1}(v_{i-1}),v_{i})$ holds for all successors $v_{i-1}$ of $v_{i}$ by definition.

For the induction basis, we have $\mathbf{b}_{0}=\iota_{0}(v_{0})$ by definition. For the induction step, we have $\iota_{i+1}(v_{i+1})\sqsubseteq\mathsf{au}(\iota_{i}(v_{i}),v_{i+1})\sqsubseteq^{IH}\mathsf{au}(\mathbf{b}_{i},v_{i+1})=\mathbf{b}_{i+1}$.

Thus, we get $\mathbf{b}_{n}\sqsupseteq\iota_{n}(v_{n})=\mathsf{won}$, and player even wins the antagonistic update game.

At the same time, player even cannot win from any vertex $v$ with $\iota_{\min}(v)\neq\mathsf{won}$, and $\iota_{\min}$ provides a witness strategy for player odd for this.

Player even cannot win from any vertex $v$ with $\iota_{\min}(v)\neq\mathsf{won}$, and $\iota_{\min}$ provides a witness strategy for player odd.

We recall that the construction of $\iota_{\min}$ by Lemma 8 provides

$\iota_{\min}(v)\sqsubseteq\max_{\sqsubseteq}\{\mathsf{au}(\iota_{\min}(s),v)\mid(v,s)\in E\}$ for $v\in V_{e}$, and

$\iota_{\min}(v)\sqsubseteq\min_{\sqsubseteq}\{\mathsf{au}(\iota_{\min}(s),v)\mid(v,s)\in E\}$ for $v\in V_{o}$.

The latter provides the existence of some particular successor $s$ of $v$ with $\iota_{\min}(v)\sqsubseteq\mathsf{au}(\iota_{\min}(s),v)$. The witness strategy of player odd is to always choose such a vertex.

Let $\rho=v_{n},v_{n-1},v_{n-2},\ldots,v_{1}$ be a sequence obtained by any strategy of player even from a starting vertex $v_{n}$ with $\iota_{\min}(v_{n})\neq\mathsf{won}$, such that player even chooses to evaluate the backward antagonistic update game after $\rho$, and $\rho,v_{0}$ an extension in line with the strategy of player odd.

We first observe that $\iota_{\min}(v_{i+1})\sqsubseteq\mathsf{au}(\iota_{\min}(v_{i}),v_{i+1})$ holds for all $i<n$, either by the choice of the successor of $v_{i+1}$ of player odd if $v_{i+1}\in V_{o}$, or by $\iota_{\min}(v_{i+1})\sqsubseteq\max_{\sqsubseteq}\{\mathsf{au}(\iota_{\min}(s),v_{i+1})\mid(v_{i+1},s)\in E\}\sqsubseteq\mathsf{au}(\iota_{\min}(v_{i}),v_{i+1})$ if $v_{i+1}\in V_{e}$. With $\iota_{\min}(v_{n})\neq\mathsf{won}$, this provides $\iota_{\min}(v_{i})\neq\mathsf{won}$ for all $i\leq n$.

Complexity

A simple implementation can track, for each vertex, the information which position in the witness is the next one that would need to be updated to trigger a lift along an edge, and, using a binary representation in line with $\succcurlyeq$, which bit in the representation of this position has to change to consider triggering an update. (Intuitively the most significant bit that separates the current value from the next value that would trigger an update.)

For each incoming edge, the position and bit that need to be increased to trigger the next lift operation for this vertex are also stored.

We look at a vertex $v$ with one outgoing edge to its successor vertex $s$. We have $7$ different colours, $2$ through $8$. Vertex $v$ has colour $2$.

We use a representation that follows the $\succcurlyeq$ order and thus maps to , $7$ to $1$, $5$ to $2$, $3$ to $3$, $2$ to $4$, $4$ to $5$, $6$ to $6$, $8$ to $7$.

Assume that $s$ has currently a witness $\mathbf{b}=b_{2},b_{1},b_{0}=6,0,2$ attached to it, represented as $\widetilde{\mathbf{b}}=\widetilde{b}_{2},\widetilde{b}_{1},\widetilde{b}_{0}=6,0,4$.

To obtain a witness for $v$, we calculate $\mathbf{c}=\mathsf{au}(\mathbf{b},v)=6,5,2$, which is represented as $\widetilde{\mathbf{c}}=\widetilde{c}_{2},\widetilde{c}_{1},\widetilde{c}_{0}=6,2,4$. The next higher value $\mathbf{a}\sqsupset\mathbf{b}$ such that $\mathsf{au}(\mathbf{a},v)\sqsupset\mathsf{au}(\mathbf{b},v)$ is $\widetilde{\mathbf{a}}=\widetilde{a}_{2},\widetilde{a}_{1},\widetilde{a}_{0}=6,2,4$.

The lowest position $i$ with $\widetilde{a}_{i}>\widetilde{b}_{i}$ is for position $i=1$, and the difference occurs in the middle bit ($\widetilde{a}_{1}=2=010_{2}$ and $\widetilde{b}_{1}=0=000_{2}$).

For the edge from $v$ to $s$, we can store after the update that we only need to consider an update from $s$ if it increases at least the position $b_{1}$ of the witness for $s$. If $b_{1}$ is changed, we only have to consider the change if the update is at least to the value represented as 2 ($\widetilde{b}_{1}^{\prime}\geq 2$), and thus $b_{1}^{\prime}\succcurlyeq 5$. For all smaller updates of the witness of $s$, no update of the witness of $v$ needs to be considered.

The first observation is that, if the highest colour is the odd colour $o_{\max}$, then we do not need to represent this colour: if $\phi(v)=o_{\max}$ and $\mathbf{b}\neq\mathsf{won}$, then $\mathsf{up}(\mathbf{b},v)$ contains only $\_$ and $o_{\max}$ entries. Moreover, $\_$ and $o_{\max}$ entries behave in exactly the same way. This is not surprising: $o_{\max}$ is the most powerful colour, and a state with colour $o_{\max}$ cannot occur on a winning cycle.

The second observation is that, if the lowest colour is the odd colour $o_{\min}$, then we can ignore it during all update steps without violating the correctness arguments. (In fact, this colour cannot occur at all when using the update rules suggested in Calude et al. .)

We call the number of different colours, not counting the maximal and minimal colour if they are odd, the number $r$ of relevant colours.

The $1$ refers to the dedicated value $\mathsf{won}$. For the other witnesses, the values can be obtained by considering the number $i$ of integer entries. For $i$ integer entries, there are \Big{(}\begin{array}[]{c}l\\ i\end{array}\Big{)} different positions in the witnesses that could hold these $i$ integer values. Fixing these positions, there are \Big{(}\begin{array}[]{c}i+r-1\\ r-1\end{array}\Big{)} ways to assign non-increasing values from the range of relevant colours. (E.g. these can be represented by a sequence of $i$ white balls and $r-1$ black balls. The number of white balls prior to the first black ball is the number of positions assigned the highest relevant colour, the number of white balls between the first and second black ball is the number of positions assigned the next lower colour, etc.)

In particular, we get the following complexity for a constant number of colours.

A parity game with $r$ relevant colours, $n$ vertices, $m$ edges, and $e$ vertices with even colour can be solved in time O\big{(}e\cdot m\cdot(\log(e)+r)^{r-1}/(r-1)!\big{)} and space O\big{(}n\cdot\log(e)\cdot\log(r)+m\cdot\log(\log(e)\cdot\log(r))\big{)}.

We use that the length $l=\lceil\log_{2}(e+1)\rceil$ of the witnesses is logarithmic in $e$.

This also provides us with a strong fixed parameter tractability result: when we fix the number of colours to some constant $c$, we maintain a quasi bi-linear complexity in the number of edges and the number of vertices. If we fix, e.g., a monotonously growing quasi constant function $\mathsf{qc}$ (like the inverse Ackermann function), then Theorem 8.2 shows that, as soon $\mathsf{qc}(n)\geq c$, and thus almost everywhere and in particular in the limit, have $(l+r)^{r-1}/(r-1)!\leq(\log_{2}n)^{\mathsf{qc}(n)}$, or $(l+r)^{r-1}/(r-1)!\leq\mathsf{qc}(n)^{\log_{2}(\log_{2}(n))}$ if $\log_{2}(\mathsf{qc}(n)\geq c)$.

Parity games are fixed parameter tractable, using the number of colours as their parameter, with complexity O\big{(}m\cdot n\cdot\mathsf{qc}(n)^{\log\log n}\big{)} for an arbitrary quasi constant $\mathsf{qc}$, where $m$ is the number of edges and $n$ is the number of states.

For a parity game with $r$ relevant colours, $m$ edges, and $e$ vertices with even colour, and thus length $l=\lceil\log_{2}(e+1)\rceil$ of the witnesses, and h=\big{\lceil}1+\frac{r-1}{l}\big{\rceil}, one can solve the parity game in time $O(m\cdot h\cdot e^{1+c_{1.45}+\log_{2}(h)})$, and in time $O(m\cdot h\cdot e^{c_{1.45}+\log_{2}(h)})$ if $r>l^{2}$.

We note that $l+r-1\leq h\cdot l$, such that we can estimate this value by drawing $l$ out of $h\cdot l$.

The number of all ways to choose $l=\lceil\log(e+1)\rceil$ out of $h\cdot l$ numbers can, by the Wikipedia page on binomial coefficients and the inequality using the entropy in there (also can be found in ), be bounded by

This allows for identifying a class of parity games that can be solved in polynomial time.

Parity games where the number $c$ of colours is logarithmically bounded by the number $e$ of vertices with even colour ($c\in O(\log e)$) can be solved in polynomial time.

Lower Bounds

In this section, we introduce a family of examples, on which the the basic update game from is slow. (Recall that these original rules restrict the use of Lemma 3 to even colours. Adjusting the example is not hard, but effectively disallows to make effective use of $b_{0}$.)

The example is a single player game, which is drawn best as a ring. In this example, the losing player, player odd, can draw out his loss. The vertices of the game have name and colour $1,\ldots,2n$. They are all owned by player odd. There is always an edge to the next vertex (in the modulo ring). Additionally, there is an edge back to $1$ from all vertices with even name (and colour).

Obviously, all runs are winning for player even. We show how player odd can, when starting in vertex $1$, produce a play, such that forward updates produce all witnesses that use only $\_$ and even numbers.

We first observe that every value $2i-1$ is overwritten after the next move in a play by $2i$ in a witness $\mathbf{b}$.