# Deciding the topological complexity of Büchi languages *

Michal Skrzypczak, Igor Walukiewicz

► To cite this version:

Michal Skrzypczak, Igor Walukiewicz. Deciding the topological complexity of Büchi languages *. ICALP, Jul 2016, Rome, Italy. pp.99:1–99:13, 10.4230/LIPIcs.ICALP.2016.99 . hal-01394829

HAL Id: hal-01394829

https://hal.science/hal-01394829v1

Submitted on 7 Dec 2019

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Deciding the topological complexity of Büchi languages*

Michał Skrzypczak¹ and Igor Walukiewicz²

1. Institute of Informatics,
University of Warsaw, Warsaw, Poland
mskrzypczak@mimuw.edu.pl

2. LABRI, Bordeaux, France
igw@labri.fr

## Abstract

We study the topological complexity of languages of Büchi automata on infinite binary trees. We show that such a language is either Borel and WMSO-definable, or $\Sigma_1^1$-complete and not WMSO-definable; moreover it can be algorithmically decided which of the two cases holds. The proof relies on a direct reduction to deciding the winner in a finite game with a regular winning condition.

**1998 ACM Subject Classification** F.1.1 Models of Computation

**Keywords and phrases** tree automata, non-determinism, Borel sets, topological complexity, decidability

**Digital Object Identifier** 10.4230/LIPIcs.xxx.yyy.p

## 1 Introduction

The class of regular languages of infinite trees is one of the most important classes of properties of infinite computations. Similarly to the arithmetic hierarchy, the class is structured into the so called Mostowski-Rabin index hierarchy. This hierarchy reflects the complexity of a language in terms of an alternation of fix-points needed to express it, or equivalently, in terms of the minimal complexity of the acceptance condition of an automaton accepting the language. While we know for about two decades that the hierarchy is infinite [5], we are still very far from understanding it. One important objective in this area is to effectively characterise every level of the hierarchy: for a given regular language of infinite trees calculate its level in the hierarchy.

The difficulty in understanding the Mostowski-Rabin index hierarchy of tree languages is linked to the lack of deterministic acceptors for such languages. Thus, on a smaller scale, we face here the same problem as in the complexity theory, namely the problem of understanding the structure of non-deterministic computations. When restricted to deterministic acceptors, the Mostowski-Rabin hierarchy is by now well-understood. For every level we know a pattern such that the pattern appears in a deterministic tree automaton if and only if the language recognised by this automaton is hard for this level [21, 18, 19]. The pattern method has been extended to the so called game automata [12], but there is no hope to use it for non-deterministic automata.

<figure><img src="image_2.png" /></figure>

<footnote>* The first author has been supported by Poland's National Science Center grant (decision DEC-2012/07/D/ST6/02443).</footnote>
Apart from decidability questions, a promising way to understand the Mostowski–Rabin hierarchy is to relate it to the topological hierarchy. (For an introduction to the classes of topological complexity see for instance [15].) Topological properties of sets defined by automata are discussed in [24]. It is well-known that all regular languages of infinite trees are contained in the $\Delta_2^1$ level of the projective hierarchy. The languages of Büchi automata, or equivalently those definable in existential MSO logic, are contained in the $\Sigma_1^1$ level. The languages of weak-alternating automata, or equivalently definable in weak MSO (WMSO), are Borel; moreover for every finite level of the Borel hierarchy there is a complete weakly definable language [23]. In [23], Skurczyński asks if every regular language that is Borel is necessarily weakly definable. In this paper we answer this question for languages recognised by Büchi automata, as expressed by the main theorem.

**► Theorem 1.** If $\mathcal{B}$ is a non-deterministic Büchi tree automaton then one of the following possibilities holds and it is possible to effectively decide which one it is:

1. $L(\mathcal{B})$ is Borel and WMSO-definable,

2. $L(\mathcal{B})$ is $\Sigma_1^1$-complete and not WMSO-definable.

The theorem is proved through a game construction. Given a Büchi automaton $\mathcal{B}$ we construct a finite game $\mathcal{F}(\infty)$ such that if $\exists$ wins in this game then the language of $\mathcal{B}$ is $\Sigma_1^1$-complete; but if $\forall$ wins then the language of $\mathcal{B}$ can be accepted by a weak alternating automaton constructed from $\mathcal{B}$. A similar technique of relying on the finite memory determinacy of regular games was used in [1].

*Related work.* Colcombet, Kuperberg, Löding, and Vanden Boom [16, 8] have proved the algorithmic part of the above theorem; using some decidability result in the theory of cost functions and a reduction of Colcombet and Löding [9] they have shown how to decide if the language of a Büchi automaton is weakly definable. The topological counterpart of Theorem 1 seems not to follow from their construction. Our proof relies only on standard facts from automata theory, and may be simpler, at least for those who are not familiar with the theory of cost functions.

Finding effective characterisations of various classes of infinite tree languages is an important topic of language theory. As we noted above, for languages of deterministic tree automata the situation is quite well-understood; but for the case of all regular tree languages for some time it was only known how to decide if a given regular language can be accepted by an automaton with a trivial acceptance condition [17, 25]. The theory of cost functions allows to decide if a given language can be accepted by a non-deterministic co-Büchi automaton [8]. Bojańczyk and Idziaszek [2] have recently shown decidability of definability in a temporal logic EF. Bojańczyk and Place [4] show how to decide if a given language is a Boolean combination of open sets.

The study of topological properties of regular languages of trees has seen important advances too [10, 13, 6, 18, 19, 3, 11]. Over a decade ago an interesting gap property has been observed [20] for languages of deterministic tree automata: a language is either $\Pi_1^1$-complete, or contained in the $\Pi_3^0$ level of the Borel hierarchy. A similar gap property has been recently shown for languages of thin trees [14]: a regular language of thin trees, treated as a subset of all trees, is either definable in weak MSO logic or $\Pi_1^1$-complete. Our theorem shows a gap property for languages of non-deterministic Büchi automata.

## 2 Preliminaries and an outline of the construction

We write $\omega$ for the natural numbers, and $\bar{\omega}$ for the extension of $\omega$ with a greatest element $\infty$. So $n < \infty$ for all $n \in \omega$, and $\infty - 1 = \infty$. We assume standard definitions of non-
deterministic and alternating automata on infinite binary trees. All trees we consider are binary, the two directions are L and R. The root of a tree is ϵ. By $\leq$ we denote the prefix order on the nodes of a tree. In this paper we will use perfect information two player games of infinite duration. The players are denoted $∃$ (Eve) and $∀$ (Adam).

A non-deterministic Büchi automaton is a tuple $B = (Q, A, q_I \in Q, \delta \subseteq Q \times A \times Q \times Q, F \subseteq Q)$. We will use the standard notion of a run $\rho$ over a tree $t$. A run of $B$ is accepting if on every branch some state from $F$ appears infinitely often. A weak alternating automaton is very similar but for a total quasi-order on states, and the transition relation that now sends a non-empty set of states in every direction $\delta \subseteq Q \times A \times P^+(Q) \times P^+(Q)$ (by $P^+(X)$ we denote the set of non-empty subsets of $X$). The transition relation should respect the order on the states in a sense that if $(q, a, S_L, S_R) \in \delta$ then all the states in $S_L \cup S_R$ should not be bigger than $q$, and if $q \in F$ is accepting then all not accepting states in $S_L \cup S_R$ should be strictly smaller than $q$ in this order. Every weak alternating automaton $\mathcal{A}$ induces a game on every tree $t$: the positions of this game are $(u, q)$ with $u \in \{L, R\}^*$ and $q \in Q$; the initial position is $(\epsilon, q_I)$; from a position $(u, q)$ first $∃$ chooses a transition $(q, t(u), S_L, S_R)$, then $∀$ chooses a direction $d$ and a state $q' \in S_d$, the successive position is $(ud, q')$. A play is won by $∃$ if it contains infinitely many accepting states. Without loss of generality we assume that all the considered automata are complete: for every state $q \in Q$ and every letter $a \in A$ there is at least one transition from $q$ over $a$. For an automaton $\mathcal{A}$, by $L(\mathcal{A})$ we denote the set of trees accepted by $\mathcal{A}$.

Our proof of Theorem 1 will use two games, or rather game families constructed from $\mathcal{B}$. The first game, $G(t)$, will be played on a tree $t$. The game will encode in a compact way not only the acceptance of $t$ by $\mathcal{B}$, but also possible approximations of $\mathcal{B}$ by weak automata. It is motivated by the technical core of the construction in [22]. More precisely, for every $K \in \bar{\omega}$ we will have a variant $G(t, K)$ of the game. Each game defines a language of trees

