# Two new algorithms for solving Müller games and their applications

Zihui Liang<EMAIL_ADDRESS>0000-0002-9022-6470 ,  Bakh Khoussainov
<EMAIL_ADDRESS>and  Mingyu Xiao<EMAIL_ADDRESS>0000-0002-1012-2373
University of Electronic Science and Technology of China2006 Xiyuan
AvenueChengduSichuanChina611731

###### Abstract.

Müller games form a well-established class of games for model checking and
verification. These games are played on directed graphs $\mathcal{G}$ where
Player 0 and Player 1 play by generating an infinite path through the graph.
The winner is determined by the set $X$ consisting of all vertices in the path
that occur infinitely often. If $X$ belongs to $\Omega$, a specified
collection of subsets of $\mathcal{G}$, then Player 0 wins. Otherwise, Player
1 claims the win. These games are determined, enabling the partitioning of
$\mathcal{G}$ into two sets $W_{0}$ and $W_{1}$ of winning positions for
Player 0 and Player 1, respectively. Numerous algorithms exist that decide
Müller games $\mathcal{G}$ by computing the sets $W_{0}$ and $W_{1}$. In this
paper, we introduce two novel algorithms that outperform all previously known
methods for deciding explicitly given Müller games, especially in the worst-
case scenarios. The previously known algorithms either reduce Müller games to
other known games (e.g. safety games) or recursively change the underlying
graph $\mathcal{G}$ and the collection of sets in $\Omega$. In contrast, our
approach does not employ these techniques but instead leverages subgames, the
sets within $\Omega$, and their interactions. This distinct methodology sets
our algorithms apart from prior approaches for deciding Müller games.
Additionally, our algorithms offer enhanced clarity and ease of comprehension.
Importantly, our techniques are applicable not only to Müller games but also
to improving the performance of existing algorithms that handle other game
classes, including coloured Müller games, McNaughton games, Rabin games, and
Streett games.

Müller games, McNaughton games, Rabin games, Streett games, deciding games

††copyright: acmcopyright††ccs: Theory of computation Verification by model
checking††ccs: Mathematics of computing Combinatorics††ccs: Theory of
computation Representations of games and their complexity††ccs: Theory of
computation Algorithmic game theory††ccs: Theory of computation Complexity
theory and logic

##  1\. Introduction

In the area of verification and synthesis of reactive systems, model checking,
and logic, studying games played on finite graphs is a key research topic
(Grädel et al., 2002). The most current work (Fijalkow et al., 2023) serves as
an excellent reference for the state-of-the-art methods in this area. Interest
in these games primarily arises from their role in modeling and verifying
reactive systems and their specifications as games on graphs. These games are
played on finite directed graphs between Player 0 (the controller) and Player
1 (the adversary, e.g., the environment). The players engage in ongoing
interactions with each other, and the winner is determined by the long-term
behavior of the players. Müller games, McNaughton games, coloured Müller
games, Rabin games, and Streett games constitute well-established classes of
games for verification. These games are played on bipartite graphs
$\mathcal{G}$ where Player 0 and Player 1 play the game by producing an
infinite path $\rho$ in $\mathcal{G}$. Then the winner of this play is
determined by conditions put on $\mathsf{Inf}(\rho)$ the set of all vertices
in the path that appear infinitely often. Thus, the winning conditions depend
solely on those vertices that occur infinitely often in the given play $\rho$.
Understanding the algorithmic content of determinacy results for these games
is at the core of the area.

All games that we listed above, including Müller games, are played in arenas
that we define below:

###### Definition 1.1.

An arena $\mathcal{A}$, or equivalently a game graph, is a bipartite directed
graph $(V_{0},V_{1},E)$, where

  1. (1)

$V_{0}\cap V_{1}=\emptyset$, and $V=V_{0}\cup V_{1}$ is the set of nodes of
$\mathcal{A}$. The nodes of $V$ will also be called positions.

  2. (2)

$E\subseteq V_{0}\times V_{1}\cup V_{1}\times V_{0}$ is the set of edges such
that every node has an outgoing edge.

  3. (3)

$V_{0}$ and $V_{1}$ are sets of positions from which Player 0 and Player 1,
respectively, move. Nodes in $V_{0}$ are called Player 0 positions, and nodes
in $V_{1}$ are Player 1 positions.

Let $\mathcal{A}$ be an arena. Players play the game in the arena
$\mathcal{A}$ by taking turns and moving a token along the edges of the
underlying graph. Initially, the token is placed on a node $v_{0}\in V$. If
$v_{0}\in V_{0}$, then Player 0 moves first. Conversely, if $v_{0}\in V_{1}$,
then Player 1 moves first. In each round of play, if the token is positioned
on a Player $\sigma$’s position $v$, then Player $\sigma$ chooses $u\in E(v)$,
moves the token to $u$ along the edge $(v,u)$, and the play continues on to
the next round. Formally,

###### Definition 1.2.

Let $\mathcal{A}$ be an arena. A play, that starts at position $v_{0}$, is an
infinite sequence $\rho=v_{0},v_{1},v_{2},\ldots$ such that $v_{i+1}\in
E(v_{i})$ for all $i\in\mathbb{N}$. Note that in the play we used the
assumption $E(v)\neq\emptyset$.

Given a play $\rho=v_{0},v_{1},\ldots$, the set $\mathsf{Inf}(\rho)=\\{v\in
V\mid\exists^{\omega}i(v_{i}=v)\\}$ is called the infinity set of $\rho$. The
winner of this play is determined by a condition put on $\mathsf{Inf}(\rho)$.
We list several of these conditions that are well-established in the area.

###### Definition 1.3.

Let $\mathcal{A}=(V_{0},V_{1},E)$ be an arena. All the games below are called
regular games:

  1. (1)

A Müller game is the tuple $\mathcal{G}=(\mathcal{A},\Omega)$, where
$\Omega\subseteq 2^{V}$. Sets in $\Omega$ are called winning conditions. We
say that Player 0 wins the play $\rho=v_{0},v_{1},\ldots$ if
$\mathsf{Inf}(\rho)\in\Omega$. Otherwise, Player 1 wins.

  2. (2)

A McNaughton game is the tuple $\mathcal{G}=(\mathcal{A},W,\Omega)$, where
$W\subseteq V$, and $\Omega\subseteq 2^{W}$ is a collection of winning
conditions. Player 0 wins $\rho=v_{0},v_{1},\ldots$ if $\mathsf{Inf}(\rho)\cap
W\in\Omega$. Else, Player 1 wins.

  3. (3)

A coloured Müller game is $\mathcal{G}=(\mathcal{A},c,\Omega)$, where
$c:V\rightarrow C$ is a mapping from $V$ into the set $C$ of colors, and
$\Omega\subseteq 2^{C}$. Call sets in $\Omega$ winning conditions. Player 0
wins $\rho=v_{0},v_{1},\ldots$ if $c(\mathsf{Inf}(\rho))\in\Omega$. Else,
Player 1 wins.

  4. (4)

A Rabin game is the tuple
$\mathcal{G}=(\mathcal{A},(U_{1},V_{1}),\ldots,(U_{k},V_{k}))$, where
$U_{i},V_{i}\subseteq V$, $(U_{i},V_{i})$ is a winning condition, and the
index $k\geq 0$ is an integer. Player 0 wins $\rho=v_{0},v_{1},\ldots$ if
there is a pair $(U_{i},V_{i})$ such that $\mathsf{Inf}(\rho)\cap
U_{i}\neq\emptyset$ and $\mathsf{Inf}(\rho)\cap V_{i}=\emptyset$. Else, Player
1 wins.

  5. (5)

A Streett game is the tuple
$\mathcal{G}=(\mathcal{A},(U_{1},V_{1}),\ldots,(U_{k},V_{k}))$, where $U_{i}$,
$V_{i}$ are as in Rabin game. Player 0 wins $\rho=v_{0},v_{1},\ldots$ if for
all $i\in\\{1,\ldots,k\\}$ if $\mathsf{Inf}(\rho)\cap U_{i}\neq\emptyset$ then
$\mathsf{Inf}(\rho)\cap V_{i}\neq\emptyset$. Otherwise, Player 1 wins.

  6. (6)

A KL game is the tuple
$\mathcal{G}=(\mathcal{A},(u_{1},S_{1}),\ldots,(u_{t},S_{t}))$, where
$u_{i}\in V$, $S_{i}\subseteq V$ is a winning condition, and the index $t\geq
0$ is an integer. Player 0 wins $\rho=v_{0},v_{1},\ldots$ if there is a pair
$(u_{i},S_{i})$ such that $u_{i}\in\mathsf{Inf}(\rho)$ and
$\mathsf{Inf}(\rho)\subseteq S_{i}$. Else, Player 1 wins.

The first three games are symmetric, e.g., for the Müller game
$\mathcal{G}=(\mathcal{A},\Omega)$ its symmetric counter-part
$(\mathcal{A},2^{V}\setminus\Omega)$ is also Müller game. Player 0 loses in
game $(\mathcal{A},\Omega)$ if and only if Player 1 wins in
$(\mathcal{A},2^{V}\setminus\Omega)$. Rabin games can be considered as Streett
games. Player 0 wins Rabin game $\mathcal{G}$ if and only if Player 0 loses
the Streett game $\mathcal{G}$. The first five winning conditions have become
well-established. The last condition is new. The motivation behind this new
winning condition lies in the transformation of Rabin and Streett games into
Müller games via the KL winning condition. In a precise sense, as will be seen
in Section 7, the KL condition serves as a compressed Rabin winning condition.

