1

# A Universal Attractor Decomposition Algorithm
for Parity Games

Marcin Jurdziński  nnnn-nnnn-nnnn-nnnn Department of Computer
ScienceUniversity of Warwick<EMAIL_ADDRESS>and  Rémi Morvan
nnnn-nnnn-nnnn-nnnn ENS Paris-Saclay<EMAIL_ADDRESS>
###### Abstract.

An attractor decomposition meta-algorithm for solving parity games is given
that generalizes the classic McNaughton-Zielonka algorithm and its recent
quasi-polynomial variants due to Parys (2019), and to Lehtinen, Schewe, and
Wojtczak (2019). The central concepts studied and exploited are attractor
decompositions of dominia in parity games and the ordered trees that describe
the inductive structure of attractor decompositions.

The main technical results include the embeddable decomposition theorem and
the dominion separation theorem that together help establish a precise
structural condition for the correctness of the universal algorithm: it
suffices that the two ordered trees given to the algorithm as inputs embed the
trees of some attractor decompositions of the largest dominia for each of the
two players, respectively.

The universal algorithm yields McNaughton-Zielonka, Parys’s, and Lehtinen-
Schewe-Wojtczak algorithms as special cases when suitable universal trees are
given to it as inputs. The main technical results provide a unified proof of
correctness and deep structural insights into those algorithms.

This paper motivates a research program of developing new efficient algorithms
for solving parity games by designing new classes of small trees that embed
the largest dominia in relevant classes of parity games. An early success
story in this research program is the recent development, by Daviaud,
Jurdziński, and Thejaswini (2019), of Strahler-universal trees, which embed
dominia in games of bounded register number, introduced by Lehtinen (2018).
When run on these trees, the universal algorithm can solve games with bounded
register number in polynomial time and in quasi-linear space.

A symbolic implementation of the universal algorithm is also given that
improves the symbolic space complexity of solving parity games in quasi-
polynomial time from $O(d\lg n)$—achieved by Chatterjee, Dvořák, Henzinger,
and Svozil (2018)—down to $O(\lg d)$, where $n$ is the number of vertices and
$d$ is the number of distinct priorities in a parity game. This not only
exponentially improves the dependence on $d$, but it also entirely removes the
dependence on $n$.

parity games, universal trees, attractor decompositions, separation,
embedding, quasi-polynomial, symbolic algorithms

††conference: University of Warwick; January 2020; Coventry, UK††journalyear:
2020††doi: ††copyright: none††ccs: Software and its engineering General
programming languages††ccs: Social and professional topics History of
programming languages

##  1\. Context

###  1.1. Parity games and their significance

Parity games play a fundamental role in automata theory, logic, and their
applications to verification (Emerson and Jutla, 1991), program analysis
(Baldan et al., 2019; Hausmann and Schröder, 2019), and synthesis (Grädel et
al., 2002; Luttenberger et al., 2019). In particular, parity games are very
intimately linked to the problems of emptiness and complementation of non-
deterministic automata on trees (Emerson and Jutla, 1991; Zielonka, 1998),
model checking and satisfiability checking of fixpoint logics (Emerson and
Jutla, 1991; Emerson et al., 1993; Bradfield and Walukiewicz, 2018),
evaluation of nested fixpoint expressions (Hasuo et al., 2016; Baldan et al.,
2019; Hausmann and Schröder, 2019), or fair simulation relations (Etessami et
al., 2005). It is a long-standing open problem whether parity games can be
solved in polynomial time (Emerson et al., 1993).

The impact of parity games goes well beyond their home turf of automata
theory, logic, and formal methods. For example, an answer (Friedmann, 2009) of
a question posed originally for parity games (Vöge and Jurdziński, 2000) has
strongly inspired major breakthroughs on the computational complexity of
fundamental algorithms in stochastic planning (Fearnley, 2010) and linear
optimization (Friedmann, 2011b; Friedmann et al., 2011), and parity games
provide the foundation for the theory of nested fixpoint expressions used in
program analysis (Baldan et al., 2019; Hausmann and Schröder, 2019) and
coalgebraic model checking (Hasuo et al., 2016).

###  1.2. Related work

The major breakthrough in the study of algorithms for solving parity games
occurred in 2017 when Calude, Jain, Khoussainov, Li, and Stephan (Calude et
al., 2017) have discovered the first quasi-polynomial algorithm. Three
other—and seemingly distinctly different—techniques for solving parity games
in quasi-polynomial time have been proposed in quick succession soon after: by
Jurdziński and Lazić (Jurdziński and Lazić, 2017), by Lehtinen (Lehtinen,
2018), and by Parys (Parys, 2019).

Czerwiński, Daviaud, Fijalkow, Jurdziński, Lazić, and Parys (Czerwiński et
al., 2019) have also uncovered an underlying combinatorial structure of
universal trees as provably underlying the techniques of Calude et al., of
Jurdziński and Lazić, and of Lehtinen. Czerwiński et al. have also established
a quasi-polynomial lower bound for the size of smallest universal trees,
providing evidence that the techniques developed in those three papers may be
insufficient for leading to futher improvements in the complexity of solving
parity games. The work of Parys (Parys, 2019) has not been obviously subject
to the quasi-polynomial barrier of Czerwiński et al., making it a focus of
current activity. It is worth noting, though, that Lehtinen, Schewe, and
Wojtczak (Lehtinen et al., 2019), who have improved the complexity of Parys’s
algorithm somewhat, have made an informal observation that the tree of
recursive calls of their algorithm is also universal. The algorithms of Parys
and of Lehtinen et al. are modifications of the classic McNaughton-Zielonka
algorithm (McNaughton, 1993; Zielonka, 1998), which has exponential running
time in the worst case (Friedmann, 2011a), but consistently outperforms most
other algorithms in practice (van Dijk, 2018).

###  1.3. Our contributions

In this work we provide a meta-algorithm—the _universal attractor
decomposition algorithm_ —that generalizes McNaughton-Zielonka, Parys’s, and
Lehtinen-Schewe-Wojtczak algorithms. There are multiple benefits of
considering the universal algorithm.

Firstly, in contrast to Parys’s and Lehtinen-Schewe-Wojtczak algorithms, the
universal algorithm has a very simple and transparent structure that minimally
departs from the classic McNaughton-Zielonka algorithm. Secondly, we observe
that Lehtinen-Schewe-Wojtczak algorithm, as well as non-adaptive versions (see
Sections 3.2 and 4.4) of McNaughton-Zielonka and Parys’s algorithms, all arise
from the universal algorithm by using specific classes of universal trees,
strongly linking the theory of universal trees to the only class of quasi-
polynomial algorithms that had no established formal relationship to universal
trees so far.

Thirdly, we further develop the theory of dominia and their attractor
decompositions in parity games, initiated by Daviaud, Jurdziński, and Lazić
(Daviaud et al., 2018) and by Daviaud, Jurdziński, and Lehtinen (Daviaud et
al., 2019), and we prove two new structural theorems (the embedabble
decomposition theorem and the dominion separation theorem) about ordered trees
of attractor decompositions. Fourthly, we use the structural theorems to
provide a unified proof of correctness of various McNaughton-Zielonka-style
algorithms, identifying very precise structural conditions on the trees of
recusive calls of the universal algorithm that result in it correctly
identifying the largest dominia.

Finally, we observe that thanks to its simplicity, the universal algorithm is
particularly well-suited for solving parity games efficiently in a symbolic
model of computation, when large sizes of input graphs prevent storing them
explicitly in memory. Indeed, we argue that already a routine implementation
of the universal algorithm improves the state-of-the-art symbolic space
complexity of solving parity games in quasi-polynomial time from $O(d\lg n)$
to $O(d)$, but we also show that a more sophisticated symbolic data structure
allows to further reduce the symbolic space of the universal algorithm to
$O(\lg d)$.

##  2\. Dominia and decompositions

###  2.1. Strategies, traps, and dominia

A _parity game_ $\mathcal{G}$ consists of a finite directed graph $(V,E)$, a
partition $(V_{\mathrm{Even}},V_{\mathrm{Odd}})$ of the set of vertices $V$,
and a function $\pi:V\to\left\\{\,0,1,\dots,d\,\right\\}$ that labels every
vertex $v\in V$ with a non-negative integer $\pi(v)$ called its _priority_. We
say that a cycle is _even_ if the highest vertex priority on the cycle is
even; otherwise the cycle is _odd_. We say that a parity game is _$(n,d)$
-small_ if it has at most $n$ vertices and all vertex priorities are at most
$d$.

For a set $S$ of vertices, we write $\mathcal{G}\cap S$ for the substructure
of $\mathcal{G}$ whose graph is the subgraph of $(V,E)$ induced by the sets of
vertices $S$. Sometimes, we also write $\mathcal{G}\setminus S$ to denote
$\mathcal{G}\cap(V\setminus S)$. We assume throughout that every vertex has at
least one outgoing edge, and we reserve the term _subgame_ to substructures
$\mathcal{G}\cap S$, such that every vertex in the subgraph of $(V,E)$ induced
by $S$ has at least one outgoing edge. For a subgame
$\mathcal{G}^{\prime}=\mathcal{G}\cap S$, we sometimes write
$V^{\mathcal{G}^{\prime}}$ for the set of vertices $S$ that the subgame
$\mathcal{G}^{\prime}$ is induced by. When convenient and if the risk of
confusion is contained, we may simply write $\mathcal{G}^{\prime}$ instead of
$V^{\mathcal{G}^{\prime}}$.

A (positional) _Even strategy_ is a set $\sigma\subseteq E$ of edges such
that:

  * •

for every $v\in V_{\mathrm{Even}}$, there is an edge $(v,u)\in\sigma$,

  * •

for every $v\in V_{\mathrm{Odd}}$, if $(v,u)\in E$ then $(v,u)\in\sigma$.

We sometimes call all the edges in such an Even strategy $\sigma$ the
_strategy edges_ , and the definition of an Even strategy requires that every
vertex in $V_{\mathrm{Even}}$ has an outgoing strategy edge, and every
outgoing edge of a vertex in $V_{\mathrm{Odd}}$ is a strategy edge.

For a non-empty set of vertices $T$, we say that an Even strategy $\sigma$
_traps Odd in $T$_ if no strategy edge leaves $T$, that is, $w\in T$ and
$(w,u)\in\sigma$ imply $u\in T$. We say that a set of vertices $T$ is a _trap
for Odd_ if there is an Even strategy that traps Odd in $R$.

Observe that if $T$ is a trap in a game $\mathcal{G}$ then $\mathcal{G}\cap T$
is a subgame of $\mathcal{G}$. For brevity, we sometimes say that a subgame
$\mathcal{G}^{\prime}$ is a trap if $\mathcal{G}^{\prime}=\mathcal{G}\cap T$
and the set $T$ is a trap in $\mathcal{G}$. Moreover, the following simple
_“trap transitivity”_ property holds: if $T$ is a trap for Even in game
$\mathcal{G}$ and $T^{\prime}$ is a trap for Even in subgame $\mathcal{G}\cap
T$ then $T^{\prime}$ is a trap in $\mathcal{G}$.

For a set of vertices $D\subseteq V$, we say that an Even strategy $\sigma$ is
an _Even dominion strategy on $D$_ if:

  * •

$\sigma$ traps Odd in $D$,

  * •

every cycle in the subgraph $(D,\sigma)$ is even.

Finally, we say that a set $D$ of vertices is an _Even dominion_ if there is
an Even dominion strategy on it.

Odd strategies, trapping Even, and Odd dominia are defined in an analogous way
by swapping the roles of the two players. It is an instructive exercise to
prove the following two facts about Even and Odd dominia.

###### Proposition 2.1 (Closure under union).

