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

TL;DR

This paper presents an efficient implementation of a quasi-polynomial time algorithm for solving parity games, improving practical performance and providing new complexity bounds and algorithmic insights.

Contribution

It introduces a backward implementation of Calude et al.'s algorithm using a progress measure, with modifications enabling efficient solving and new complexity results.

Findings

First implementation of a quasi-polynomial parity game solver

Achieved quasi bi-linear complexity for fixed colors

Provided matching lower bounds for existing algorithms

Abstract

Parity games play an important role in model checking and synthesis. In their paper, Calude et al. have shown that these games can be solved in quasi-polynomial time. We show that their algorithm can be implemented efficiently: we use their data structure as a progress measure, allowing for a backward implementation instead of a complete unravelling of the game. To achieve this, a number of changes have to be made to their techniques, where the main one is to add power to the antagonistic player that allows for determining her rational move without changing the outcome of the game. We provide a first implementation for a quasi-polynomial algorithm, test it on small examples, and provide a number of side results, including minor algorithmic improvements, a quasi bi-linear complexity in the number of states and edges for a fixed number of colours, and matching lower bounds for the algorithm of Calude et al.

Figures

Tables

Table 1. Table 1: Running times (in seconds) of the four algorithms tested: quasi-polynomial time algorithm presented in this paper (QPT), small progress measure (SPM), Zielonka’s recursive algorithm (REC), the classic strategy improvement (CSI), and the implementation [ 35 ] of the quasi-polynomial time algorithm (JL’17) from [ 20 ] . Entry “–” means that the algorithm did not terminate within the set timeout of two minutes. For the steadygame examples we state the minimum and the maximum measured execution time for the ten examples generated for each size.

Example Class	Nodes	Colours	QPT	SPM	REC	CSI	JL’17 [20, 35]
steadygame	100	100	min:  0.01	min:  0.01	min:  0.01	min:  0.01	min:  10.16
			max: 0.02	max: 0.02	max: 0.01	max: 0.01	max: –
steadygame	200	200	min:  0.01	min:  0.01	min:  0.01	min:  0.01	min:  –
			max: 0.09	max: 0.06	max: 0.01	max: 0.03	max: –
steadygame	1000	1000	min:  0.09	min:  1.55	min:  0.01	min:  0.14	min:  –
			max: 1.51	max: 1.67	max: 0.04	max: 0.23	max: –
steadygame	5000	5000	min:  1.51	min:  41.49	min:  0.23	min:  1.56	min:  –
			max: 102	max: –	max: 0.44	max: 4.12	max: –
steadygame	10000	10000	min:  5.1	min:  –	min:  0.68	min:  3.07	min:  –
			max: –	max: –	max: 1.89	max: 8.25	max: –
Friedmann’s trap	77	66	0.01	–	0.01	0.26	–
Friedmann’s trap	230	120	0.01	–	0.01	22.72	–
Friedmann’s trap	377	156	0.01	–	0.01	–	–
recursive ladder	250	152	0.01	–	–	0.01	0.66
recursive ladder	1000	752	0.02	–	–	0.01	–
recursive ladder	25000	15002	0.45	–	–	0.56	–

Equations

$$p_1,p_2,p_3,\dots ,p_{2^i},$$

$$b_k,b_{k-1},\dots ,b_1,b_0,$$

$$p_{i,1},p_{i,2},\dots ,p_{i,2^i}.$$

$$\mathsf{au}(\mathbf{b},v)={\min}_{\sqsubseteq}\big{\{}\mathsf{up}(\mathbf{c},v)\mid\mathbf{c}\sqsupseteq\mathbf{b}\big{\}}$$

$${\min }_{⊑}\{\mathbf{d}=d_k,d_{k-1},\dots ,d_0;\mathbf{d}⊒\mathbf{b}\text{ and }{d}_0=\_\}.$$

$${\mathbf{a}}_{i+1}=\mathsf{au}({\mathbf{a}}_i,v_i)$$

$$⊑\mathsf{up}({\mathbf{a}}_i,v_i)$$

$${⊑}^{IH}\mathsf{up}({\mathbf{b}}_i,v_i)={\mathbf{b}}_{i+1}.$$