$$L(\mathcal{G}, K) = \{t \mid \exists \text{ wins } \mathcal{G}(t, K)\}. \qquad (1)$$

The game $G(t, \infty)$ will encode the acceptance of $t$ by $\mathcal{B}$, i.e., $L(\mathcal{G}, \infty) = L(\mathcal{B})$. For every $K \in \omega$, the game $G(t, K)$ will encode the acceptance of $t$ by some specific weak alternating automaton obtained from $\mathcal{B}$; in particular $L(\mathcal{G}, K)$ will be wmso-definable. The parameter $K$ will control the quality of the approximation of $\mathcal{B}$, in a sense that

$$L(\mathcal{G}, 0) \supseteq L(\mathcal{G}, 1) \supseteq \dots \supseteq L(\mathcal{B})$$

We will show that $L(\mathcal{B})$ is wmso-definable if and only if $L(\mathcal{B}) = L(\mathcal{G}, K)$ for some finite bound $K \in \omega$. Moreover, we will show that a candidate $K_0$ for this bound can be computed from $\mathcal{B}$. These results will be obtained from the analysis of another game that we call $\mathcal{F}$.

The game $\mathcal{F}$, and its variants $\mathcal{F}(K)$ for all $K \in \bar{\omega}$, will be central for our arguments. For every $K \in \bar{\omega}$, the game $\mathcal{F}(K)$ will be finite in a sense that there will be a finite number of positions reachable from the initial position. The game $\mathcal{F}(K)$ will in some sense simulate $G(t, K)$ for an unknown $t$. We will show that when $K \in \omega$ is too small for $\mathcal{B}$, i.e. when $L(\mathcal{G}, K) \supseteq L(\mathcal{B})$, then $∃$ has a winning strategy in $\mathcal{F}(K)$. Next, we examine $\mathcal{F}(\infty)$ and show that the winner in this game determines if $L(\mathcal{B})$ is wmso-definable. If $∃$ does not win in $\mathcal{F}(\infty)$ then she does not win in $\mathcal{F}(K_0)$ for some $K_0$ computable from $\mathcal{B}$ (Proposition 10). Thus $L(\mathcal{B}) = L(\mathcal{G}, K_0)$ is wmso-definable. The most difficult part of the proof is to show that if $∃$ wins in $\mathcal{F}(\infty)$ then $L(\mathcal{B})$ is $\Sigma_1$-complete and thus not wmso-definable (Proposition 11).

The way in which the game $\mathcal{F}$ is obtained from $\mathcal{G}$ is motivated by the concept of history determinism and in particular by the combinatorial structure of domination games, see [7].
### 3 The game $\mathcal{G}(t)$

Let us start with the game $\mathcal{G}(t)$. The positions of $\mathcal{G}(t)$ are of the form $(q, u, K, z)$ where $q \in Q^B$ is a state, $u \in \{\text{L}, \text{R}\}^*$ is a node of $t$, $K \in \bar{\omega}$ is a counter value, and $z$ is one of the three special symbols: *choice*, *safe*, or *reach*. The $z$ component determines the possible choices from a position $(q, u, K, z)$:

* $z = \text{choice}$: In this case $\forall$ chooses $z' \in \{\text{safe}, \text{reach}\}$. If he chooses $z' = \text{safe}$ then $K' = K$, if he chooses $z' = \text{reach}$ then $K' = K - 1$; in particular if $K = 0$ then $\forall$ has to choose $z' = \text{safe}$. The game proceeds to the position $(q, u, K', z')$.

* $z = \text{safe}$: First $\exists$ proposes a transition of $\mathcal{B}$ of the form $(q, t(u), q_\text{L}, q_\text{R})$ and then $\forall$ chooses a direction $d \in \{\text{L}, \text{R}\}$. The game proceeds to the position $(q_d, ud, K, \text{choice})$.

* $z = \text{reach}$: First $\exists$ proposes a transition of $\mathcal{B}$ of the form $(q, t(u), q_\text{L}, q_\text{R})$ and then $\forall$ chooses a direction $d \in \{\text{L}, \text{R}\}$. If $q_d$ is an accepting state then the game proceeds to the position $(q_d, ud, K, \text{choice})$, otherwise it proceeds to the position $(q_d, ud, K, \text{reach})$.

Every play of $\mathcal{G}(t)$ is infinite. Such a play is won by $\forall$ if $z = \text{reach}$ from some point on. In the opposite case (i.e. if $z = \text{choice}$ infinitely many times) $\exists$ wins.

As we can see from the definition, the game proceeds in phases. It is $\forall$ who chooses if the game should be in a *safe* phase or in a *reach* phase. In the *safe* phase players just construct a path from a run of $\mathcal{B}$ ignoring the acceptance condition. In the *reach* phase $\exists$ needs to provide a finite part of a run until the next accepting states. The counter $K$ gives a bound on the number of *reach* phases: each time $\forall$ chooses *reach*, $K$ is decreased. Notice that if $K$ is $\infty$ then it stays $\infty$ during the whole play, so there can be infinitely many *reach* phases.

For $K \in \bar{\omega}$ we denote by $\mathcal{G}(t, K)$ the game $\mathcal{G}(t)$ with the initial position $(q_1^B, \epsilon, K, \text{choice})$.

**Example 2.** For our running example we consider trees over the alphabet $\{a, b\}$ and a Büchi automaton $\mathcal{B}$ accepting the trees with a branch having infinitely many occurrences of $a$. This automaton has three states $q_a, q_b, \top$, with both $q_a$, and $\top$ accepting. For a state $q_x$ the transition relation $\delta^B$ on a letter $y$ contains the transitions $(q_x, y, q_y, \top)$ and $(q_x, y, \top, q_y)$; for $x, y \in \{a, b\}$. From $\top$ the automaton stays in $\top$ on every letter and in every direction.

Using the notation from (1) we can see that for $K = 0$ the language $L(\mathcal{G}, K)$ is simply the language of all trees. For $K > 0$, it is the language of trees having a path such that every node on this path has a descendant whose label is $a$ and the subtree rooted in this descendant is in $L(\mathcal{G}, K - 1)$.

The next three lemmas give connections between the game $\mathcal{G}(t)$ and the automaton $\mathcal{B}$. They refer to the languages $L(\mathcal{G}, K)$ of the game as defined in (1).

**Lemma 3.** $L(\mathcal{B}) = L(\mathcal{G}, \infty)$.

*Proof.* First assume that $t \in L(\mathcal{B})$ and let $\rho^B$ be an accepting run of $\mathcal{B}$ on $t$. Then clearly $\exists$ can win the game $\mathcal{G}(t, \infty)$ by just playing $\rho^B$. When $\forall$ chooses $z = \text{reach}$, ultimately an accepting state of $\mathcal{B}$ will be visited and $z$ will be set to *choice*. Therefore, every play will be won by $\exists$.

Now assume that $\exists$ wins $\mathcal{G}(t, \infty)$. We construct a run of $\mathcal{B}$ on $t$ by looking at plays when $\forall$ always chooses to set $z$ to *reach* whenever possible. The directions chosen by $\forall$ are used to generate $\rho^B$. Clearly, the run $\rho^B$ obtained this way is accepting. ◀

The next lemma follows directly from the monotonicity — the smaller the value $K$ is, the less choices are available for $\forall$.

**Lemma 4.** If $\exists$ wins $\mathcal{G}(t)$ from a position $(q, u, K, z)$ and $K' \le K \in \bar{\omega}$ then $\exists$ wins $\mathcal{G}(t)$ from the position $(q, u, K', z)$. In other words $L(\mathcal{G}, K') \supseteq L(\mathcal{G}, K) \supseteq L(\mathcal{G}, \infty)$.
The last of the three lemmas makes a connection with WMSO.

**► Lemma 5.** For every $K \in \omega$ the set of trees $L(\mathcal{G}, K)$ can be recognised by a weak alternating automaton (or equivalently, it is WMSO-definable).

**Proof.** Intuitively, the game $\mathcal{G}(t, K)$ encodes the game induced by a weak alternating automaton $\mathcal{W}$ on a tree $t$. The value $K$ corresponds to the weak index of the automaton.

More formally, the states of the automaton $\mathcal{W}$ are $Q \times \{0, 1, \dots, K\} \times \{\text{choice}, \text{reach}\}$. The initial state is $(q_I, K, \text{choice})$ and the order is

$$Q \times \{0\} \times \{\text{choice}\} \prec Q \times \{0\} \times \{\text{reach}\} \prec \dots \prec Q \times \{K\} \times \{\text{choice}\} \prec Q \times \{K\} \times \{\text{reach}\}.$$

The accepting states are of the form $Q \times \{K'\} \times \{\text{choice}\}$. The transition relation for a state $(q, K', z)$ over a letter $a$ contains, for every pair of transitions $(q, a, q_L, q_R)$, $(q, a, q'_L, q'_R)$ of $\mathcal{B}$, the transition $((q, K', z), a, S_L, S_R)$, with $S_d$ for $d = \text{L, R}$ defined as follows:

- if $z = \text{choice}$ and $K' = 0$ then $S_d = \{(q_d, K', \text{choice})\}$,

- if $z = \text{choice}$, $K' > 0$, and $q_d \notin F$ then $S_d = \{(q_d, K', \text{choice}), (q'_d, K' - 1, \text{reach})\}$,