The games defined above possess natural parameters. In Müller game, the
parameter is $\Omega$. In McNaughton games the parameter is the pair
$(W,\Omega)$. In colored Müller games the parameter is $(C,\Omega)$. For $KL$
games the parameter is $(u_{1},S_{1}),\ldots,(u_{t},S_{t}))$ and the index
$t$. In Rabin and Streett games the parameter is the winning condition
sequence $(U_{1},V_{1}),\ldots,(U_{k},V_{k})$ and the index $k$, the length of
the sequence of the winning condition pairs. We denote the parameter values by
$p$, so the value of $p$ belong to the set $\\{|W|,|C|,t,k,|\Omega|\\}$. The
values of these parameters, when $p=t$, $p=k$ or $p=|\Omega|$, can be
exponential on the size of the arenas.

###### Definition 1.4.

Let $\mathcal{G}$ be any of the regular games above. We say that $\mathcal{G}$
is explicitly given if $V$, $E$, and all the winning conditions of the game
$\mathcal{G}$, e.g., the sets in $\Omega$ in case $\mathcal{G}$ is a Müller
game, are fully presented as input.

For instance, the (input) size of explicitly given Müller game is thus bounded
by $|V|+|E|+2^{|V|}\cdot|V|$. In particular, the explicit representation of
any of the regular games can be exponential on the size of the arena of the
game.

A strategy for Player $\sigma$ is a function that receives as input initial
segments of plays $v_{0},v_{1},\ldots,v_{k}$ where $v_{k}\in V_{\sigma}$ and
outputs some $v_{k+1}$ such that $v_{k+1}\in E(v_{k})$. For regular games, an
important class of strategies are finite state strategies. The key is that
these strategies depend only on a finite bounded part of the full history of
the plays. R. McNaughton in (McNaughton, 1993) proved that the winner in
McNaughton games always has a finite state winning strategy. W. Zielonka
proves that the winners of regular games have finite state winning strategies
(Zielonka, 1998).

In the study of regular games, the focus is naturally placed on solving them.
Solving a given regular game entails two key objectives. First, one aims to
devise an algorithm that, when provided with a regular game $\mathcal{G}$,
partitions the set $V$ of positions into two sets $Win_{0}$ and $Win_{1}$ such
that $v\in Win_{\sigma}$ if and only if Player $\sigma$ wins the game starting
at $v$, where $\sigma\in\\{0,1\\}$. We call this the decision problem where
one wants to find out the winner of the game. Second, one would like to design
an algorithm that, given a regular game, extracts a winning strategy for the
victorious player. This is known as the synthesis problem where one wants to
design a winning strategy for the winner.

##  2\. Background and our contribution

In this section, we briefly provide a background on algorithms that solve the
above mentioned games with an emphasis on Müller games. We then introduce the
basic well-established concepts needed in the study of games played on graphs.

###  2.1. Known algorithms

We start with Müller games. McNaughton in (McNaughton, 1993) decides Müller
games in time $O(a^{|V|}|V|!|V|^{3})$ for some constant $a>1$. He proves that
the winner has a finite state winning strategy with at most $|V|!$ states.
Nerode, Remmel, and Yakhnis (Nerode et al., 1996) decide Müller games in
$O(|V|!\cdot 2^{|V|}|V|^{3}|E|)$. W. Zielenka (Zielonka, 1998) examines Müller
games through specifically constructed Zielenka trees. The size of each
Zielonka tree is $O(2^{|V|})$ in the worst case. S. Dziembowski, M.
Jurdzinski, and I. Walukiewicz in (Dziembowski et al., 1997) show that
deciding Müller games with Zielonka trees as part of the input is in
$\text{NP}\cap\text{co-NP}$. They also show that the bound $|V|!$ on the
memory of winning strategies is sharp. D. Neider, R. Rabinovich, and M.
Zimmermann reduce Müller games to safety games with $O((|V|!)^{3})$ vertices
and safety games can be solved in linear time (Neider et al., 2014). F. Horn
in (Horn, 2008) provides the first polynomial time decision algorithm for
explicitly given Müller games. The running time of his algorithm is
$O(|V|\cdot|\Omega|\cdot(|V|+|\Omega|)^{2})$. F. Horn’s correctness proof has
a non-trivial flaw. B. Khoussainov, Z. Liang, and M. Xiao in (Liang et al.,
2023) provide a correct proof of Horn’s algorithm through new techniques and
methods. Those techniques improve the running time of deciding Müller games to
$O(|\Omega|\cdot(|V|+|\Omega|)\cdot|V_{0}|\log|V_{0}|)$.

All the known algorithms that decide Müller games are either recursive
algorithms or reductions to other known classes of games. Some recursive
algorithms are based on induction techniques that decrease the sizes of arenas
$\mathcal{G}$ or the winning condition $\Omega$, and then recompute the
winning sets repeatedly. For instance, McNaughton algorithm, Nerode, Remmel,
Yakhnis algorithm, and Zielenka’s algorithm are of this type. These algorithms
typically produce $|V|!$ running time for deciding Müller games. Other
recursive algorithms are based on changing the structure of the underlying
graphs and the winning sets. For instance, Horn’s algorithm increases the size
of the underlying set to $|V|+|E|+|\Omega|+|\Omega||V|$. An example of an
algorithm that reduces Müller games to another class of known games is by D.
Neider, R. Rabinovich, and M. Zimmermann (Neider et al., 2014). They reduce
Müller games to safety games. Their reduction increases the size of the graph
of the safety game to $O((|V|!)^{3})$. As we noted above, Horn’s algorithm
runs in time $O(|V|\cdot|\Omega|\cdot(|V|+|\Omega|)^{2})$ polynomial on the
size of the explicitly given Müller games. The degree of $|\Omega|$ in this
bound is $|\Omega|^{3}$. The degree of $|\Omega|$ in the bound
$O(|\Omega|\cdot(|V|+|\Omega|)\cdot|V_{0}|\log|V_{0}|)$ from (Liang et al.,
2023) is $|\Omega|^{2}$. This is a significant reduction because the size of
$\Omega$ can be exponential on $|V|$.

With respect to McNaughton games, McNaughton (McNaughton, 1993) provided the
first algorithm that decides the games in time
$O(a^{|W|}\cdot|W|!\cdot|V|^{3})$, for a constant $a>1$. Nerode, Remmel, and
Yakhnis in (Nerode et al., 1996) improved the bound to $O(|W||E||W|!)$. A.
Dawar and P. Hunter proved that finding the winner in McNaughton games is
PSPACE-complete problem (Hunter and Dawar, 2008). This implied that deciding
the winner in games with all other winning conditions from Definition 1.3 is
also PSPACE-complete (Hunter and Dawar, 2008).

As McNaughton games can easily be transformed into coloured Müller games,
there has been a lot of work on designing algorithms for coloured Müller
games. The standard algorithm that decides coloured Müller games uses
induction on cardinality of $C$ (Fijalkow et al., 2023). These algorithms run
in time $O(|C||E|(|C||V|)^{|C|-1})$. C. Calude, S. Jain, B. Khoussainov, W.
Li, and F. Stephan, using their breakthrough quasi-polynomial time algorithm
for parity games, improve all the known algorithms for colored Müller games
(Calude et al., 2017). Their algorithm runs in time
$O(|C|^{5|C|}\cdot|V|^{5})$. Björklund, Sandberg and Vorobyov (Björklund et
al., 2003) showed that under the Exponential Time Hypothesis it is impossible
to decide colored Müller games in $O(2^{o(|C|)}\cdot|V|^{a})$ for any constant
$a$. C. Calude, S. Jain, B. Khoussainov, W. Li, and F. Stephan in (Calude et
al., 2017) improved this by showing that under the Exponential Time Hypothesis
it is impossible to decide colored Müller games in
$2^{o(|C|\cdot\log(|C|))}Poly(|V|)$, where $|C|\leq\sqrt{|V|}$.

We mention two algorithms with the best running time bounds for deciding Rabin
and Streett games. Horn’s algorithm for deciding Streett games has the running
time $O(k!|V|^{2k})$. N. Piterman and A. Pnuelli in 2006 provide algorithms
that decide Rabin games $O(|E||V|^{k+1}kk!)$ and Streett games in $O(nkk!)$
(Piterman and Pnueli, 2006).

Finally, the common feature of all these algorithms and their analysis is that
they all take into account the parameters. Hence they appear in describing the
running times. We stress that the running times of these algorithms, in terms
of the parameters $p$, where $p$ is either $|W|$ or $k$ or $|C|$, contain
multiplicative term $p!$ or $p^{p}$. Therefore, when the sizes of the
parameters are large, all the algorithms mentioned above produce the worst
case running times. In practice, these algorithms have limited power as they
can be applied to games with rather small parameters. In this paper, we design
algorithms with exponential running time on the size of the vertex sets, thus
outperforming known algorithms that decide games with large parameters.

###  2.2. Basic concepts

To explain our contributions, we define standard well-established concepts
used throughout our algorithms.

###### Definition 2.1.

A pseudo-arena of $\mathcal{A}$ determined by $X$ is
$\mathcal{A}(X)=(X_{0},X_{1},E_{X})$ where $X_{0}=V_{0}\cap X$,
$X_{1}=V_{1}\cap X$, $E_{X}=E\cap(X\times X)$. If this pseudo-arena is an
arena, then we call it the subarena of $\mathcal{A}$ determined by $X$. By
$\mathcal{G}(X)$ denote the Müller game played on the subarena
$\mathcal{A}(X)$.