$$2^{({\log }_2(e)+1)\cdot h\cdot ((1/h)\cdot {\log }_2(h)+((h-1)/h)\cdot {\log }_2(h/(h-1)))}$$

Full text

1 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 [10, 8, 25, 4, 39, 19, 24, 28, 37, 3, 26, 23, 2, 21, 30, 11, 34, 6, 31, 5, 20], in part due to their practical applications. Solving parity games is the central and most expensive step in many model checking [22, 10, 9, 38, 7, 1], satisfiability checking [38, 22, 36, 32], and synthesis [27, 33, 17] 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 [18], 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 [25, 39], which despite being one of the oldest algorithms has been found to be quite competitive in practice [14]. Strategy improvement algorithms use a local search technique [37], 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 [19]. 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. [5] 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 [21], 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. [5] 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ć [20] have developed an adaptation of the classical small-progress measures algorithm [19] 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. [5]. 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.

Our contribution.

In this paper, we develop a progress-measure based algorithm for solving parity games that uses the succinct witnesses of Calude et al. [5]. 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. [5] 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. [5] 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})$; 2. 2.

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

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ć [20], while (2) and (3) are new. Moreover, we believe that it is interesting that the witnesses of Calude et al. [5] 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. [5]. 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.

2 Preliminaries

$\mathbb{N}$ denotes the set of positive natural numbers $\{1,2,3,\ldots\}$. Parity games are turn-based zero-sum games played between two players—even and odd, or maximiser and minimiser—over finite graphs. A parity game $\mathcal{P}$ is a tuple $(V_{e},V_{o},E,C,\phi)$, where $(V=V_{e}\cup V_{o},E)$ is a finite directed graph with the set of vertices $V$ partitioned into a set $V_{e}$ of vertices controlled by player even and a set $V_{o}$ of vertices controlled by player odd, $E\subseteq V\times V$ is the set of edges, $C\subseteq\mathbb{N}$ is a set of colours, and $\phi:V\to C$ is the colour mapping. We require that every vertex has at least one outgoing edge.

A parity game $\mathcal{P}$ is played between the two players, even and odd, by moving a token along the edges of the graph. A play of such a game starts by placing a token on some initial vertex $v_{0}\in V$. The player controlling this vertex then chooses a successor vertex $v_{1}$ such that $(v_{0},v_{1})\in E$ and the token is moved to this successor vertex. In the next turn the player controlling the vertex $v_{1}$ chooses the successor vertex $v_{2}$ with $(v_{1},v_{2})\in E$ and the token is moved accordingly. Both players move the token over the arena in this manner and thus form a play of the game. Formally, a play of a game $\mathcal{P}$ is an infinite sequence of vertices $\langle v_{0},v_{1},\ldots\rangle\in V^{\omega}$ such that, for all $i\geq 0$, we have that $(v_{i},v_{i+1})\in E$. We write $\mathsf{Plays}_{\mathcal{P}}(v)$ for the set of plays of the game $\mathcal{P}$ that start from a vertex $v\in V$ and $\mathsf{Plays}_{\mathcal{P}}$ for the set of plays of the game. We omit the subscript when the arena is clear from the context. We extend the colour mapping $\phi:V\to C$ from vertices to plays by defining the mapping $\phi:\mathsf{Plays}\to C^{\omega}$ as $\langle v_{0},v_{1},\ldots\rangle\mapsto\langle\phi(v_{0}),\phi(v_{1}),\ldots\rangle$.

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; 2. 2.

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

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

as (2), and $\sigma$ must be memoryless.

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

3 QP Algorithms

We discuss a variation of the algorithm of Calude et al. [5].

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 [5], 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.

$i$-Witnesses

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$

[TABLE]

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

[TABLE]

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

[TABLE]

• •

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 [5]. 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}$.

Lemma 1

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

Proof

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

Lemma 2

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

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

Lemma 3

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

Proof

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. [5], we also allow this operation to be performed in the case where $d$ is odd.

Lemma 4

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

Proof

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

Lemma 5

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

Proof

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.

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

Theorem 4.1

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.