If $D$ and $D^{\prime}$ are Even (resp. Odd) dominia then $D\cup D^{\prime}$
is also an Even (resp. Odd) dominion.

###### Proposition 2.2 (Dominion disjointness).

If $D$ is an Even dominion and $D^{\prime}$ is an Odd dominion then $D\cap
D^{\prime}=\emptyset$.

From closure under union it follows that in every parity game, there is the
largest Even dominion $W_{\mathrm{Even}}$ (which is the union of all Even
dominia) and the largest Odd dominion $W_{\mathrm{Odd}}$ (which is the union
of all Odd dominia), and from dominion disjointness it follows that the two
sets are disjoint. The positional determinacy theorem states that, remarkably,
the largest Even dominion and the largest Odd dominion form a partition of the
set of vertices.

###### Theorem 2.3 (Positional determinacy (Emerson and Jutla, 1991)).

Every vertex in a parity game is either in the largest Even dominion or in the
largest Odd dominion.

###  2.2. Reachability strategies and attractors

In a parity game $\mathcal{G}$, for a target set of vertices $B$ (“bullseye”)
and a set of vertices $A$ such that $B\subseteq A$, we say that an Even
strategy $\sigma$ is an _Even reachability strategy to $B$ from $A$_ if every
infinite path in the subgraph $(V,\sigma)$ that starts from a vertex in $A$
contains at least one vertex in $B$.

For every target set $B$, there is the largest (with respect to set inclusion)
set from which there is an Even reachability strategy to $B$ in $\mathcal{G}$;
we call this set the _Even attractor to $B$ in $\mathcal{G}$_ and denote it by
$\mathrm{Attr}_{\mathrm{Even}}^{\mathcal{G}}(B)$. _Odd reachability
strategies_ and _Odd attractors_ are defined analogously.

We highlight the simple facts that if $A$ is an attractor for a player in
$\mathcal{G}$ then its complement $V\setminus A$ is a trap for her; and that
attractors are monotone operators: if $B^{\prime}\subseteq B$ then the
attractor to $B^{\prime}$ is included in the attractor to $B$.

###  2.3. Attractor decompositions

If $\mathcal{G}$ is a parity game in which all priorities do not exceed a non-
negative even number $d$ then we say that

$\mathcal{H}\>=\>\left\langle
A,(S_{1},\mathcal{H}_{1},A_{1}),\dots,(S_{k},\mathcal{H}_{k},A_{k})\right\rangle$

is an _Even $d$-attractor decomposition_ of $\mathcal{G}$ if:

  * •

$A$ is the Even attractor to the (possibly empty) set of vertices of priority
$d$ in $\mathcal{G}$;

and setting $\mathcal{G}_{1}=\mathcal{G}$, for all $i=1,2,\dots,k$, we have:

  * •

$S_{i}$ is a non-empty trap for Odd in $\mathcal{G}_{i}$ in which every vertex
priority is at most $d-2$;

  * •

$\mathcal{H}_{i}$ is a $(d-2)$-attractor decomposition of subgame
$\mathcal{G}\cap S_{i}$;

  * •

$A_{i}$ is the Even attractor to $S_{i}$ in $\mathcal{G}_{i}$;

  * •

$\mathcal{G}_{i+1}=\mathcal{G}_{i}\setminus A_{i}$;

and the game $\mathcal{G}_{k+1}$ is empty. If $d=0$ then we require that
$k=0$.

The following proposition states that if a subgame induced by a trap for Odd
has an Even attractor decomposition then the trap is an Even dominion. Indeed,
a routine proof argues that the union of all the reachability strategies,
implicit in the attractors listed in the decomposition, is an Even dominion
strategy.

###### Proposition 2.4.

If $d$ is even, $T$ is a trap for Odd in $\mathcal{G}$, and there is an Even
$d$-attractor decomposition of $\mathcal{G}\cap T$, then $T$ is an Even
dominion in $\mathcal{G}$.

If $\mathcal{G}$ is a game in which all priorities do not exceed an odd number
$d$, then an _Odd $d$-attractor decomposition_ of $\mathcal{G}$ is defined
analogously, with the roles of the two players swapped throughout the
definition. As expected and by symmetry, if a trap for Even has an Odd
attractor decomposition then it is an Odd dominion.

###### Proposition 2.5.

If $d$ is odd, $T$ is a trap for Even in $\mathcal{G}$, and there is an Odd
$d$-attractor decomposition of $\mathcal{G}\cap T$, then $T$ is an Odd
dominion in $\mathcal{G}$.

In the next subsection we argue that attractor decompositions are witnesses
for the largest dominia and that the classic recursive McNaughton-Zielonka
algorithm can be amended to produce such witnesses. Since McNaughton-Zielonka
algorithm produces Even and Odd attractor decompositions, respectively, of
subgames that are induced by sets of vertices that are complements of each
other, a by-product of its analysis is a constructive proof of the positional
determinacy theorem (Theorem 2.3).

###  2.4. McNaughton-Zielonka algorithm

procedure  _$\text{McN-Z}_{\mathrm{Even}}$(_$\mathcal{G},d$_)_:

if  _$d=0$_ then

return _$V^{\mathcal{G}}$_

$i\leftarrow 0;\;\mathcal{G}_{1}\leftarrow\mathcal{G}$

repeat

$i\leftarrow i+1$

$D_{i}\leftarrow\pi^{-1}(d)\cap\mathcal{G}_{i}$

$\mathcal{G}_{i}^{\prime}\leftarrow\mathcal{G}_{i}\setminus\mathrm{Attr}_{\mathrm{Even}}^{\mathcal{G}_{i}}(D_{i})$

$U_{i}\leftarrow\textnormal{{$\text{McN-Z}_{\mathrm{Odd}}$}}\left(\mathcal{G}_{i}^{\prime},d-1\right)$

$\mathcal{G}_{i+1}\leftarrow\mathcal{G}_{i}\setminus\mathrm{Attr}^{\mathcal{G}_{i}}_{\mathrm{Odd}}(U_{i})$

until  _$U_{i}=\emptyset$_

return _$V^{\mathcal{G}_{i}}$_

procedure  _$\text{McN-Z}_{\mathrm{Odd}}$(_$\mathcal{G},d$_)_:

$i\leftarrow 0;\;\mathcal{G}_{1}\leftarrow\mathcal{G}$

repeat

$i\leftarrow i+1$

$D_{i}\leftarrow\pi^{-1}(d)\cap\mathcal{G}_{i}$

$\mathcal{G}_{i}^{\prime}\leftarrow\mathcal{G}_{i}\setminus\mathrm{Attr}_{\mathrm{Odd}}^{\mathcal{G}_{i}}(D_{i})$

$U_{i}\leftarrow\textnormal{{$\text{McN-Z}_{\mathrm{Even}}$}}\left(\mathcal{G}_{i}^{\prime},d-1\right)$

$\mathcal{G}_{i+1}\leftarrow\mathcal{G}_{i}\setminus\mathrm{Attr}^{\mathcal{G}_{i}}_{\mathrm{Even}}(U_{i})$

until  _$U_{i}=\emptyset$_

return _$V^{\mathcal{G}_{i}}$_

Algorithm 1 McNaughton-Zielonka algorithm

The classic recursive McNaughton-Zielonka algorithm (Algorithm 1) computes the
largest dominia in a parity game. In order to obtain the largest Even dominion
in a parity game $\mathcal{G}$, it suffices to call
$\textnormal{{$\text{McN-Z}_{\mathrm{Even}}$}}(\mathcal{G},d)$, where $d$ is
even and all vertex priorities in $\mathcal{G}$ are at most $d$. In order to
obtain the largest Odd dominion in a parity game $\mathcal{G}$, it suffices to
call $\textnormal{{$\text{McN-Z}_{\mathrm{Odd}}$}}(\mathcal{G},d)$, where $d$
is odd and all vertex priorities in $\mathcal{G}$ are at most $d$.

The procedures $\text{McN-Z}_{\mathrm{Even}}$ and
$\text{McN-Z}_{\mathrm{Odd}}$ are mutually recursive and whenever a recursive
call is made, the second argument $d$ decreases by $1$. Figure 1 illustrates
one iteration of the main loop in a call of procedure
$\text{McN-Z}_{\mathrm{Even}}$. The outer rectangle denotes subgame
$\mathcal{G}_{i}$, the thin horizontal rectangle at the top denotes the set
$D_{i}$ of the vertices in $\mathcal{G}_{i}$ whose priority is $d$, and the
set below the horizontal wavy line is subgame $\mathcal{G}_{i}^{\prime}$,
which is the set of vertices in $\mathcal{G}_{i}$ that are not in the
attractor $\mathrm{Attr}_{\mathrm{Even}}^{\mathcal{G}_{i}}(D_{i})$. The
recursive call of $\text{McN-Z}_{\mathrm{Odd}}$ returns the set $U_{i}$, and
$\mathcal{G}_{i+1}$ is the subgame to the left of the vertical zig-zag line,
and it is induced by the set of vertices in $\mathcal{G}_{i}$ that are not in
the attractor $\mathrm{Attr}_{\mathrm{Odd}}^{\mathcal{G}_{i}}(U_{i})$.

A way to prove the correctness of McNaughton-Zielonka algorithm we wish to
highlight here is to enhance the algorithm slightly to produce not just a set
of vertices but also an Even attractor decomposition of the set and an Odd
attractor decomposition of its complement. We explain how to modify procedure
$\text{McN-Z}_{\mathrm{Even}}$ and leave it as an exercise for the reader to
analogously modify procedure $\text{McN-Z}_{\mathrm{Odd}}$. In procedure
$\textnormal{{$\text{McN-Z}_{\mathrm{Even}}$}}(\mathcal{G},d)$, replace the
line

$U_{i}\leftarrow\textnormal{{$\text{McN-Z}_{\mathrm{Odd}}$}}(\mathcal{G}_{i}^{\prime},d-1)$

by the line

$U_{i},\mathcal{H}_{i},\mathcal{H}_{i}^{\prime}\leftarrow\textnormal{{$\text{McN-Z}_{\mathrm{Odd}}$}}(\mathcal{G}_{i}^{\prime},d-1)\,.$

Moreover, if upon termination of the repeat-until loop we have

$\mathcal{H}_{i}\>=\>\left\langle\emptyset,(S_{1},\mathcal{I}_{1},A_{1}),\dots,(S_{k},\mathcal{I}_{k},A_{k})\right\rangle$

then instead of returning just the set $V^{\mathcal{G}_{i}}$, let the
procedure return both $V^{\mathcal{G}_{i}}$ and the following two objects:

(1)
$\left\langle\mathrm{Attr}_{\mathrm{Even}}^{\mathcal{G}_{i}}(D_{i}),(S_{1},\mathcal{I}_{1},A_{1}),\dots,(S_{k},\mathcal{I}_{k},A_{k})\right\rangle$

and

(2)
$\left\langle\emptyset,\left(U_{1},\mathcal{H}_{1}^{\prime},\mathrm{Attr}_{\mathrm{Odd}}^{\mathcal{G}_{1}}(U_{1})\right),\dots,\left(U_{i},\mathcal{H}_{i}^{\prime},\mathrm{Attr}_{\mathrm{Odd}}^{\mathcal{G}_{i}}(U_{i})\right)\right\rangle$

Figure 1. Attractors and subgames in one iteration of the loop in attractor
decomposition algorithms.

In an inductive argument by induction on $d$ and $i$, the inductive hypothesis
is that:

  * •

$\mathcal{H}_{i}^{\prime}$ is an Odd $(d-1)$-attractor decomposition of the
subgame $\mathcal{G}^{\prime}_{i}\cap U_{i}$;

  * •

$\mathcal{H}_{i}$ is an Even $d$-attractor decomposition of the subgame
$\mathcal{G}^{\prime}_{i}\setminus U_{i}$;

