Succinct progress measures for solving parity games

Introduction

A parity game is a deceptively simple combinatorial game played by two players—Even and Odd—on a directed graph. From the starting vertex, the players keep moving a token along edges of the graph until a lasso-shaped path is formed, that is the first time the token revisits some vertex, thus forming a loop. The set of vertices is partitioned into those owned by Even and those owned by Odd, and the token is always moved by the owner of the vertex it is on. Every vertex is labelled by a positive integer, typically called its priority. What are the two players trying to achieve? This is the crux of the definition: they compete for the highest priority that occurs on the loop of the lasso; if it is even then Even wins, and if it is odd then Odd wins.

A number of variants of the algorithmic problem of solving parity games are considered in the literature. The input always includes a game graph as described above. The deciding the winner variant has an additional part of the input—the starting vertex—and the question to answer is whether or not Even has a winning strategy—a recipe for winning no matter what choices Odd makes. Alternatively, we may expect that the algorithm returns the set of starting vertices from which Even has a winning strategy, or that it returns (a representation of) a winning strategy itself; the former is referred to as finding the winning positions, and the latter as strategy synthesis.

A fundamental result for parity games is positional determinacy : each position is either winning for Even or winning for Odd, and each player has a positional strategy that is winning for her from each of her winning positions. The former is straightforward because parity games—the way we defined them here—are finite games, but the latter is non-trivial. When playing according to a positional strategy, in every vertex that a player owns, she always follows the same outgoing edge, no matter where the token has arrived to the vertex from. The answer to the strategy synthesis problem typically is in the form of a positional strategy succinctly represented by a set of edges: (at least) one edge outgoing from each vertex owned by Even.

Throughout the paper, we write $V$ and $E$ for the sets of vertices and edges in a parity game graph and $\pi(v)$ for the (positive integer) priority of a vertex $v\in V$. We also use $n$ to denote the number of vertices; $\eta$ to denote the numbers of vertices with an odd priority; $m$ for the number of edges; and $d$ for the smallest even number that is not smaller than the priority of any vertex. We say that a cycle is even if and only if the highest priority of a vertex on the cycle is even. We will write $\lg x$ to denote $\log_{2}x$, and $\log x$ whenever the base of the logarithm is moot.

Parity games are fundamental in logic and verification because they capture—in an easy-to-state combinatorial game form—the intricate expressive power of nesting least and greatest fixpoint operators (interpreted over appropriate complete lattices), which play a central role both in the theory and in the practice of algorithmic verification. In particular, the modal $\mu$-calculus model checking problem is polynomial-time equivalent to solving parity games , but parity games are much more broadly applicable to a multitude of modal, temporal, and fixpoint logics, and in the theory of automata on infinite words and trees .

The problem of solving parity games has been found to be both in NP and in coNP in the early 1990’s . Such problems are said to be well characterised and are considered very unlikely to be NP-complete. Parity games share the rare complexity-theoretic status of being well characterised, but not known to be in P, with such prominent problems as factoring, simple stochastic games, and mean-payoff games . Earlier notable examples include linear programming and primality, which were known to be well characterised for many years before breakthrough polynomial-time algorithms were developed for them in the late 1970’s and the early 2000’s, respectively.

After decades of algorithmic improvements for the modal mu-calculus model checking and for solving parity games , a recent breakthrough came from Calude et al. who gave the first algorithm that works in quasi-polynomial time, where the best upper bounds known previously were subexponential of the form $n^{O(\sqrt{n})}$ . Remarkably, Calude et al. have also established fixed parameter tractability for the key parameter $d$—the number of distinct vertex priorities.

2 Progress measures

Our work is inspired by the succinct counting technique of Calude et al. , but it is otherwise rooted in earlier work on rankings and progress measures , and in particular it is centered on their uses for algorithmically solving games on finite game graphs .

What is a progress measure? Paraphrasing Klarlund’s ideas, Vardi coined the following slogans:

A progress measure is a mapping on program states that quantifies how close each state is to satisfying a property about infinite computations. On every program transition the progress measure must change in a way ensuring that the computation converges toward the property.

[existence of progress measures] is not surprising from a recursion-theoretic point of view [and it] is in essence expressed by the Kleene-Suslin Theorem of descriptive set theory,

the goal of research in this area should not be merely to prove existence of progress measures, but rather to prove the existence of progress measures with some desirable properties.

For example, Klarlund , as well as Kupferman and Vardi considered (appropriate relaxations of) progress measures on infinite graphs and applied them to complementation and checking emptiness of automata on infinite words and trees. Jurdziński , Piterman and Pnueli , and Schewe focused instead on optimising the magnitude of progress measures for Mostowski’s parity conditions and for Rabin conditions on finite graphs in order to improve the complexity of solving games with parity, Rabin, and Streett winning conditions.