Proof

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.

5 The Data-structure for the Progress Measure

Recall that there are two obstacles in implementing the algorithm of Calude et al. [5] 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:

• •

$\mathbf{b}=\_,4,2$, and

• •

$\mathbf{c}=9,8,\_$.

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.

[TABLE]

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

[TABLE]

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.

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

Theorem 6.1

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.

Proof

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

[TABLE]

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

Lemma 6

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

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

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

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

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

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

Proof

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

(3) follows from (1) and (2).

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

(5) follows with (1) and (4).

This almost immediately implies the correctness.

Theorem 6.2

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

Proof

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.

Corollary 1

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

7 Value Iteration

The antagonistic update game offers a direct connection to value iteration. For value iteration, we use a progress measure, a function $\iota:V\rightarrow\mathbb{W}$, where $\mathbb{W}$ denotes the set of possible backwards witnesses. That is, a progress measure assigns a backwards witness to each vertex.

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.

Lemma 7

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

Proof

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.

Lemma 8

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

Proof

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

This closes the induction step.

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.

Lemma 9

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

Proof

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.

Assume that player even selects a successor from her vertices as described above, and $v_{n},v_{n-1},\ldots,v_{0}$ is a play created this way. Let $\mathbf{b}_{0}=\_,\ldots,\_$ be the minimal element of $\mathbb{W}$, and $\mathbf{b}_{i+1}=\mathsf{au}(\mathbf{b}_{i},v_{i+1})$. Then we show by induction that $\mathbf{b}_{i}\sqsupseteq\iota_{i}(v_{i})$.

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.

Lemma 10

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.

Proof

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

Let $\mathbf{b}_{0}=\_,\ldots,\_$ be the minimal element of $\mathbb{W}$, and $\mathbf{b}_{i+1}=\mathsf{au}(\mathbf{b}_{i},v_{i+1})$. Then $\mathbf{b}_{0}\sqsubseteq\iota_{\min}(v_{0})$, and the monotonicity of $\mathsf{au}$ in the first element inductively provides $\mathbf{b}_{i}\sqsubseteq\iota_{\min}(v_{i})$ for all $i\leq n$. Thus $\mathbf{b}_{n}\neq\mathsf{won}$, and player even loses the update game.

8 Complexity

We use natural representation for the set of colours as integers written in binary, encoding the $\_$ as [math]. The first observation is that the number of individual lift operations is, for each vertex, limited to $|\mathbb{W}|$.

Lemma 11

For each vertex the number of lift operations is restricted to $|\mathbb{W}|$. The overall number of lift operations is restricted to $|V|\cdot|\mathbb{W}|$. The number of lift operations an edge (or: source or target vertex of an edge, respectively) is involved in is restricted to $|\mathbb{W}|$. Summing up over all edges and over the number of lift operations their target or source vertex is involved in amounts to $O(|E|\cdot|\mathbb{W}|)$.

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

Obviously, the most expensive path to $\iota_{\min}$ is for each position to go through all values of $|\mathbb{W}|$ in this case. But in this case, tracking the information mentioned in the previous section reduces the average cost of an update to $O(1)$. The information that we store for this is, for each vertex, the current witness that represents its current value before and after executing the antagonistic update, and the next value that would lead to a lift operation on the antagonistic value.

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.

Example 1

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 [math] to [math], $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.

Theorem 8.1

For a parity game with $n$ vertices and $m$ edges, the algorithm can be implemented to run in $O(m\cdot|\mathbb{W}|)$ time and $O(n\cdot\log|\mathbb{W}|+m\log\log|\mathbb{W}|)$ space.

Note that the $\log\log|\mathbb{W}|$ information per edge is only required to allow for a discounted update cost of $O(1)$. It can be traded for a $\log|\mathbb{W}|$ increase in the running time. This leaves the estimation of $|\mathbb{W}|$.

To improve the complexity especially in the relevant lower range of colours, we first look into reducing the size of $\mathbb{W}$, and then look into keeping the discounted update complexity low. We make three observations that can be used to reduce the size of $\mathbb{W}$; they can be integrated in the overall proof, starting with the raw and basic update steps.

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. [5].)