Let us consider Player $\sigma$, where $\sigma\in\\{0,1\\}$. The opponent of
Player $\sigma$ is denoted by Player $\bar{\sigma}$. Traps are sub-arenas in
games where one of the players has no choice but stay. Here is a formal
definition:

###### Definition 2.2 ($\sigma$-trap).

A subarena $\mathcal{A}(X)$ is a $\sigma$-trap for Player $\sigma$ if each of
the following two conditions are satisfied: (1) For all $x\in
X_{\bar{\sigma}}$ there is a $y\in X_{\sigma}$ such that $(x,y)\in E$. (2) For
all $x\in X_{\sigma}$ it is the case that $E(x)\subseteq X$.

Thus, if $\mathcal{A}(X)$ is a $\sigma$-trap, then Player $\bar{\sigma}$ can
stay in $\mathcal{A}(X)$ forever if the player wishes to do so.

Let $T$ be a subset of the arena $\mathcal{A}=(V_{0},V_{1},E)$. The attractor
of Player $\sigma$ to the set $T\subseteq V$, denoted
$Attr_{\sigma}(T,\mathcal{A})$, is the set of positions from where Player
$\sigma$ can force the plays into $T$. The attractor
$Attr_{\sigma}(T,\mathcal{A})$ is computed as follows:

$W_{0}=T$, $W_{i+1}=W_{i}\cup\\{u\in V_{\sigma}\mid E(u)\cap
W_{i}\neq\emptyset\\}\cup\\{u\in V_{\bar{\sigma}}\mid E(u)\subseteq W_{i}\\}$,
and then set $Attr_{\sigma}(T,\mathcal{A})=\bigcup_{i\geq 0}W_{i}$.

The set $Attr_{\sigma}(T,\mathcal{A})$ can be computed in $O(|E|)$. We call
$Attr_{\sigma}$ the attractor operator. Note that the set $V\setminus
Attr_{\sigma}(T,\mathcal{A})$, the complement of the $\sigma$-attractor of
$T$, is a $\sigma$-trap for all $T$. This set is the emptyset if and only if
$V=Attr_{\sigma}(T,\mathcal{A})$.

As explained in Section 2.1, all the previously known algorithms take into
account the parameters $p\in\\{|W|,|C|,k\\}$, and their running times contain
the multiplicative terms $p^{p}$ or $p!$. Thus, these algorithms are suited
for games with small parameters, and they are prohibitively slow when the game
parameters are large. Hence, designing exponential time algorithms for large
games are important as they greatly outperform all the known algorithms for
regular games.

In order to address this large vs small games issue we utilize the Lambert
$\boldsymbol{W}$ function $LW$. The function $LW(z)$ is a solution to the
equation $we^{w}=z$. By (Hoorfar and Hassani, 2008), for $z>1$, we have the
following:

$LW(z)\geq\frac{\log z}{1+\log z}(\log z-\log\log z+1)>\log\log z.$

It is easy to see the following sequence of implications that are derived from
comparing $p^{p}$ and $e^{n}$, where $n=|V|$:

$p^{p}>e^{n}\Rightarrow e^{p\ln p}>e^{n}\Rightarrow p\ln p>n\Rightarrow e^{\ln
p}\ln p>n\Rightarrow\ln p>LW(n)\Rightarrow p>e^{LW(n)}.$

Since $LW(n)e^{LW(n)}=n$ we get the equality $e^{LW(n)}=\frac{n}{LW(n)}$. This
implies $p>\frac{n}{LW(n)}$.

###### Definition 2.3.

Let $p\in\\{|C|,|W|,k\\}$ be a game parameter. A regular game $\mathcal{G}$ is
large if $p>\frac{c\cdot n}{LW(c\cdot n)}$.

It can formally be argued that with increasing $n$, the probability of
selecting a large game tends to $1$. For example, let us randomly select a
McNaughton game $\mathcal{G}$ played on arena of size $n$. Each game
$\mathcal{G}$ contains a unique ordered winning condition $\Omega$. Then the
number of total games and the number of small games on the arena of
$\mathcal{G}$ are:

$\sum_{i=0}^{2^{n}}\binom{2^{n}}{i}i!\ =\
\sum_{i=0}^{2^{n}}\frac{2^{n}!}{(2^{n}-i)!}\ \ \ \ \ \ \ \ \ \mbox{and}\ \ \ \
\ \ \ \ \ \ \ \ \
\sum_{i=0}^{2^{\lfloor\frac{n}{LW(n)}\rfloor}}\frac{2^{n}!}{(2^{n}-i)!}<\sum_{i=0}^{2^{\lfloor\frac{n}{\log\log
n}\rfloor}}\frac{2^{n}!}{(2^{n}-i)!},\ \mbox{respectively.}$

When $n\rightarrow\infty$, the ratio of the small games to large games
approaches $0$. Hence, the probability of selecting a large game approaches to
$1$. Therefore, understanding decision algorithms for large games is an
important, and theoretically natural, issue. Also, this paper motivates the
study of small games as for large games we provide efficient solutions.

##  3\. Our contribution

We list our three main contributions:

  * •

We develop two algorithms for deciding Müller games. We start with Müller
games because (1) they can be decided in polynomial time when given
explicitly, (2) they serve as a platform for demonstrating our core concepts
and the data structure. The first algorithm runs in time
$O(3^{|V|}(|V|+|E|))$. The second algorithm runs in time $O(3^{|V|}|V|)$. By
utilizing these two algorithms, we provide the most efficient polynomial time
algorithms to date that decide explicitly given Müller games. To illustrate
this, when Müller games are large, the best known algorithm runs in time
$O(|\Omega|\cdot(|V|+|\Omega|)\cdot|V_{0}|\log|V_{0}|)$ (Liang et al., 2023).
Our first algorithm runs in time $O(3^{|V|}(|V|+|E|))$ and the second in
$O(3^{|V|}|V|)$. These are, obviously, important improvements.

  * •

Our algorithms distinguish themselves from the previously known algorithms in
three ways. First, our algorithms neither reduce the sizes of the arenas nor
alter the winning conditions. This is the feature of the many recursive
algorithms that decide Müller games. Second, our algorithms avoid the
transformation of Müller games into other well-known classes of games, such as
safety games. This is contrary to most reduction techniques employed in Müller
game decision processes. Thus, in terms of these two aspects, our techniques
are novel. Third, our methods are based on well-established notions such as
subarena, traps, and the attractor operator that we already defined in Section
2.2. Our algorithms interplay these notions making them clean and simple, and
hence easy to implement. The central technical concept used in this interplay
is the notion of full win. A player fully wins a subarena $\mathcal{A}(X)$ if
the player wins the Müller game $\mathcal{G}(X)$ from any position in $X$. Our
algorithms collect all the subarenas that Player 0 fully wins, and then, based
on this collection, decide $\mathcal{G}$.

  * •

Finally, our methods are universal in the following sense. We can apply our
methods directly to decide all other regular games. This is an obvious
advantage and distinction of our algorithms from all the other algorithms that
solve regular games. The running times of known algorithms that decide regular
games have parameters in them. Using our methods for deciding Müller games, we
show that McNaughton games and colored Müller games can be decided in time
$O(3^{|V|}\cdot|V|)$. For Rabin (and Streett) games we have the running bound
$O((3^{|V|}+k)\cdot|V|^{2})$. With this, we significantly improve the running
bounds of all the known algorithms when games are large. As an example, we
improve the known bound for coloured Müller games obtained from the
breakthrough quasi-polynomial time algorithm from (Calude et al., 2017).

The table below summarises our results and compares them to the state of the
art.

| Best known running times | Our algorithm (s)
---|---|---
Müller games | $O(|\Omega|\cdot(|V|+|\Omega|)\cdot|V_{0}|\log|V_{0}|)$ | $O(min\\{|\Omega|\cdot(|V|+|\Omega|)\cdot|V_{0}|\log|V_{0}|,\ 3^{|V|}|V|\\})$
McNaughton games | $O(|W||E||W|!)$ | $O(3^{|V|}|V|)$
Colored Müller games | $O(|C|^{5|C|}\cdot|V|^{5})$
Rabin games | $O(|E||V|^{k+1}kk!)$ | $O((3^{|V|}+2^{|V|}k)\cdot|V|)$, $O((3^{|V|}+k)|V|^{2})$
Streett games | $O(|V|kk!)$
KL games | none |  $O((3^{|V|}+2^{|V|}t)\cdot|V|)$, $O(3^{|V|}|V|^{2})$

Other important comment is this. We mentioned the result by C. Calude, S.
Jain, B. Khoussainov, W. Li and F. Stephan stating that under the Exponential
Time Hypothesis coloured Müller games cannot be decided in
$2^{o(|C|\cdot\log(|C|))}Poly(|V|)$, where $|C|\leq\sqrt{|V|}$111In their
paper (Calude et al., 2017), C. Calude, S. Jain, B. Khoussainov, W. Li and F.
Stephan claim a misleading statement that it is impossible to decide coloured
Müller games in time $2^{o(|C|\cdot\log(|C|))}Poly(|V|)$, where $|C|\leq|V|$.
However, their proof actually implies that $|C|\leq\sqrt{|V|}$.. Our algorithm
shows that when $|C|>\frac{\ln 3\cdot n}{LW(\ln 3\cdot n)}$ we can solve
coloured Müller games most efficiently. Indeed, when the game is large, our
algorithm runs in $O(3^{|V|}|V|)$ which is
$2^{o(|C|\cdot\log(|C|))}Poly(|V|)$. Also, by the mentioned result of
Björklund, Sandberg and Vorobyov (Björklund et al., 2003), under the
Exponential Time Hypothesis, our results are almost optimal for coloured
Müller games. We do not know if there is a better exponential time algorithm
that decides coloured Müller games, where $|C|$ belongs to the interval
$(\sqrt{|V|},\ \frac{\ln 3\cdot|V|}{LW(\ln 3\cdot|V|)})$.