In the case of parity games, this allowed Jurdziński to devise the lifting algorithm that works in time $n^{d/2+O(1)}$, where $n$ is the number of vertices and $d$ is the number of distinct vertex priorities. Schewe improved the running time to $n^{d/3+O(1)}$ by combining the divide-and-conquer dominion technique of Jurdziński et al. with a modification of the lifting algorithm, using the latter to detect medium-sized dominions more efficiently.

3 Our contribution

We follow the work of Jurdziński and Schewe who have developed efficient algorithms for solving parity games by proving existence of small progress measures. Our contribution is to prove that every progress measure on a finite game graph is—in an appropriate sense—equivalent to a succinctly represented progress measure. This paves the way to the design of an algorithm that slightly improves the quasi-polynomial time complexity of the algorithm of Calude et al. , and that significantly improves the space complexity from quasi-polynomial down to quasi-linear.

More specifically and technically, we argue that navigation paths from the root to nodes in ordered trees of height $h$ and with at most $n$ leaves can be succinctly encoded using at most approximately $\lg h\cdot\lg n$ bits by means of bounded adaptive multi-counters. The statement and the proof of this tree coding result are entirely independent of parity games, and they are notable in their own right. The concept of ordered tree coding that we introduce seems fundamental and it may find unrelated applications.

Our application of the tree coding result to parity games is based on the fact that a progress measure for a graph with $n$ vertices and $d$ distinct vertex priorities can be viewed as a labelling of vertices by (the navigation paths from the root to) leaves of an ordered tree of height $d/2$ and with at most $n$ leaves. It then follows that there are approximately at most $2^{\lg d\cdot\lg n}=n^{\lg d}$ possible encodings to consider for every vertex, a considerable gain over the naive bound $2^{d/2\cdot\lg n}=n^{d/2}$ that determined the complexity of Jurdziński’s algorithm. We argue, however, that the lifting technique developed by Jurdziński can be adapted to iteratively compute a succinct representation of a progress measure in the quasi-polynomial time $O\left(n^{\lg d}\right)$ and quasi-linear space $O(n\log n\cdot\log d)$.

4 Related work

The high-level idea of the algorithm of Calude et al. bears similarity to the approach of Bernet et al. : first devise a finite safety automaton that recognizes infinite sequences of priorities that result in a win for Even (in the case of Bernet et al., given an explicit upper bound on the number of occurrences of each odd priority before an occurrence of a higher priority), and then solve the safety game obtained from the product automaton that simulates the safety automaton on the game graph.

The key innovation of Calude et al. is their succinct counting technique which allows them to devise a finite (safety) automaton (not made explicit, but easy to infer from their work) with only $n^{O(\log d)}$ states, while that of Bernet et al. may have $\Omega\left((n/d)^{d/2}\right)$ states. On the other hand, Calude et al. construct the safety game explicitly before solving it, thus requiring not only quasi-polynomial time but also quasi-polynomial space, and not just in the worst case but always. In contrast, Bernet et al. develop a technique for solving the safety game symbolically without explicitly constructing it, hence avoiding superpolynomial space complexity; as they point out: “The algorithm actually turns out to be the same as [the lifting] algorithm of Jurdzinski” (although, in fact, they bring down rather than lift up).

Contemporaneously and independently from the early version of our work , Fearnley et al. have developed a technique of lifting Calude et al.’s play summaries so as to efficiently solve Calude et al.’s safety game without constructing it explicitly, and Gimbert and Ibsen-Jensen have given slightly improved upper bounds on the running time of Calude et al.’s algorithm. While our succinct progress measures and bounded adaptive multi-counters are notably different from Calude et al.’s and Fearnley et al.’s play summaries, the complexity bounds achieved by us, by Fearnley et al., and by Gimbert and Ibsen-Jensen are remarkably similar. For the benchmark case when $d\leq\lg n$, Calude et al. gave the $O(n^{5})$ upper bound on the running time, and our $O(mn^{2.38})$ bound is slightly better than the $O(mn^{2.55})$ improved bound derived for Calude et al.’s algorithm by Gimbert and Ibsen-Jensen. In the general case, Calude et al. gave the $O(n^{\lg d+6})$ upper bound on the running time of their algorithm for finding the winning positions and $O(n^{\lg d+7})$ for strategy synthesis. For the case $d=\omega(\log n)$, we establish the $O\left(dm\eta^{\lg(d/{\lg\eta})+1.45}\right)$ running time upper bound, which is roughly the same as the one obtained by Fearnley et al., and Gimbert and Ibsen-Jensen achieve the analogous $O\left(dmn^{\lg(d/{\lg n})+1.45}\right)$ upper bound for Calude et al.’s algorithm. Notably, however, both Fearnley et al. and Gimbert and Ibsen-Jesen claim those bounds only for the cases $d\geq\log^{2}\eta$ and $d=\Omega(\log^{2}n)$, respectively.