and the inductive step is then to show that:

  * •

for every $i$, (2) is an Odd $(d+1)$-attractor decomposition of subgame
$\mathcal{G}\setminus\mathcal{G}_{i+1}$;

  * •

upon termination of the repeat-until loop, (1) is an Even $d$-attractor
decomposition of subgame $\mathcal{G}_{i+1}$.

The general arguments in such a proof are well known (McNaughton, 1993;
Zielonka, 1998; Jurdziński et al., 2008; Daviaud et al., 2018) and hence we
omit the details here.

###### Theorem 2.6.

McNaughton-Zielonka algorithm can be enhanced to produce both the largest Even
and Odd dominia, and an attractor decomposition of each. Every vertex is in
one of the two dominia.

##  3\. Universal trees and algorithms

Every call of McNaughton-Zielonka algorithm takes small polynomial time if the
recursive calls it makes are excluded. This is because in every execution of
the main repeat-until loop, the two attractor computations can be performed in
time linear in the size of the game graph, and the loop can only be performed
at most linearly many times since the sets $U_{1},U_{2},\dots,U_{i}$ are
mutually disjoint. Therefore, the running time of McNaughton-Zielonka
algorithm is mostly determined by the number of recursive calls it makes
overall. While numerous experiments indicate that the algorithm performs very
well on some classes of random games and on games arising from applications in
model checking, termporal logic synthesis, and equivalence checking (van Dijk,
2018), it is also well known that there are families of parity games on which
McNaughton-Zielonka algorithm performs exponentially many recursive calls
(Friedmann, 2011a).

Parys (Parys, 2019) has devised an ingenious modification of McNaughton-
Zielonka algorithm that reduced the number of recursive calls of the algorithm
to quasi-polynomial number $n^{O(\lg n)}$ in the worst case. Lehtinen, Schewe,
and Wojtczak (Lehtinen et al., 2019) have slightly modified Parys’s algorithm
in order to improve the running time from $n^{O(\lg n)}$ down to $d^{O(\lg
n)}$ for $(n,d)$-small parity games. They have also made an informal
observation that the tree of recursive calls of their recursive procedure is
universal.

In this paper, we argue that McNaughton-Zielonka algorithm, Parys’s algorithm,
and Lehtinen-Schewe-Wojtczak algorithm are special cases of what we call a
_universal attractor decomposition algorithm_. The universal algorithm is
parameterized by two ordered trees and we prove a striking structural result
that if those trees are capacious enough to embed (in a formal sense explained
later) ordered trees that describe the “shape” of some attractor
decompositions of the largest Even and Odd dominia in a parity game, then the
universal algorithm correctly computes the two dominia. It follows that if the
algorithm is run on two universal trees then it is correct, and indeed we
reproduce McNaughton-Zielonka, Parys’s, and Lehtinen-Schewe-Wojtczak
algorithms by running the universal algorithm on specific classes of universal
trees. In particular, Lehtinen-Schewe-Wojtczak algorithm is obtained by using
the succinct universal trees of Jurdziński and Lazić (Jurdziński and Lazić,
2017), whose size nearly matches the quasi-polynomial lower bound on the size
of universal trees (Czerwiński et al., 2019).

###  3.1. Universal ordered trees

#### Ordered trees.

Ordered trees are defined inductively; an ordered tree is the trivial tree
$\left\langle\right\rangle$ or a sequence
$\left\langle\mathcal{T}_{1},\mathcal{T}_{2},\dots,\mathcal{T}_{k}\right\rangle$,
where $\mathcal{T}_{i}$ is an ordered tree for every $i=1,2,\dots,k$. The
trivial tree has only one node called the root, which is a leaf; and a tree of
the form
$\left\langle\mathcal{T}_{1},\mathcal{T}_{2},\dots,\mathcal{T}_{k}\right\rangle$
has the root with $k$ children, the root is not a leaf, and the $i$-th child
of the root is the root of ordered tree $\mathcal{T}_{i}$.

For an ordered tree $\mathcal{T}$, we write $\mathrm{height}(\mathcal{T})$ for
its _height_ and $\mathrm{leaves}(\mathcal{T})$ for its _number of leaves_.
Both are defined by routine induction: the height of the trivial tree is $0$
and it has $1$ leaf; the height of tree
$\left\langle\mathcal{T}_{1},\mathcal{T}_{2},\dots,\mathcal{T}_{k}\right\rangle$
is $1$ plus the maximum height of trees $\mathcal{T}_{1}$, $\mathcal{T}_{2}$,
…, $\mathcal{T}_{k}$; and the number of leaves of tree
$\left\langle\mathcal{T}_{1},\mathcal{T}_{2},\dots,\mathcal{T}_{k}\right\rangle$
is the sum of the numbers of leaves of trees $\mathcal{T}_{1}$,
$\mathcal{T}_{2}$, …, $\mathcal{T}_{k}$.

#### Trees of attractor decompositions.

The definition of an attractor decomposition is inductive and we define an
ordered tree that reflects the hierarchical structure of an attractor
decomposition. If $d$ is even and

$\mathcal{H}=\left\langle
A,(S_{1},\mathcal{H}_{1},A_{1}),\dots,(S_{k},\mathcal{H}_{k},A_{k})\right\rangle$

is an Even $d$-attractor decomposition then we define the _tree of attractor
decomposition $\mathcal{H}$_, denoted by $\mathcal{T}_{\mathcal{H}}$, to be
the trivial ordered tree $\left\langle\right\rangle$ if $k=0$, and otherwise,
to be the ordered tree
$\left\langle\mathcal{T}_{\mathcal{H}_{1}},\mathcal{T}_{\mathcal{H}_{2}},\dots,\mathcal{T}_{\mathcal{H}_{k}}\right\rangle$,
where for every $i=1,2,\dots,k$, tree $\mathcal{T}_{\mathcal{H}_{i}}$ is the
tree of attractor decomposition $\mathcal{H}_{i}$. Trees of Odd attractor
decompositions are defined analogously.

Observe that the sets $S_{1},S_{2},\dots,S_{k}$ in an attractor decomposition
as above are non-empty and pairwise disjoint, which implies that trees of
attractor decompositions are small relative to the number of vertices and the
number of distinct priorities in a parity game. More precisely, we say that an
ordered tree is _$(n,h)$ -small_ if its height is at most $h$ and it has at
most $n$ leaves. The following proposition can be proved by routine structural
induction.

###### Proposition 3.1.

If $\mathcal{H}$ is an attractor decomposition of an $(n,d)$-small parity game
then its tree $\mathcal{T}_{\mathcal{H}}$ is $(n,\lceil d/2\rceil)$-small.

#### Embedding ordered trees.

Intuitively, an ordered tree _embeds_ another if the latter can be obtained
from the former by pruning some subtrees. More formally, every ordered tree
embeds the trivial tree $\left\langle\right\rangle$, and
$\left\langle\mathcal{T}_{1},\mathcal{T}_{2},\dots,\mathcal{T}_{k}\right\rangle$
embeds
$\left\langle\mathcal{T}_{1}^{\prime},\mathcal{T}_{2}^{\prime},\dots,\mathcal{T}_{\ell}^{\prime}\right\rangle$
if there are indices $i_{1},i_{2},\dots,i_{\ell}$, such that $1\leq
i_{1}<i_{2}<\cdots<i_{\ell}\leq k$ and for every $j=1,2,\dots,\ell$, we have
that $\mathcal{T}_{i_{\ell}}$ embeds $\mathcal{T}_{j}^{\prime}$.

#### Universal ordered trees.

We say that an ordered tree is $(n,h)$-universal (Czerwiński et al., 2019) if
it embeds every $(n,h)$-small ordered tree. The complete $n$-ary tree of
height $h$ can be defined by induction on $h$: if $h=0$ then $C_{n,0}$ is the
trivial tree $\left\langle\right\rangle$, and if $h>0$ then $C_{n,h}$ is the
ordered tree $\left\langle C_{n,h-1}\right\rangle^{n}$. The tree $C_{n,h}$ is
obviously $(n,h)$-universal but its size is exponential in $h$.

We define two further classes $P_{n,h}$ and $S_{n,h}$ of $(n,h)$-universal
trees whose size is only quasipolynomial, and hence they are significantly
smaller than the complete $n$-ary trees of height $h$. Both classes are
defined by induction on $n+h$.

If $h=0$ then both $P_{n,h}$ and $S_{n,h}$ are defined to be the trivial tree
$\left\langle\right\rangle$. If $h>0$ then $P_{n,h}$ is defined to be the
ordered tree

$\left\langle P_{\lfloor n/2\rfloor,h-1}\right\rangle^{\lfloor
n/2\rfloor}\cdot\left\langle P_{n,h-1}\right\rangle\cdot\left\langle
P_{\lfloor n/2\rfloor,h-1}\right\rangle^{\lfloor n/2\rfloor}\,,$

and $S_{n,h}$ is defined to be the ordered tree

$S_{\lfloor n/2\rfloor,h}\cdot\left\langle S_{n,h-1}\right\rangle\cdot
S_{\lfloor n/2\rfloor,h}\,.$

We leave it as an instructive exercise to the reader to prove the following
proposition.

###### Proposition 3.2.

Ordered trees $C_{n,h}$, $P_{n,h}$ and $S_{n,h}$ are $(n,h)$-universal.

A proof of universality of $S_{n,h}$ is implicit in the work of Jurdziński and
Lazić (Jurdziński and Lazić, 2017), whose _succinct multi-counters_ are merely
an alternative presentation of trees $S_{n,h}$. Parys (Parys, 2019) has shown
that the number of leaves in trees $P_{n,h}$ is $n^{\lg n+O(1)}$ and
Jurdziński and Lazić (Jurdziński and Lazić, 2017) have proved that the number
of leaves in trees $S_{n,h}$ is $n^{\lg h+O(1)}$. Czerwiński et al.
(Czerwiński et al., 2019) have established a quasi-polynomial lower bound on
the number of leaves in $(n,h)$-universal trees, which the size of $S_{n,h}$
exceeds only by a small polynomial factor.

###  3.2. Universal algorithm

Every call of McNaughton-Zielonka algorithm (Algorithm 1) repeats the main
loop until the set $U_{i}$ (returned by a recursive call) is empty. If the
number of iterations for each value of $d$ is large then the overall number of
recursive calls may be exponential in $d$ in the worst case, and that is
indeed what happens for some families of hard parity games (Friedmann, 2011a).

procedure
_$\text{Univ}_{\mathrm{Even}}$(_$\mathcal{G},d,\mathcal{T}^{\mathrm{Even}},\mathcal{T}^{\mathrm{Odd}}$_)_:

let
$\mathcal{T}^{\mathrm{Odd}}=\left\langle\mathcal{T}^{\mathrm{Odd}}_{1},\mathcal{T}^{\mathrm{Odd}}_{2},\dots,\mathcal{T}^{\mathrm{Odd}}_{k}\right\rangle$

$\mathcal{G}_{1}\leftarrow\mathcal{G}$

for  _$i\leftarrow 1$ to $k$_ do

$D_{i}\leftarrow\pi^{-1}(d)\cap\mathcal{G}_{i}$

$\mathcal{G}_{i}^{\prime}\leftarrow\mathcal{G}_{i}\setminus\mathrm{Attr}_{\mathrm{Even}}^{\mathcal{G}_{i}}(D_{i})$

$U_{i}\leftarrow\textnormal{{$\text{Univ}_{\mathrm{Odd}}$}}\left(\mathcal{G}_{i}^{\prime},d-1,\mathcal{T}^{\mathrm{Even}},\mathcal{T}^{\mathrm{Odd}}_{i}\right)$