##  4\. Deciding Müller Games

For this section let us fix a Müller game $\mathcal{G}$ played on arena
$\mathcal{A}$. Let $Win_{\sigma}(\mathcal{G})$ be the set of all $v$ in
$\mathcal{G}$ such that player $\sigma$ wins $\mathcal{G}$ starting from $v$.
An important notion will be the following:

###### Definition 4.1.

If $Win_{\sigma}(\mathcal{G})=V$, then player $\sigma$ fully wins
$\mathcal{G}$. Otherwise, we say that player $\sigma$ cannot fully win
$\mathcal{G}$.

Note that even if Player $\sigma$ cannot fully win $\mathcal{G}$, there might
still be positions $v$ that the player wins $\mathcal{G}$ starting at $v$. We
would like to collect all the subarenas $X$ such that a given player fully
wins the game played on $\mathcal{G}(X)$. Note that even if Player $\sigma$
fully wins $\mathcal{G}(X)$, this does not imply that $X$ is a
$\bar{\sigma}$-trap. Now we start some analysis of subarenas.

###### Lemma 4.2.

If there exists a $\sigma$-trap $\mathcal{A}(X)$ so that Player $\sigma$
cannot fully win $\mathcal{G}(X)$, then there exists a $\sigma$-trap
$\mathcal{A}(Y)$ so that $Y\subseteq X$ and Player $\bar{\sigma}$ fully wins
$\mathcal{G}(Y)$.

###### Proof.

Let $\mathcal{A}(X)$ be a $\sigma$-trap that Player $\sigma$ cannot fully win.
Let $Y=Win_{\bar{\sigma}}(\mathcal{G}(X))$. Then $Y\neq\emptyset$, Player
$\bar{\sigma}$ fully wins $\mathcal{G}(Y)$ and $\mathcal{A}(Y)$ is a
$\sigma$-trap in both $\mathcal{G}(X)$ and $\mathcal{G}$. ∎

###### Corollary 4.3.

If no $\bar{\sigma}$-trap $\mathcal{A}(X)$ with $X\subsetneq V$ exists that
Player $\sigma$ fully wins, then Player $\bar{\sigma}$ fully wins all these
$\bar{\sigma}$-traps.

###### Proof.

Assume that there is a $\bar{\sigma}$-trap $\mathcal{A}(Y)$ with $Y\subsetneq
V$ such that Player $\bar{\sigma}$ cannot fully win $\mathcal{G}(Y)$. Then by
Lemma 4.2, there exists a $\bar{\sigma}$-trap $\mathcal{A}(Z)$ with
$Z\subseteq Y$ so that Player $\sigma$ fully wins $\mathcal{G}(Z)$. This is a
contradiction. ∎

###### Lemma 4.4.

If $X\notin\Omega$ and there does not exist a 1-trap $\mathcal{A}(X)$ with
$X\subsetneq V$ in $\mathcal{G}$, then Player 1 fully wins $\mathcal{G}$.

###### Proof.

Note that for all $v\in V$ we have $Attr_{1}(\\{v\\},\mathcal{A})=V$.
Otherwise, for some $v\in V$ we will have a 1-trap $\mathcal{A}(X)$ with
$X=V\setminus Attr_{1}(\\{v\\},\mathcal{A})$. Now we construct a winning
strategy for Player 1 as follows. Let $v_{0},v_{1},\ldots,v_{k-1}$ be all
positions in $\mathcal{G}$. Initially set $i=0$. Player 1 forces the token to
$v_{i}$ and once the token arrives at $v_{i}$, set $i=i+1\mod k$. With this
strategy, the token is moved through each position infinitely often. Since
$V\notin\Omega$, Player 1 fully wins $\mathcal{G}$. ∎

Now we characterise all subarenas $X$ that are fully won by the players. Of
course, our characterization will be based on whether or not $X\in\Omega$.

###### Lemma 4.5.

Let $X\in\Omega$ be a subarena in $\mathcal{G}$. Player 0 fully wins
$\mathcal{G}(X)$ if and only if for all 0-traps $\mathcal{A}(Y)$ with
$Y\subsetneq X$ in $\mathcal{G}(X)$, Player 0 fully wins $\mathcal{G}(Y)$.

###### Proof.

Assume that there exists a 0-trap $\mathcal{A}(Y)$ with $Y\subsetneq X$ in
$\mathcal{G}(X)$ so that Player 0 cannot fully win $\mathcal{G}(Y)$. By Lemma
4.2, there exists a 0-trap $\mathcal{A}(Z)$ in $\mathcal{G}(X)$ so that Player
1 fully wins $\mathcal{G}(Z)$. Therefore, since $Z$ is a $0$-trap, Player 1
wins the game $\mathcal{G}$ starting from any position $v\in Z$. Indeed,
Player $1$ keeps the token inside $\mathcal{A}(Z)$, and follows the winning
strategy in $\mathcal{G}(Z)$. Therefore, Player 0 cannot fully win
$\mathcal{G}(X)$.

Assume that for all 0-traps $\mathcal{A}(Y)$ with $Y\subsetneq X$ in
$\mathcal{G}(X)$, Player 0 fully wins $\mathcal{G}(Y)$. We construct the
following winning strategy for Player 0 in $\mathcal{G}(X)$. Let
$X=\\{v_{0},v_{1},\ldots,v_{k-1}\\}$ and $i$ initially be 0.

  * •

If the token is in $Attr_{0}(\\{v_{i}\\},\mathcal{A}(X))$, then Player 0
forces the token to $v_{i}$ and once the token arrives at $v_{i}$, sets
$i=i+1\mod k$. Otherwise,

  * •

since $\mathcal{A}(X\setminus Attr_{0}(\\{v_{i}\\},\mathcal{A}(X)))$ is a
0-trap in $\mathcal{G}(X)$, Player 0 uses a winning strategy in
$\mathcal{G}(X\setminus Attr_{0}(\\{v_{i}\\},\mathcal{A}(X)))$.

Consider any play consistent with the strategy described. If the token finally
stays in $\mathcal{A}(X\setminus Attr_{0}(\\{v_{i}\\},\mathcal{A}(X)))$ for
some $i$, then Player 0 wins the game. Otherwise, the token must be moved
through every vertex in $X$ infinitely often. Since $X\in\Omega$, Player 0
wins. This implies that Player 0 fully wins $\mathcal{G}(X)$. ∎

###### Corollary 4.6.

Let $X\in 2^{V}\setminus\Omega$ be a subarena in $\mathcal{G}$. Player 1 fully
wins $\mathcal{G}(X)$ if and only if for all 1-traps $\mathcal{A}(Y)$ with
$Y\subsetneq X$ in $\mathcal{G}(X)$, Player 1 fully wins $\mathcal{G}(Y)$.

###### Proof.

The proof follows from the symmetry of Müller games, and Lemma 4.5 above. ∎

Lemma 4.5 considers the case when $X\in\Omega$ forms a subarena, and provides
necessary and sufficient conditions for Player 0 to fully win the game
$\mathcal{G}(X)$. The next lemma considers the case when $X$ is a subarena but
$X$ is a winning condition for Player 1, that is, $X\in 2^{V}\setminus\Omega$.
The lemma provides necessary and sufficient conditions for Player 0 to fully
win the game $\mathcal{G}(X)$.

###### Lemma 4.7.

Let $X\in 2^{V}\setminus\Omega$ be a subarena in $\mathcal{G}$. Player 0 fully
wins $\mathcal{G}(X)$ if and only if there exists a 1-trap $\mathcal{A}(Y)$
with $Y\subsetneq X$ in $\mathcal{G}(X)$ such that the following two
conditions are satisfied:

  1. (1)

Player 0 fully wins $\mathcal{G}(Y)$, and

  2. (2)

$Attr_{0}(Y,\mathcal{A}(X))=X$ or Player 0 fully wins $\mathcal{G}(X\setminus
Attr_{0}(Y,\mathcal{A}(X)))$.

###### Proof.

Assume that there exists a 1-trap $\mathcal{A}(Y)$ with $Y\subsetneq X$ in
$\mathcal{G}(X)$ such that Player 0 fully wins $\mathcal{G}(Y)$ and
$Attr_{0}(Y,\mathcal{A}(X))=X$. Now define the following strategy for Player
0. Starting at any position in $X$, first force the play into the set $Y$. As
soon as the token is placed in $Y$, use the winning strategy to fully win
$\mathcal{A}(Y)$. Since $Y$ is a 1-trap, Player 1 fully wins $\mathcal{G}(X)$.

Now consider the next case, where we assume that there exists a 1-trap
$\mathcal{A}(Y)$ with $Y\subsetneq X$ in $\mathcal{G}(X)$ such that Player 0
fully wins both games: $\mathcal{G}(Y)$ and $\mathcal{G}(X\setminus
Attr_{0}(Y,\mathcal{A}(X)))$. Below we construct the following winning
strategy for Player 0 that guarantees that the player fully wins
$\mathcal{G}(X)$.

  * •