Bojańczyk and Czerwiński [3, Chapter 3] have recently developed a reworking of the algorithm of Calude et al. that is based on constructing a deterministic safety automaton of quasi-polynomial size that separates the language of all infinite words of vertices in which all cycles are even from its odd counterpart. We supplement the main results in this paper by developing separating automata of quasi-polynomial size that are based on the bounded adaptive multi-counters. They seem significantly different from the separating automata of Calude et al. cum Bojańczyk and Czerwiński which are based on play summaries. Moreover, both the construction and the proof of correctness are perhaps surprisingly simple.

Succinct tree coding

What is an ordered tree? One formalisation is that it is a prefix-closed set of sequences of elements of a linearly ordered set. For clarity, in contrast to graphs, we refer to those sequences as nodes, and the maximal nodes (w.r.t. the prefix ordering) are called leaves. The root of the tree is the empty sequence, sequences of length $1$ are the children of the root, sequences of length $2$ are their children, and so on. We also refer to the elements of the linearly ordered set that occur in the sequences as branching directions: for example, if we use the non-negative integers with the usual ordering as branching directions, then the node $(3,0,5)$ is the child of the node $(3,0)$ reached from it via branching direction $5$. Moreover, we refer to the sequences of branching directions that uniquely identify nodes as their navigation paths.

What do we mean by ordered-tree coding? The notion we find useful in the context of this work is an order-preserving relabelling of branching directions, allowing for the relabellings at various nodes to differ from one another (or, in other words, to be adaptive). The intention when coding in this way is to obtain an isomorphic ordered tree, and the intended purpose is to be able to more succinctly encode the navigation paths for each leaf in the tree.

We define the set $B_{g,h}$ of $g$-bounded adaptive $h$-counters to consist of $h$-tuples of binary strings whose total length is at most $g$. For example, $(0,\varepsilon,1,0)$ and $(\varepsilon,1,\varepsilon,0)$ are $3$-bounded adaptive $4$-counters, but $(0,1,\varepsilon,\varepsilon,0)$ and $(10,\varepsilon,01,\varepsilon)$ are not—the former is a $5$-tuple, and the total length of the binary strings in the latter is $4$.

We define a strict linear ordering $<$ on finite binary strings as follows, for both binary digits $b$, and for all binary strings $s$ and $s^{\prime}$:

Equivalently, it is the ordering on the rationals obtained by the mapping

We extend the ordering to $B_{g,h}$ lexicographically. For example, $(00,\varepsilon,1)<(0,0,0)$ because $00<0$, and $(\varepsilon,011,1)<(\varepsilon,\varepsilon,000)$ because $011<\varepsilon$.

If $L_{<}\not=\emptyset$, apply the inductive hypothesis to the subtree with $L_{<}$ as the set of leaves, and append one leading to the binary strings that code the first branching direction.

If $L_{>}\not=\emptyset$, apply the inductive hypothesis to the subtree with $L_{>}$ as the set of leaves, and append one leading $1$ to the binary strings that code the first branching direction.

The lemma is illustrated, for an ordered tree of height $2$ and with $8$ leaves, in Figures 1 and 2.

of $\lceil\lg\eta\rceil$-bounded adaptive $i$-counters, where $0\leq i\leq d/2$, which is the dominating term in the worst-case running time bounds of our lifting algorithm for solving parity games.

Succinct progress measures

For finite parity game graphs, a progress measure is a mapping from the $n$ vertices to $d/2$-tuples of non-negative integers (that also satisfies the so-called progressiveness conditions on an appropriate set of edges, as detailed below). Note that an alternative interpretation is that a progress measure maps every vertex to a leaf in an ordered tree $T$ in which each of the at most $n$ leaves has a navigation path of length $d/2$.