$\mathcal{G}_{i+1}\leftarrow\mathcal{G}_{i}\setminus\mathrm{Attr}^{\mathcal{G}_{i}}_{\mathrm{Odd}}(U_{i})$

return _$V^{\mathcal{G}_{k+1}}$_

procedure
_$\text{Univ}_{\mathrm{Odd}}$(_$\mathcal{G},d,\mathcal{T}^{\mathrm{Even}},\mathcal{T}^{\mathrm{Odd}}$_)_:

let
$\mathcal{T}^{\mathrm{Even}}=\left\langle\mathcal{T}^{\mathrm{Even}}_{1},\mathcal{T}^{\mathrm{Even}}_{2},\dots,\mathcal{T}^{\mathrm{Even}}_{\ell}\right\rangle$

$\mathcal{G}_{1}\leftarrow\mathcal{G}$

for  _$i\leftarrow 1$ to $\ell$_ do

$D_{i}\leftarrow\pi^{-1}(d)\cap\mathcal{G}_{i}$

$\mathcal{G}_{i}^{\prime}\leftarrow\mathcal{G}_{i}\setminus\mathrm{Attr}_{\mathrm{Odd}}^{\mathcal{G}_{i}}(D_{i})$

$U_{i}\leftarrow\textnormal{{$\text{Univ}_{\mathrm{Even}}$}}\left(\mathcal{G}_{i}^{\prime},d-1,\mathcal{T}^{\mathrm{Even}}_{i},\mathcal{T}^{\mathrm{Odd}}\right)$

$\mathcal{G}_{i+1}\leftarrow\mathcal{G}_{i}\setminus\mathrm{Attr}^{\mathcal{G}_{i}}_{\mathrm{Even}}(U_{i})$

return _$V^{\mathcal{G}_{\ell+1}}$_

Algorithm 2 The universal algorithm

In our _universal attractor decomposition algorithm_ (Algorithm 2), every
iteration of the main loop performs exactly the same actions as in McNaughton-
Zielonka algorithm (see Algorithm 1 and Figure 1), but the algorithm uses a
different mechanism to determine how many iterations of the main loop are
performed in each recursive call. In the mutually recursive procedures
$\text{Univ}_{\mathrm{Odd}}$ and $\text{Univ}_{\mathrm{Even}}$, this is
determined by the numbers of children of the root in the input trees
$\mathcal{T}^{\mathrm{Even}}$ (the third argument) and
$\mathcal{T}^{\mathrm{Odd}}$ (the fourth argument), respectively. Note that
the sole recursive call of $\text{Univ}_{\mathrm{Odd}}$ in the $i$-th
iteration of the main loop in a call of $\text{Univ}_{\mathrm{Even}}$ is given
subtree $\mathcal{T}_{i}^{\mathrm{Odd}}$ as its fourth argument and,
analogously, the sole recursive call of $\text{Univ}_{\mathrm{Even}}$ in the
$j$-th iteration of the main loop in a call of $\text{Univ}_{\mathrm{Odd}}$ is
given subtree $\mathcal{T}_{j}^{\mathrm{Even}}$ as its third argument.

Define the _interleaving_ operation on two ordered trees inductively as
follows:
$\left\langle\right\rangle\bowtie\mathcal{T}=\left\langle\right\rangle$ and
$\left\langle\mathcal{T}_{1},\mathcal{T}_{2},\dots,\mathcal{T}_{k}\right\rangle\bowtie\mathcal{T}=\left\langle\mathcal{T}\bowtie\mathcal{T}_{1},\mathcal{T}\bowtie\mathcal{T}_{2},\dots,\mathcal{T}\bowtie\mathcal{T}_{k}\right\rangle$.
Then the following simple proposition provides an explicit description of the
tree of recursive calls of our universal algorithm.

###### Proposition 3.3.

If $d$ is even then the tree of recursive calls of a call
$\textnormal{{$\text{Univ}_{\mathrm{Even}}$}}\left(\mathcal{G},d,\mathcal{T}^{\mathrm{Even}},\mathcal{T}^{\mathrm{Odd}}\right)$
is the interleaving
$\mathcal{T}^{\mathrm{Odd}}\bowtie\mathcal{T}^{\mathrm{Even}}$ of trees
$\mathcal{T}^{\mathrm{Odd}}$ and $\mathcal{T}^{\mathrm{Even}}$.

###### Proposition 3.4.

If $d$ is odd then the tree of recursive calls of a call
$\textnormal{{$\text{Univ}_{\mathrm{Odd}}$}}\left(\mathcal{G},d,\mathcal{T}^{\mathrm{Even}},\mathcal{T}^{\mathrm{Odd}}\right)$
is the interleaving
$\mathcal{T}^{\mathrm{Even}}\bowtie\mathcal{T}^{\mathrm{Odd}}$ of trees
$\mathcal{T}^{\mathrm{Even}}$ and $\mathcal{T}^{\mathrm{Odd}}$.

The following elementary proposition helps estimate the size of an
interleaving of two ordered trees and hence the running time of a call of the
universal algorithm that is given two ordered trees as inputs.

###### Proposition 3.5.

If $\mathcal{T}$ and $\mathcal{T}^{\prime}$ are ordered trees then:

  * •

$\mathrm{height}(\mathcal{T}\bowtie\mathcal{T}^{\prime})\leq\mathrm{height}(\mathcal{T})+\mathrm{height}(\mathcal{T}^{\prime})$;

  * •

$\mathrm{leaves}(\mathcal{T}\bowtie\mathcal{T}^{\prime})\leq\mathrm{leaves}(\mathcal{T})\cdot\mathrm{leaves}(\mathcal{T}^{\prime})$.

In contrast to the universal algorithm, the tree of recursive calls of
McNaughton-Zielonka algorithm is not pre-determined by a structure separate
from the game graph, such as the pair of trees $\mathcal{T}^{\mathrm{Even}}$
and $\mathcal{T}^{\mathrm{Odd}}$. Instead, McNaughton-Zielonka algorithm
determines the number of iterations of its main loop adaptively, using the
adaptive _empty-set early termination rule_ : terminate the main loop as soon
as $U_{i}=\emptyset$. We argue that if we add the empty-set early termination
rule to the universal algorithm in which both trees
$\mathcal{T}^{\mathrm{Even}}$ and $\mathcal{T}^{\mathrm{Odd}}$ are the tree
$C_{n,d/2}$ then its behaviour coincides with McNaughton-Zielonka algorithm.

###### Proposition 3.6.

The universal algorithm performs the same actions and produces the same output
as McNaughton-Zielonka algorithm if it is run on an $(n,d)$-small parity game
and with both trees $\mathcal{T}^{\mathrm{Even}}$ and
$\mathcal{T}^{\mathrm{Odd}}$ equal to $C_{n,d/2}$, and if it uses the adaptive
empty-set early termination rule.

The idea of using rules for implicitly pruning the tree of recursive calls of
a McNaughton-Zielonka-style algorithm that are significantly different from
the adaptive empty-set early termination rule is due to Parys (Parys, 2019).
In this way, he has designed the first McNaughton-Zielonka-style algorithm
that works in quasi-polynomial time $n^{O(\lg n)}$ in the worst case, and
Lehtinen, Schewe, and Wojtczak (Lehtinen et al., 2019) have refined Parys’s
algorithm, improving the worst-case running time down to $n^{O(\lg d)}$. Both
algorithms use two numerical arguments (one for $\mathrm{Even}$ and one for
$\mathrm{Odd}$) and “halving tricks” on those parameters, which results in
pruning the tree of recursive calls down to quasi-polynomial size in the worst
case. We note that our universal algorithm yields the algorithms of Parys and
of Lehtinen et al., respectively, if, when run on an $(n,d)$-small parity game
and if both trees $\mathcal{T}^{\mathrm{Even}}$ and
$\mathcal{T}^{\mathrm{Odd}}$ set to be the $(n,d/2)$-universal trees
$P_{n,d/2}$ and $S_{n,d/2}$, respectively.

###### Proposition 3.7.

The universal algorithm performs the same actions and produces the same output
as Lehtinen-Schewe-Wojtczak algorithm if it is run on an $(n,d)$-small parity
game with both trees $\mathcal{T}^{\mathrm{Even}}$ and
$\mathcal{T}^{\mathrm{Odd}}$ equal to $S_{n,d/2}$.

The correspondence between the universal algorithm run on $(n,d/2)$-universal
trees $P_{n,d/2}$ and Parys’s algorithm is a bit more subtle. While both run
in quasi-polynomial time in the worst case, the former may perform more
recursive calls than the latter. The two coincide, however, if the the former
is enhanced with a simple adaptive tree-pruning rule similar to the empty-set
early termination rule. The discussion of this and other adaptive tree-pruning
rules will be better informed once we have dicussed sufficient conditions for
the correctness of our universal algorithm. Therefore, we will return to
elaborating the full meaning of the following proposition in Section 4.4.

###### Proposition 3.8.

The universal algorithm performs the same actions and produces the same output
as a non-adaptive version of Parys’s algorithm if it is run on an
$(n,d)$-small parity games with both trees $\mathcal{T}^{\mathrm{Even}}$ and
$\mathcal{T}^{\mathrm{Odd}}$ equal to $P_{n,d/2}$.

##  4\. Correctness via structural theorems

The proof of correctness of McNaughton-Zielonka algorithm that is based on the
algorithm recursively producing attractor decompositions of largest Even and
Odd dominia (as discussed in Section 2.4) critically relies on the
$U_{i}=\emptyset$ termination condition of the main loop in McNaughton-
Zielonka algorithm. The argument breaks down if the loop terminates before
that empty-set condition obtains. Instead, Parys (Parys, 2019) has developed a
novel _dominion separation technique_ to prove correctness of his algorithm
and Lehtinen et al. (Lehtinen et al., 2019) use the same technique to justify
theirs.

In this paper, we significantly generalize the dominion separation technique
of Parys, which allows us to intimately link the correctness of our meta-
algorithm to shapes (modelled as ordered trees) of attractor decompositions of
largest Even and Odd dominia. We say that the universal algorithm is correct
on a parity game if $\text{Univ}_{\mathrm{Even}}$ returns the largest Even
dominion and $\text{Univ}_{\mathrm{Odd}}$ returns the largest Odd dominion. We
also say that an ordered tree $\mathcal{T}$ _embeds a dominion_ $D$ in a
parity game $\mathcal{G}$ if it embeds the tree of some attractor
decomposition of $\mathcal{G}\cap D$. The main technical result we aim to
prove in this section is the sufficiency of the following condition for the
universal algorithm to be correct.

###### Theorem 4.1 (Correctness of universal algorithm).

The universal algorithm is correct on a parity game $\mathcal{G}$ if it is run
on ordered trees $\mathcal{T}^{\mathrm{Even}}$ and
$\mathcal{T}^{\mathrm{Odd}}$, such that $\mathcal{T}^{\mathrm{Even}}$ embeds
the largest Even dominion in $\mathcal{G}$ and $\mathcal{T}^{\mathrm{Odd}}$
embeds the largest Odd dominion in $\mathcal{G}$.

###  4.1. Embeddable decomposition theorem

Before we prove Theorem 4.1 in Section 4.2, in this section we establish
another technical result—the embeddable decomposition theorem—that enables our
generalization of Parys’s dominion separation technique. Its statement is
intuitive: a subgame induced by a trap has a simpler attractor decomposition
structure than the whole game itself; its proof, however, seems to require
some careful surgery.

###### Theorem 4.2 (Embeddable decomposition).