If the token is in $\mathcal{A}(Attr_{0}(Y,\mathcal{A}(X)))$, then Player 0
forces the token into $\mathcal{A}(Y)$ and then follows a winning strategy
that fully wins $\mathcal{G}(Y)$.

  * •

Otherwise, Player 0 follows the winning strategy in $\mathcal{G}(X\setminus
Attr_{0}(Y,\mathcal{A}(X)))$.

Consider any play $\rho$ consistent with the strategy. If the token in the
play is placed into $\mathcal{A}(Attr_{0}(Y,\mathcal{A}(X)))$, then Player 0
wins just like in the previous case. Otherwise, the token along this play will
never move into $\mathcal{A}(Attr_{0}(Y,\mathcal{A}(X)))$. Since Player 0
follows a winning strategy in $\mathcal{G}(X\setminus
Attr_{0}(Y,\mathcal{A}(X)))$, the play must be won by Player 0. Therefore,
Player 0 fully wins the game in $\mathcal{G}(X)$. So, this proves one
direction of the lemma.

Now we prove the other direction of the lemma. We assume that Player 0 fully
wins the game $\mathcal{G}(X)$. We need to consider several cases.

Case 1: Assume that there is no 1-trap $\mathcal{A}(Y)$ with $Y\subsetneq X$
in $\mathcal{G}(X)$. By Lemma 4.4, Player 1 fully wins $\mathcal{G}(X)$. This
obviously contradicts with our assumption.

Case 2: Assume that for all 1-traps $\mathcal{A}(Y)$ with $Y\subsetneq X$,
Player 0 cannot fully win $\mathcal{G}(Y)$. Then by Corollary 4.3, Player 1
fully wins all these $\mathcal{G}(Y)$, and by Corollary 4.6, Player 1 fully
wins $\mathcal{G}(X)$.

Case 3: Assume that for all 1-traps $\mathcal{A}(Y)$ with $Y\subsetneq X$ in
$\mathcal{G}(X)$, if Player 0 fully wins $\mathcal{G}(Y)$ then
$Attr_{0}(Y,\mathcal{A}(X))\neq X$ and Player 0 cannot fully win
$\mathcal{G}(X\setminus Attr_{0}(Y,\mathcal{A}(X)))$. Let $\mathcal{A}(Y)$ be
any of such 1-traps. Since $\mathcal{A}(X\setminus
Attr_{0}(Y,\mathcal{A}(X)))$ is a 0-trap in $\mathcal{G}(X)$, by Lemma 4.2,
there exists a 0-trap $\mathcal{A}(Z)$ in $\mathcal{G}(X)$ so that Player 1
fully wins $\mathcal{G}(Z)$. By forcing the token in $\mathcal{A}(Z)$ and
following the winning strategy in $\mathcal{G}(Z)$, Player 1 wins
$\mathcal{G}(X)$ starting from any $v$ in $Z$. Therefore, Player 0 cannot
fully win $\mathcal{G}(X)$. ∎

Let $\mathcal{G}=(\mathcal{A},\Omega)$ be a Müller game where
$V=\\{v_{1},v_{2},\ldots,v_{n}\\}$. We assign a $n$-bit binary number $i$ to
each non-empty pseudo-arena $\mathcal{A}(S_{i})$ in $\mathcal{G}$ so that
$S_{i}=\\{v_{j}\mid\text{the $j$th bit of $i$ is 1}\\}$. We partition all
subgames $\mathcal{G}(S_{i})$ into two sets $P=\\{S_{i}\mid
i\in[1,2^{n}-1]\text{ and Player 0 fully wins }\mathcal{G}(S_{i})\\}$ and
$Q=\\{S_{i}\mid i\in[1,2^{n}-1]\text{ and Player 0 cannot fully win
}\mathcal{G}(S_{i})\\}$ with the following algorithm.

Input: A Müller game $\mathcal{G}=(\mathcal{A},\Omega)$
---
Output: The partitioned sets $P$ and $Q$.
$P\leftarrow\emptyset$, $Q\leftarrow\emptyset$;
for $i=1$ to $2^{n}-1$ do
$S_{i}\leftarrow\\{v_{j}\mid\text{the $j$th bit of $i$ is 1}\\}$;
$is\\_win=$false;
if $\mathcal{A}(S_{i})$ is not an arena then
break;
end
if $S_{i}\in\Omega$ then
$is\\_win\leftarrow\text{true}$
for $S_{j}\subsetneq S_{i}$ do $\longrightarrow$ Lemma 4.5
if $\mathcal{A}(S_{j})$ is a 0-trap in $\mathcal{G}(S_{i})$ and $S_{j}\in Q$
then
$is\\_win\leftarrow$false;
break;
end
end
else
for $S_{j}\subsetneq S_{i}$ do $\longrightarrow$ Lemma 4.7
if $\mathcal{A}(S_{j})$ is a 1-trap in $\mathcal{G}(S_{i})$ and $S_{j}\in P$
then
if $Attr_{0}(S_{j},\mathcal{A}(S_{i}))=S_{i}$ or $S_{i}\setminus
Attr_{0}(S_{j},\mathcal{A}(S_{i}))\in P$ then
$is\\_win\leftarrow$true;
break;
end
end
end
end
if $is\\_win=$true then
$P\leftarrow P\cup\\{S_{i}\\}$;
else
$Q\leftarrow Q\cup\\{S_{i}\\}$;
end
end
return $P$ and $Q$
Figure 1. Algorithm 1 for partitioning subgames of a Müller game

We now explain the algorithm. The algorithm, given a Müller game $\mathcal{G}$
as input, and returns the collections $P$ and $Q$:

  * •

$P=\\{S_{i}\mid i\in[1,2^{n}-1]\text{ and Player 0 fully wins
}\mathcal{G}(S_{i})\\}$, and

  * •

$Q=\\{S_{i}\mid i\in[1,2^{n}-1]\text{ and Player 0 cannot fully win
}\mathcal{G}(S_{i})\\}$.

At each iteration, the algorithm either keeps both $P$ and $Q$ intact or
extends either $P$ or $Q$. According to the algorithm, if $\mathcal{A}(S_{i})$
is not an arena, then $S_{i}$ is disregarded. If $\mathcal{A}(S_{i})$ is an
arena, then by using Lemmas 4.5 and 4.7, we put $\mathcal{A}(S_{i})$ either
into $P$ or into $Q$.

  1. (1)

If $S_{i}\in\Omega$, then:

    1. (a)

If there exists a 0-trap $\mathcal{A}(S_{j})$ in $\mathcal{G}(S_{i})$ so that
$S_{j}\in Q$ then $S_{i}$ is added to $Q$.

    2. (b)

Otherwise, $S_{i}$ is added to $P$.

  2. (2)

Otherwise:

    1. (a)

If there exists a 1-trap $\mathcal{A}(S_{j})$ in $\mathcal{G}(S_{i})$ so that
$Attr_{0}(S_{j},\mathcal{A}(S_{i}))=S_{i}$ or $S_{i}\setminus
Attr_{0}(S_{j},\mathcal{A}(S_{i}))\in P$ then $S_{i}$ is added to $P$.

    2. (b)

Otherwise, $S_{i}$ is added to $Q$.

###### Lemma 4.8.

At the end of Algorithm 1, we have the following two equalities:

  * •

$P=\\{S_{i}\mid i\in[1,2^{n}-1]\text{ and Player 0 fully wins
}\mathcal{G}(S_{i})\\}$, and

  * •

$Q=\\{S_{i}\mid i\in[1,2^{n}-1]\text{ and Player 0 cannot fully win
}\mathcal{G}(S_{i})\\}$.

###### Proof.

If $i=1$ then $\mathcal{A}(S_{1})$ isn’t an arena, and hence $S_{1}$ is
disregarded. For $i=2,3,\ldots,2^{n}-1$, we want to show that at the end of
$i$th iteration, (1) if Player 0 fully wins $\mathcal{G}(S_{i})$ then $S_{i}$
is added to $P$, and (2) if Player 0 cannot fully win $\mathcal{G}(S_{i})$
then $S_{i}$ is added to $Q$. Assume for all $j=1,2,\ldots,i-1$, (1) if Player
0 fully wins $\mathcal{G}(S_{j})$ then $S_{j}$ is added to $P$, and (2) if
Player 0 cannot fully win $\mathcal{G}(S_{j})$ then $S_{j}$ is added to $Q$.
If $\mathcal{A}(S_{i})$ isn’t an arena then $S_{i}$ is disregarded. Otherwise:

  1. (1)

If $S_{i}\in\Omega$, then by Lemma 4.5, Player 0 fully wins
$\mathcal{G}(S_{i})$ if and only if for all 0-traps $\mathcal{A}(S_{j})$ in
$\mathcal{G}(S_{i})$, Player 0 fully wins $\mathcal{G}(S_{j})$. Since for all
these $S_{j}$, $j<i$, we have that if Player 0 fully wins
$\mathcal{G}(S_{j})$, then $S_{j}\in P$, otherwise $S_{j}\in Q$. Therefore,
Player 0 fully wins $\mathcal{G}(S_{i})$ if and only if for all 0-traps
$\mathcal{A}(S_{j})$ in $\mathcal{G}(S_{i})$, $S_{j}\in P$.

  2. (2)