What are the conditions that such a mapping needs to satisfy to be a progress measure? For every priority $p\in\{1,2,\dots,d\}$, we obtain the $p$-truncation $(r_{d-1},r_{d-3},\dots,r_{1})|_{p}$ of the $d/2$-tuple $(r_{d-1},r_{d-3},\dots,r_{1})$ of non-negative integers, one per each odd priority, by removing the components corresponding to all odd priorities $i$ lower than $p$. For example, we have $(2,7,1,4)|_{8}=\varepsilon$, $(2,7,1,4)|_{5}=(2,7)$ and $(2,7,1,4)|_{2}=(2,7,1)$. We compare tuples using the lexicographic order. We say that an edge $(v,u)\in E$ is progressive in $\mu$ if

and the inequality is strict when $\pi(v)$ is odd. Finally, the mapping $\mu:V\to T$ is a progress measure if:

for every vertex owned by Even, some outgoing edge is progressive in $\mu$, and

for every vertex owned by Odd, every outgoing edge is progressive in $\mu$.

2 Trimmed progress measures

Observe that the progressiveness condition of every edge $(v,u)\in E$ is formulated by referring to the $\pi(v)$-truncations of the tuples labelling vertices $v$ and $u$, so if the label of $v$ is $(r_{d-1},r_{d-3},\dots,r_{1})$ then the components $r_{i}$ for $i<\pi(v)$ are superfluous for stating the condition. It is therefore reasonable to consider trimmed progress measures that label vertices with tuples $(r_{d-1},r_{d-3},\dots,r_{k+2},r_{k})$ of length at most $d/2$, rather than insisting on all vertices having labels of length exactly $d/2$. In the alternative interpretation discussed above, such a trimmed progress measure may then map some vertices to nodes in an ordered tree (of height at most $d/2$) that are not leaves.

We clarify that if two tuples of different lengths are to be compared lexicographically, and if the shorter one is a prefix of the longer one, then the shorter one is defined to be lexicographically strictly smaller than the longer one For example, we have $(1,0)<(1,0,3)$, but $(1,0,3)<(1,1)$. Moreover, truncations of tuples of length smaller than $d/2$ are defined analogously; in particular, if $p\leq k$ then $(r_{d-1},r_{d-3},\dots,r_{k})|_{p}=(r_{d-1},r_{d-3},\dots,r_{k})$.

3 Succinct progress measures

It is well known that existence of a progress measure is sufficient and necessary for existence of a winning strategy for Even from every starting vertex . Our main contribution in this section is the observation (Lemma 4) that this is also true for existence of a succinct progress measure, in which the ordered tree $T$ is such that:

finite binary strings ordered as in (1) are used as branching directions instead of non-negative integers, and

for every navigation path, the sum of lengths of the binary strings used as branching directions is at most $\lceil\lg\eta\rceil$;

or in other words, that every navigation path in $T$ is a $\lceil\lg\eta\rceil$-bounded adaptive $i$-counter, for some $i,0\leq i\leq d/2$; recall that $\eta$ is the number of vertices with an odd priority.

In succinct progress measures, truncations and lexicographic ordering of tuples, as well as progressiveness of edges, are defined analogously. Again, we clarify that if two tuples of different lengths are to be compared lexicographically, and if the shorter one is a prefix of the longer one, then the shorter one is defined to be lexicographically strictly smaller than the longer one. For example, we have $(01,\varepsilon)<(01,\varepsilon,00)$, but $(01,\varepsilon,000)<(1000,\varepsilon)$.

4 Sufficiency

Sufficiency does not require a new argument because the standard reasoning—for example as in [14, Proposition 4]—relies only on the ordered tree structure (through truncations), and not on what ordered set is used for the branching directions. We provide a proof here for completeness.

If there is a succinct progress measure then there is a positional strategy for Even that is winning for her from every starting vertex.

Let $\mu$ be a succinct progress measure. Let Even use a positional strategy that only follows edges that are progressive in $\mu$. Since every edge outgoing from vertices owned by Odd is also progressive in $\mu$, it follows that only progressive edges will be used in every play consistent with the strategy. Therefore, in order to verify that the strategy is winning for Even, it suffices to prove that if all edges in a simple cycle are progressive in $\mu$ then the cycle is even.

Let $v_{1},v_{2},\dots,v_{k}$ be a simple cycle in which all edges $(v_{1},v_{2})$, $(v_{2},v_{3})$, …, $(v_{k-1},v_{k})$, and $(v_{k},v_{1})$ are progressive in $\mu$. For the sake of contradiction, suppose that the highest priority $p$ that occurs on the cycle is odd, and without loss of generality, let $\pi(v_{1})=p$. By progressivity of all the edges on the cycle, we have that

5 Necessity

We prove necessity by first slightly strengthening the existence of the least progress measure result [14, Theorem 11], and then by applying the succinct tree coding lemma (Lemma 1).