If $T$ is a trap for Even in a parity game $\mathcal{G}$ and
$\mathcal{G}^{\prime}=\mathcal{G}\cap T$ is the subgame induced by $T$, then
for every Even attractor decomposition $\mathcal{H}$ of $\mathcal{G}$, there
is an Even attractor decomposition $\mathcal{H}^{\prime}$ of
$\mathcal{G}^{\prime}$, such that $\mathcal{T}_{\mathcal{H}}$ embeds
$\mathcal{T}_{\mathcal{H}^{\prime}}$.

In order to streamline the proof of the embeddable decomposition theorem, we
state the following two propositions, which synthesize or generalize some of
the arguments that were also used by Parys (Parys, 2019) and Lehtinen et al.
(Lehtinen et al., 2019). Proofs are included in the Appendix.

###### Proposition 4.3.

Suppose that $R$ is a trap for Even in game $\mathcal{G}$. Then if $T$ is a
trap for Odd in $\mathcal{G}$ then $T\cap R$ is a trap for Odd in subgame
$\mathcal{G}\cap R$, and if $T$ is an Even dominion in $\mathcal{G}$ then
$T\cap R$ is an Even dominion in $\mathcal{G}\cap R$.

The other proposition is illustrated in Figure 2. Its statement is more
complex than that of the first proposition. The statement and the proof
describe the relationship between the Even attractor of a set $B$ of vertices
in a game $\mathcal{G}$ and the Even attractor of the set $B\cap T$ in subgame
$\mathcal{G}\cap T$, where $T$ is a trap for Even in $\mathcal{G}$.

Figure 2. Traps and attractors in Proposition 4.4.

###### Proposition 4.4.

Let $B\subseteq V^{\mathcal{G}}$ and let $T$ be a trap for Even in game
$\mathcal{G}$. Define $A=\mathrm{Attr}_{\mathrm{Even}}^{\mathcal{G}}(B)$ and
$A^{\prime}=\mathrm{Attr}_{\mathrm{Even}}^{\mathcal{G}\cap T}(B\cap T)$. Then
$T\setminus A^{\prime}$ is a trap for Even in subgame $\mathcal{G}\setminus
A$.

Finally, we are ready to prove the embeddable decomposition theorem by
induction on the number of leaves of the tree of attractor decomposition
$\mathcal{H}$.

######  Proof of Theorem 4.2.

Without loss of generality, assume that $d$ is even and

$\mathcal{H}=\left\langle
A,(S_{1},\mathcal{H}_{1},A_{1}),\dots,(S_{k},\mathcal{H}_{k},A_{k})\right\rangle$

is an Even $d$-attractor decomposition of $\mathcal{G}$, where $A$ is the Even
attractor to the set $D$ of vertices of priority $d$ in $\mathcal{G}$. In
Figure 3, set $T$ and the subgame $\mathcal{G}^{\prime}$ it induces form the
pentagon obtained from the largest rectangle by removing the triangle above
the diagonal line in the top-left corner. Sets $A$, $S_{1}$, and $A_{1}$ are
also illustrated, together with sets $A^{\prime}$, $S_{1}^{\prime}$,
$A_{1}^{\prime}$ and subgames $\mathcal{G}_{1}$, $\mathcal{G}_{2}$,
$\mathcal{G}_{1}^{\prime}$, and $\mathcal{G}_{2}^{\prime}$, which are defined
as follows.

Let $\mathcal{G}_{1}=\mathcal{G}\setminus A$, and
$\mathcal{G}_{2}=\mathcal{G}_{1}\setminus A_{1}$. We will define sets
$A^{\prime}$, $S_{1}^{\prime}$, $A_{1}^{\prime}$, …, $S_{\ell}^{\prime}$,
$A_{\ell}^{\prime}$, and Even $(d-2)$-attractor decompositions
$\mathcal{H}_{1}^{\prime},\dots,\mathcal{H}_{\ell}^{\prime}$ of subgames
$\mathcal{G}\cap S_{1}^{\prime}$, …, $\mathcal{G}\cap S_{\ell}^{\prime}$,
respectively, such that

$\mathcal{H}^{\prime}=\left\langle
A^{\prime},(S_{1}^{\prime},\mathcal{H}_{1}^{\prime},A_{1}^{\prime}),\dots,(S_{k}^{\prime},\mathcal{H}_{\ell}^{\prime},A_{\ell}^{\prime})\right\rangle$

is an Even $d$-attractor decomposition of subgame $\mathcal{G}^{\prime}$ and
$\mathcal{T}_{\mathcal{H}}$ embeds $\mathcal{T}_{\mathcal{H}^{\prime}}$.

Let $A^{\prime}$ be the Even attractor to $D\cap T$ in $\mathcal{G}^{\prime}$
and let $\mathcal{G}_{1}^{\prime}=\mathcal{G}^{\prime}\setminus A^{\prime}$.
Set $S_{1}^{\prime}=S_{1}\cap\mathcal{G}_{1}^{\prime}$, let $A_{1}^{\prime}$
be the Even attractor to $S_{1}^{\prime}$ in $\mathcal{G}_{1}^{\prime}$, and
let $\mathcal{G}_{2}^{\prime}=\mathcal{G}_{1}^{\prime}\setminus
A_{1}^{\prime}$.

Firstly, since $D\subseteq V^{\mathcal{G}}$ and $T$ is a trap for Even in
$\mathcal{G}$, by Proposition 4.4, we have that $\mathcal{G}_{1}^{\prime}$ is
a trap for Even in subgame $\mathcal{G}_{1}$. Since $S_{1}\subseteq
V^{\mathcal{G}_{1}}$ and subgame $\mathcal{G}_{1}^{\prime}$ is a trap for Even
in subgame $\mathcal{G}_{1}$, again by Proposition 4.4, we conclude that
$\mathcal{G}_{2}^{\prime}$ is a trap for Even in subgame $\mathcal{G}_{2}$.

Secondly, we argue that $S_{1}^{\prime}$ is an Even dominion in subgame
$\mathcal{G}_{1}^{\prime}$. This follows by recalling that $S_{1}$ is a
dominion for Even in $\mathcal{G}_{1}$ and $\mathcal{G}_{1}^{\prime}$ is a
trap for Even in $\mathcal{G}_{1}$, and then applying Proposition 4.3.

Thirdly, we argue that $S_{1}^{\prime}$ is a trap for Even in subgame
$\mathcal{G}\cap S_{1}$. This follows by recalling that $S_{1}$ is a trap for
Odd in $\mathcal{G}_{1}$ and that $\mathcal{G}_{1}^{\prime}$ is a trap for
Even in $\mathcal{G}_{1}$, and then applying Proposition 4.3.

Figure 3. Attractors, subgames, and dominia in the proof of the embeddable
decomposition theorem.

We are now in a position to apply the inductive hypothesis twice in order to
complete the definition of the attractor decomposition $\mathcal{H}^{\prime}$.
Firstly, recall that $S_{1}^{\prime}$ is a trap for Even in subgame
$\mathcal{G}\cap S_{1}$ and that $\mathcal{H}_{1}$ is a $(d-2)$-attractor
decomposition of $\mathcal{G}\cap S_{1}$, so we can apply the inductive
hypothesis to obtain a $(d-2)$-attractor decomposition
$\mathcal{H}_{1}^{\prime}$ of subgame $\mathcal{G}\cap S_{1}^{\prime}$, such
that $\mathcal{T}_{\mathcal{H}_{1}}$ embeds
$\mathcal{T}_{\mathcal{H}_{1}^{\prime}}$. Secondly, note that

$\mathcal{I}\>=\>\left\langle\emptyset,(S_{2},\mathcal{H}_{2},A_{2}),\dots,(S_{k},\mathcal{H}_{k},A_{k})\right\rangle$

is a $d$-attractor decomposition of $\mathcal{G}_{2}$. We find a $d$-attractor
decomposition $\mathcal{I}^{\prime}$ of subgame $\mathcal{G}_{2}^{\prime}$,
such that $\mathcal{T}_{\mathcal{I}}$ embeds
$\mathcal{T}_{\mathcal{I}^{\prime}}$. Recalling that
$\mathcal{G}_{2}^{\prime}$ is a trap for Even in subgame $\mathcal{G}_{2}$, it
suffices to use the inductive hypothesis for subgame
$\mathcal{G}_{2}^{\prime}$ of game $\mathcal{G}_{2}$ and the $d$-attractor
decomposition $\mathcal{I}$ of $\mathcal{G}_{2}$.

Verifying that $\mathcal{H}^{\prime}$ is a $d$-attractor decomposition of
$\mathcal{G}^{\prime}$ is routine. That $\mathcal{T}_{\mathcal{H}}$ embeds
$\mathcal{T}_{\mathcal{H}^{\prime}}$ also follows routinely from
$\mathcal{T}_{\mathcal{H}_{1}}$ embedding
$\mathcal{T}_{\mathcal{H}_{1}^{\prime}}$ and $\mathcal{T}_{\mathcal{I}}$
embedding $\mathcal{T}_{\mathcal{I}^{\prime}}$. ∎

###  4.2. Dominion separation theorem

The simple dominion disjointness property (Proposition 2.2) states that every
Even dominion is disjoint from every Odd dominion. For two sets $A$ and $B$,
we say that another set $X$ _separates $A$ from $B$_ if $A\subseteq X$ and
$X\cap B=\emptyset$. In this section we establish a very general dominion
separation property for subgames that occur in iterations of the universal
algorithm. This allows us to prove one of the main technical results of this
paper (Theorem 4.1) that describes a detailed structural sufficient condition
for the correctness of the universal algorithm.

###### Theorem 4.5 (Dominion separation).

Let $\mathcal{G}$ be an $(n,d)$-small parity game and let
$\mathcal{T}^{\mathrm{Even}}=\left\langle\mathcal{T}^{\mathrm{Even}}_{1},\dots,\mathcal{T}^{\mathrm{Even}}_{\ell}\right\rangle$
and
$\mathcal{T}^{\mathrm{Odd}}=\left\langle\mathcal{T}^{\mathrm{Odd}}_{1},\dots,\mathcal{T}^{\mathrm{Odd}}_{k}\right\rangle$
be trees of height at most $\lceil d/2\rceil$ and $\lfloor d/2\rfloor$,
respectively.

  1. (a)

If $d$ is even and $\mathcal{G}_{1},\dots,\mathcal{G}_{k+1}$ are the games
that are computed in the successive iterations of the loop in the call
$\textnormal{{$\text{Univ}_{\mathrm{Even}}$}}\left(\mathcal{G},d,\mathcal{T}^{\mathrm{Even}},\mathcal{T}^{\mathrm{Odd}}\right)$,
then for every $i=0,1,\dots,k$, we have that $\mathcal{G}_{i+1}$ separates
every Even dominion in $\mathcal{G}$ that tree $\mathcal{T}^{\mathrm{Even}}$
embeds from every Odd dominion in $\mathcal{G}$ that tree
$\left\langle\mathcal{T}_{1}^{\mathrm{Odd}},\ldots,\mathcal{T}_{i}^{\mathrm{Odd}}\right\rangle$
embeds.

  2. (b)

If $d$ is odd and $\mathcal{G}_{1},\dots,\mathcal{G}_{\ell+1}$ are the games
that are computed in the successive iterations of the loop in the call
$\textnormal{{$\text{Univ}_{\mathrm{Odd}}$}}\left(\mathcal{G},d,\mathcal{T}^{\mathrm{Even}},\mathcal{T}^{\mathrm{Odd}}\right)$,
then for every $i=0,1,\dots,\ell$, we have that $\mathcal{G}_{i+1}$ separates
every Odd dominion in $\mathcal{G}$ that tree $\mathcal{T}^{\mathrm{Odd}}$
embeds from every Even dominion in $\mathcal{G}$ that tree
$\left\langle\mathcal{T}_{1}^{\mathrm{Even}},\ldots,\mathcal{T}_{i}^{\mathrm{Even}}\right\rangle$
embeds.