If $S_{i}\notin\Omega$, then by Lemma 4.7, Player 0 fully wins
$\mathcal{G}(S_{i})$ if and only if there exists a 1-trap $\mathcal{A}(S_{j})$
with $S_{j}\subsetneq S_{i}$ in $\mathcal{G}(S_{i})$ so that (1) Player 0
fully wins $\mathcal{G}(S_{j})$ and (2)
$Attr_{0}(S_{j},\mathcal{A}(S_{i}))=S_{i}$ or Player 0 fully wins
$\mathcal{G}(S_{k})$ where $S_{k}=S_{i}\setminus
Attr_{0}(S_{j},\mathcal{A}(S_{i}))$. Since for all these $S_{j}$ and $S_{k}$,
$j<i$ and $k<i$, we have that if Player 0 fully wins $\mathcal{G}(S_{j})$ (or
$\mathcal{G}(S_{k})$), then $S_{j}\in P$ (or $S_{k}\in P$), otherwise
$S_{j}\in Q$ (or $S_{k}\in Q$). Therefore, Player 0 fully wins
$\mathcal{G}(S_{i})$ if and only if there exists a 1-trap $\mathcal{A}(S_{j})$
with $S_{j}\subsetneq S_{i}$ in $\mathcal{G}(S_{i})$ so that (1) $S_{j}\in P$
and (2) $Attr_{0}(S_{j},\mathcal{A}(S_{i}))=S_{i}$ or $S_{i}\setminus
Attr_{0}(S_{j},\mathcal{A}(S_{i}))\in P$.

By hypothesis, the proof is done. ∎

###### Lemma 4.9.

Let $\mathcal{A}(X)$ and $\mathcal{A}(Y)$ be 1-traps. If Player 0 fully wins
$\mathcal{G}(X)$ and $\mathcal{G}(Y)$ then Player 0 fully wins
$\mathcal{G}(X\cup Y)$.

###### Proof.

We construct a winning strategy for Player 0 in $\mathcal{G}(X\cup Y)$ as
follows. If the token is in $Attr_{0}(X,\mathcal{A}(X\cup Y))$, Player 0
forces the token into $X$ and once the token arrives at $X$, Player 0 follows
the winning strategy in $\mathcal{G}(X)$. Otherwise, Player 0 follows the
winning strategy in $\mathcal{G}(Y)$. ∎

###### Lemma 4.10.

If for all $S_{i}\in P$, the arena $\mathcal{A}(S_{i})$ isn’t 1-trap in
$\mathcal{G}$, then $Win_{0}(\mathcal{G})=\emptyset$ and
$Win_{1}(\mathcal{G})=V$. Otherwise, let $\mathcal{A}(S_{max})$ be the maximal
1-trap in $\mathcal{G}$ so that $S_{max}\in P$. Then
$Win_{0}(\mathcal{G})=S_{max}$ and $Win_{1}(\mathcal{G})=V\setminus S_{max}$.

###### Proof.

For the first part of the lemma, assume that
$Win_{0}(\mathcal{G})\neq\emptyset$. By Lemma 4.8, for all arenas
$\mathcal{A}(X)$, $X\in P$ if and only if Player 0 fully wins
$\mathcal{G}(X)$. Now note that $Win_{0}(\mathcal{G})\neq\emptyset$ is 1-trap
such that Player 0 fully wins $\mathcal{G}(Win_{0}(\mathcal{G}))$. This
contradicts with the assumption of the first part. For the second part,
consider all 1-traps $X$ in $P$. Player 0 fully wins the games
$\mathcal{G}(X)$ in each of these 1-traps by definition of $P$. By Lemma 4.9,
Player 0 fully wins the union of these 1-traps. Clearly, this union is
$S_{max}\in P$. Consider $V\setminus S_{max}$. This set is a $0$-trap. Suppose
Player 1 does not win $\mathcal{G}(V\setminus S_{max})$ fully. Then there
exists a $0$-trap $Y$ in game $\mathcal{G}(V\setminus S_{max})$ such that
Player 0 fully wins $\mathcal{G}(Y)$. For every Player 1 position in $y\in Y$
and outgoing edge $(y,x)$ we have either $x\in Y$ or $x\in S_{max}$. This
implies $S_{max}\cup Y$ is 1-trap such that Player 0 fully wins
$\mathcal{G}(S_{max}\cup Y)$. So, $S_{max}\cup Y$ must be in $P$. This
contradicts with the choice of $S_{max}$. ∎

##  5\. Implementation

In this section, we will introduce the data structure and, based on the data
structure, provide two algorithms for deciding Müller games.

###  5.1. Algorithm 1

Let $\mathcal{G}=(\mathcal{A},\Omega)$ be a Müller game where
$V=\\{v_{1},v_{2},\ldots,v_{n}\\}$. We already assigned $n$-bit binary numbers
$i$ to non-empty pseudo-arenas $\mathcal{A}(S_{i})$ in $\mathcal{G}$, where
$S_{i}=\\{v_{j}\mid\text{the $j$th bit of $i$ is 1}\\}$. With this encoding,
we can apply a binary tree to maintain any given collection of vertex sets
$\mathcal{S}=\\{S_{i_{1}},S_{i_{2}},\ldots,S_{i_{k}}\\}$ so that insertions,
deletions and queries to any of these sets takes $O(n)$ time, traversing all
$\mathcal{S}$ takes time $O(2^{n})$, and building the binary tree from
$\mathcal{S}$ takes $O(kn)$. So, from now on, we apply the binary trees to
maintain $\Omega$, $P$ and $Q$. Building the binary tree from $\Omega$ takes
$O(2^{n}n)$ time.

###### Lemma 5.1.

There exists an algorithm that computes $P$ and $Q$ for a Müller game in time
$O(3^{|V|}\cdot(|V|+|E|))$.

###### Proof.

We use the Algorithm 1 from Figure 1. We enumerate all $S_{i}$ so that
$\mathcal{A}(S_{i})$ is an arena. Since checking whether a pseudo-arena is an
arena takes $O(|E|)$ time, this process takes $O(2^{|V|}\cdot|E|)$ time. Then,
we enumerate all $S_{j}$ with $S_{j}\subsetneq S_{i}$ and there are
$\sum_{k=1}^{|V|}\binom{|V|}{k}(2^{k}-1)<3^{|V|}$ such pairs of $S_{i}$ and
$S_{j}$. By applying the binary trees, the enumeration takes $O(3^{|V|})$
time. If $S_{i}\in\Omega$ then verifying whether $\mathcal{A}(S_{j})$ is a
0-trap in $\mathcal{G}(S_{i})$ takes $O(|E|)$ time and checking whether
$S_{j}$ is in $Q$ takes $O(|V|)$ time. If $S_{i}\notin\Omega$ then verifying
whether $\mathcal{A}(S_{j})$ is a 1-trap in $\mathcal{G}(S_{i})$ takes
$O(|E|)$ time, checking whether a vertex set is in $P$ takes $O(|V|)$ time and
computing $Attr_{0}(S_{j},\mathcal{A}(S_{i}))$ takes $O(|E|)$ time. Hence the
operations on $S_{j}$ takes $O(|V|+|E|)$ time. This algorithm runs in
$O(3^{|V|}\cdot(|V|+|E|))$ time. ∎

###### Lemma 5.2.

Given Müller game $\mathcal{G}$ and $P$, there exists an algorithm which
computes $Win_{0}(\mathcal{G})$ and $Win_{1}(\mathcal{G})$ in time
$O(2^{|V|}\cdot(|V|+|E|))$.

###### Proof.

By Lemma 4.10, we enumerate $S_{i}$ from $i=2^{|V|}-1$ to $i=1$. Since
checking whether $S_{i}\in P$ and $\mathcal{A}(S_{i})$ is a 1-trap in
$\mathcal{G}$ takes $O(|V|+|E|)$ time, it takes $O(2^{|V|}\cdot(|V|+|E|))$
time to find the first $S_{i}$ so that $S_{i}\in P$ and $\mathcal{A}(S_{i})$
is a 1-trap in $\mathcal{G}$. If such $S_{i}$ exists, then $Win_{0}=S_{i}$ and
$Win_{1}=V\setminus S_{i}$, otherwise $Win_{0}=\emptyset$ and $Win_{1}=V$.
This algorithm takes $O(2^{|V|}\cdot(|V|+|E|))$ time in total. ∎

By Lemmas 5.1 and 5.2, the following theorem is proved.

###### Theorem 5.3.

There exists an algorithm that, given a Müller game $\mathcal{G}$, decides
$\mathcal{G}$ in time $O(3^{|V|}\cdot(|V|+|E|))$.

###  5.2. Algorithm 2

We want to improve Algorithm 1 by reducing the computation of the attractor
operator. For this, we need to strengthen Lemma 4.7 that will be used in our
next algorithm.

###### Lemma 5.4.

Let $X\in 2^{V}\setminus\Omega$ be a subarena in $\mathcal{G}$. Player 0 fully
wins $\mathcal{G}(X)$ if and only if there exists a 1-trap $\mathcal{A}(Y)$
with $Y\subsetneq X$ in $\mathcal{G}(X)$ such that the following condition is
satisfied:

  1. (1)

Player 0 fully wins $\mathcal{G}(Y)$ and $|Y|=|X|-1$, or

  2. (2)

Player 0 fully wins $\mathcal{G}(Y)$, $Y=Attr_{0}(Y,\mathcal{A}(X))$ and
Player 0 fully wins $\mathcal{G}(X\setminus Y)$.

###### Proof.