As discussed earlier in this section, the range of a progress measure is the set of nodes in a tree of height $d/2$ and with at most $n$ leaves. By applying Lemma 1 to this tree we may conclude that there is a tree coding in which branching directions on every navigation path use at most $\lceil\lg n\rceil$ bits. This way we come short [sic] of satisfying our definition of a succinct progress measure: the definition allows us, on every path, to use at most $\lceil\lg\eta\rceil$ bits for branching directions, which may be strictly smaller than $\lceil\lg n\rceil$.

In order to overcome this hurdle, we first define the operation of a trimming of a progress measure. Let $\mu$ be a progress measure. We define the trimming $\mu^{\downarrow}$ of $\mu$ as follows: for every vertex $v$, we let $\mu^{\downarrow}(v)$ be the longest prefix of $\mu(v)$ whose last component is not ; in particular, if $\mu(v)$ is a sequence of s of length $d/2$ then $\mu^{\downarrow}(v)$ is the empty sequence. For convenience, we also define the inverse operation: if $\mu$ is a trimmed progress measure then for every vertex $v$, we let $\mu^{\uparrow}(v)$ be the sequence of length $d/2$ obtained by adding an appropriate number (possibly none) of s at the end of $\mu(v)$.

Recall that by [14, Corollary 8] and by the proof of [14, Theorem 11] the least progress measure $\mu_{*}$ exists, where the relevant order on mappings from vertices to sequences of non-negative integers is pointwise lexicographic.

The trimming $\mu_{*}^{\downarrow}$ of the least progress measure $\mu_{*}$ is a trimmed progress measure and the ordered tree that it maps to has at most $\eta$ leaves.

That $\mu_{*}^{\downarrow}$ is a trimmed progress measure follows routinely from $\mu_{*}$ being a progress measure and from the definion of a trimmed progress measure.

We argue that for every leaf in the ordered tree $T$ that $\mu_{*}^{\downarrow}$ maps into, there is a vertex $v\in V$ with an odd priority, such that $\mu_{*}^{\downarrow}(v)$ is that leaf, which implies the other claim of the lemma.

Let $\lambda=(r_{d-1},r_{d-3},\dots,r_{k})$ be a leaf in $T$. For the sake of contradiction, assume that every vertex $v\in V$ such that $\mu_{*}^{\downarrow}(v)=\lambda$ has an even priority. Note that—by the definition of a trimming—$r_{k}\not=0$, and hence—because $\mu_{*}$ is the least progress measure—$k>\pi(v)$. We define the mapping $\mu_{\lambda}$ as follows:

for all $v\in V$. We argue that $\mu_{\lambda}$ is a trimmed progress measure, and hence $\mu_{\lambda}^{\uparrow}$ is a progress measure, which—because $\mu_{\lambda}^{\uparrow}$ is strictly smaller than $\mu_{*}$—duly contradicts the assumption that $\mu_{*}$ was the least progress measure.

We only need to verify that every edge $(v,u)\in E$, such that $\mu_{*}^{\downarrow}(v)=\lambda$, and that is progressive in $\mu_{*}^{\downarrow}$, is also progressive in $\mu_{\lambda}$. This is straightforward if $\mu_{*}^{\downarrow}(u)=\lambda$. Otherwise, we have $\mu_{*}^{\downarrow}(v)|_{\pi(v)}>\mu_{*}^{\downarrow}(u)|_{\pi(v)}$, which implies that

We now argue that $\mu_{\lambda}(v)|_{\pi(v)}\geq\mu_{\lambda}(u)|_{\pi(v)}$ by considering the following two cases.

where the inequality follows from (2) and because no component in the least progress measure $\mu_{*}$ exceeds $n$. ∎

Necessity now follows from applying the succinct coding lemma (Lemma 1) to the tree with at most $\eta$ leaves, which is obtained by Lemma 3.

If there is a strategy for Even that is winning for her from every starting vertex, then there is a succinct progress measure.

Lifting algorithm

Without loss of generality, we assume that $\eta\leq n/2$. Otherwise, we have that the number of vertices with an even priority is less than $n/2$, and we can apply the algorithm below to the dual game obtained by reducing the priority of each vertex by $1$ and exchanging the roles of the two players; the winning set and a winning strategy for player Even in the dual game computed by the algorithm are the winning set and a winning strategy for player Odd in the original one. Note that the algorithm can be applied without any asymptotic penalty (and only cosmetic changes) to games in which vertices of priority are allowed, and hence the analysis of the algorithm applies to both the original game and its dual.

Consider the following linearly ordered set of bounded adaptive multi-counters:

and let $S_{\eta,d}^{\top}$ denote the same set with an extra top element $\top$. We extend the notion of succinct progress measures to mappings $\mu:V\to S_{\eta,d}^{\top}$ by:

defining the truncations of $\top$ as $\top{|_{p}}=\top$ for all $p$;

regarding edges $(v,u)\in E$ such that $\mu(v)=\mu(u)=\top$ and $\pi(v)$ is odd as progressive in $\mu$.

The set of all mappings $V\to S_{\eta,d}^{\top}$ ordered pointwise is a complete lattice.

If $\mu^{*}$ is the least succinct progress measure, then $\{v\,:\,\mu^{*}(v)\neq\top\}$ is the set of winning positions for Even, and any choice of edges progressive in $\mu^{*}$, at least one going out of each vertex she owns, is her winning positional strategy.

The partial order of all mappings $V\to S_{\eta,d}^{\top}$ is the pointwise product of $n$ copies of the finite linear order $S_{\eta,d}^{\top}$.

This holds for any family of inflationary monotone operators on a finite complete lattice. Consider any such maximal sequence from $\mu$. It is an upward chain from $\mu$ to some $\mu^{*}$ which is a simultaneous fixed point of all the operators. For any $\mu^{\prime}\geq\mu$ which is also a simultaneous fixed point, a simple induction confirms that $\mu^{*}\leq\mu^{\prime}$.

Here we have a rewording of the definition of a succinct progress measure, cf. Section 3.

The set of winning positions for Even is contained in $\{v\,:\,\mu^{*}(v)\neq\top\}$ by Lemma 4 because $\mu^{*}$ is the least succinct progress measure.

Since $\mu^{*}$ is a succinct progress measure, we have that, for every progressive edge $(v,w)$, if $\mu^{*}(v)\neq\top$ then $\mu^{*}(w)\neq\top$. It remains to apply Lemma 2 to the subgame consisting of the vertices $\{v\,:\,\mu^{*}(v)\neq\top\}$, the chosen edges from vertices owned by Even, and all edges from vertices owned by Odd. ∎

Note that the algorithm in Table 1 is a solution to both variants of the algorithmic problem of solving parity games: it finds the winning positions and produces a positional winning strategy for Even.

2 Algorithm analysis

The following lemma offers various estimates for the size of the set $S_{\eta,d}$ of succinct adaptive multi-counters used in the lifting algorithm in Table 1, and which is the dominating factor in the worst-case upper bounds on the running time of the algorithm. A particular focus is the analysis pinpointing the range of the numbers of distinct priorities $d$ (measured as functions of the number $\eta$ of vertices with an odd priority) in which the algorithm may cease to be polynomial-time. The “phase transition” occurs when $d$ is logarithmic in $\eta$: if $d=o(\log\eta)$ then the size of $S_{\eta,d}$ is $O\left(\eta^{1+o(1)}\right)$, if $d=\Theta(\log\eta)$ then the size of $S_{\eta,d}$ is bounded by a polynomial in $\eta$ but its degree depends on the constant hidden in the big-$\Theta$, and if $d=\omega(\log\eta)$ then the size of $S_{\eta,d}$ is superpolynomial in $\eta$.

$|S_{\eta,d}|\leq 2^{\lceil\lg\eta\rceil}\binom{\lceil\lg\eta\rceil+d/2+1}{d/2}$.

If $d=O(1)$ then $|S_{\eta,d}|=O\left(\eta\lg^{d/2}\eta\right)$.

If $d/2=\lceil\delta\lg\eta\rceil$, for some constant $\delta>0$, then $|S_{\eta,d}|=\Theta\left(\eta^{\lg(\delta+1)+\lg(e_{\delta})+1}\middle/\sqrt{\log\eta}\right)$, where $e_{\delta}=(1+1/\delta)^{\delta}$.

If $d=o(\log\eta)$ then $|S_{\eta,d}|=O\left(\eta^{1+o(1)}\right)$.

If $d=O(\log\eta)$ then $|S_{\eta,d}|$ is bounded by a polynomial in $\eta$.

If $d=\omega(\log\eta)$ then $|S_{\eta,d}|$ is superpolynomial in $\eta$ and $|S_{\eta,d}|=O\left(d\eta^{\lg(d/{\lg\eta})+1.45}\right)$.

There are $2^{\lceil\lg\eta\rceil}$ bit sequences of length $\lceil\lg\eta\rceil$ and for every $i,0\leq i\leq d/2$, there are

distinct ways of distributing the number $\lceil\lg\eta\rceil$ of bits to $i+1$ components (the $i$ components in the succinct adaptive $i$-counter, and an extra one for the “unused” bits). By the “parallel summation” binomial identity, we obtain