Before we prove the dominion separation theorem, we recall a simple
proposition from Parys (Parys, 2019), also stated explicitly by Lehtinen et
al. (Lehtinen et al., 2019). Note that it is a straightfoward corollary of the
dual of Proposition 4.4 (in case $B\cap T=\emptyset$).

###### Proposition 4.6.

If $T$ is a trap for Odd in $\mathcal{G}$ and $T\cap B=\emptyset$ then we also
have that $T\cap\mathrm{Attr}_{\mathrm{Odd}}^{\mathcal{G}}(B)=\emptyset$.

######  Proof of Theorem 4.5.

We prove the statement of part (a); the proof of part (b) is analogous.

The proof is by induction on the height of tree
$\mathcal{T}^{\mathrm{Odd}}\bowtie\mathcal{T}^{\mathrm{Even}}$ (the “outer”
induction). If the height is $0$ then tree $\mathcal{T}^{\mathrm{Odd}}$ is the
trivial tree $\left\langle\right\rangle$; hence $k=0$, the algorithm returns
the set $V^{\mathcal{G}_{1}}=V^{\mathcal{G}}$, which contains the largest Even
dominion, and which is trivially disjoint from the largest Odd dominion
(because the latter is empty).

If the height of
$\mathcal{T}^{\mathrm{Odd}}\bowtie\mathcal{T}^{\mathrm{Even}}$ is positive,
then we split the proof of the separation property into two parts.

Figure 4. Attractors, subgames, and dominia in the first part of the proof of
the dominion separation theorem.

#### Even dominia embedded by $\mathcal{T}^{\mathrm{Even}}$ are included in
$\mathcal{G}_{i+1}$.

We prove by induction on $i$ (the “inner” induction) that for
$i=0,1,2,\dots,k$, if $M$ is an Even dominion in $\mathcal{G}$ that
$\mathcal{T}^{\mathrm{Even}}$ embeds, then $M\subseteq\mathcal{G}_{i+1}$.

For $i=0$, this is moot because $\mathcal{G}_{1}=\mathcal{G}$.

For $i>0$, let $M$ be an Even dominion that has an Even $d$-attractor
decomposition $\mathcal{H}$ such that $\mathcal{T}^{\mathrm{Even}}$ embeds
$\mathcal{T}_{\mathcal{H}}$. The inner inductive hypothesis (for $i-1$)
implies that $M\subseteq\mathcal{G}_{i}$.

The reader is encouraged to systematically refer to Figure 4 to better follow
the rest of this part of the proof.

Let
$M^{\prime}=M\setminus\mathrm{Attr}_{\mathrm{Even}}^{\mathcal{G}_{i}}(D_{i})$.
Because
$\mathcal{G}_{i}\setminus\mathrm{Attr}_{\mathrm{Even}}^{\mathcal{G}_{i}}(D_{i})$
is a trap for Even in $\mathcal{G}_{i}$ and $M$ is a trap for Odd in
$\mathcal{G}_{i}$, the dual of Proposition 4.3 yields that $M^{\prime}$ is a
trap for Even in $\mathcal{G}_{i}\cap M$.

Then, because $\mathcal{H}$ is an Even $d$-attractor decomposition of
$\mathcal{G}\cap M$, it follows by Theorem 4.2 that there is an Even
$d$-attractor decomposition $\mathcal{H}^{\prime}$ of $\mathcal{G}_{i}\cap
M^{\prime}$ such that $\mathcal{T}_{\mathcal{H}}$ embeds
$\mathcal{T}_{\mathcal{H}^{\prime}}$, and hence also
$\mathcal{T}^{\mathrm{Even}}$ embeds $\mathcal{T}_{\mathcal{H}^{\prime}}$.

Therefore, because $M^{\prime}$ is an Even dominion in the game
$\mathcal{G}_{i}\setminus\mathrm{Attr}_{\mathrm{Even}}^{\mathcal{G}_{i}}(D_{i})$,
part (b) of the outer inductive hypothesis yields $M^{\prime}\cap
U_{i}=\emptyset$.

Finaly, because $M\setminus
M^{\prime}\subseteq\mathrm{Attr}_{\mathrm{Even}}^{\mathcal{G}_{i}}(D_{i})$ and
$(M^{\prime}\setminus M)\cap U_{i}=\emptyset$, it follows that $M\cap
U_{i}=\emptyset$. By Proposition 4.6, we obtain
$M\cap\mathrm{Attr}_{\mathrm{Odd}}^{\mathcal{G}_{i}}(U_{i})=\emptyset$ and
hence $M\subseteq\mathcal{G}_{i+1}$.

Figure 5. Attractors, subgames, and dominia in the second part of the proof of
the dominion separation theorem.

#### Odd dominia embedded by
$\left\langle\mathcal{T}_{1}^{\mathrm{Odd}},\ldots,\mathcal{T}_{i}^{\mathrm{Odd}}\right\rangle$
are disjoint from $\mathcal{G}_{i+1}$.

We prove by induction on $i$ (another “inner” induction) that for
$i=0,1,\dots,k$, if $M$ is an Odd dominion in $\mathcal{G}$ that
$\left\langle\mathcal{T}^{\mathrm{Odd}}_{1},\ldots,\mathcal{T}^{\mathrm{Odd}}_{i}\right\rangle$
embeds, then $\mathcal{G}_{i+1}\cap M=\emptyset$.

For $i=0$, note that
$\left\langle\mathcal{T}_{1}^{\mathrm{Odd}},\dots,\mathcal{T}_{i}^{\mathrm{Odd}}\right\rangle=\left\langle\right\rangle$
and the only Odd dominion $M$ in $\mathcal{G}$ that has an Odd
$(d+1)$-attractor decomposition whose tree is the trivial tree
$\left\langle\right\rangle$ is the empty set, and hence $\mathcal{G}_{1}\cap
M=\emptyset$, because $\mathcal{G}_{1}=\mathcal{G}$.

The reader is encouraged to systematically refer to Figure 5 to better follow
the rest of this part of the proof.

For $i>0$, let

$\mathcal{H}=\left\langle\emptyset,(S_{1},\mathcal{H}_{1},A_{1}),\dots,(S_{\bar{\imath}},\mathcal{H}_{\bar{\imath}},A_{\bar{\imath}})\right\rangle$

be an Odd $(d+1)$-attractor decomposition of $\mathcal{G}\cap M$ such that
$\left\langle\mathcal{T}^{\mathrm{Odd}}_{1},\dots,\mathcal{T}^{\mathrm{Odd}}_{i}\right\rangle$
embeds $\mathcal{T}_{\mathcal{H}}$. Note that the embedding implies that
$\bar{\imath}\leq i$.

If
$\left\langle\mathcal{T}_{1}^{\mathrm{Odd}},\dots,\mathcal{T}_{i-1}^{\mathrm{Odd}}\right\rangle$
embeds $\mathcal{T}_{\mathcal{H}}$ then the inner inductive hypothesis (for
$i-1$) implies that $\mathcal{G}_{i}\cap M=\emptyset$ and thus
$\mathcal{G}_{i+1}\cap M=\emptyset$ since
$\mathcal{G}_{i+1}\subseteq\mathcal{G}_{i}$.

Otherwise, it must be the case that

(3) $\text{$\mathcal{T}^{\mathrm{Odd}}_{i}$ embeds
$\mathcal{T}_{\mathcal{H}_{\bar{\imath}}}$}\,.$

Observe that the set $A_{\leq{\bar{\imath}}-1}=A_{1}\cup A_{2}\cup\cdots\cup
A_{{\bar{\imath}}-1}$ is a trap for Even in $\mathcal{G}\cap M$, and hence by
trap transitivity it is a trap for Even in $\mathcal{G}$ because $M$ is a trap
for Even in $\mathcal{G}$. Moreover, subgame $\mathcal{G}\cap
A_{\leq{\bar{\imath}}-1}$ has an Odd $(d+1)$-attractor decomposition

$\mathcal{I}\>=\>\left\langle\emptyset,(S_{1},\mathcal{H}_{1},A_{1}),\dots,(S_{\bar{\imath}-1},\mathcal{H}_{\bar{\imath}-1},A_{\bar{\imath}-1})\right\rangle$

in $\mathcal{G}$ and hence—by Proposition 2.5—it is an Odd dominion in
$\mathcal{G}$, and ordered tree
$\left\langle\mathcal{T}_{1}^{\mathrm{Odd}},\dots,\mathcal{T}_{i-1}^{\mathrm{Odd}}\right\rangle$
embeds $\mathcal{T}_{\mathcal{I}}$. Hence, the inner inductive hypothesis (for
$i-1$) yields

(4) $\mathcal{G}_{i}\cap A_{\leq\bar{\imath}-1}\>=\>\emptyset\,.$

Set $M^{\prime}=\mathcal{G}_{i}\cap M$ and note that not only
$M^{\prime}\subseteq A_{\bar{\imath}}$, but also $M^{\prime}$ is a trap for
Odd in $A_{\bar{\imath}}$, because $\mathcal{G}_{i}$ is a trap for Odd in
$\mathcal{G}$. Moreover—by Proposition 4.3—$M^{\prime}$ is an Odd dominion in
$\mathcal{G}_{i}$ because $\mathcal{G}_{i}$ is a trap for Odd in $\mathcal{G}$
and $M$ is a dominion for Odd in $\mathcal{G}$.

Observe that
$\mathcal{J}=\left\langle\emptyset,(S_{\bar{\imath}},\mathcal{H}_{\bar{\imath}},A_{\bar{\imath}})\right\rangle$
is an Odd $(d+1)$-attractor decomposition of $\mathcal{G}\cap
A_{\bar{\imath}}$. By the embeddable decomposition theorem (Theorem 4.2), it
follows that there is an Odd $(d+1)$-attractor decomposition $\mathcal{K}$ of
$\mathcal{G}\cap M^{\prime}$ such that $\mathcal{T}_{\mathcal{J}}$ embeds
$\mathcal{T}_{\mathcal{K}}$. Because of this embedding, $\mathcal{K}$ must
have the form
$\mathcal{K}=\left\langle\emptyset,(S^{\prime},\mathcal{K}^{\prime},M^{\prime})\right\rangle$.
Since $\mathcal{T}_{\mathcal{J}}$ embeds $\mathcal{T}_{\mathcal{K}}$, we also
have that $\mathcal{T}_{\mathcal{H}_{\bar{\imath}}}$ embeds
$\mathcal{T}_{\mathcal{K}^{\prime}}$, and hence—by
(3)—$\mathcal{T}^{\mathrm{Odd}}_{i}$ embeds
$\mathcal{T}_{\mathcal{K}^{\prime}}$.

Note that $S^{\prime}$ is a trap for Odd in $\mathcal{G}\cap M^{\prime}$ in
which every vertex priority is at most $d-1$, because $\mathcal{K}$ is an Odd
$(d+1)$-attractor decomposition of $\mathcal{G}\cap M^{\prime}$. It follows
that $S^{\prime}$ is also an Odd dominion in
$\mathcal{G}_{i}\setminus\mathrm{Attr}_{\mathrm{Even}}^{\mathcal{G}_{i}}(D_{i})$.

The outer inductive hypothesis then yields $S^{\prime}\subseteq U_{i}$. It
follows that

$M^{\prime}=\mathrm{Attr}_{\mathrm{Odd}}^{\mathcal{G}_{i}\cap
M^{\prime}}(S^{\prime})\subseteq\mathrm{Attr}^{\mathcal{G}_{i}}_{\mathrm{Odd}}(S^{\prime})\subseteq\mathrm{Attr}^{\mathcal{G}_{i}}_{\mathrm{Odd}}(U_{i})\,,$