Finally, we observe that, for the least relevant entry $b_{0}$ of an witness $\mathbf{b}$, it does not matter if this entry contains $\_$ or an odd value. We can therefore simply not use odd values at this position. (Using the third observation has no impact on the complexity of the problem, but still approximately halves the size of $\mathbb{W}$, and is therefore useful in practice.)

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

Lemma 12

For a parity game with $r$ relevant colours and $e$ vertices with even colour, and thus with length $l=\lceil\log_{2}(e+1)\rceil$ of the witnesses, |\mathbb{W}|\leq 1+\sum\limits_{i=0}^{l}\Big{(}\begin{array}[]{c}l\\ i\end{array}\Big{)}\cdot\Big{(}\begin{array}[]{c}i+r-1\\ r-1\end{array}\Big{)}.

Proof

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

This allows for two easy estimations of the size of $|\mathbb{W}|$: If the number $c$ of colours is small (especially if $c$ is constant), then we can use the coarse estimate |\mathbb{W}|\in O\Big{(}e\cdot\Big{(}\begin{array}[]{c}l+r-1\\ l\end{array}\Big{)}\Big{)}.

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

Theorem 8.2

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

Corollary 2

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 “high” number of colours, we can improve the estimation: if $r\geq l^{2}$, then the case $i=l$ dominates the overall cost, such that |\mathbb{W}|\in O\Big{(}\big{(}\begin{array}[]{c}l+r-1\\ l\end{array}\big{)}\Big{)}.

Theorem 8.3

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 use the constant $c_{1.45}=\lim_{h\rightarrow\infty}\log_{2}(1+1/h)\cdot h=\log_{2}\mathsf{e}<1.45$, where $\mathsf{e}\approx 2.718$ is the Euler number; using that $(1+1/h)^{h}<\mathsf{e}$ and thus $\log_{2}(1+1/h)\cdot h<c_{1.45}$ holds for all $h\in\mathbb{N}$.

Proof

To estimate $\mathbb{W}$, we again start with analysing the size of \Big{(}\begin{array}[]{c}l+r-1\\ l\end{array}\Big{)}.

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 [29]), be bounded by

[TABLE]

The estimation uses that $\log(1+1/(h-1))\cdot(h-1)<c_{1.45}$ holds for all $h\in\mathbb{N}$.

Theorem 8.1 now provides $O(m\cdot h\cdot e^{1+c_{1.45}+\log_{2}(h)})$ time bound. If the number of colours is high ($r>l^{2}$), then we observe that |\mathbb{W}|\leq 1+\sum_{i=0}^{l}\Big{(}\begin{array}[]{c}l\\ i\end{array}\Big{)}\cdot\Big{(}\begin{array}[]{c}i+r-1\\ i\end{array}\Big{)}\in O\Big{(}\big{(}\begin{array}[]{c}l+r-1\\ l\end{array}\big{)}\Big{)} holds, as the sum is dominated by \Big{(}\begin{array}[]{c}l\\ l\end{array}\Big{)}\cdot\Big{(}\begin{array}[]{c}l+r-1\\ l\end{array}\Big{)}. This allows for the second estimate $O(m\cdot h\cdot e^{c_{1.45}+\log_{2}(h)})$ of the running time when $r>l^{2}$ holds.

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

Corollary 3

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.

9 Lower Bounds

In this section, we introduce a family of examples, on which the the basic update game from [5] 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}$.

The strategy of player odd to create a long path is simple. We consider three cases.

If, in the current witness $\mathbf{b}=b_{k},\ldots,b_{0}$, we have $b_{0}=\_$ and the token is at a position $2i$, then moving to $1$, and thus next to $2$, results in the next larger witness without odd entries than $\mathbf{b}$.

If $b_{0}\neq\_$, then we have that $b_{0}=2i$, and $\mathbf{b}$ has no smaller entries than $2i$. If all of these entries are consecutively on the right of $\mathbf{b}$, then we obtain the next larger witness without odd entries than $\mathbf{b}$ by going through $2i+1$ to $2i+2$. Player odd therefore chooses to continue by moving the token to vertex $2i+1$ in this case.