First we show that Lemma 4.7 implies this lemma. Let $X\in
2^{V}\setminus\Omega$ be a subarena in $\mathcal{G}$. Assume that exists a
1-trap $\mathcal{A}(Y)$ with $Y\subsetneq X$ in $\mathcal{G}(X)$ such that
Player 0 fully wins $\mathcal{G}(Y)$ and $Attr_{0}(Y,\mathcal{A}(X))=X$. Then
it is easy to see that there exists a 1-trap $\mathcal{A}(Y^{\prime})$ with
$|Y^{\prime}|=|X|-1$ in $\mathcal{G}(X)$ so that Player 0 fully wins
$\mathcal{G}(Y^{\prime})$. If there exists a 1-trap $\mathcal{A}(Y)$ with
$Y\subsetneq X$ in $\mathcal{G}(X)$ such that Player 0 fully wins
$\mathcal{G}(Y)$ and $\mathcal{G}(X\setminus Attr_{0}(Y,\mathcal{A}(X)))$,
then we set $Y^{\prime}=Attr_{0}(Y,\mathcal{A}(X))$. Thus we have that Player
0 fully wins $\mathcal{G}(Y^{\prime})$ and $\mathcal{G}(X\setminus
Y^{\prime})$.

Now we show that conditions (1) and (2) of this lemma imply Lemma 4.7. If
there exists a 1-trap $\mathcal{A}(Y)$ with $Y\subsetneq X$ in
$\mathcal{G}(X)$ such that Player 0 fully wins $\mathcal{G}(Y)$ and
$|Y|=|X|-1$, then $Attr_{0}(Y,\mathcal{A}(X))=X$. If there exists a 1-trap
$\mathcal{A}(Y)$ with $Y\subsetneq X$ in $\mathcal{G}(X)$ such that Player 0
fully wins $\mathcal{G}(Y)$, $Y=Attr_{0}(Y,\mathcal{A}(X))$ and Player 0 fully
wins $\mathcal{G}(X\setminus Y)$, then Player 0 also fully wins
$\mathcal{G}(X\setminus Attr_{0}(Y,\mathcal{A}(X)))$. Therefore, we have that
there exists a 1-trap $\mathcal{A}(Y)$ with $Y\subsetneq X$ in
$\mathcal{G}(X)$ such that the following two conditions are satisfied: (a)
Player 0 fully wins $\mathcal{G}(Y)$, and (b) $Attr_{0}(Y,\mathcal{A}(X))=X$
or Player 0 fully wins $\mathcal{G}(X\setminus Attr_{0}(Y,\mathcal{A}(X)))$.
These two conditions are statements of Lemma 4.7. ∎

Now we apply Lemma 5.4 that changes Algorithm 1 as follows. Run Algorithm 1
but replace the part of Algorithm 1 that corresponds to Lemma 4.7 with the
following code.

for $S_{j}\subsetneq S_{i}$ do $\longrightarrow$ Lemma 5.4
---
if $\mathcal{A}(S_{j})$ is a 1-trap in $\mathcal{G}(S_{i})$ and $S_{j}\in P$
then
if $|S_{j}|=|S_{i}|-1$ then
$is\\_win\leftarrow$true;
break;
end
if $S_{j}=Attr_{0}(S_{j},\mathcal{A}(S_{i}))$ and $S_{i}\setminus S_{j}\in P$
then
$is\\_win\leftarrow$true;
break;
end
end
end
Figure 2. Algorithm 2: the replacing part of Algorithm 1

Now by repeating the proof of Lemma 4.8, we get the following.

###### Lemma 5.5.

At the end of Algorithm 2, we have the following two equalities:

  * •

$P=\\{S_{i}\mid i\in[1,2^{n}-1]\text{ and Player 0 fully wins
}\mathcal{G}(S_{i})\\}$, and

  * •

$Q=\\{S_{i}\mid i\in[1,2^{n}-1]\text{ and Player 0 cannot fully win
}\mathcal{G}(S_{i})\\}$.

In the following lemmas, we apply a binary tree to enumerate the sets
$X\subseteq 2^{V}$. For each vertex $v\in V$, we maintain the number of
outgoing edges from $v$ to vertices in $X$ by $out_{X}(v)$. During the
traversing on the binary tree, there are $O(2^{|V|})$ insertions and deletions
of vertices. Therefore, maintaining $out_{X}(v)$ takes $O(2^{|V|}\cdot|V|)$
time in total. Also let $out(v)=|E(v)|$ for $v\in V$. Then we have the
following: $\mathcal{A}(X)$ is an arena if and only if for all $v\in X$,
$out_{X}(v)\neq 0$. $\mathcal{A}(X)$ is a $\sigma$-trap if and only if for all
$v\in X\cap V_{\sigma}$, $out_{X}(v)=out(v)$ and for all $v\in X\cap
V_{\bar{\sigma}}$, $out_{X}(v)>0$. For a $\bar{\sigma}$-trap $\mathcal{A}(X)$,
$Attr_{\sigma}(X,\mathcal{A})=X$ if and only if for all $v\in
V_{\sigma}\setminus X$, $out_{X}(v)=0$ and for all $v\in
V_{\bar{\sigma}}\setminus X$, $out_{X}(v)<out(v)$. Hence, the following lemma
is proved.

###### Lemma 5.6.

There exists an $O(2^{|V|}\cdot|V|)$-time algorithm for each of the following
enumerations:

  * •

Enumerating all arenas $\mathcal{A}(X)$ in $\mathcal{G}$.

  * •

Enumerating all $\sigma$-traps $\mathcal{A}(X)$ in $\mathcal{G}$.

  * •

Enumerating all $\bar{\sigma}$-traps $\mathcal{A}(X)$ in $\mathcal{G}$ so that
$Attr_{\sigma}(X,\mathcal{A})=X$.

Similar to the proofs of Lemmas 5.1 and 5.2, applying Algorithm 2 and Lemma
5.6, we get the following lemma.

###### Lemma 5.7.

There exists an algorithm that computes $P$ and $Q$ for a Müller game in time
$O(3^{|V|}\cdot|V|)$.

###### Lemma 5.8.

There is an algorithm that, given Müller game $\mathcal{G}$ and $P$, computes
$Win_{0}(\mathcal{G})$ and $Win_{1}(\mathcal{G})$ in $O(2^{|V|}\cdot|V|)$.

By Lemmas 5.7 and 5.8, the following theorem is proved.

###### Theorem 5.9.

There exists an algorithm that solves the Müller game $\mathcal{G}$ in time
$\mathbf{O}(3^{|V|}\cdot|V|)$.

##  6\. Deciding explicitly given Müller games in polynomial time

This is a brief section where we describe our polynomial time algorithm that
decides explicitly given Müller games. Currently, it is the best algorithm in
terms of running times of algorithms that solve Müller games. For instance,
when the input is exponential in the size of the arena, our algorithm
outperforms with running time $O(3^{|V|}\cdot|V|)$ rather than the best known
running time $O(|\Omega|\cdot(|V|+|\Omega|)\cdot|V_{0}|\log|V_{0}|)$ from
(Liang et al., 2023). Here is the algorithm.

On input $\mathcal{G}$ Müller game, run the following two algorithms in
parallel:

  * •

Run any of our algorithms, say Algorithm 1, on $\mathcal{G}$, and

  * •

Run the polynomial time algorithm from (Liang et al., 2023) on $\mathcal{G}$.

Stop, once any of these algorithms outputs $W_{0}$ and $W_{1}$.

##  7\. Applications

In this section we explain how our methods for deciding Müller games can be
extended to all other regular games. To do so, we recast all our results in
Sections 4 and 5 with an eye towards the rest of the regular games.

Lemma 4.2 and Corollary 4.3 and their proofs stay unchanged for all regular
games.

In Lemma 4.4, Corollary 4.6, Lemma 4.7 and Lemma 5.4, the assumption
“$X\not\in\Omega$” is changed to the following:

  * •

For McNaughton games: “$X\cap W\not\in\Omega$”,

  * •

For coloured Müller games: “$c(X)\not\in\Omega$”,

  * •

For KL games: “For $i\in\\{1,\ldots,t\\}$ we have if $u_{i}\in X$ then
$X\not\subseteq S_{i}$”.

  * •

For Rabin games: “For $i\in\\{1,\ldots,k\\}$ we have if $X\cap
U_{i}\neq\emptyset$ then $X\cap V_{i}\neq\emptyset$”.

  * •

For Streett games: “There is an $i\in\\{1,\ldots,k\\}$ such that $X\cap
U_{i}\neq\emptyset$ and $X\cap V_{i}=\emptyset$”.

Then the proofs of all the lemmas and the corollary with these new assumptions
are carried out verbatim for each of these cases. Note that all requirements
put on $X$ are transformations of the winning conditions to Müller game
winning conditions stated for Player 1. Similarly, in Lemma 4.5 the assumption
“$X\in\Omega$” is changed to the following:

  * •

For McNaughton games: “$X\cap W\in\Omega$”,

  * •

For coloured Müller games: “$c(X)\in\Omega$”,

  * •

For KL games: “There is an $i\in\\{1,\ldots,t\\}$ such that $u_{i}\in X$ and
$X\subseteq S_{i}$”.

  * •

For Rabin games: “There is an $i\in\\{1,\ldots,k\\}$ such that $X\cap
U_{i}\neq\emptyset$ and $X\cap V_{i}=\emptyset$”.

  * •

For Streett games: “For $i\in\\{1,\ldots,k\\}$ we have if $X\cap
U_{i}\neq\emptyset$ then $X\cap V_{i}\neq\emptyset$”.