where the first inclusion holds because $M^{\prime}$ is a trap for Even in
$\mathcal{G}_{i}$, and the second follows from monotonicity of the attractor
operator. When combined with with (4), this implies $\mathcal{G}_{i+1}\cap
M=\emptyset$. ∎

###  4.3. Correctness and complexity

The dominion separation theorem (Theorem 4.5) allows us to conclude the proof
of the main universal algorithm correctness theorem (Theorem 4.1). Indeed, if
trees $\mathcal{T}^{\mathrm{Even}}$ and $\mathcal{T}^{\mathrm{Odd}}$ satisfy
the conditions of Theorem 4.1 then, by the dominion separation theorem, the
set returned by the call
$\textnormal{{$\text{Univ}_{\mathrm{Even}}$}}\left(\mathcal{G},d,\mathcal{T}^{\mathrm{Even}},\mathcal{T}^{\mathrm{Odd}}\right)$
separates the largest Even dominion from the largest Odd dominion, and
hence—by the positional determinacy theorem (Theorem 2.3)—it is the largest
Even dominion. The argument for procedure $\text{Univ}_{\mathrm{Odd}}$ is
analogous.

We note that the universal algorithm correctness theorem, together with
Propositions 3.8 and 3.7, imply correctness of the non-adaptive version of
Parys’s algorithm (Parys, 2019) and of Lehtinen-Schewe-Wojtczak algorithm
(Lehtinen et al., 2019), because trees of attractor decompositions are
$(n,d/2)$-small (Proposition 3.1) and trees $P_{n,d/2}$ and $S_{n,d/2}$ are
$(n,d/2)$-universal.

The following fact, an alternative restatement of the conclusion of Lehtinen
et al. (Lehtinen et al., 2019), is a simple corollary of the precise
asymptotic upper bounds on the size of the universal trees $S_{n,d/2}$
established by Jurdziński and Lazić (Jurdziński and Lazić, 2017), and of
Propositions 3.7, 3.3, and 3.5.

###### Proposition 4.7 (Complexity).

The universal algorithm that uses universal trees $S_{n,d/2}$ (aka. Lehtinen-
Schewe-Wojtczak algorithm) solves $(n,d)$-small parity games in polynomial
time if $d=O(\log n)$, and in time $n^{2\lg(d/{\lg n})+O(1)}$ if
$d=\omega(\log n)$.

###  4.4. Acceleration by tree pruning

As we have discussed in Section 3.2, Parys (Parys, 2019) has achieved a
breakthrough of developing the first quasi-polynomial McNaughton-Zielonka-
style algorithm for parity games by pruning the tree of recursive calls down
to quasi-polynomial size. Proposition 3.8 clarifies that Parys’s scheme can be
reproduced by letting the universal algorithm run on universal trees
$P_{n,d/2}$, but as it also mentions, just doing so results in a “non-
adaptive” version of Parys’s algorithm. What is the “adaptive” version
actually proposed by Parys?

Recall that the root of tree $P_{n,h}$ has $n+1$ children, the first $n/2$ and
the last $n/2$ children are the roots of copies of tree $P_{n/2,h-1}$, and the
middle child is the root of a copy of tree $P_{n,h-1}$. The adaptive version
of Parys’s algorithm also uses another tree-prunning rule, which is adaptive
and a slight generalization of the empty-set rule: whenever the algorithm is
processing the block of the first $n/2$ children of the root or the last $n/2$
children of the root, if one of the recursive calls in this block returns an
empty set then the rest of the block is omitted.

We expect that our structural results (such as Theorems 4.1 and 4.5) will
provide insights to inspire development and proving correctness of further and
more sophisticated adaptive tree-pruning rules, but we leave it to future
work. This may be critical for making quasi-polynomial versions of McNaughton-
Zielonka competitive in practice with its basic version that is exponential in
the worst case, but remains very hard to beat in practice (van Dijk, 2018;
Parys, 2019).

##  5\. Symbolic algorithms

Parity games that arise in applications, for example from the automata-
theoretic model checking approaches to verification and automated synthesis,
often suffer from the _state-space explosion problem_ : the sizes of models
are exponential (or worse) in the sizes of natural descriptions of the
modelled objects, and hence the models obtained may be too large to store them
explicitly in memory. One method of overcoming this problem that has been
successful in the practice of algorithmic formal methods is to represent the
models symbolically rather than explicitly, and to develop algorithms for
solving the models that work directly on such succinct symbolic
representations (Burch et al., 1992).

We adopt the _set-based symbolic model of computation_ that was already
considered for parity games by Chatterjee, Dvořák, Henzinger, and Svozil
(Chatterjee et al., 2018). In this model, any standard computational
operations on any standard data structures are allowed, but there are also the
following symbolic resources available: _symbolic set variables_ can be used
to store sets of vertices in the graph of a parity game; basic set-theoretic
operations on symbolic set variables are available as _primitive symbolic
operations_ ; the _controllable predecessors_ operations are available as
primite symbolic operations: the Even (resp. Odd) controllable predecessor,
when applied to a symbolic set variable $X$, returns the set of vertices from
which Even (resp. Odd) can force to move into the set $X$, by taking just one
outgoing edge. Since symbolic set variables can represent possibly very large
and complex objects, they should be treated as a costly resource.

Chatterjee et al. (Chatterjee et al., 2018) have given a symbolic set-based
algorithm that on $(n,d)$-small parity games uses $O(d\log n)$ of symbolic set
variables and runs in quasi-polynomial time. While the dependence on $n$ is
only logarithmic, a natural question is whether this dependence is inherent.
Given that $n$ can be prohibitively large in applications, reducing dependence
on $n$ is desirable. In this section we argue that it is not only possible to
eliminate the dependence on $n$ entirely, but it is also possible to
exponentially improve the dependence on $d$, resulting in a quasi-polynomial
symbolic algorithm for solving parity games that uses only $O(\lg d)$ symbolic
set variables.

###  5.1. Universal algorithm symbolically

In the set-based symbolic model of computation, it is routine to compute the
attractors efficiently: it is sufficient to iterate the controllable
predecessor operations. Using the results of Jurdziński and Lazić (Jurdziński
and Lazić, 2017), on can also represent a path of nodes from the root to a
leaf in the tree $S_{n,d/2}$ in $O(\lg n\cdot\lg d)$ bits, and for every node
on such a path, to compute its number of children in $O(\lg n\cdot\lg d)$
standard primitive operations. This allows to run the whole universal
algorithm (Algorithm 2) on an $(n,d)$-small parity game and two copies of
trees $S_{n,d/2}$, using only $O(\lg n\cdot\lg d)$ bits to represent the
relevant nodes in the trees $\mathcal{T}^{\mathrm{Even}}$ and
$\mathcal{T}^{\mathrm{Odd}}$ throughout the execution.

The depth of the tree of recursive calls of the universal algorithm on an
$(n,d)$-small parity game is at most $d$. Moreover, in every recursive call,
only a small constant number of set variables is needed because only the
latest sets $V^{\mathcal{G}_{i}}$, $D_{i}$, $V^{\mathcal{G}^{\prime}_{i}}$,
and $U_{i}$ are needed at any time. It follows that the overall number of
symbolic set variables needed to run the universal algorithm is $O(d)$. Also
note that every recursive call can be implemented symbolically using a
constant number of primitive symbolic operations and two symbolic attractor
computations.

This improves the symbolic space from Chatterjee et al.’s $O(d\lg n)$ to
$O(d)$, while keeping the running time quasipolynomial. Moreover, this
symbolic algorithm is very simple and straightforward to implement, which
makes it particularly promising and attractive for empirical evaluation and
deployment in applications.

###  5.2. Succinct symbolic partitions

In this section we describe how the number of symbolic set variables in the
symbolic implementation of the universal algorithm can be further reduced from
$O(d)$ to $O(\log d)$. We use letters $G$, $D$, $G^{\prime}$, and $U$ to
denote the sets $V^{\mathcal{G}_{i}}$, $D_{i}$,
$V^{\mathcal{G}^{\prime}_{i}}$, and $U_{i}$ for some $i$-th iteration of any
of the recursive calls of the universal algorithm. Observe that we do not need
to keep the symbolic variables that store the sets $D$, $G^{\prime}$, and $U$
on the stack of recursive calls because on any return from a recursive call,
their values are not needed to proceed. How can we store the sets denoted by
all the symbolic set variables $G$ on the stack using only $O(\log d)$
symbolic set variables, while the height of the stack may be as large as $d$?

Firstly, we argue that we can symbolically represent any sequence
$\left\langle G_{d-1},\dots,G_{i}\right\rangle$ of set variables that would
normally occur on the stack of recursive calls of the universal algorithm, by
another sequence $\left\langle H_{d-1},\dots,H_{0}\right\rangle$, in which the
sets form a partition of the set of vertices in the parity game. Indeed, a
sequence $\left\langle G_{d},\dots,G_{i}\right\rangle$ on the stack of
recursive calls at any time forms a descending chain w.r.t. inclusion, and
$G_{d}$ is the set of all vertices, so it suffices to consider the sequence
$\left\langle G_{d}\setminus G_{d-1},\dots,G_{i+1}\setminus
G_{i},G_{i},\emptyset,\dots,\emptyset\right\rangle$.

Secondly, we argue that the above family of $d$ mutually disjoint sets can be
succinctly represented and maintained using $O(\log d)$ set variables.
W.l.o.g., assume that $d$ is a power of $2$. For every $k=1,2,\dots,\lg d$,
and for every $i=1,2,\dots,d$, let $\mathrm{bit}_{k}(i)$ be the $k$-th digit
in the binary representation of $i$ (and zero if there are less than $k$
digits). We now define the following sequence of sets $\left\langle
S_{1},S_{2},\dots,S_{\lg d}\right\rangle$ that provides a succinct
representation of the sequence $\left\langle
H_{d-1},\dots,H_{0}\right\rangle$. For every $k=1,2,\dots,\lg d$, we set:

$S_{k}\>=\>\bigcup\left\\{H_{i}\>:\>0\leq i\leq d-1\text{ and
}\mathrm{bit}_{k}(i)=1\right\\}\,.$

By sets $\left\langle H_{d-1},\dots,H_{0}\right\rangle$ forming a partition of
the set of all vertices, it follows that for every $i=0,1,\dots,d-1$, we have:

$H_{i}\>=\>\bigcap\left\\{S_{k}\>:\>1\leq k\leq\lg d\text{ and
}\mathrm{bit}_{k}(i)=1\right\\}\\\
\cap\;\bigcap\left\\{\overline{S_{k}}\>:\>1\leq k\leq\lg d\text{ and
}\mathrm{bit}_{k}(i)=0\right\\}\,,$

where $\overline{X}$ is the complement of set $X$.

What remains to be shown is that the operations on the sequence of sets
$\left\langle G_{d-1},\dots,G_{i}\right\rangle$ that reflect changes on the
stack of recursive calls of the universal algorithm can indeed be implemented
using small numbers of symbolic set operations on the succinct representation
$\left\langle S_{1},\dots,S_{\lg d}\right\rangle$ of the sequence
$\left\langle H_{d-1},\dots,H_{0}\right\rangle$. We note that there are two
types of changes to the sequence $\left\langle
G_{d-1},\dots,G_{i}\right\rangle$ that the universal algorithm makes:

  1. (a)

all components are as before, except for $G_{i}$ that is replaced by
$G_{i}\setminus B$, for some set $B\subseteq G_{i}$;

  2. (b)

all components are as before, except that a new entry $G_{i-1}$ is added equal
to $G_{i}\setminus B$, for some set $B\subseteq G_{i}$.

The corresponding changes to the sequence $\left\langle
H_{d-1},\dots,H_{0}\right\rangle$ are then:

  1. (a)