In cases 3) and 6) below we analyse the simpler expressions $\binom{\lceil\lg\eta\rceil+d/2}{d/2}$ and $\binom{\lceil\lg\eta\rceil+d/2}{\lceil\lg\eta\rceil}$, respectively, instead of the above $\binom{\lceil\lg\eta\rceil+d/2+1}{d/2}$, in order to declutter calculations. This is justified because in each context the respective simpler expression is within a constant factor of the latter one, and hence the asymptotic results are not affected by the simplification.

This is easy to verify for $d=2$ and $d=4$. If $d\geq 6>2e$ then for sufficiently large $\eta$ we have:

To avoid hassle, consider only the values of $\eta$ and $\delta$, such that both $\lg\eta$ and $\delta\lg\eta$ are integers. Let $d=2\delta\lg\eta$ and apply [1, Lemma 4.7.1] (reproduced as Lemma 11 in the Appendix) to the binomial coefficient

where $H(p)=-p\lg p-(1-p)\lg(1-p)$ is the binary entropy function, defined for $p\in$. A skilful combinator will be able to verify the identity

This is a corollary of part 3) by observing that $\lim_{\delta\downarrow 0}e_{\delta}=1$ and hence:

Again, this is a corollary of part 3) by observing that the expression $\lg(\delta+1)+\lg(e_{\delta})+1$ is $O(1)$ as a function of $\eta$.

The first statement is a corollary of part 3) by observing that $\lim_{\delta\to\infty}\lg(\delta+1)=\infty$ and $\lim_{\delta\to\infty}e_{\delta}=e$, and hence:

In order to prove the latter statement, note that

and $\lg e+o(1)<1.4427$ for sufficiently large $\eta$. ∎

If $d=O(1)$ then the algorithm runs in time $O\left(m\eta\lg^{d/2+1}\eta\right)$.

If $d=o(\log\eta)$ then the algorithm runs in time $O(m\eta^{1+o(1)})$.

If $d\leq 2\lceil\delta\lg\eta\rceil$, for some positive constant $\delta$, then the algorithm runs in time

In particular, if $d\leq\lceil\lg\eta\rceil$, then the running time is $O\left(m\eta^{2.38}\right)$.

If $d=\omega(\log\eta)$ then the algorithm runs in time $O\left(dm\eta^{\lg(d/{\lg\eta})+1.45}\right)$.

The algorithm works in space $O(n\log n\cdot\log d)$.

The work space requirement is dominated by the number of bits needed to store a single mapping $\mu:V\to S_{\eta,d}^{\top}$, which is at most $n\lceil\lg\eta\rceil\lceil\lg d\rceil$.

From there, the various stated bounds are obtained by Lemma 6. For the last statement in part 3), note that if $\delta=1/2$ then $d\leq\lceil\lg\eta\rceil$ implies $d/2\leq\lceil\delta\lg\eta\rceil$, and

where the padding by s is up to the total length $\lceil\lg\eta\rceil$ of $\sigma$.

If $k\leq\pi(v)$ and the total length of $s_{i}$ for $i\geq\pi(v)$ is less than $\lceil\lg\eta\rceil$, then obtain $\sigma$ as

where the padding by s (if any) is up to the total length $\lceil\lg\eta\rceil$ of $\sigma$.

The algorithm runs in time $\max\left\{2^{O(d\log d)},O\left(mn^{2.38}\right)\right\}$. ∎

Separating automata

Bojańczyk and Czerwiński [3, Chapter 3] have recently developed a reworking of the algorithm of Calude et al. that proceeds by:

constructing a deterministic safety automaton that separates the language of all infinite words of vertices in which all cycles are even from its odd counterpart;

forming a safety game as a synchronous product of the given parity game and the constructed separating automaton, in which the winning condition for Even is the acceptance condition of the automaton;

Their approach clarifies that the bulk of the quasi-polynomial time breakthrough can be seen as showing how to construct a separating automaton of quasi-polynomial size.

In the rest of this section, we develop separating automata of quasi-polynomial size that are based on the bounded adaptive multi-counters.

Working with notations $V$, $n$, $\pi$, $d$ and $\eta$ as before, let us say that:

a cycle in a word of vertices is an infix whose first and last elements are the same;

the language $\textup{All\-Cycles\-Even}_{V,\pi}$ consists of all infinite words of vertices in which all cycles are even;

the language $\textup{Limsup\-Odd}_{V,\pi}$ consists of all infinite words of vertices in which the highest priority occurring infinitely often is odd;