Otherwise, there is a rightmost $b_{j}=\_$, such that right of it are only entries $2i$ (for all $h<j$, $b_{h}=2i$), and there is also a $2i$ value to the left (for some $h>j$, $b_{h}=2i$). Then the next larger witness without odd entries than $\mathbf{b}$ is obtained by replacing $b_{j}$ by $2$ and all entries to its right by $\_$. This can be obtained by going to vertex 1 and, subsequently, to vertex 2. Player odd therefore chooses to continue by moving the token to vertex $1$ in this case.

10 Implementation

We implemented our algorithm in C++ and tested its performance on Mac OS X with 1.7 GHz Intel Core i5 CPU and 4 GB of RAM. We then compared it with the small progress measure algorithm [19], Zielonka’s recursive algorithm [39], the classic strategy improvement algorithm [37] as implemented in the PGSolver version 4.0 [15, 16], and the implementation [35] of an alternative recently developed succinct progress measure algorithm from [20]. We tested their performance, with timeout set to two minutes, on around 250 different parity games of various sizes generated using PGSolver. These examples include the following classes.

• •

Friedmann’s trap examples [12], which show exponential lower bound for the classic strategy improvement algorithm;

• •

random parity games of sizes, $s$, ranging from 100 to 10000 that were generated using PGSolver’s command steadygame $s$ 1 6 1 6 (for each $s$ we generated ten instances);

• •

recursive ladder construction [13] generated using PGSolver’s command recursiveladder.

PGSolver implements several optimisation steps before the algorithm of choice is invoked. These include SCC decomposition, detection of special cases, priority compression, and priority propagation as described in [15]. To illustrate this, the small progress measures algorithm in PGSolver was able to solve all Friedmann’s trap examples in 0.01 seconds when using these optimisations. However, without these optimisations, it failed to terminate within the set timeout of two minutes. As our aim was to compare different algorithms and not the heuristics or preprocessing steps involved, we invoked PGSolver with options “-dgo -dsd -dlo -dsg” to switch off some of these optimisation steps. We believe this gives a better and fairer picture of the relative performance of these algorithms. Some of these optimisations are embedded in the algorithms themselves and cannot be switched off. For example, the small progress measure algorithm implemented in PGSolver starts off with the computation of maximal values that may ever need to be considered [15]. In future, we plan to include these optimisation preprocessing techniques into our tool as well.

The more interesting results of our tests are presented in Table 1. As expected, our algorithm is outperformed by strategy improvement and recursive algorithm on randomly generated examples. Our algorithm is very fast on Friedmann’s trap examples, because player odd wins from all nodes and a fixed point is reached very quickly using a small number of entries in the witnesses. Finally, we tested the algorithms on the recursive ladder construction, which is a class of examples for which the recursive algorithm runs in exponential time. As expected, the small progress measure and the recursive algorithm fail to terminate for examples as small as 250 nodes. Our algorithm as well as the classic strategy improvement solved these instances very quickly. Interestingly, the worst performing algorithm is [20], which currently has the best theoretical upper bound on its running time. The most likely reason for this is that their single step of the value iteration is a lot more complicated than ours. As a result, even if less such steps are required to reach a fixed point, the algorithm performs badly as each step is a lot slower. In conclusion, our algorithm complements quite well the existing well-established algorithms for parity games and can be faster than any of them depending on the class of examples being considered.

The implementation of our algorithm along with all the examples that we used in this comparison are available at https://cgi.csc.liv.ac.uk/~dominik/parity/.

Acknowledgements

We thank Ding Xiang Fei for pointing out an error in a previous version of this manuscript. Sanjay Jain was supported in part by NUS grant C252-000-087-001. Further, Sanjay Jain and Frank Stephan were supported in part by the Singapore Ministry of Education Academic Research Fund Tier 2 grant MOE2016-T2-1-019 / R146-000-234-112. Sven Schewe and Dominik Wojtczak were supported in part by EPSRC grant EP/M027287/1. Further, John Fearnley, Sven Schewe and Dominik Wojtczak were supported in part by EPSRC grant EP/P020909/1.