- if $z = \text{choice}$, $K' > 0$ and $q_d \in F$ then $S_d = \{(q_d, K', \text{choice}), (q'_d, K' - 1, \text{choice})\}$,

- if $z = \text{reach}$ and $q_d \notin F$ then $S_d = \{(q_d, K', \text{reach})\}$,

- if $z = \text{reach}$ and $q_d \in F$ then $S_d = \{(q_d, K', \text{choice})\}$.

For a tree $t$ the game induced by the automaton $\mathcal{W}$ is equivalent to the game $\mathcal{G}(t, K)$. Therefore, $L(\mathcal{W}) = L(\mathcal{G}, K)$ can be recognised by a weak alternating automaton. ◀

# 4 The game $\mathcal{F}$

We proceed to a definition of the game $\mathcal{F}$, and its variants $\mathcal{F}(K)$, for $K \in \bar{\omega}$. For all $K \in \bar{\omega}$, the game $\mathcal{F}(K)$ will simulate $\mathcal{G}(t, K)$ with an unknown $t$ generated on-the-fly.

Let us fix a non-deterministic parity tree automaton $\mathcal{A}$ recognising the complement of $L(\mathcal{B})$ ($\mathcal{A}$ may not be equivalent to a Büchi automaton). We will construct $\mathcal{F}$ from $\mathcal{A}$ and $\mathcal{B}$. Intuitively, in $\mathcal{F}$ we ask the players to proceed as follows:

- $\exists$ should successively construct a tree $t$ and a run $\rho^A$ of $\mathcal{A}$ on $t$;

- at the same time $\forall$ should select directions in this tree constructing an infinite branch $\alpha$ of $t$, aiming to show that the run $\rho^A$ proposed by $\exists$ is not accepting;

- moreover $\exists$ would aim at showing that the tree $t$ she constructs is difficult in a sense that she can win $\mathcal{G}(t, K)$ for all finite $K$. $\forall$ will aim to refute this claim, by showing that she can win with some finite $K$. It is crucial for our argument that $\forall$ can do this in a history-deterministic way in the sense of [7].

## 4.1 Positions and multi-transitions

The positions of $\mathcal{F}$ are of the form $(S, p, \kappa, r)$ where:

- $S \in \mathbb{P}(Q^B \times \{\text{safe}, \text{reach}\})$ is a set of active states,

- $p \in Q^A$ is a state of the automaton $\mathcal{A}$,

- $\kappa: S \to \bar{\omega}$ assigns to the active states their counter values,

- $r \in \{0, 1, 2\}$ is a sub-round number.

Using the first and the third component $\exists$ will try to prove that she wins in all the games $\mathcal{G}(t, K)$. In the second component she will construct a run of $\mathcal{A}$. The fourth component makes the definition of the game more modular.

Similarly as before, for $K \in \bar{\omega}$ by $\mathcal{F}(K)$ we denote the game $\mathcal{F}$ with the initial position $((q_I^B, \text{safe}), q_I^A, \kappa, 0)$ where $\kappa(q_I^B, \text{safe}) = K$.
<figure><img src="image_3.png" /><figcaption>■ **Figure 1** An example multi-transition $\mu$. The dots correspond to the active states and the state of $\mathcal{A}$. The convention is that all the active states from the *safe* phase are drawn on the left, all the active states from the *reach* phase are drawn in the middle, then comes the state of $\mathcal{A}$, and finally the counter values $\kappa$ and the sub-round number $r$ are drawn on the right. For the purpose of layout, we additionally draw an edge between the states $p$ and $p'$ of $\mathcal{A}$ (this edge does not belong to $e$). The blue dotted line separates the *safe* phase from the *reach* phase. Boldfaced edges are boldfaced. Every active state in $S'$ has one incoming boldfaced edge as required by (2).</figcaption></figure>

We say that an active state $(q, z)$ is *in the safe phase* if $z = \text{safe}$; and *in the reach phase* if $z = \text{reach}$. A pair $(s, s')$ *changes phases* if $s$ and $s'$ are in different phases. So $(s, s')$ can *change phases from safe to reach*, or *change phases from reach to safe*.

The edges of $\mathcal{F}$ will have an additional structure (i.e. an edge will be more than just a pair of positions of the game). This richer structure will be used to define the winning condition of $\mathcal{F}$ that will refer to a sequence of edges. From our definition it will be easy to see how to transform such a game into a standard two player game. To underline that edges have additional structure we refer to them as *multi-transitions*.

A *multi-transition* $\mu$ from a position $(S, p, \kappa, r)$ to a position $(S', p', \kappa', r')$ contains:

- the pre-state $(S, p, \kappa, r)$,

- the post-state $(S', p', \kappa', r')$ with $r' = r + 1 \bmod 3$,

- a set $e \subseteq S \times S'$ of edges from the active states in $S$ to the active states in $S'$,

- a set $\bar{e} \subseteq e$ of boldfaced edges, with exactly one boldfaced edge leading to every $s' \in S'$:

$$ \forall_{s' \in S'} |\{s : (s, s') \in \bar{e}\}| = 1 \qquad (2) $$

We additionally require the following condition on $\kappa$, called *boldface-decreasing*. Assume that $(s, s') \in \bar{e}$. If $(s, s')$ changes phases from *safe* to *reach* then$^1$ $\kappa'(s') = \max(\kappa(s)-1, 0)$. Otherwise $\kappa'(s') = \kappa(s)$.

An example multi-transition is depicted in Figure 1. The role of $e$ is to trace the origins of each active state in a similar way as for determinisation of Büchi automata. With the boldfaced edges $\forall$ will indicate which of the possible origins of an active state he finds the most promising for him. The *boldface-decreasing* condition says that on boldfaced traces the counter should behave in the same way as in a game $G(t, K)$ for the tree $t$ being constructed. The exact rules how the multi-transitions are selected by the players are given in Section 4.2.

Notice that for a fixed $K \in \bar{\omega}$ the game $\mathcal{F}(K)$ has only finitely many reachable positions and finitely many multi-transitions — if $K = \infty$ then all the counter values $\kappa$ are equal $\infty$, otherwise the counter values in the reachable positions are at most $K$.

## 4.2 Rules of the game $\mathcal{F}$

In this section we describe the rules of the game $\mathcal{F}$. From a position $(S, p, \kappa, r)$ the players interact constructing a new position $(S', p', \kappa', r')$ and a multi-transition between the two

<footnote>$^1$ By the rules of the game, we shall never have $\kappa(s) < 1$ in this case.</footnote>
positions. For this they select a set of edges $e \subseteq S \times (Q^B \times \{safe, reach\})$ and a state $p' \in Q^A$ according to the rules given below. Then $\forall$ chooses an arbitrary multi-transition $\mu$ that respects $(S, p, \kappa, r)$, $e$, and $p'$ in the following sense:

- the pre-state of $\mu$ is $(S, p, \kappa, r)$,

- the post-state of $\mu$ is $(S', p', \kappa', r')$; where $S' = \{s' : (s, s') \in e\}$ consists of the targets of the edges $e$, $\kappa'$ is determined by the boldface-decreasing condition, and $r' = r + 1$ mod 3,

- the edges of $\mu$ are $e$,

- the boldfaced edges $\bar{e}$ of $\mu$ can be chosen arbitrarily by $\forall$ subject to condition (2).

Observe that a multi-transition $\mu$ that respects $(S, p, \kappa, r)$, $e$, and $p'$ is unique but for the choice of the boldfaced edges $\bar{e}$.

Assume that the current position in $\mathcal{F}$ is $(S, p, \kappa, r)$ and consider the following cases depending on the number of the sub-round $r$. In all the cases the players construct a multi-transition $\mu$ that leads to a post-state $(S', p', \kappa', r')$:

(R0) $r = 0$: There are two cases. If the reach phase is not empty i.e. $S \cap (Q^B \times \{reach\}) \neq \emptyset$, then $e$ contains all the pairs $(s, s)$ for $s \in S$. The second case is when there are no states in the reach phase. We call this situation a flush. In that case $\forall$ can choose<fnref n="2" /> any set $C \subseteq Q^B$ of states $q$ such that

$$ (q, safe) \in S \quad \text{and} \quad \kappa(q, safe) > 0. \qquad (3) $$

The chosen active states get copied to the reach phase thanks to the edge relation defined as: $e = \{(s, s) | s \in S\} \cup \{((q, safe), (q, reach)) | q \in C\}$. In both cases the state $p' = p$ of $\mathcal{A}$ is not changed and $\forall$ chooses $\mu$ that respects $(S, p, \kappa, r)$, $e$, and $p'$.

(R1) $r = 1$: $\exists$ declares: (i) a letter $a \in A$; (ii) a transition $\delta_s = (q, a, q_L^s, q_R^s)$ of $\mathcal{B}$, for every $s = (q, z) \in S$; (iii) a transition $\delta = (p, a, p'_L, p'_R)$ of $\mathcal{A}$. Then $\forall$ responds by selecting a direction $d \in \{L, R\}$. We put $p' = p'_d$, and $e$ contains all the pairs of the form $((q, z), (q'_d, z))$ for $s = (q, z) \in S$. $\forall$ chooses $\mu$ that respects $(S, p, \kappa, r)$, $e$, and $p'$.

(R2) $r = 2$: Deterministically, every active state $(q, reach)$ in the reach phase with $q$ accepting (i.e. $q \in F$) is moved to the safe phase. Formally, for each $(q, z) \in S$, the relation $e$ contains pairs $((q, z), (q, z'))$ such that either: (i) $z = z' = safe$; or (ii) $z = z' = reach$ and $q \notin F$; or (iii) $z = reach, z' = safe$, and $q \in F$. The state $p' = p$ of $\mathcal{A}$ is not changed. $\forall$ chooses $\mu$ that respects $(S, p, \kappa, r)$, $e$, and $p'$.

An example round of $\mathcal{F}$ is presented in Figure 2.

If $(s, s') \in e$ we say that $s'$ is a $\mu$-successor of $s$. By the definition of the sub-rounds of the game, we obtain the following fact.

**Fact 6.** Every active state has between one and two $\mu$-successors. The only case when an active state $(q, z)$ can have two $\mu$-successors is when $r = 0$, $z = safe$, and we have a flush.

## 4.3 The winning condition of $\mathcal{F}$

Now we will define the winning condition for $\exists$ in $\mathcal{F}$. It will depend on the sequence of multi-transitions $\pi = \mu_0\mu_1...$ that were played in $\mathcal{F}$. We will refer to the pre-state of $\mu_n$ as $(S_n, p_n, \kappa_n, r_n)$. Analogously, we will use $(S'_n, p'_n, \kappa'_n, r'_n)$ for the post-state, $e_n$ for the

<footnote n="2">² Even if $\forall$ declares $C = \emptyset$, the fact that the reach phase was empty implies that we have a flush.</footnote>
<figure><img src="image_4.png" /><figcaption>■ **Figure 2** A round of the game $\mathcal{F}$. A round consists of three consecutive sub-rounds with $r = 0, 1, 2$. At the sub-round (R0) we have a *flush* — the *reach* phase was empty and $\forall$ decided to copy three out of the four active states from the *safe* phase to the *reach* phase. In the sub-round (R1) $\exists$ has played a letter $a$ and a number of transitions; and $\forall$ has chosen the direction $d = \mathbf{l}$. The $\Lambda$-shaped structures correspond to transitions over $a$ of the respective automata. The nodes in circles denote the accepting states of $\mathcal{B}$ that are moved to the *safe* phase. The values of $\kappa$ follow the boldfaced edges except the three boldfaced edges in the sub-round (R0) where the active states change phases from *safe* to *reach* and the values of $\kappa$ are decremented by 1.</figcaption></figure>

edges, and $\bar{e}_n$ for the boldfaced edges of $\mu_n$, respectively. Since $\pi$ is a play, $(S'_n, p'_n, \kappa'_n, r'_n) = (S_{n+1}, p_{n+1}, \kappa_{n+1}, r_{n+1})$ and $r_n \equiv n \bmod 3$.

A trace in $\pi$ is a sequence $\alpha = s_0, s_1, \dots$ such that $(s_i, s_{i+1}) \in e_i$ of all $i$. A trace is *boldfaced* if $(s_i, s_{i+1}) \in \bar{e}_i$ for all $i$. For every $s \in S'_n$ there is a boldfaced trace ending in $s$, and it is unique due to condition (2); we call it the *boldfaced history of s in $\pi$*.

The winning condition will be a boolean combination of three properties of plays. We list them separately as they will be of independent interest in the proof.

**W1** Infinitely many times there is a *flush* in the sub-round (R0).

**W2** Some boldfaced trace changes phases infinitely many times.

**W3** The sequence of states $p_0, p_1, \dots$ of the automaton $\mathcal{A}$ is accepting.
Now we declare a play to be winning for $\exists$ if it satisfies

$$ W1 \wedge (W2 \vee W3). \qquad (4) $$

Note that Condition W2 implies Condition W1—if some trace in a play changes phases infinitely often then the play must have infinitely many times a *flush*.

Intuitively, Condition W1 expresses that $\exists$ has not stayed forever in the *reach* phase — she has reached an accepting state of $\mathcal{B}$ whenever $\forall$ asked for it.

Condition W2 says that $\forall$ has not succeeded to bound the number of changes of phases; so he has failed to prove that on the constructed tree $t$ he can win in $\mathcal{G}(t, K)$ for some finite $K$. Condition W3 takes care of the situation when the constructed tree is not in $L(\mathcal{B})$. One can think of it as an escape option for $\exists$. She uses it when $\forall$ plays very cautiously and gives $\exists$ no chance to construct a trace satisfying Condition W2; an extreme example is when $\forall$ never chooses to move some active states to the *reach* phase.
<figure><img src="image_5.png" /><figcaption>■ **Figure 3** A symbolic representation of a strategy $\sigma_{\exists}$ of $\exists$. The subscript $x$ in $q_x^s$ or $q_x^r$ stands for $a$ or $b$. The superscript indicates if a state is in the *safe* phase or in the *reach* phase. Only branches not evidently losing for the player $\forall$ are presented.</figcaption></figure>

► **Example 7.** Let $\mathcal{B}$ be the Büchi automaton from the example on page 4. Consider an automaton $\mathcal{A}$ accepting the complement of $L(\mathcal{B})$, namely the set of trees with only finitely many $a$'s on every branch. This automaton is a deterministic co-Büchi automaton having two states: $p_a$ and $p_b$, with $p_a$ being a rejecting state. So a run of $\mathcal{A}$ will be accepting if on every branch the state $p_a$ appears only finitely often. For a state $p_x$ the transition relation $\delta^A$ on a letter $y \in \{a, b\}$ contains the transition $(p_x, y, p_y, p_y)$.

We claim that $\exists$ has a winning strategy in $\mathcal{F}(\infty)$ constructed from $\mathcal{B}$ and $\mathcal{A}$. This strategy is schematically presented in Figure 3. For compactness of the notation we omit the third component of the position that is always $\infty$ and omit active states of the form $(\top, z)$ — it is trivial for $\exists$ to play from them.

The root position is a *flush*, so $\forall$ can choose whether to copy the unique active state to the *reach* phase. If he does not (i.e. he goes up in the picture) then $\exists$ chooses $b$ and plays the transition $(q_x, b, q_b, \top)$. Then it is clear that it is better for $\forall$ to move to the left. The game gets to a similar position as in the root. If $\forall$ constantly chooses to play like this then he will lose as the play will have infinitely many times a *flush* and only states $p_b$, thus it will satisfy Conditions W1 and W3.

If $\forall$ decides to copy the active state during a *flush* then $\exists$ still chooses $b$ but plays different transitions for the two copies: for the active state in the *safe* phase she chooses $(q_x, b, q_b, \top)$, for the active state in the *reach* phase she chooses $(q_x, b, \top, q_b)$. If $\forall$ chooses the left direction then the play gets to a similar position as in the root. Since there is a *flush*, and $\forall$ does not manage to see a new $p_a$ state, the result is the same as in the case when $\forall$ has not copied the active state. If $\forall$ chooses the right direction then the play reaches a position where the only interesting active state is in the *reach* phase. Then $\exists$ chooses the letter $a$ and the transition $(q_b, a, q_a, \top)$. It is then more interesting for $\forall$ to move to the left. The play reaches a position of the same form as the one in the root. The interesting thing that happens on this path is that the unique boldfaced trace changes phases. So, if $\forall$ chooses infinitely often to copy an active state and then go to the right then the play will satisfy Conditions W1 and W2. Otherwise there will be only finitely many occurrences of the state $p_a$ and $\forall$ will lose since there still will be infinitely many times a *flush*.

We have already noticed that for every $K \in \overline{\omega}$, the game $\mathcal{F}(K)$ is finite. By the definition of Conditions W1, W2, and W3, the winning condition of $\mathcal{F}(K)$ is a regular property of sequences of multi-transitions. By adding multi-transitions of $\mathcal{F}(K)$ to the positions, one can obtain an equivalent game with the winning condition on sequences of positions. So up
to presentation, $\mathcal{F}(K)$ is essentially a finite game with a regular winning condition, and we
can solve it effectively.

► **Fact 8.** For a fixed $K \in \bar{\omega}$, the winner of $\mathcal{F}(K)$ can be effectively found and he/she can win using a finite memory winning strategy. Let $m_\forall$ be the bound on the size of the memory of $\forall$ needed to win the game $\mathcal{F}(\infty)$.

**5 Characterisation**

We show that $\mathcal{F}(\infty)$ characterises when $L(\mathcal{B})$ is WMSO-definable. This is formulated in the following two propositions that complete the proof of Theorem 1. They rely on the following standard fact, see for instance [24].

► **Fact 9.** If $L$ is a language of a Büchi tree automaton then $L \in \Sigma_1^1$. If $L$ is a WMSO-definable tree language then $L$ is Borel.

► **Proposition 10.** If $\forall$ wins $\mathcal{F}(\infty)$ then $L(\mathcal{B})$ is WMSO-definable.

► **Proposition 11.** If $\exists$ wins $\mathcal{F}(\infty)$ then $L(\mathcal{B})$ is $\Sigma_1^1$-complete and not WMSO-definable.

**5.1 Proof of Proposition 10**

The proof of Proposition 10 is based on the existence of finite memory strategies in finite
games with regular conditions, and the link with the game $\mathcal{G}$ given by the following lemma.

► **Lemma 12.** Consider $K \in \bar{\omega}$. If there exists<fnref n="3" /> a tree $t \notin L(\mathcal{B})$ such that $\exists$ wins $\mathcal{G}(t, K)$ then $\exists$ wins $\mathcal{F}(K)$. In other words if $L(\mathcal{G}, K) \not\subseteq L(\mathcal{B})$ then $\exists$ wins $\mathcal{F}(K)$.

**Proof.** Take such a tree $t \notin L(\mathcal{B})$, and let $\rho^A$ be an accepting run of the automaton $\mathcal{A}$ on $t$. Let $\sigma_\exists$ be a winning strategy of $\exists$ in $\mathcal{G}(t, K)$. We can assume that it is positional. We define a winning strategy of $\exists$ in $\mathcal{F}(K)$.

The only sub-round when $\exists$ makes some choice is the sub-round (R1). Suppose that the sequence of directions already played by $\forall$ was $u$, and the play reaches a position $(S_u, p_u, \kappa_u, 1)$. Now $\exists$ should choose a letter, a transition of $\mathcal{A}$, and a transition of $\mathcal{B}$ for every active state. As the letter, let $\exists$ play the letter of $t$, namely $t(u)$. As the transition of $\mathcal{A}$ she plays the transition from $\rho^A$ in $u$. What remains to show is how $\exists$ chooses the transitions of $\mathcal{B}$. For this let us assume an invariant saying that for every $(q, z) \in S_u$, the winning strategy $\sigma_\exists$ in $\mathcal{G}(t, K)$ is defined from the position $(q, u, \kappa_u(s), z)$. The invariant then allows us to finish the definition of the strategy. For an active state $s = (q, z)$ let $\exists$ choose the same transition as from the position $(q, u, \kappa_u(s), z)$ in $\mathcal{G}(t, K)$ (this is possible since $\sigma_\exists$ is positional). It is direct to check that our invariant is preserved.

We need to prove that the above strategy is winning. Clearly Condition W3 is guaranteed to hold as $\rho^A$ is an accepting run of $\mathcal{A}$ on $t$. It remains to prove Condition W1. After every *flush*, for every copied active state $(q, reach) \exists$ follows the strategy $\sigma_\exists$ in $\mathcal{G}(t, K)$. Since $\sigma_\exists$ is winning it leads eventually to an accepting state. As no states are added to the *reach* phase before the next *flush*, there is a global bound on the number of steps after which no more active states will stay in the *reach* phase. Therefore, every play consistent with this strategy will have infinitely many times a *flush* and thus will satisfy Condition W1. ◀

► **Lemma 13.** There exists a finite value $K_0 \in \omega$ that can be computed from $\mathcal{B}$ such that if $\forall$ wins $\mathcal{F}(\infty)$ then he wins $\mathcal{F}(K_0)$.

<footnote n="3">³ Notice that by Lemma 3, such a tree cannot exist for $K = \infty$.</footnote>
**Proof.** Observe that $\mathcal{F}(\infty)$ is a finite game effectively constructed from the automaton $\mathcal{B}$. By Fact 8 we can decide who is the winner in $\mathcal{F}(\infty)$. If $\exists$ wins then let $K_0 = 0$. If $\forall$ wins then he has a finite memory winning strategy. Let $\sigma_\forall$ be such a strategy and let $m_\forall$ be the size of its memory. We set $K_0$ to be the product of: $m_\forall$, the number of positions in $\mathcal{F}(\infty)$, and the number of possible active states (twice the number of states of $\mathcal{B}$).

Observe that we can execute the strategy $\sigma_\forall$ in the game $\mathcal{F}(K_0)$ as long as $\forall$ does not violate Condition (3) that prohibits copying an active state $s$ from the safe phase to the reach phase when $\kappa(s) = 0$. We show that indeed $\forall$ does not violate this condition when playing $\sigma_\forall$.

Suppose to the contrary that in $\mathcal{F}(K_0)$ there is a play, obtained when $\forall$ is simulating $\sigma_\forall$, reaching in the sub-round (R0) a position such that for some active state $s = (q, \text{safe})$ we have $\kappa(s) = 0$. This play corresponds to a play in $\mathcal{F}(\infty)$. During this play some boldfaced trace changes phases from safe to reach exactly $K_0$ times. By a standard pumping argument we can find a loop in $\sigma_\forall$ such that on this loop there is a boldfaced trace that is itself a loop and that changes phases at least twice. Following this loop in $\sigma_\forall$ we get a play respecting the strategy $\sigma_\forall$ with a boldfaced trace on it that changes phases infinitely often. So it satisfies Condition W2. As we have already noted, Condition W2 implies Condition W1. So the play is winning for $\exists$, a contradiction. ◀

**Proof of Proposition 10.** Assume that $\forall$ wins $\mathcal{F}(\infty)$. By Lemma 13 we know that $\forall$ wins $\mathcal{F}(K_0)$ for some fixed $K_0$. Using the notation from (1), we claim that:

$$L(\mathcal{B}) = L(\mathcal{G}, K_0).$$

By Lemma 5 we know that the latter language is WMSO-definable, so the equality finishes the argument. Lemma 4 gives us:

$$L(\mathcal{B}) = L(\mathcal{G}, \infty) \subseteq L(\mathcal{G}, K_0).$$

Assume for the sake of contradiction that the inclusion is strict, i.e., there exists $t \in L(\mathcal{G}, K_0) \setminus L(\mathcal{B})$. By Lemma 12 this implies that $\exists$ wins $\mathcal{F}(K_0)$. But this contradicts the fact that $\forall$ wins $\mathcal{F}(K_0)$. ◀

## 5.2 Proof of Proposition 11

Suppose that $\exists$ wins in $\mathcal{F}(\infty)$. Let us fix a winning strategy $\sigma_\exists$ for $\exists$ in $\mathcal{F}(\infty)$.

We need to prove that $L(\mathcal{B})$ is $\Sigma_1$-hard, so we will construct an appropriate continuous reduction. Let $\omega$Tr denote the space of partial $\omega$-branching trees. Such a tree $\tau$ is a non-empty, prefix-closed subset of $\omega^*$. We say that an $\omega$-branching tree $\tau$ is *ill-founded* if it contains an infinite branch, i.e. there exists $\alpha \in \omega^\omega$ such that for every $x \prec \alpha$ we have $x \in \tau$. We use IF to denote the set of all ill-founded $\omega$-branching trees. If an $\omega$-branching tree is not ill-founded then it is *well-founded*.

► Fact 14. IF is $\Sigma_1$-complete.

Therefore, it is enough to construct a continuous reduction from IF to $L(\mathcal{B})$. Our aim is to construct a tree $t(\tau)$ such that $t(\tau) \in L(\mathcal{B})$ if and only if $\tau$ is ill-founded. The tree $t(\tau)$ will be obtained by evaluating the strategy $\sigma_\exists$ against a certain family of strategies of $\forall$, called $\tau$-genuine strategies.

Let us explain this point in more detail. A strategy for $\exists$ in $\mathcal{F}(\infty)$ can be seen as a strategy tree where branching represents the choices of $\forall$ (see Figure 3). Recall from the definition of the game that $\forall$ not only chooses directions (in the sub-round (R1)), but also
copies active states to the *reach* phase (during a *flush* in the sub-round (R0)), and selects boldfaced edges (in all the sub-rounds). We want to extract from the strategy tree $\sigma_{\exists}$ a tree where we leave only branching corresponding to the choice of directions. To this end we define $\tau$-genuine strategies of $\forall$, where his choices to copy and to select boldfaced edges are determined by the history of the play so far. This means that a strategy tree for $\exists$ against all $\tau$-genuine strategies of $\forall$ will be a tree with branching corresponding only to the choices of directions by $\forall$. Then we show that we have not restricted the power of $\forall$ too much, namely from this strategy tree for $\exists$ we can read out the required tree $t(\tau)$.

To properly define $\tau$-genuine strategies of $\forall$ we will use the Kleene-Brouwer ordering, see [15, Section 2.G]. For $x, y \in \omega^*$, we say that $x \le_{KB} y$ if either: (i) $x \ge y$, or (ii) for some $n < m < \omega$ and $v, x', y' \in \omega^*$ we have $x = vnx'$ and $y = vmy'$. Intuitively, $x \le_{KB} y$ if $x$ is below or to the left of $y$. $\epsilon$ is the $\le_{KB}$-maximal element of $\omega^*$. There is no $\le_{KB}$-minimal element in $\omega^*$, e.g. for every $x \in \omega^*$ and its 0-successor $x \cdot 0$ we have $x \cdot 0 <_{KB} x$.

**Fact 15** (See [15, Proposition 2.12]). An $\omega$-branching tree $\tau$ is well-founded if and only if $\le_{KB}$ is a well-order on the vertices of $\tau$.

For certain technical reasons it will be useful to have the following construction.

**Definition 16.** First, assume that list: $\omega \to \omega^*$ has the property that for each $x \in \omega^*$, the pre-image list$^{-1}(\{x\})$ is infinite (i.e. every vertex appears infinitely many times in this enumeration). Now, given $x \in \omega^*$ let $\text{down}(x, n)$ be either list($n$) if list($n$) $<_{KB} x$ or $x \cdot 0$ otherwise.

**Fact 17.** The following conditions are satisfied for every $x \in \omega^*$:

- $\forall_{n \in \omega}$ down$(x, n) <_{KB} x$,

- for every $y <_{KB} x$ there are infinitely many $n$ such that $\text{down}(x, n) = y$.

Now we can proceed with the definition of $\tau$-genuine strategies. Our aim is to make sure that for every sequence of successive directions $d_0, d_1, \dots$ played in the sub-rounds (R1), there is a unique $\tau$-genuine strategy of $\forall$. A $\tau$-genuine strategy will depend on certain additional information accumulated during a play, and this information will be related to the $\omega$-branching tree $\tau$. Therefore, $\forall$ will keep track of an *extended position* — a position $(S, p, \kappa, r)$ of $\mathcal{F}$ together with a mapping $\nu: S \to \tau$ and a counter $c \in \omega$. The function $\nu$ will measure the progress of every active state with respect to the $\le_{KB}$ order over $\tau$. The counter $c$ will count the number of times when a *flush* happened in the play.

The initial extended position of the game is the initial position of $\mathcal{F}(\infty)$ together with $\nu$ assigning to $(q_1^B, \text{safe})$ the root $\epsilon$ of $\tau$; and the counter $c = 0$.

A strategy $\sigma_\forall$ of $\forall$ is called $\tau$-genuine if it satisfies the three conditions defined below: genuine-copying, flush-counting, and KB-tracking.

A strategy $\sigma_\forall$ satisfies genuine-copying if during a *flush* in the sub-round (R0) it copies an active state $s$ from the *safe* phase to the *reach* phase if and only if $\text{down}(\nu(s), c) \in \tau$.

The condition of *flush-counting* says that $\forall$ increments $c$ by 1 exactly when there is a *flush* in the sub-round (R0); otherwise he keeps the value $c$ unchanged.

The last condition *KB-tracking* determines how the set of boldfaced edges $\bar{e}$ should be chosen and how to update $\nu$. We say that a multi-transition $\mu$ from $(S, p, \kappa, r, \nu, c)$ to $(S', p', \kappa', r', \nu', c')$ with edges $e$ and boldfaced edges $\bar{e}$ satisfies the *KB-tracking* condition when:

- If $\mu$ is not a *flush* then for every $s' \in S'$:

$$ \nu'(s') = \max_{\le_{KB}} \{\nu(s) : (s, s') \in e\}. $$
Moreover, the unique boldfaced edge to $s'$ should come from $s_0$ realising the maximum above, i.e., $\nu'(s') = \nu(s_0)$ (if there is more than one such $s_0$ then we choose the smallest one according to some fixed ordering on active states).

- If $\mu$ is a flush then for every $s' \in S'$ from the safe phase, the vertex $\nu'(s')$ of $\tau$ and the boldfaced edges are determined as above. For every $s' \in S'$ in the reach phase there is a unique $s \in S$ with $(s, s') \in e$. This edge needs to be boldfaced and we set

$$ \nu'(s') = \text{down}(\nu(s), c). $$

Notice that in this last case the node down($\nu(s), c$) is in $\tau$ thanks to the genuine-copying condition.

**Fact 18.** Using the above notions, the following inequalities hold:

- if $(s, s') \in \bar{e}$ then $\nu(s) \geq_{\text{KB}} \nu'(s')$,

- if $(s, s') \in e$ and $(s, s')$ changes phases from safe to reach then $\nu(s) >_{\text{KB}} \nu'(s')$,

- if $(s, s') \in e$ and $(s, s')$ does not change phases from safe to reach then $\nu(s) \leq_{\text{KB}} \nu'(s')$.

**Corollary 19.** Suppose $\tau$ is well-founded. If $\pi$ is an infinite play of $\mathcal{F}(\infty)$ consistent with a $\tau$-genuine strategy of $\forall$ then $\pi$ does not satisfy W2 (no boldfaced trace changes phases infinitely many times).

**Remark.** Observe that all the choices of $\forall$ except the directions $d$ are uniquely determined in a $\tau$-genuine strategy. Therefore, to define a $\tau$-genuine strategy it is enough to say what will be the directions proposed by $\forall$ in the sub-rounds (R1). For the next definition it is also useful to note that all the maximal plays in $\mathcal{F}(\infty)$ are infinite.

**Definition 20.** For every $\alpha \in \{\text{L}, \text{R}\}^\omega$ by $\sigma_\forall(\tau, \alpha)$ we denote the unique $\tau$-genuine strategy of $\forall$ that for every $n \in \omega$ plays $d = \alpha(n)$ in the $n$-th sub-round (R1). Let $\pi(\tau, \alpha)$ be the infinite play of $\mathcal{F}(\infty)$ obtained when $\exists$ is playing $\sigma_\exists$ and $\forall$ is playing $\sigma_\forall(\tau, \alpha)$.

For every finite prefix $u \prec \alpha$ we denote by $\pi(\tau, u)$ the corresponding prefix of $\pi(\tau, \alpha)$. This play is defined until $\forall$ is asked to determine the $(n+1)$-th direction in the sub-round (R1). Let $(S_u, p_u, \kappa_u, r_u, \nu_u, c_u)$ be the extended position of this play at the beginning of the last round (i.e. when $r_u = 0$).

We can finally define the tree $t(\tau)$.

**Definition 21.** We define the tree $t(\tau)$ together with a run $\rho^A(\tau)$ of $\mathcal{A}$. For a vertex $u \in \{\text{L}, \text{R}\}^*$, let $t(\tau)(u)$ and $\rho^A(\tau)(u)$ be the letter $a$ and the state $p$ of $\mathcal{A}$ played by $\exists$ in the sub-round (R1) of the last round of the play $\pi(\tau, u)$.

Observe that by the construction, $\rho^A(\tau)$ is a run of $\mathcal{A}$ over $t(\tau)$. Notice also that since the strategy $\sigma_\forall(\tau, u)$ queries whether $v \in \tau$ for finitely many $v$ at a time, the function mapping $\tau$ to $t(\tau)$ is continuous. We show that indeed the mapping is the required reduction from IF as expressed by the following two lemmas.

**Lemma 22.** If $\tau$ is well-founded then $\rho^A(\tau)$ is accepting and thus $t(\tau) \notin L(\mathcal{B})$.

**Lemma 23.** If $\tau$ is ill-founded then $t(\tau) \in L(\mathcal{B})$.

**Proof of Lemma 22.** The proof uses Corollary 19. Consider any infinite branch $\alpha$ of $t(\tau)$ and the corresponding play $\pi(\tau, \alpha)$ of $\sigma_\exists$ against $\sigma_\forall(\tau, \alpha)$. Since $\sigma_\exists$ is winning we know that it satisfies the disjunction $W2 \lor W3$. By Corollary 19 we know that no play consistent with $\sigma_\forall(\tau, \alpha)$ can satisfy Condition W2. Therefore, Condition W3 needs to be satisfied and therefore, the run $\rho^A(\tau)$ is accepting on $\alpha$. ◀
The rest of this section is devoted to the proof of Lemma 23 we fix an $\omega$-branching ill-founded tree $\tau \in \mathbf{IF}$. We then extract an accepting run $\rho^B$ of $\mathcal{B}$ on $t(\tau)$ from the strategy $\sigma_\exists$ in $\mathcal{F}(\infty)$. The crucial point is to make sure that $\forall$ will copy infinitely often the active states of the constructed run to the *reach* phase. For this we need to rely on the condition of *genuine-copying*. Let us now describe how this construction works on our running example.

**Example 24.** Recall the example from page 4 and the winning strategy for $\exists$ from the example on page 8 (see Figure 3). In this strategy $\forall$ has a choice of whether to copy or not the active state $q_x^s$; this corresponds to going down or up from the root, respectively. Next, $\forall$ chooses a direction. In a $\tau$-genuine strategy a state $q_x^s$ is assigned a node $\nu(q_x^s)$ of $\tau$ and $c$ counts the number of flushes. The condition of genuine-copying requires $\forall$ to copy the state $q_x^s$ to the reach phase if $\text{down}(\nu(q_x^s), c) \in \tau$. Since all loops of $\sigma_\exists$ contain a *flush*, the value $c$ counts the number of times either of the loops has been taken.

According to the definition of a $\tau$-genuine strategy, the only moment when the value $\nu(q_x^s)$ may change is when $\forall$ copies (i.e. takes the down successor of the root at Figure 3) and in that case the value $\nu(q_x^r)$ becomes $\text{down}(\nu(q_x^s), c)$ according to the *KB-tracking* condition. This becomes the new value of $\nu(q_x^s)$ if and only if the play then follows the direction $\mathbf{R}$.

If $\tau$ is well-founded then there is no infinite $\leq_{\text{KB}}$-descending chain in $\tau$ and therefore, for every branch $\alpha \in \{\text{L}, \mathbf{R}\}^\omega$, the play $\pi(\tau, \alpha)$ follows only finitely many times the down path of $\sigma_\exists$. Therefore, the produced tree $t(\tau)$ contains only finitely many letters $a$ on every branch and $t(\tau) \notin \mathbf{L}(\mathcal{B})$.

Now assume that $\tau$ is ill-founded and $v_0 >_{\text{KB}} v_1 >_{\text{KB}} \dots$ is an infinite $\leq_{\text{KB}}$-descending chain of nodes of $\tau$. We will use this sequence to find a branch of $t(\tau)$ that contains infinitely many $a$'s. We start in the root of $t(\tau)$ and keep track of the current vertex $\nu(q_x^s)$ of $\tau$. We will preserve an invariant that when being in a node $u \in \{\text{L}, \mathbf{R}\}^*$ with $n$ the number of occurrences of $a$ on $u$ in $t(\tau)$ then $\nu(q_x^s) = v_n$ — the vertex of $\tau$ pointed to by $\nu$ is the $n$-th vertex in our $\leq_{\text{KB}}$-descending chain. Consider the following two cases:

1. If $\text{down}(\nu(q_x^s), c) = v_{n+1}$ then $\forall$ chooses to copy, i.e., go down from the root. We follow the $\mathbf{R}$-successor in $t(\tau)$. Then $t(\tau)(u_\mathbf{R}) = a$ and the game gets to the node $u_\mathbf{R L}$. The number of times we have seen an $a$ is incremented (i.e. $n' = n + 1$), and the invariant is preserved since after this loop we have $\nu(q_x^s) = v_{n+1}$.

2. Otherwise either (i) $\text{down}(\nu(q_x^s), c) \notin \tau$ so $\forall$ does not copy, or (ii) $\text{down}(\nu(q_x^s), c) \in \tau$ so $\forall$ copies, but we choose the direction $\mathbf{L}$. In both cases we end up in the left successor of our current node (i.e. in $u_\mathbf{L}$). The new value $\nu(q_x^s)$ does not change, neither does $n$. Therefore, in both cases the invariant $\nu(q_x^s) = v_n$ is preserved. Since the value of $c$ tends to infinity, Fact 17 tells us that $\text{down}(\nu(q_x^s), c) = v_{n+1}$ will eventually hold, and we will see an $a$. In the limit, the branch of $t(\tau)$ we follow will have infinitely many letters $a$.

**Proof of Lemma 23.** We fix an $\omega$-branching ill-founded tree $\tau \in \mathbf{IF}$. Our aim is to extract an accepting run $\rho^B$ of $\mathcal{B}$ over $t(\tau)$ from the strategy $\sigma_\exists$ in $\mathcal{F}(\infty)$ that will be confronted with a family of $\tau$-genuine strategies of $\forall$, see in particular Definition 20. Condition W1 will imply that the constructed run of $\mathcal{B}$ is accepting. The crucial point is to make sure that $\forall$ will copy infinitely often the active states of the constructed run to the *reach* phase. For this we need to rely on the condition of *genuine-copying*.

Since $\tau$ is ill-founded, there exists a sequence $v_0 >_{\text{KB}} v_1 >_{\text{KB}} \dots$ of nodes of $\tau$. Without loss of generality we can assume that $v_0 = \epsilon$ and that $v_0, v_1, \dots$ form an infinite branch of $\tau$.

To define $\rho^B$ we will inductively select, for every $u \in \{\text{L}, \mathbf{R}\}^*$, an active state $s_u = (q_u, z_u)$ such that $s_u$ belongs to $S_u$ — the set of active states at the end of the play $\pi(\tau, u)$. The crucial constraint is that for every infinite branch $\alpha$, the active states $(s_u)_{u<\alpha}$ will lie on a single trace in the play $\pi(\tau, \alpha)$. We will refer to this condition as *trace-following*. See
<figure><img src="image_6.png" /><figcaption>Figure 4 An illustration of the trace-following condition. The graph is obtained by evaluating the strategy $\sigma_{\exists}$ against the strategies $\sigma_{\forall}(\tau, \alpha)$ for all possible values of $\alpha$. To simplify the image we present only the active states $S$ and the edges $e$ between them. The boldfaced edges $\bar{e}$ are not drawn since they do not intervene in this construction. The dashed edges are the edges connecting the chosen active states — we follow these edges. The blue dotted paths separate the safe phase from the reach phase. The green background shadow shows the tree-shape of the construction — we can control the direction $d$ chosen by $\forall$ in the sub-round (R1), to move either to the left or the right subtree. The black horizontal lines separate the successive rounds of the game, each of them consists of the three sub-rounds. The letters $a$, $b$, and $c$ are the letters of the tree $t(\tau)$ in the respective nodes.</figcaption></figure>

Figure 4 for an illustration of this condition. It will be used in such a way to guarantee that the mapping $\rho^B(u) = q_u$ is actually a run of $B$ over $t(\tau)$.

Additionally $s_u$ will be chosen so that the following invariant is satisfied

$$ \nu_u(s_u) \geq_{KB} v_{n_u}, \qquad (5) $$

for $n_u$ the number of times the trace through $(s_w)_{w \sim u}$ changes phases from safe to reach. The invariant says that $\nu_u(s_u)$ should be above or to the right of the $n_u$-th vertex of our fixed infinite branch in $\tau$.

We start with $s_\epsilon = (q_1^B, \text{safe})$. Clearly the trace-following condition and the invariant are satisfied since $\nu_\epsilon(s_\epsilon) = \epsilon$.

Assume that $s_u$ is defined and satisfies the above invariant. Consider $d \in \{\text{L}, \text{R}\}$. Our aim is to define $s_{ud}$. Consider the $(|u|+1)$-th round of the play $\pi(ud)$. It consists of the sub-rounds (R0), (R1), and (R2); where in the sub-round (R1) $\forall$ chooses the direction $d$. Starting from $s_u$ we select a trace through these three sub-rounds that will lead us to $s_{ud}$. Notice that by Fact 6 the condition of trace-following uniquely determines the successive active states to choose, except the situation when an active state has two $\mu$-successors in the sub-round (R0) when a flush happens. In that case, $z_u = \text{safe}$ and the two $\mu$-successors of $s_u$ are $(q_u, \text{safe})$ and $(q_u, \text{reach})$. We follow $(q_u, \text{reach})$ if and only if

$$ \text{down}(\nu_u(s_u), c_u) = v_{n_u+1}; \qquad (6) $$

Recall that $c_u$ is the number of times a flush happened in the play $\pi(\tau, u)$. Observe that a
$\tau$-genuine strategy indeed creates an edge from $s_u$ to $(q_u, reach)$ if the above condition holds (because of genuine-copying and the fact that $v_{n_u+1} \in \tau$).

Let $s_{ud}$ be the active state that is reached by following the trace according to the above condition.

► Fact 25. The invariant (5) is preserved.

**Proof.** This fact relies on Fact 18. The only case when for some $(s, s') \in e$ we have $\nu(s) >_{KB} \nu'(s')$ is when $(s, s')$ changes phases from safe to reach. This case is covered by (6) and we are then guaranteed to satisfy

$$ \nu'_{u}(s') = \text{down}(\nu_{u}(s_{u}), c_{u}) = v_{n_{u}+1} = v_{n'_{u}}, $$

because of the definition of $\nu'$ and the fact that the new value $n'_{u}$ is incremented because in this sub-round the followed trace changes phases from safe to reach.

In all other cases we have $\nu(s) \le_{KB} \nu'(s')$ by Fact 18 and we know that $n_u = n'_u$. Therefore, we know that:

$$ \nu'_{u}(s') \ge_{KB} \nu_{u}(s_{u}) \ge_{KB} v_{n_{u}} = v_{n'_{u}}. $$

<figure><img src="image_7.png" /></figure>

It remains to prove that $\rho^B$ is an accepting run of $\mathcal{B}$ on $t(\tau)$. Assume contrarily that there exists an infinite branch $\alpha$ such that there are only finitely many accepting states in $\rho^B$ on $\alpha$. By W1 we know that during the play $\pi(\tau, \alpha)$ there was infinitely many times a flush. It means that the trace through $(s_u)_{u<\alpha}$ changed phases from safe to reach only finitely many times (every time this trace changes phases from reach to safe, it has to go back to the safe phase later on and it implies an accepting state in $\rho^B$). Therefore, for some $u \prec \alpha$ and all $w$ such that $u \preceq w \prec \alpha$ we have

$$ n_u = n_w. \tag{7} $$

Recall that $c_w$ is the number of times a flush happened on the play $\pi(\tau, w)$ and the play $\pi(\tau, \alpha)$ contains infinitely many times a flush. So for every $i \ge c_u$ there is $w \prec \alpha$ such that $u \preceq w$, $c_w = i$ and there is a flush at $w$. Take such a node $w$ for which $\text{list}(c_w) = v_{n_u+1}$; it exists by Fact 17. The invariant (5) gives us $\nu_w(s_w) \ge_{KB} v_{n_w} = v_{n_u}$; the latter equality due to $n_u = n_w$. As $v_{n_u} >_{KB} v_{n_u+1}$ we know that $\text{down}(\nu_w(s_w), c_w) = v_{n_w+1}$. The rule (6) applies here and we choose the $(q_w, reach)$ successor of $s_w$. Let $d$ be the direction such that $wd \prec \alpha$. We know that $n_{wd} = n_w + 1$, a contradiction with (7).

<figure><img src="image_8.png" /></figure>

# 6 Conclusions

While regular languages of infinite trees are widely used nowadays, their structure is still very poorly understood. The main reason for this is probably the lack of deterministic acceptors for such languages. This paper exhibits a gap property for languages of non-deterministic Büchi tree automata: such a language is either weakly definable, or $\Sigma_1$-complete. Our proof uses a reduction to a finite game. Given a Büchi automaton $\mathcal{B}$, we construct a game $\mathcal{F}(\infty)$ of exponential size w.r.t. $\mathcal{B}$, and with a parity condition of size proportional to the size of $\mathcal{B}$. Thus our reduction gives an EXPTIME decision algorithm. This matches a known lower bound [25].
References

1 Mikołaj Bojańczyk. Star height via games. In *LICS*, pages 214–219, 2015.

2 Mikołaj Bojańczyk and Tomasz Idziaszek. Algebra for infinite forests with an application to the temporal logic EF. In *CONCUR*, pages 131–145, 2009.

3 Mikołaj Bojańczyk, Damian Niwiński, Alexander Rabinovich, Adam Radziwończyk-Syta, and Michał Skrzypczak. On the Borel complexity of MSO definable sets of branches. *Fundamenta Informaticae*, 98(4):337–349, 2010.

4 Mikołaj Bojańczyk and Thomas Place. Regular languages of infinite trees that are Boolean combinations of open sets. In *ICALP*, pages 104–115, 2012.

5 Julian Bradfield. The modal mu-calculus alternation hierarchy is strict. *Theoretical Computer Science*, 195:133–153, 1997.

6 Jérémie Cabessa, Jacques Duparc, Alessandro Facchini, and Filip Murlak. The Wadge hierarchy of max-regular languages. In *FSTTCS*, pages 121–132, 2009.

7 Thomas Colcombet. Fonctions régulières de coût. Habilitation thesis, Université Paris Diderot—Paris 7, 2013.

8 Thomas Colcombet, Denis Kuperberg, Christof Löding, and Michael Vanden Boom. Deciding the weak definability of Büchi definable tree languages. In *CSL*, pages 215–230, 2013.

9 Thomas Colcombet and Christof Löding. The non-deterministic Mostowski hierarchy and distance-parity automata. In *ICALP (2)*, pages 398–409, 2008.

10 Jacques Duparc, Olivier Finkel, and Jean-Pierre Ressayre. Computer science and the fine structure of Borel sets. *Theoretical Computer Science*, 257(1–2):85–105, 2001.

11 Jacques Duparc, Olivier Finkel, and Jean-Pierre Ressayre. The Wadge hierarchy of Petri nets w-languages. In *LFCS*, pages 179–193, 2013.

12 Alessandro Facchini, Filip Murlak, and Michał Skrzypczak. Rabin-Mostowski index problem: A step beyond deterministic automata. In *LICS*, pages 499–508, 2013.

13 Olivier Finkel. Borel ranks and Wadge degrees of context free omega-languages. *Mathematical Structures in Computer Science*, 16(5):813–840, 2006.

14 Tomasz Idziaszek, Michał Skrzypczak, and Mikołaj Bojańczyk. Regular languages of thin trees. *Theory of Computing Systems*, pages 1–50, 2015.

15 Alexander Kechris. *Classical descriptive set theory*. Springer-Verlag, New York, 1995.

16 Denis Kuperberg and Michael Vanden Boom. Quasi-weak cost automata: A new variant of weakness. In *FSTTCS*, volume 13 of *LIPIcs*, pages 66–77, 2011.

17 Ralf Küsters and Thomas Wilke. Deciding the first level of the $\mu$-calculus alternation hierarchy. In *FST TCS 2002*, volume 2556 of *LNCS*, pages 241–252, 2002.

18 Filip Murlak. The Wadge hierarchy of deterministic tree languages. *Logical Methods in Logical Methods in Comput. Sci.*, 4(4), 2008.

19 Filip Murlak. Weak index versus Borel rank. In *STACS'08*, LIPIcs, pages 573–584, 2008.

20 Damian Niwiński and Igor Walukiewicz. A gap property of deterministic tree languages. *Theor. Comput. Sci.*, 1(303):215–231, 2003.

21 Damian Niwiński and Igor Walukiewicz. Deciding nondeterministic hierarchy of deterministic tree automata. *Electronic Notes in Theoretical Computer Science*, 123:195–208, 2005.

22 Michael Oser Rabin. Weakly definable relations and special automata. In *Proceedings of the Symposium on Mathematical Logic and Foundations of Set Theory*, pages 1–23. North-Holland, 1970.

23 Jerzy Skurczyński. The Borel hierarchy is infinite in the class of regular sets of trees. *Theoretical Computer Science*, 112(2):413–418, 1993.

24 Wolfgang Thomas and Helmut Lescow. Logical specifications of infinite computations. In *REX School/Symposium*, pages 583–621, 1993.
25 Igor Walukiewicz. Deciding low levels of tree-automata hierarchy. In *Workshop on Logic, Language, Information and Computation*, volume 67 of *Electronic Notes in Theoretical Computer Science*, pages 61–75, 2002.