the set $S_{\eta,d}^{\bot}$ is the linearly ordered set $S_{\eta,d}$ of bounded adaptive multi-counters, with an extra bottom element $\bot$ whose truncations are defined as $\bot|_{p}=\bot$;

a pair $(\sigma,\tau)$ of multi-counters is progressive with respect to a priority $p$ if and only if: $\sigma|_{p}\geq\tau|_{p}$ and, when $\pi(v)$ is odd, either the inequality is strict or $\sigma=\tau=\bot$.

Let $\mathcal{D}_{V,\pi}$ be the following deterministic automaton that reads infinite words of vertices:

the set of states is $S_{\eta,d}^{\bot}$, the initial state is the maximum multi-counter

from state $\sigma$, reading $v$ leads to the greatest state $\tau$ such that $(\sigma,\tau)$ is progressive with respect to $\pi(v)$;

The automaton accepts if and only if its run is safe, i.e. does not visit an unsafe state.

The property we now establish implies that the automaton separates the language of all infinite words of vertices in which all cycles are even from its odd counterpart, because the latter is included in the language where the highest priority occuring infinitely often is odd.

The automaton $\mathcal{D}_{V,\pi}$ accepts all words in the language $\textup{All\-Cycles\-Even}_{V,\pi}$ and rejects all words in the language $\textup{Limsup\-Odd}_{V,\pi}$.

That every word with the highest priority occuring infinitely often odd is rejected can be seen straightforwardly, since more than $2^{\lceil\lg\eta\rceil}$ occurences of such a priority in a word without intermediate occurences of higher priorities necessarily cause the multi-counters to underflow to $\bot$.

The interesting half of the statement follows from the next claim by monotonicity of the truncation operations. Here $\mathcal{N}_{V,\pi}$ is the nondeterministic extension of the automaton $\mathcal{D}_{V,\pi}$ by replacing the ‘greatest’ requirement for the successor states with ‘any’. Being nondeterministic, $\mathcal{N}_{V,\pi}$ accepts an infinite word if and only if some run on it is safe.

On every finite or infinite word over $V$ in which all cycles are even, the automaton $\mathcal{N}_{V,\pi}$ has a safe run.

We establish the claim by an induction on $\lceil\lg\eta\rceil$ and $d/2$ that follows the same pattern as the proof of Lemma 1.

The base case, $\eta=1$ and $d/2=0$, is trivial.

It suffices to consider words $\varpi$ that contain no vertices of the highest even priority $d$. Since $\varpi$ has no odd cycles, it can be decomposed as $\varpi_{1}\,\varpi_{\varepsilon}\,\varpi_{0}$, where:

if the word $\varpi_{1}$ is nonempty, then it ends with a vertex of the highest odd priority $d-1$ and the set $V_{1}$ of all other odd-priority vertices that occur in $\varpi_{1}$ has cardinality at most $\eta/2$;

the set $V_{\varepsilon}$ of all vertices that occur in the word $\varpi_{\varepsilon}$ contains no vertex of priority $d-1$;

if the word $\varpi_{0}$ is nonempty, then it begins with a vertex of the highest odd priority $d-1$ and the set $V_{0}$ of all other odd-priority vertices that occur in $\varpi_{0}$ has cardinality at most $\eta/2$.

It remains to compose a safe run of the automaton $\mathcal{N}_{V,\pi}$ on the word $\varpi$ by concatenating the following subruns, where we focus on the most involved case of $\varpi_{1}$ and $\varpi_{0}$ both nonempty:

obtain a safe run of the automaton $\mathcal{N}_{V_{1},\pi}$ on the word $\varpi_{1}$ without its last vertex by the inductive hypothesis, and append one leading $1$ to the first binary strings in all its states;

obtain a safe run of the automaton $\mathcal{N}_{V_{\varepsilon},\pi}$ on the word $\varpi_{\varepsilon}$ by the inductive hypothesis, and insert $\varepsilon$ as the first binary string in all its states;

obtain a safe run of the automaton $\mathcal{N}_{V_{0},\pi}$ on the word $\varpi_{0}$ without its first vertex by the inductive hypothesis, and append one leading to the first binary strings in all its states. ∎

That also completes the proof the theorem. ∎

Acknowledgements

We thank Kousha Etessami, John Fearnley, Filip Mazowiecki, and Sven Schewe for helpful comments; and Adam Lewis (a second-year undergraduate at the time) for finding and fixing a bug in the proof of Theorem 7.

References

Appendix

where $H(p)=-p\lg p-(1-p)\lg(1-p)$ is the binary entropy function.