all components are as before, except that set $H_{i+1}$ is replaced by
$H_{i+1}\cup B$, and set $H_{i}$ is replaced by $H_{i}\setminus B$;

  2. (b)

all components are as before, except that set $H_{i}$ is replaced by $B$, and
set $H_{i-1}$ is replaced by $H_{i}\setminus B$.

To implement the update of type (a), it suffices to perform the following
update to the succinct representation:

$S^{\prime}_{k}\>=\>\begin{cases}S_{k}&\text{if
$\mathrm{bit}_{k}(i+1)=\mathrm{bit}_{k}(i)$},\\\ S_{k}\cup B&\text{if
$\mathrm{bit}_{k}(i+1)=1$ and $\mathrm{bit}_{k}(i)=0$},\\\ S_{k}\setminus
B&\text{if $\mathrm{bit}_{k}(i+1)=0$ and $\mathrm{bit}_{k}(i)=1$}.\end{cases}$

and to to implement the update of type (b), it suffices to perform the
following:

$S^{\prime}_{k}\>=\>\begin{cases}S_{k}&\text{if
$\mathrm{bit}_{k}(i)=\mathrm{bit}_{k}(i-1)$},\\\ S_{k}\setminus(H_{i}\setminus
B)&\text{if $\mathrm{bit}_{k}(i)=1$ and $\mathrm{bit}_{k}(i-1)=0$},\\\
S_{k}\cup(H_{i}\setminus B)&\text{if $\mathrm{bit}_{k}(i)=0$ and
$\mathrm{bit}_{k}(i-1)=1$}.\end{cases}$

This completes the proof sketch of the main technical result in this section.

###### Theorem 5.1.

There is a symbolic algorithm that solves $(n,d)$-small parity games using
$O(\lg d)$ symbolic set variables, $O(\log d\cdot\log n)$ bits of conventional
space, and whose running time is polynomial if $d=O(\log n)$, and
$n^{2\lg(d/{\lg n})+O(1)}$ if $d=\omega(\log n)$.

###### Acknowledgements.

The first author has been supported by the EPSRC grant EP/P020992/1 (Solving
Parity Games in Theory and Practice). The idea of the design of the universal
algorithm has been discovered independently and later by Nathanaël Fijalkow;
we thank him for sharing his conjectures with us and exchanging ideas about
adaptive tree-pruning rules. We also thank Alexander Kozachinskiy and
Thejaswini K. S. for helpful comments on earlier drafts of the paper.

## References

  * (1)
  * Baldan et al. (2019) P. Baldan, B. König, C. Mika-Michalski, and T. Padoan. 2019\.  Fixpoint games on continuous lattices.  _Proceedings of the ACM on Programming Languages_ 3, POPL, January 2019 (2019), 26:1–26:29.
  * Bradfield and Walukiewicz (2018) J. C. Bradfield and I. Walukiewicz. 2018.  _Handbook of Model Checking_.  Springer, Chapter The mu-calculus and model checking, 871–919.
  * Burch et al. (1992) J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. 1992.  Symbolic model checking: $10^{20}$ states and beyond.  _Inf. Comput._ 98, 2 (1992), 142–170.
  * Calude et al. (2017) C. S. Calude, S. Jain, B. Khoussainov, W. Li, and F. Stephan. 2017.  Deciding parity games in quasipolynomial time. In _STOC 2017_. ACM, Montreal, QC, Canada, 252–263.
  * Chatterjee et al. (2018) K. Chatterjee, W. Dvořák, M. Henzinger, and A. Svozil. 2018.  Quasipolynomial set-based symbolic algorithms for parity games. In _LPAR-22_ _(EPiC Series in Computing)_ , Vol. 57. EasyChair, Awassa, Ethiopia, 233–253.
  * Czerwiński et al. (2019) W. Czerwiński, L. Daviaud, N. Fijalkow, M. Jurdziński, R. Lazić, and P. Parys. 2019\.  Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games. In _SODA 2019_. SIAM, San Diego, CA, 2333–2349.
  * Daviaud et al. (2018) L. Daviaud, M. Jurdziński, and R. Lazić. 2018\.  A pseudo-quasi-polynomial algorithm for mean-payoff parity games. In _LICS 2018_. ACM, Oxford, UK, 325–334.
  * Daviaud et al. (2019) L. Daviaud, M. Jurdziński, and K. Lehtinen. 2019\.  Alternating weak automata from universal trees. In _CONCUR 2019_ _(Leibniz International Proceedings in Informatics (LIPIcs))_ , Vol. 140. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Amsterdam, the Netherlands, 18:1–18:14.
  * Emerson and Jutla (1991) E. A. Emerson and C. S. Jutla. 1991.  Tree automata, mu-calculus and determinacy. In _FOCS 1991_. IEEE Computer Society, San Juan, Puerto Rico, 368–377.
  * Emerson et al. (1993) E. A. Emerson, C. S. Jutla, and P. Sistla. 1993.  On model-checking for fragments of $\mu$-calculus. In _CAV 1993_ _(LNCS)_ , Vol. 697. Springer, Elounda, Greece, 385–396.
  * Etessami et al. (2005) K. Etessami, T. Wilke, and R. A. Schuller. 2005.  Fair simulation relations, parity games, and state space reduction for Büchi automata.  _SIAM J. Comput._ 34, 5 (2005), 1159–1175.
  * Fearnley (2010) J. Fearnley. 2010\.  Exponential lower bounds for policy iteration. In _ICALP 2010_ _(LNCS)_ , Vol. 6199. Springer, Bordeaux, France, 551–562.
  * Friedmann (2009) O. Friedmann. 2009\.  An exponential lower bound for the parity game strategy improvement algorithm as we know it. In _LICS 2009_. IEEE Computer Society, Los Angeles, CA, USA, 145–156.
  * Friedmann (2011a) O. Friedmann. 2011a.  Recursive algorithm for parity games requires exponential time.  _RAIRO — Theor. Inf. and Applic._ 45, 4 (2011), 449–457.
  * Friedmann (2011b) O. Friedmann. 2011b.  A subexponential lower bound for Zadeh’s pivoting rule for solving linear programs and games. In _IPCO 2011_ _(LNCS)_ , Vol. 6655. Springer, New York, NY, USA, 192–206.
  * Friedmann et al. (2011) O. Friedmann, T. D. Hansen, and U. Zwick. 2011.  Subexponential lower bounds for randomized pivoting rules for the simplex algorithm. In _STOC 2011_. ACM, San Jose, CA, USA, 283–292.
  * Grädel et al. (2002) E. Grädel, W. Thomas, and T. Wilke (Eds.). 2002.  _Automata, Logics, and Infinite Games: A Guide to Current Research_. LNCS, Vol. 2500.  Springer.
  * Hasuo et al. (2016) I. Hasuo, S. Shimizu, and C. Cîrstea. 2016.  Lattice-theoretic progress measures and coalgebraic model checking. In _POPL 2016_. ACM, St. Petersburg, FL, USA, 718–732.
  * Hausmann and Schröder (2019) D. Hausmann and L. Schröder. 2019.  Computing nested fixpoints in quasipolynomial time.  arXiv:1907.07020.
  * Jurdziński and Lazić (2017) M. Jurdziński and R. Lazić. 2017.  Succinct progress measures for solving parity games. In _LICS 2017_. IEEE Computer Society, Reykjavik, Iceland, 1–9.
  * Jurdziński et al. (2008) M. Jurdziński, M. Paterson, and U. Zwick. 2008\.  A deterministic subexponential algorithm for solving parity games.  _SIAM J. Comput._ 38, 4 (2008), 1519–1532.
  * Lehtinen (2018) K. Lehtinen. 2018\.  A modal $\mu$ perspective on solving parity games in quasi-polynomial time. In _LICS 2018_. IEEE, Oxford, UK, 639–648.
  * Lehtinen et al. (2019) K. Lehtinen, S. Schewe, and D. Wojtczak. 2019.  Improving the complexity of Parys’ recursive algorithm.  arXiv:1904.11810
  * Luttenberger et al. (2019) M. Luttenberger, P. J. Meyer, and S. Sickert. 2019.  Practical synthesis of reactive systems from LTL specifications via parity games.  arXiv:1903.12576.
  * McNaughton (1993) R. McNaughton. 1993\.  Infinite games played on finite graphs.  _Annals of Pure and Applied Logic_ 65, 2 (1993), 149–184.
  * Parys (2019) P. Parys. 2019.  Parity games: Zielonka’s algorithm in quasi-polynomial time. In _MFCS 2019_ _(Leibniz International Proceedings in Informatics (LIPIcs))_ , Vol. 138. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Aachen, Germany, 10:1–10:13.
  * van Dijk (2018) T. van Dijk. 2018\.  Oink: An implementation and evaluation of modern parity game solvers. In _TACAS 2018_ _(LNCS)_ , Vol. 10805. Springer, Thessaloniki, Greece, 291–308.
  * Vöge and Jurdziński (2000) J. Vöge and M. Jurdziński. 2000.  A discrete strategy improvement algorithm for solving parity games. In _CAV 2000_ _(LNCS)_ , Vol. 1855. Springer, Chicago, IL, USA, 202–215.
  * Zielonka (1998) W. Zielonka. 1998\.  Infinite games on finitely coloured graphs with applications to automata on infinite trees.  _Theoretical Computer Science_ 200, 1–2 (1998), 135–183.

##  Appendix A Appendix

###### Proof of Proposition 4.3.

Firstly, we argue that $T\cap R$ is a trap for Odd in subgame $\mathcal{G}\cap
R$. Let $v\in(T\cap R)\cap V_{\mathrm{Odd}}$. We need to argue that if
$(v,w)\in E$ and $w\in R$ then $w\in T$, which follows directly from the
assumption that $T$ is a trap for Odd in $\mathcal{G}$. Let $v\in(T\cap R)\cap
V_{\mathrm{Even}}$. We need to argue that there is $(v,w)\in E$, such that
$w\in T\cap R$. Observe that there is an edge $(v,w)\in E$, such that $w\in
T$, because $T$ is a trap for Odd in $\mathcal{G}$. Note, however, that we
also have $w\in R$ because $R$ is a trap for Even in $\mathcal{G}$.

Now suppose that $T$ is not only a trap for Odd in $\mathcal{G}$ but it is
also an Even dominion in $\mathcal{G}$ and let $\sigma$ be an Even dominion
strategy on $T$. Note that $\sigma$ is also an Even dominion strategy on
$T\cap R$ in subgame $\mathcal{G}\cap R$ because $R$ is a trap for Even. ∎

###### Proof of Proposition 4.4.

Firstly, we argue that $A\cap T\subseteq A^{\prime}$. Let $\sigma$ be an Even
reachability strategy from $A$ to $B$ in $\mathcal{G}$. Note that $\sigma$ is
also an Even reachability strategy from $A\cap T$ to $B\cap T$ in
$\mathcal{G}\cap T$ because $T$ is a trap for Even in $\mathcal{G}$. It then
follows that $A\cap T\subseteq A^{\prime}$ because $A^{\prime}$ is the Even
attractor to $B\cap T$ in $\mathcal{G}\cap T$.

Secondly, we argue that $T\setminus A^{\prime}$ is a trap for Even in
$\mathcal{G}\setminus A$. Note that $T\setminus A^{\prime}$ is a trap for Even
in $\mathcal{G}$ by trap transitivity: $T$ is a trap for Even in
$\mathcal{G}$, and $T\setminus A^{\prime}$ is a trap for Even in
$\mathcal{G}\cap T$ because it is a complement of an Even attractor. From
$A\cap T\subseteq A^{\prime}$ it follows that $T\setminus A^{\prime}$ is
disjoint from $A$, and hence it is also a trap for Even in
$\mathcal{G}\setminus A$. ∎