Then the proof of the lemma with these new assumptions is carried out word by
word for each of the cases. Just as above, all the conditions put in $X$ are
essentially transformation of the games to Müller games stated for Player 0.

It is not too hard to see that for McNaughton games and coloured Müller games,
we can easily recast the algorithms presented in Section 5. There will be no
influence on running time complexity. Hence, we get the following complexity-
theoretic result as in Theorem 5.9:

###### Theorem 7.1.

There exist algorithms that decide McNaughton and coloured Müller games
$\mathcal{G}$ in time $\mathbf{O}(3^{|V|}\cdot|V|)$. ∎

Note that the algorithms presented in Section 5 can also be applied to KL,
Rabin and Streett games. However, one needs to be careful with the parameters
involved. They add additional running time costs. Namely, the algorithms
should verify the assumptions, put on the sets $X$, dictated by KL, Rabin and
Streett conditions.

We start with the transformation from KL games to Müller games. Let
$\mathcal{G}=(\mathcal{A},(u_{1},S_{1}),\ldots,(u_{t},S_{t}))$ be a KL game.
Define the following Müller condition set $\Omega^{\prime}$:
$X\in\Omega^{\prime}\ \mbox{if and only if for some pair $(u_{i},S_{i})$ we
have}\ u_{i}\in X\mbox{ and }X\subseteq S_{i}$.

###### Lemma 7.2.

The transformation from KL games to Müller games takes $O(3^{|V|}|V|^{2})$
time.

###### Proof.

We apply a binary tree to maintain $\Omega^{\prime}$. Then enumerate all pairs
$(u_{i},S_{i})$ and add all $X$ with $u_{i}\in X$ and $X\subseteq S_{i}$ into
$\Omega^{\prime}$. Let $\mathcal{S}_{i}$ be the set of all $S_{i,j}\subseteq
V$ so that $(v_{i},S_{i,j})$ is a winning condition. Since
$\mathcal{S}_{i}\subseteq 2^{V}$, for all pairs $(u_{k},S_{k})$ with
$u_{k}=v_{i}$, there are at most $3^{|V|}$ additions of $X$s. Therefore, the
transformation takes $O(3^{|V|}|V|^{2})$ time in total. ∎

As an immediate corollary we get the following complexity-theoretic result for
KL games.

###### Theorem 7.3.

There exists an algorithm that, given a KL game $\mathcal{G}$, decides
$\mathcal{G}$ in time $O(3^{|V|}|V|^{2})$. ∎

Now we transform Rabin games $\mathcal{G}$ to Müller games. Direct translation
to Müller games is costly as each pair $(U_{i},V_{i})$ in the Rabin winning
condition defines the collection of sets $X$ such that $X\cap
U_{i}\neq\emptyset$ and $X\cap V_{i}=\emptyset$. The collection of all these
sets $X$ form the Müller condition set $\Omega$. As the index $k$ is
$O(2^{2|V|})$, the direct transformation is expensive. Our goal is to avoid
this cost through $KL$ games. The following lemma is easy:

###### Lemma 7.4.

Let $X\subseteq V$ and let $(U_{i},V_{i})$ be a winning pair in Rabin game
$\mathcal{G}$. Set $Y_{i}=U_{i}\setminus V_{i}$ and $Z_{i}=V\setminus V_{i}$.
Then $X\cap U_{i}\neq\emptyset$ and $X\cap V_{i}=\emptyset$ if and only if
$X\cap Y_{i}\neq\emptyset$ and $X\subseteq Z_{i}$.

Thus, we can replace the winning condition $(U_{1},V_{1}),\ldots(U_{k},V_{k})$
in a given Rabin game to the equivalent winning condition
$(Y_{1},Z_{1}),\ldots,(Y_{k},Z_{k})$. We still have Rabin winning condition
but we use this new winning condition $(Y_{1},Z_{1}),\ldots,(Y_{k},Z_{k})$ to
build the desired $KL$ game:

###### Lemma 7.5.

The transformation from Rabin games to KL games takes $O(k|V|^{2})$ time.

###### Proof.

Enumerate all pairs $(U_{i},V_{i})$, compute $Y_{i}=U_{i}\setminus V_{i}$,
$Z_{i}=V\setminus V_{i}$ and add all pairs $(u_{j},S_{j})$ with $u_{j}\in
Y_{i}$ and $S_{j}=Z_{i}$ into KL conditions. By applying binary trees, the
transformation takes $O(k|V|^{2})$. This transformation preserves the winning
sets $W_{0}$ and $W_{1}$. ∎

Thus, the transformed KL games can be viewed as a compressed version of Rabin
games.

###### Corollary 7.6.

The transformation from Rabin games to Müller games takes
$O((k+3^{|V|})|V|^{2})$ time.

Note that deciding Rabin games is equivalent to deciding Streett games. Thus,
combining the arguments above, we get the following complexity-theoretic
result:

###### Theorem 7.7.

There exist algorithms that decide Rabin and Streett games $\mathcal{G}$ in
time $\mathbf{O}((k+3^{|V|})\cdot|V|^{2})$. ∎

##  8\. Conclusion

The algorithms presented in this work give rise to numerous questions that
warrant further exploration. For instance, we know that explicitly given
Müller games can be decided in polynomial time. Yet, we do not know if there
are polynomial time algorithms that decide explicitly given McNaughton games
and coloured Müller games. Another intriguing line of research is to establish
connections between our algorithms and the parameters of the games, with the
aim of incorporating these parameters into the running time analysis. Another
natural question is to try to decrease the base $3$ in the running times of
our algorithms, thereby further optimizing the efficiency. This reduction of
computational overhead may uncover new insights and lead to even more
efficient algorithms.

## References

  * (1)
  * Björklund et al. (2003) Henrik Björklund, Sven Sandberg, and Sergei Vorobyov. 2003\.  On fixed-parameter complexity of infinite games. In _The Nordic Workshop on Programming Theory (NWPT 2003)_ , Vol. 34. Citeseer, 29–31.
  * Calude et al. (2017) Cristian S Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. 2017.  Deciding parity games in quasipolynomial time. In _Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing_. 252–263.  STOC 2017 Best Paper Award.
  * Dziembowski et al. (1997) Stefan Dziembowski, Marcin Jurdzinski, and Igor Walukiewicz. 1997\.  How much memory is needed to win infinite games?. In _Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science_. IEEE, 99–110.
  * Fijalkow et al. (2023) Nathanaël Fijalkow, Nathalie Bertrand, Patricia Bouyer-Decitre, Romain Brenguier, Arnaud Carayol, John Fearnley, Hugo Gimbert, Florian Horn, Rasmus Ibsen-Jensen, Nicolas Markey, Benjamin Monmege, Petr Novotný, Mickael Randour, Ocan Sankur, Sylvain Schmitz, Olivier Serre, and Mateusz Skomra. 2023\.  Games on Graphs.  arXiv:2305.10546 [cs.GT]  To be published by Cambridge University Press. Editor: Nathanaël Fijalkow.
  * Grädel et al. (2002) Erich Grädel, Wolfgang Thomas, and Thomas Wilke. 2002\.  Automata, logics, and infinite Games. LNCS, vol. 2500\.
  * Hoorfar and Hassani (2008) Abdolhossein Hoorfar and Mehdi Hassani. 2008.  Inequalities on the Lambert W function and hyperpower function.  _J. Inequal. Pure and Appl. Math_ 9, 2 (2008), 5–9.
  * Horn (2008) Florian Horn. 2008\.  Explicit Muller games are PTIME. In _IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science_. Schloss Dagstuhl-Leibniz-Zentrum für Informatik.
  * Hunter and Dawar (2008) Paul Hunter and Anuj Dawar. 2008.  Complexity bounds for muller games.  _Theoretical Computer Science (TCS)_ (2008).
  * Liang et al. (2023) Zihui Liang, Bakh Khoussainov, Toru Takisaka, and Mingyu Xiao. 2023.  Connectivity in the Presence of an Opponent. In _31st Annual European Symposium on Algorithms (ESA 2023)_ _(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 274)_ , Inge Li Gørtz, Martin Farach-Colton, Simon J. Puglisi, and Grzegorz Herman (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 79:1–79:14.  https://doi.org/10.4230/LIPIcs.ESA.2023.79
  * McNaughton (1993) Robert McNaughton. 1993\.  Infinite games played on finite graphs.  _Annals of Pure and Applied Logic_ 65, 2 (1993), 149–184.
  * Neider et al. (2014) Daniel Neider, Roman Rabinovich, and Martin Zimmermann. 2014\.  Down the Borel hierarchy: Solving Muller games via safety games.  _Theoretical Computer Science_ 560 (2014), 219–234.
  * Nerode et al. (1996) Anil Nerode, Jeffrey B Remmel, and Alexander Yakhnis. 1996\.  McNaughton games and extracting strategies for concurrent programs.  _Annals of Pure and Applied Logic_ 78, 1-3 (1996), 203–242.
  * Piterman and Pnueli (2006) Nir Piterman and Amir Pnueli. 2006.  Faster solutions of Rabin and Streett games. In _21st Annual IEEE Symposium on Logic in Computer Science (LICS’06)_. IEEE, 275–284.
  * Zielonka (1998) Wieslaw Zielonka. 1998\.  Infinite games on finitely coloured graphs with applications to automata on infinite trees.  _Theoretical Computer Science_ 200, 1-2 (1998), 135–183.