A Dichotomy Theorem for Ordinal Ranks in MSO

Niwiński, Damian; Parys, Paweł; Skrzypczak, Michał

doi:10.4230/LIPIcs.STACS.2025.69

A Dichotomy Theorem for Ordinal Ranks in MSO

Damian Niwiński

Institute of Informatics, University of Warsaw, Poland Paweł Parys

Institute of Informatics, University of Warsaw, Poland Michał Skrzypczak

Institute of Informatics, University of Warsaw, Poland

Abstract

We focus on formulae $\exists X.\,\varphi(\vec{Y},X)$ of monadic second-order logic over the full binary tree, such that the witness $X$ is a well-founded set. The ordinal rank $\mathrm{rank}(X)<\omega_{1}$ of such a set $X$ measures its depth and branching structure. We search for the least upper bound for these ranks, and discover the following dichotomy depending on the formula $\varphi$ . Let $\eta_{\varphi}$ be the minimal ordinal such that, whenever an instance $\vec{Y}$ satisfies the formula, there is a witness $X$ with $\mathrm{rank}(X)\leq\eta_{\varphi}$ . Then $\eta_{\varphi}$ is either strictly smaller than $\omega^{2}$ or it reaches the maximal possible value $\omega_{1}$ . Moreover, it is decidable which of the cases holds. The result has potential for applications in a variety of ordinal-related problems, in particular it entails a result about the closure ordinal of a fixed-point formula.

Keywords and phrases:

dichotomy result, limit ordinal, countable ordinals, nondeterministic tree automata

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Automata over infinite objects ; Theory of computation

\rightarrow

Tree languages

Related Version:

Full Version: https://arxiv.org/abs/2501.05385

Acknowledgements:

The authors would like to thank Marek Czarnecki for preliminary discussions on related subjects.

Funding:

All authors supported by the National Science Centre, Poland (grant no. 2021/41/B/ST6/03914).

DOI:

10.4230/LIPIcs.STACS.2025.69

Event:

42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)

Editors:

Olaf Beyersdorff, Michał Pilipczuk, Elaine Pimentel, and Nguyễn Kim Thắng

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

The concept of well-founded relation plays a central role in foundations of mathematics. It gives rise to ordinal numbers, which underlie the basic results in set theory, for example that any two sets can be compared in cardinality. Well-foundedness is no less important in the realm of computer science, where it often underlies the proofs of termination of non-deterministic processes, especially when no efficient bound on the length of a computation is known. In such cases, the complexity of possible executions is usually measured using an ordinal called rank. Such a rank can be seen as a measure of the depth of the considered partial order, taking into account suprema of lengths of possible descending chains. Estimates on a rank can provide upper-bounds on the computational complexity of the considered problem [26].

In this work, we adopt the perspective of mathematical foundations of program verification and model-checking. We focus on the monadic second-order logic (MSO) interpreted in the infinite binary tree (with the left and right successors as the only non-logical predicates), which is one of the reference formalisms in the area [29]. The famous Rabin Tree Theorem [25] established its decidability, but – half a century after its introduction – the theory is still an object of study. On one hand, it has led to numerous extensions, often shifting the decidability result far beyond the original theory (see e.g. [4, 24]). On the other hand, a number of natural questions regarding Rabin’s theory remain still open, including a large spectrum of simplification problems. For example, we still do not know whether we can decide if a given formula admits an equivalent form with all quantifiers restricted to finite sets. Similar questions have been studied in related formalisms like $\mu$ -calculus or automata; for example if we can effectively minimise the Mostowski index of a parity tree automaton [11, 15], or the $\mu\nu$ -alternation depth of a $\mu$ -calculus formula [5].

On positive side, some decidability questions have been solved by reduction to the original theory. For example, it has been observed [22] that for a given formula $\varphi(\vec{X})$ , the cardinality of the family of tuples of sets $\vec{X}$ satisfying $\varphi(\vec{X})$ can be computed; this cardinality can be either finite, $\aleph_{0}$ , or $\mathfrak{c}$ . Later on, Bárány, Kaiser, and Rabinovich [3] proved a more general result: they studied cardinality quantifiers $\exists^{\geq\kappa}X.\,\varphi(\vec{Y},X)$ , stating that there are at least $\kappa$ distinct sets $X$ satisfying $\varphi(\vec{Y},X)$ , and showed that these quantifiers can be expressed in the standard syntax of MSO; thus the extended theory remains decidable.

In the present work, instead of asking how many sets $X$ witness to the formula $\exists X.\,\varphi(\vec{Y},X)$ , we ask how complex these witnesses must be in terms of their depth-and-branching structure. A set $X$ of nodes of a tree is well-founded if it contains no infinite chain with respect to the descendant order. In this case, a countable ordinal number $\mathrm{rank}(X)$ is well defined (see Section 2 below); intuitively, the smaller $\mathrm{rank}(X)$ , the simpler the set $X$ is, in terms of its branching structure.

We consider formulae of the form $\exists X.\,\varphi(\vec{Y},X)$ , where $\varphi$ is an arbitrary formula of MSO (it may contain quantifiers). We assume that, whenever the formula is satisfied for some valuation of variables $\vec{Y}$ , the value of $X$ witnessing the formula is a well-founded set. Note that well-foundedness of a set is expressible in MSO (it suffices to say that each branch contains only finitely many nodes in $X$ ), hence the requirement can be expressed within $\varphi$ . For a fixed formula as above, we ask what is the minimal ordinal $\eta_{\varphi}$ , such that the rank of a witness can be bounded by $\eta_{\varphi}$ ,

\eta_{\varphi}\stackrel{{\scriptstyle\text{def}}}{{=}}\adjustlimits{\sup}_{% \vec{Y}}{\min}_{X}\,\mathrm{rank}(X),

(1.1)

where $\vec{Y}$ and $X$ range, as expected, over the values satisfying $\varphi(\vec{Y},X)$ .

Since $\eta_{\varphi}$ is a supremum of countable ordinals, its value is at most $\omega_{1}$ (the least uncountable ordinal). It can be achieved, for example, by the formula “ $X=Y$ and $Y$ is a well-founded set”, as there are well-founded sets of arbitrarily large countable ranks. On the other hand, for each pair of natural numbers $(k,l)$ , one can construct a formula $\varphi$ with rank $\eta_{\varphi}=\omega\cdot k+l$ in an analogous way to Czarnecki [12], see Lemma 9.4 below. The main result of this work shows that no other ordinals can be obtained:

Theorem 1.1.

For any formula $\exists X.\,\varphi(\vec{Y},X)$ as above, the ordinal $\eta_{\varphi}$ is either strictly smaller than $\omega^{2}$ or equal to $\omega_{1}$ . Moreover, it can be effectively decided which of the cases holds. In the former case, it is possible to compute a number $N\in\mathbb{N}$ such that $\eta_{\varphi}<\omega\cdot N$ .

We also show that, in contrast to the aforementioned cardinality quantifiers, the property that $\mathrm{rank}(X)$ is smaller than $\omega^{2}$ cannot be expressed directly in MSO (see Corollary 9.3).

The proof of Theorem 1.1 develops the game-based technique used previously to characterise certain properties of MSO-definable tree languages (see e.g. [9, 28]). Each application of this technique requires a specific game, designed in a way which reflects the studied property. The game should have a finite arena and be played between two perfectly-informed players $\exists$ and $\forall$ . The winning condition of the game is given by a certain $\omega$ -regular set. Then, the seminal result of Büchi and Landweber [8] yields that the game is determined and the winner of this game can be effectively decided. The construction of the game is such that a winning strategy of each of the players provides a witness of either of the considered possibilities: if $\exists$ wins then $\eta_{\varphi}=\omega_{1}$ and if $\forall$ wins then $\eta_{\varphi}<\omega\cdot N$ for some computable $N$ . The crucial difficulty of this approach lies in a proper definition of the game, so that both these implications actually hold.

Related work

In the context of $\mu$ -calculus, one asks how many iterations are needed to reach a fixed point; this aspect concerns complexity of model checking (cf. [7, 14]), as well as expressive power of the logic (cf. [7, 6]). Recall that, in an infinite structure, a least fixed point $\mu X.\,F(X)$ is in general reached in a transfinite number of iterations: $\emptyset,F(\emptyset),\ldots,F^{\alpha}(\emptyset),\ldots$ , where, for a limit ordinal $\alpha$ , $F^{\alpha}(\emptyset)=\bigcup_{\xi<\alpha}F^{\xi}(\emptyset)$ . It is therefore natural to ask if, for a given formula, one can effectively find a closure ordinal $\eta_{F}$ , such that, in any model, the fixed point can be reached in $\eta_{F}$ , but in general not less, iterations. Fontaine [18] effectively characterised the formulae such that in each model the fixed point is reached in a finite number of steps. Czarnecki [12] observed that some formulae have no closure ordinals but, for each ordinal $\eta<\omega^{2}$ , there is a formula whose closure ordinal is $\eta$ . He also raised the following question.

Question 1.2 (Czarnecki [12]).

Is there a $\mu$ -calculus formula of the form $\mu X.\,F(X)$ that has a closure ordinal $\eta_{F}\geq\omega^{2}$ ?

Gouveia and Santocanale [19] exhibited an example of a formula with an essential alternation of the least and greatest fixed-point operators whose closure ordinal is $\omega_{1}$ ; clearly this limit can be achieved only in uncountable models. In general, it remains open whether a formula $\mu X.\,F(X)$ of the $\mu$ -calculus may have a countable closure ordinal $\eta_{F}\geq\omega^{2}$ . Afshari and Leigh [2] claimed a negative answer for formulas of the alternation-free fragment of $\mu$ -calculus; however, as the authors have later admitted [1], the proof contained some gaps. In a recent paper [1], Afshari, Barlucchi, and Leigh update the proof and extend the result to formulae of the so-called $\Sigma$ -fragment of the $\mu$ -calculus. More specifically, the authors consider systems of equations $X_{1}=F_{1}(X_{1},\ldots,X_{n}),\ldots,X_{n}=F_{n}(X_{1},\ldots,X_{n})$ , where the formulae $F_{i}$ may contain closed sub-formulae of the full $\mu$ -calculus, but the variables $X_{i}$ do not fall in the scope of any fixed-point operators. The authors show that if a countable number of iterations $\eta$ suffice to reach the least fixed point of such a system in any Kripke frame then $\eta<\omega^{2}$ . (Note that, by Bekič principle, each component of such a solution can be expressed by a single formula with the nested $\mu$ -operators.)

As a direct consequence of our result, we obtain an alternative proof for formulae of the form $\mu X.\,F(X)$ , where $X$ does not fall in the scope of any fixed-point operator, but arbitrary closed subformulae may appear in $F$ . (This corresponds to the case of $n=1$ in the equation system of [1].) We show that no such formula has a closure ordinal $\eta_{F}$ satisfying $\omega^{2}\leq\eta_{F}<\omega_{1}$ , and moreover, it can be decided whether $\eta_{F}<\omega^{2}$ ; see Section 10. This is achieved via a well-known reduction of the $\mu$ -calculus to the MSO theory of the binary tree, based on the tree-model property [7], and a natural encoding of a tree model.

In the studies of topological complexity of MSO-definable tree languages, it has been also observed that dichotomies may help to solve decision problems. An open problem related to the aforementioned question of definability with finite-set quantifiers, is whether we can decide if a tree language belongs to the Borel hierarchy (in general, it need not). A positive answer is known if a tree language is given by a deterministic parity automaton [23], based on the following dichotomy: such a language is either $\Pi^{1}_{1}$ -complete (very hard), or on the level $\Pi^{0}_{3}$ (relatively low) of Borel hierarchy. Skrzypczak and Walukiewicz [28] gave a proof in the case when a tree language is given by a non-deterministic Büchi tree automaton, inspired by a rank-related dichotomy conjectured in the previous work of the first author [27, Conjecture 4.4]. There, an ordinal has been associated with each Büchi tree automaton, and it turns out (in view of [28]) that this ordinal either equals $\omega_{1}$ or is smaller than $\omega^{2}$ , in which case the tree language is Borel. It should be mentioned that a procedure to decide if a Büchi definable tree language is weakly definable was given earlier by Colcombet et al. [10].

Relation between ordinals and automata has been also considered in the studies of automatic structures. In particular, Delhommé [13] showed that automatic ordinals are smaller than $\omega^{\omega}$ while tree-automatic ordinals (defined in terms of automata on finite trees) can go higher, but not above $\omega^{\omega^{\omega}}$ . Later, Finkel and Todorcevic [17] showed that $\omega$ -tree automatic ordinals are smaller than $\omega^{\omega^{\omega}}$ as well. These results may appear in contrast with our more restrictive bound of $\omega^{2}$ ; however, representation by automatic structures is in general more powerful than expressibility in MSO, so the two approaches are not directly related.

2 Basic notions

$\mathbb{N}=\{0,1,2,\ldots\}$ denotes the set of natural numbers. We use standard notation for ordinal numbers, with $0$ being the least ordinal number, $\omega$ being the least infinite ordinal, and $\omega_{1}$ the least uncountable ordinal. Although $\omega$ and $\mathbb{N}$ coincide as sets, we distinguish the two notations to emphasise the perspective.

Words.

An alphabet $A$ is any finite non-empty set, whose elements are called letters. A word over $A$ is a finite sequence of letters $w=w_{0}\cdots w_{n-1}$ , with $w_{i}\in A$ for $i<n$ , and $n$ being the length of $w$ . The empty word, denoted $\varepsilon$ , is the unique word of length $0$ . By $u v$ we denote the concatenation of words $u=u_{0}\cdots u_{n-1}$ and $v=v_{0}\cdots v_{m-1}$ , that is, $uv=u_{0}\cdots u_{n-1}v_{0}\cdots v_{m-1}$ .

$A^{\ast}$ denotes the set of all finite words over the alphabet $A$ , while $A^{\omega}$ denotes the set of all $\omega$ -words over $A$ , that is, functions $\alpha\colon\mathbb{N}\to A$ . If $\alpha\in A^{\omega}$ is an infinite word and $n\in\mathbb{N}$ then by $\alpha{\upharpoonright}_{n}$ we denote the finite word consisting of the first $n$ letters of $\alpha$ , that is, $\alpha_{0}\cdots\alpha_{n-1}\in A^{\ast}$ .

Trees.

Let $\mathtt{{\scriptstyle L}}$ and $\mathtt{{\scriptstyle R}}$ denote two distinct letters called directions. For a direction $d\in\{\mathtt{{\scriptstyle L}},\mathtt{{\scriptstyle R}}\}$ , the opposite direction is denoted $\bar{d}\neq d$ . Words over the alphabet $\{\mathtt{{\scriptstyle L}},\mathtt{{\scriptstyle R}}\}$ are called nodes, with the empty word $\varepsilon$ often called the root. An $\omega$ -word $\alpha\in\{\mathtt{{\scriptstyle L}},\mathtt{{\scriptstyle R}}\}^{\omega}$ is called an infinite branch. A node $u$ is called the parent of its children $u\mathtt{{\scriptstyle L}}$ and $u\mathtt{{\scriptstyle R}}$ .

A (full infinite binary) tree over an alphabet $A$ is a function $t\colon\{\mathtt{{\scriptstyle L}},\mathtt{{\scriptstyle R}}\}^{\ast}\to A$ , assigning letters $t(u)\in A$ to nodes $u\in\{\mathtt{{\scriptstyle L}},\mathtt{{\scriptstyle R}}\}^{\ast}$ . The set of all trees over $A$ is denoted $\mathrm{Tr}_{A}$ . A subtree of a tree $t\in\mathrm{Tr}_{A}$ in a node $u\in\{\mathtt{{\scriptstyle L}},\mathtt{{\scriptstyle R}}\}^{\ast}$ is the tree $t{\upharpoonright}_{u}$ over $A$ defined by taking $t{\upharpoonright}_{u}(v)=t(uv)$ .

Automata.

Instead of working with formulae of MSO, we use another equivalent formalism, namely non-deterministic parity tree automata [29]. An automaton is a tuple $\mathcal{A}=(A,Q,q_{\mathrm{I}},\Delta,\Omega)$ , where $A$ is an alphabet, $Q$ is a finite set of states, $q_{\mathrm{I}}\in Q$ is an initial state, $\Delta\subseteq Q\times A\times Q\times Q$ is a transition relation, and $\Omega\colon Q\to\{i,\ldots,j\}\subseteq\mathbb{N}$ is a priority mapping. A run of an automaton $\mathcal{A}$ from a state $q\in Q$ over a tree $t\in\mathrm{Tr}_{A}$ is a tree $\rho\in\mathrm{Tr}_{Q}$ such that $\rho(\varepsilon)=q$ and for every node $u\in\{\mathtt{{\scriptstyle L}},\mathtt{{\scriptstyle R}}\}^{\ast}$ the quadruple

\big{(}\rho(u),t(u),\rho(u\mathtt{{\scriptstyle L}}),\rho(u\mathtt{{% \scriptstyle R}})\big{)},

is a transition of $\mathcal{A}$ (i.e., belongs to $\Delta$ ).

A sequence of states $(q_{0},q_{1},\ldots)\in Q^{\omega}$ is accepting if $\limsup_{n\to\infty}\Omega(q_{n})$ is an even natural number. A run $\rho$ is accepting if for every infinite branch $\alpha\in\{\mathtt{{\scriptstyle L}},\mathtt{{\scriptstyle R}}\}^{\omega}$ the sequence of states $\big{(}\rho(\alpha{\upharpoonright}_{n})\big{)}_{n\in\mathbb{N}}$ that appear in $\rho$ on $\alpha$ is accepting.

A tree $t\in\mathrm{Tr}_{A}$ is accepted by an automaton $\mathcal{A}$ from a state $q\in Q$ if there exists an accepting run $\rho$ of $\mathcal{A}$ from the state $q$ over $t$ . The language of $\mathcal{A}$ , denoted $\mathrm{L}(\mathcal{A})\subseteq\mathrm{Tr}_{A}$ , is the set of trees which are accepted by the automaton from the initial state $q_{\mathrm{I}}$ . A language $L\subseteq\mathrm{Tr}_{A}$ is regular if it is $\mathrm{L}(\mathcal{A})$ for some automaton $\mathcal{A}$ .

We now recall the famous theorem of Rabin, which allows us to transform MSO formulae into equivalent tree automata.

Theorem 2.1 ([25], see also [29]).

For every MSO formula $\varphi(X_{0},\ldots,X_{n-1})$ the set of valuations satisfying $\varphi$ is a regular language over the alphabet $\{0,1\}^{n}$ .

We say that an automaton is pruned if every state $q\in Q$ appears in some accepting run, that is, there exists an accepting run $\rho$ of $\mathcal{A}$ over a tree $t$ such that $\rho(u)=q$ for some node $u\in\{\mathtt{{\scriptstyle L}},\mathtt{{\scriptstyle R}}\}^{\ast}$ . Note that every automaton can effectively be pruned, without affecting its language, by detecting and removing states that do not appear in any accepting run.

Games.

We use the standard framework of two-player games of infinite duration (see e.g., [8, 16]). The arena of such a game is given as a graph with both players having perfect information about the current position. The winning condition of the game is given by a language of infinite plays won by one of the players.

Ranks.

Recall that an ordinal $\eta$ can be seen as the linearly ordered set of all ordinals smaller than $\eta$ . Given a set $X\subseteq\{\mathtt{{\scriptstyle L}},\mathtt{{\scriptstyle R}}\}^{*}$ , a counting function is a function $\mathfrak{C}\colon X\to\eta$ such that $\mathfrak{C}(u)<\mathfrak{C}(v)$ whenever $u\in X$ is a proper descendant of $v\in X$ (such a function exists for some $\eta$ whenever $X$ is well-founded). The rank of a well-founded set $X$ is the least ordinal $\eta$ for which a counting function from $X$ to $\eta$ exists.

Taking the automata-based perspective, instead of working with monadic variables $\vec{Y}$ and $X$ , we consider labellings of the tree by certain finite alphabets. In particular, a set of nodes $X\subseteq\{\mathtt{{\scriptstyle L}},\mathtt{{\scriptstyle R}}\}^{\ast}$ can be identified with its characteristic function, that is, a tree $x\in\mathrm{Tr}_{\{0,1\}}$ over the alphabet $\{0,1\}$ . Such a tree is well-founded if no infinite branch contains infinitely many nodes labelled by $1$ . The set of well-founded trees is denoted $\mathrm{WF}\subseteq\mathrm{Tr}_{\{0,1\}}$ . Likewise, we define the rank of $x\in\mathrm{WF}$ , denoted $\mathrm{rank}(x)$ , as the least $\eta$ for which there is a counting function from the set of $1$ -labelled nodes of $x$ to $\eta$ . The considered rank is analogous with the standard rank of well-founded trees (e.g., [21, Section 2.E]).

Example 2.2.

The tree $x_{0}\in\mathrm{Tr}_{\{0,1\}}$ with all nodes labelled by $0$ has rank $0$ .

Consider a tree $x_{\omega}$ where a node $v$ has label $1$ if $v=\mathtt{{\scriptstyle R}}^{i}\mathtt{{\scriptstyle L}}^{j}$ with $1\leq j\leq i$ . It is a comb: the rightmost branch is labelled by zeros, and below its $i$ -th node we have a tooth of $i$ nodes labelled by ones, going left. The rank of $x_{\omega}$ is $\omega$ .

Such combs can be nested: suppose that $x_{\omega\cdot 2}$ starts analogously to $x_{\omega}$ , but below every tooth we again insert $x_{\omega}$ (i.e., $x_{\omega\cdot 2}{\upharpoonright}_{\mathtt{{\scriptstyle R}}^{i}\mathtt{{% \scriptstyle L}}^{i+1}}=x_{\omega}$ for every $i$ ); then $\mathrm{rank}(x_{\omega\cdot 2})=\omega\cdot 2$ . Repeating this, we can insert $x_{\omega\cdot n}$ below every tooth of $x_{\omega}$ , and obtain $x_{\omega\cdot(n{+}1)}$ of rank $\omega\cdot(n{+}1)$ , for every $n\in\mathbb{N}$ .

Then, we can place every $x_{\omega\cdot n}$ at node $\mathtt{{\scriptstyle R}}^{n}\mathtt{{\scriptstyle L}}$ , below a $0$ -labelled rightmost branch; the resulting tree has rank $\omega^{2}$ . In a similar manner we can create a tree having rank equal to any countable ordinal $\eta$ .

3 Problem formulation

We begin by formulating the problem under consideration. Instead of working with a formula $\varphi(\vec{Y},X)$ , we assume that $A$ is some alphabet and $\Gamma$ is a regular language over the alphabet $A\times\{0,1\}$ . We identify a tree $\tau$ over $A\times\{0,1\}$ with a pair $(t,x)$ , where $t\in\mathrm{Tr}_{A}$ and $x\in\mathrm{Tr}_{\{0,1\}}$ such that $\tau(u)=\big{(}t(u),x(u)\big{)}$ for every node $u\in\{\mathtt{{\scriptstyle L}},\mathtt{{\scriptstyle R}}\}^{\ast}$ . Thus, $\Gamma\subseteq\mathrm{Tr}_{A\times\{0,1\}}$ can be seen as a relation whose elements are pairs $(t,x)$ . We additionally require that whenever $(t,x)\in\Gamma$ then $x$ is well-founded, which means that $\Gamma$ (treated as a relation) is contained in $\mathrm{Tr}_{A}\times\mathrm{WF}$ . We say that such a relation is regular if it is regular as a language over $A\times\{0,1\}$ .

Let $\pi_{A}(\Gamma)$ be the projection of $\Gamma$ onto the $A$ coordinate, that is, the set of those trees $t\in\mathrm{Tr}_{A}$ for which there exists a (necessarily well-founded) tree $x\in\mathrm{Tr}_{\{0,1\}}$ such that $(t,x)\in\Gamma$ . Similarly, for a tree $t\in\mathrm{Tr}_{A}$ by $\Gamma_{t}$ we denote the section of $\Gamma$ over the tree $t$ , that is, the set $\{x\in\mathrm{Tr}_{\{0,1\}}\mid(t,x)\in\Gamma\}$ .

The following definition is just a reformulation of Formula 1.1 in terms of a relation $\Gamma$ .

Definition 3.1.

The closure ordinal of a relation $\Gamma\subseteq\mathrm{Tr}_{A}{\times}\mathrm{WF}\subseteq\mathrm{Tr}_{A\times% \{0,1\}}$ (or of an automaton recognising it) is defined as

\eta_{\Gamma}\stackrel{{\scriptstyle\text{def}}}{{=}}\adjustlimits{\sup}_{\ t% \in\pi_{A}(\Gamma)\ }{\min}_{x\in\Gamma_{t}}\,\mathrm{rank}(x).

Example 3.2.

Consider the following automaton $\mathcal{A}$ over the alphabet $\{\mathsf{b},\mathsf{c}\}\times\{0,1\}$ . Its states are $p_{0},q_{1},q_{2},q_{3},r_{0},r_{1}$ with $q_{1}$ being initial, where the subscript provides the priority of a state (i.e., $\Omega(p_{i})=\Omega(q_{i})=\Omega(r_{i})=i$ ). The transitions are, for all $i\in\{0,1\}$ , $j\in\{1,2,3\}$ , and $a\in\{\mathsf{b},\mathsf{c}\}$ ,

$\displaystyle(p_{0},(a,0),p_{0},p_{0}),$	$\displaystyle(q_{j},(\mathsf{c},0),q_{3},p_{0}),$	$\displaystyle(q_{j},(\mathsf{c},0),p_{0},r_{0}),$
$\displaystyle(q_{j},(\mathsf{b},0),q_{2},p_{0}),$	$\displaystyle(q_{j},(\mathsf{c},0),p_{0},q_{3}),$	$\displaystyle(r_{i},(\mathsf{b},i),r_{1},r_{0}),$
$\displaystyle(q_{j},(\mathsf{b},0),p_{0},q_{1}),$	$\displaystyle(q_{j},(\mathsf{c},0),r_{0},p_{0}),$	$\displaystyle(r_{i},(\mathsf{c},0),p_{0},p_{0}).$

In this example, we should see $\mathsf{c}$ -labelled nodes as separators, splitting the whole tree into $\mathsf{b}$ -labelled fragments. Let us see when a pair $(t,x)\in\mathrm{Tr}_{\{\mathsf{b},\mathsf{c}\}\times\{0,1\}}$ can be accepted. Note first that $\mathcal{A}$ accepts $(t,x_{0})$ from $p_{0}$ for every tree $t$ , and for $x_{0}$ having all nodes labelled by $0$ . Next, observe that states $q_{j}$ become aligned along a single branch, either finite or infinite. If in $t$ there is a branch that infinitely often goes left, but visits only finitely many $\mathsf{c}$ -labelled nodes, then we can align the $q_{j}$ states along this branch, and $(t,x_{0})$ will be accepted. Indeed, just below every $\mathsf{c}$ we have $q_{3}$ (state of large odd priority; has to occur finitely often); below every $\mathsf{b}$ , if we go left we have $q_{2}$ , and if we go right we have $q_{1}$ (so the parity condition requires infinitely many left-turns). Another possibility is that the branch with states $q_{j}$ is finite, and below some $\mathsf{c}$ -labelled node the state changes to $r_{0}$ . Now the run sends $r_{1}$ to every left child, and $r_{0}$ to every right child; hence every left child in $x$ should have label $1$ , and every right child – label $0$ . We can continue the zone of states $r_{i}$ until reaching a node labelled by $\mathsf{c}$ ; such a node allows us to change the state into $p_{0}$ and accept anything below. The acceptance condition requires that there are only finitely many states $r_{1}$ (hence also nodes with label $1$ in $x$ ) on every branch; the tree $x$ is necessarily well-founded.

This determines the optimal rank of a witness $x$ for a tree $t$ . Namely, if in $t$ there is a branch that infinitely often goes left, but visits only finitely many $\mathsf{c}$ -labelled nodes, we have a witness of rank $0$ . Otherwise, we should consider every zone of $\mathsf{b}$ -labelled nodes in $t$ , surrounded by $\mathsf{c}$ -labelled nodes; consider $x$ having $1$ in every left child in that zone; and take the minimum of ranks of such trees $x$ , over all choices of zones (not including the topmost zone, above the first $\mathsf{c}$ on a branch). Thus, every witness of a tree $t$ has rank at least $\eta$ if and only if every such zone results in rank at least $\eta$ , and the former case does not hold. Such a tree exists for every $\eta<\omega_{1}$ , so the closure ordinal of $\mathcal{A}$ is $\omega_{1}$ .

4 The dichotomy game

We now move to the definition of the game $\mathcal{G}_{\mathcal{A}}$ designed to decide the dichotomy from Theorem 1.1.

Note that for every regular relation $\Gamma\subseteq\mathrm{Tr}_{A\times\{0,1\}}$ there exists another regular relation $\Gamma^{\prime}\subseteq\mathrm{Tr}_{A\times\{0,1\}}$ with the same closure ordinal, but such that $\pi_{A}(\Gamma^{\prime})$ is the set of all trees over $A$ . To see this, it is enough to take $\Gamma^{\prime}=\Gamma\cup\{(t,x^{\prime})\mid x^{\prime}\in\mathrm{WF}\land% \neg\exists x.(t,x)\in\Gamma\}$ . Then $\min_{x\in\Gamma_{t}}\,\mathrm{rank}(x)=\min_{x\in\Gamma^{\prime}_{t}}\,% \mathrm{rank}(x)$ for $t\in\pi_{A}(\Gamma)$ and $\min_{x\in\Gamma^{\prime}_{t}}\,\mathrm{rank}(x)=0$ for $t\not\in\pi_{A}(\Gamma)$ .

Towards the proof of Theorem 1.1, we consider some relation $\Gamma\subseteq\mathrm{Tr}_{A\times\{0,1\}}$ such that $\Gamma\subseteq\mathrm{Tr}_{A}\times\mathrm{WF}$ and $\pi_{A}(\Gamma)=\mathrm{Tr}_{A}$ . Reformulating Theorem 1.1, we need to show that either $\eta_{\Gamma}<\omega\cdot N$ for some $N\in\mathbb{N}$ , or $\eta_{\Gamma}=\omega_{1}$ , and we can effectively decide which case holds. We assume that $\Gamma$ is given by a pruned (i.e., all states appear in some accepting run) automaton $\mathcal{A}=(A,Q,q_{\mathrm{I}},\Delta,\Omega)$ .

First, a side is a symbol $s\in\{\mathsf{T},\mathsf{R}\}$ (which stands for “trunk” and “reach”), and a mode is a symbol $m\in\{\mathbf{\text{\leavevmode\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate\hbox{% \lower 1.8269pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p069% -Niwinski.latexml-figure0.pdf}}}}}},\mathbf{\text{\leavevmode\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\hbox{\lower 1.8269pt\hbox{{\leavevmode% \includegraphics{}{}{dagpub-tikzpictures/p069-Niwinski.latexml-figure1.pdf}}}}% }}\}$ (which stands for non-branching and binary-branching).

A quadruple $(\delta,s,m,d)\in\Delta\times\{\mathsf{T},\mathsf{R}\}\times\{\mathbf{\text{% \leavevmode\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\hbox{\lower 2.651pt\hbox{{% \leavevmode\includegraphics{}{}{dagpub-tikzpictures/p069-Niwinski.latexml-% figure2.pdf}}}}}},\mathbf{\text{\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{\lower 3.23169pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-% tikzpictures/p069-Niwinski.latexml-figure3.pdf}}}}}}\}\times\{\mathtt{{% \scriptstyle L}},\mathtt{{\scriptstyle R}}\}$ such that $s=\mathsf{R}$ implies $m=\mathbf{\text{\leavevmode\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\hbox{\lower 1.826% 9pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p069-Niwinski.la% texml-figure4.pdf}}}}}}$ (i.e., $m=\mathbf{\text{\leavevmode\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\hbox{\lower 1.826% 9pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p069-Niwinski.la% texml-figure5.pdf}}}}}}$ is allowed only for $s=\mathsf{T}$ ) is called a selector for $(\delta,s)$ , where $\delta$ is of the form $\big{(}q,(a,i),q_{\mathtt{{\scriptstyle L}}},q_{\mathtt{{\scriptstyle R}}}\big% {)}$ with $a\in A$ , $i\in\{0,1\}$ . Such a selector agrees with a direction $d^{\prime}\in\{\mathtt{{\scriptstyle L}},\mathtt{{\scriptstyle R}}\}$ if either $m=\mathbf{\text{\leavevmode\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\hbox{\lower 2.651% pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p069-Niwinski.lat% exml-figure6.pdf}}}}}}$ or $d^{\prime}=d$ (i.e., both directions $d^{\prime}$ are fine if $m=\mathbf{\text{\leavevmode\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\hbox{\lower 3.231% 69pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p069-Niwinski.l% atexml-figure7.pdf}}}}}}$ , but if $m=\mathbf{\text{\leavevmode\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\hbox{\lower 1.826% 9pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p069-Niwinski.la% texml-figure8.pdf}}}}}}$ then we require $d^{\prime}=d$ ). The output side of a selector $(\delta,s,m,d)$ in direction $d^{\prime}$ , where $\delta=(q,(a,i),q_{\mathtt{{\scriptstyle L}}},q_{\mathtt{{\scriptstyle R}}})$ , is

$\blacksquare$

$\mathsf{T}$ if $s=\mathsf{T}$ and $d^{\prime}=d$ , or $s=\mathsf{R}$ and $i=1$ , and
$\blacksquare$

$\mathsf{R}$ otherwise: if $s=\mathsf{T}$ and $d^{\prime}\neq d$ , or $s=\mathsf{R}$ and $i=0$ .

A state-flow is a triple $\big{(}(q,s),m,(q^{\prime},s^{\prime})\big{)}$ , where $q,q^{\prime}\in Q$ , $s,s^{\prime}\in\{\mathsf{T},\mathsf{R}\}$ , and $m\in\{\mathbf{\text{\leavevmode\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate\hbox{% \lower 1.8269pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p069% -Niwinski.latexml-figure9.pdf}}}}}},\mathbf{\text{\leavevmode\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\hbox{\lower 2.651pt\hbox{{\leavevmode% \includegraphics{}{}{dagpub-tikzpictures/p069-Niwinski.latexml-figure10.pdf}}}% }}}\}$ . A flow $\mu$ is a set of state-flows. The set $\big{\{}(q^{\prime},s^{\prime})\mid\big{(}(q,s),m,(q^{\prime},s^{\prime})\big{% )}\in\mu\big{\}}$ is called the image of $\mu$ . Note that the number of all possible state-flows, hence also of all possible flows, is finite.

Given a flow $\mu$ , we say that a flow $\bar{\mu}\subseteq\mu$ is a back-marking of $\mu$ if for every pair $(q^{\prime},s^{\prime})$ in the image of $\mu$ , precisely one state-flow leading to $(q^{\prime},s^{\prime})$ belongs to $\bar{\mu}$ . This state flow is called back-marked for $(q^{\prime},s^{\prime})$ .

Given a sequence of flows, $\mu_{1},\mu_{2},\dots$ we can define their composition as the graph with vertices $(q,s,n)\in Q\times\{\mathsf{T},\mathsf{R}\}\times\mathbb{N}$ and with a directed edge from $(q,s,n)$ to $(q^{\prime},s^{\prime},n{+}1)$ labelled by $m$ for every state-flow $\big{(}(q,s),m,(q^{\prime},s^{\prime})\big{)}\in\mu_{n+1}$ , $n\in\mathbb{N}$ . Note that in a flow there may be two state-flows with the same pairs $(q,s)$ and $(q^{\prime},s^{\prime})$ , with modes $m=\mathbf{\text{\leavevmode\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\hbox{\lower 3.231% 69pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p069-Niwinski.l% atexml-figure11.pdf}}}}}}$ and $m=\mathbf{\text{\leavevmode\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\hbox{\lower 1.826% 9pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p069-Niwinski.la% texml-figure12.pdf}}}}}}$ , leading to two parallel edges in this graph.

Assume that we are given a set $Q^{\prime}\subseteq Q$ and a letter $a\in A$ . By $\Delta_{a}(Q^{\prime})$ we denote the set of transitions of the form $\big{(}q,(a,i),q_{\mathtt{{\scriptstyle L}}},q_{\mathtt{{\scriptstyle R}}}\big% {)}$ with $q\in Q^{\prime}$ .

Finally, for two sets of states $T,R\subseteq Q$ we denote $\llparenthesis T,R\rrparenthesis\stackrel{{\scriptstyle\text{def}}}{{=}}(T{% \times}\{\mathsf{T}\})\cup(R{\times}\{\mathsf{R}\})$ . Note that every subset of $Q\times\{\mathsf{T},\mathsf{R}\}$ can be uniquely represented as $\llparenthesis T,R\rrparenthesis$ for some $T,R\subseteq Q$ .

We can now move to the definition of the crucial game $\mathcal{G}_{\mathcal{A}}$ , used to prove the desired dichotomy. The positions of $\mathcal{G}_{\mathcal{A}}$ are of the form $\llparenthesis T,R\rrparenthesis\subseteq Q\times\{\mathsf{T},\mathsf{R}\}$ (formally, one also needs additional auxiliary positions to represent the situation between particular steps of a round; we do not refer to these positions explicitly). The initial position is $\llparenthesis\{q_{\mathrm{I}}\},\emptyset\rrparenthesis$ , where $q_{\mathrm{I}}$ is the initial state of the automaton $\mathcal{A}$ . The consecutive steps in a round $n\in\mathbb{N}$ from a position $\llparenthesis T_{n},R_{n}\rrparenthesis$ are as follows:

1.

$\forall$ declares a subset $T_{n}^{\prime}\subseteq T_{n}$ .
2.

$\exists$ declares a letter $a_{n}\in A$ .
3.

$\exists$ declares a set $F_{n}$ of selectors, containing one selector for each $(\delta,s)\in(\Delta_{a_{n}}(T^{\prime}_{n}){\times}\{\mathsf{T}\})\cup(\Delta% _{a_{n}}(R_{n}){\times}\{\mathsf{R}\})$ .
4.

$\forall$ declares a direction $d_{n+1}\in\{\mathtt{{\scriptstyle L}},\mathtt{{\scriptstyle R}}\}$ .
5.

We define a flow $\mu_{n+1}$ as the set containing the state-flows $\big{(}(q,s),m,(q_{d_{n+1}},s^{\prime})\big{)}$ for each selector $(\delta,s,m,d)\in F_{n}$ that agrees with direction $d_{n+1}$ , where $s^{\prime}$ is the output side of the selector in the direction $d_{n+1}$ , and $\delta=(q,(a_{n},i),q_{\mathtt{{\scriptstyle L}}},q_{\mathtt{{\scriptstyle R}}})$ (so $q$ is the source state of $\delta$ and $q_{d_{n+1}}$ is the state sent by $\delta$ in direction $d_{n+1}$ ).
6.

$\forall$ declares some back-marking $\bar{\mu}_{n+1}$ of the flow $\mu_{n+1}$ .

The new position of the game, $\llparenthesis T_{n+1},R_{n+1}\rrparenthesis$ , is the image of the flow $\mu_{n+1}$ .

Given a play $\Pi$ of the game, the winning condition for $\exists$ is the disjunction A) ${}\lor{}$ B) of the following parts.

A): In the graph obtained as a composition of the back-markings $\bar{\mu}_{1},\bar{\mu}_{2},\dots$ there exists a path which infinitely many times changes sides between $\mathsf{T}$ and $\mathsf{R}$ .
B): In the graph obtained as a composition of the flows $\mu_{1},\mu_{2},\dots$ every infinite path either is rejecting or contains infinitely many state-flows of mode .

Above, while saying that a path going through $(q_{0},s_{0},0),(q_{1},s_{1},1),\dots$ is rejecting, we mean that the sequence of states $(q_{n})_{n\in\mathbb{N}}$ is rejecting, that is, $\limsup_{n\to\infty}\Omega(q_{n})$ is odd.

$\blacktriangleright$ Remark 4.1.

The arena of the game $\mathcal{G}_{\mathcal{A}}$ is finite and the winning condition defined above is $\omega$ -regular. Thus, the theorem of Büchi and Landweber [8] applies: one can effectively decide the winner of $\mathcal{G}_{\mathcal{A}}$ . Moreover, there exists a computable bound $M$ such that whoever wins $\mathcal{G}_{\mathcal{A}}$ , can win using a finite-memory strategy that uses at most $M$ memory states.

The following proposition formalises the relation between $\mathcal{G}_{\mathcal{A}}$ and Theorem 1.1.

Proposition 4.2.

Assume that $\mathcal{A}$ is a pruned automaton which recognises a relation $\Gamma\subseteq\mathrm{Tr}_{A}\times\mathrm{WF}$ such that $\pi_{A}(\Gamma)=\mathrm{Tr}_{A}$ (i.e., the projection of $\Gamma$ is full). Then, we have the following two implications:

1.

if player $\exists$ wins $\mathcal{G}_{\mathcal{A}}$ then $\eta_{\Gamma}=\omega_{1}$ ;
2.

if player $\forall$ wins $\mathcal{G}_{\mathcal{A}}$ then $\eta_{\Gamma}<\omega\cdot N$ , for a number $N\in\mathbb{N}$ computable based on the automaton $\mathcal{A}$ .

Figure 4.1: A depiction of a round of the game

\mathcal{G}_{\mathcal{A}}

.

Depiction of a round of $\mathcal{G}_{\mathcal{A}}$ .

Figure 4.1 depicts an example of a round of the game $\mathcal{G}_{\mathcal{A}}$ . First $\forall$ declares a subset $T^{\prime}_{n}=\{q_{0},q_{1}\}$ effectively removing the state $q_{2}$ from the $\mathsf{T}$ side. Note that some states might repeat on both sides. Once the letter $a_{n}=a$ is chosen by $\exists$ , there are six possible transitions from the considered states: one from each of them, except the state $q_{1}$ which has two possible transitions, $\delta_{1}$ over $(a,0)$ and $\delta_{2}$ over $(a,1)$ . $\exists$ declares a set of selectors

\displaystyle F_{n}=\Big{\{}

\displaystyle\big{(}\delta_{0},\mathsf{T},\mathbf{\text{\leavevmode\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\hbox{\lower 2.651pt\hbox{{\leavevmode% \includegraphics{}{}{dagpub-tikzpictures/p069-Niwinski.latexml-figure14.pdf}}}% }}},\mathtt{{\scriptstyle L}}\big{)},\big{(}\delta_{1},\mathsf{T},\mathbf{% \text{\leavevmode\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\hbox{\lower 3.23169pt\hbox{% {\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p069-Niwinski.latexml-% figure15.pdf}}}}}},\mathtt{{\scriptstyle L}}\big{)},\big{(}\delta_{2},\mathsf{% T},\mathbf{\text{\leavevmode\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\hbox{\lower 1.826% 9pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p069-Niwinski.la% texml-figure16.pdf}}}}}},\mathtt{{\scriptstyle R}}\big{)},\big{(}\delta_{3},% \mathsf{R},\mathbf{\text{\leavevmode\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate\hbox{% \lower 1.8269pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p069% -Niwinski.latexml-figure17.pdf}}}}}},\mathtt{{\scriptstyle L}}\big{)},\big{(}% \delta_{4},\mathsf{R},\mathbf{\text{\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{\lower 2.651pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-% tikzpictures/p069-Niwinski.latexml-figure18.pdf}}}}}},\mathtt{{\scriptstyle L}% }\big{)},\big{(}\delta_{5},\mathsf{R},\mathbf{\text{\leavevmode\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\hbox{\lower 3.23169pt\hbox{{\leavevmode% \includegraphics{}{}{dagpub-tikzpictures/p069-Niwinski.latexml-figure19.pdf}}}% }}},\mathtt{{\scriptstyle R}}\big{)}\Big{\}}.

Thus, the selectors for the transitions $\delta_{0}$ and $\delta_{2}$ are in the mode , while the remaining selectors are in the mode . Once $\forall$ chooses the direction $d_{n+1}=\mathtt{{\scriptstyle L}}$ , we gather into new sets $T_{n+1}$ and $R_{n+1}$ the states sent by the transitions in the direction $\mathtt{{\scriptstyle L}}$ . The transitions $\delta_{0}$ and $\delta_{1}$ provide their left states into $T_{n+1}$ . However, in the case of transition $\delta_{2}$ the direction of the selector is $\mathtt{{\scriptstyle R}}$ while the direction chosen by $\forall$ is $\mathtt{{\scriptstyle L}}$ and therefore the left state of this transition goes to $R_{n+1}$ . Regarding the transitions on the $\mathsf{R}$ side, $\delta_{3}$ provides its state to $T_{n+1}$ because this transition is over $(a,1)$ . The transition $\delta_{4}$ provides its state to $R_{n+1}$ because this transition is over $(a,0)$ . Finally, the transition $\delta_{5}$ does not provide its state anywhere, because its mode is and its direction is $\mathtt{{\scriptstyle R}}$ , different than the direction $\mathtt{{\scriptstyle L}}$ chosen by $\forall$ . The states provided by the transitions $\delta_{0}$ and $\delta_{1}$ are both $q^{\prime}_{0}$ and are therefore merged. This means that the final flow $\mu_{n+1}$ is

	$\displaystyle\Big{\{}\big{(}(q_{0},\mathsf{T}),\mathbf{\text{\leavevmode% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\hbox{\lower 3.23169pt\hbox{{% \leavevmode\includegraphics{}{}{dagpub-tikzpictures/p069-Niwinski.latexml-% figure23.pdf}}}}}},(q^{\prime}_{0},\mathsf{T})\big{)},\big{(}(q_{0},\mathsf{T}% ),\mathbf{\text{\leavevmode\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\hbox{\lower 1.826% 9pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p069-Niwinski.la% texml-figure24.pdf}}}}}},(q^{\prime}_{0},\mathsf{T})\big{)},\big{(}(q_{1},% \mathsf{T}),\mathbf{\text{\leavevmode\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate\hbox{% \lower 1.8269pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p069% -Niwinski.latexml-figure25.pdf}}}}}},(q^{\prime}_{2},\mathsf{R})\big{)},$
		$\displaystyle\hskip-70.0001pt\big{(}(q_{3},\mathsf{R}),\mathbf{\text{% \leavevmode\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\hbox{\lower 2.651pt\hbox{{% \leavevmode\includegraphics{}{}{dagpub-tikzpictures/p069-Niwinski.latexml-% figure26.pdf}}}}}},(q^{\prime}_{1},\mathsf{T})\big{)},\big{(}(q_{4},\mathsf{R}% ),\mathbf{\text{\leavevmode\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\hbox{\lower 3.231% 69pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p069-Niwinski.l% atexml-figure27.pdf}}}}}},(q^{\prime}_{3},\mathsf{R})\big{)}\Big{\}}.$

When $\forall$ chooses a back-marking $\bar{\mu}_{n+1}$ of the flow $\mu_{n+1}$ , he needs to make a choice which state-flow to select for the pair $(q^{\prime}_{0},\mathsf{T})$ as there are two possible choices.

5 Intuitions

Let us explain the intuitions behind the game. First very generally: the game is designed so that $\exists$ wins when there are trees $t$ requiring witnesses $x$ of arbitrarily large ranks. Conversely, $\forall$ wins if there is a bound $\eta$ such that every tree $t$ has a witness $x$ of rank at most $\eta$ . But because this is a finite game with an $\omega$ -regular winning condition, if $\forall$ wins then he wins with a finite-memory winning strategy; from such a strategy we can deduce that the bound $\eta$ is actually of the form $\omega\cdot N$ for some natural number $N$ depending on the size of the memory of $\forall$ .

Having the above in mind, let us discuss details of the game. The role of $\exists$ should be to show a tree $t$ (whose all witnesses $x$ have large rank), so we allow her to propose a label of a node in step 2. However, as usually in games, we do not continue in both children of the current node, but we rather ask $\forall$ to choose one direction ( $d_{n+1}$ in step 4), where $\exists$ has to continue creating the tree, and where $\forall$ thinks that it is impossible to continue.

Recall now that arbitrarily large countable ordinals can be obtained by alternately applying two operations in a well-founded way: add one, and take the supremum of infinitely many ordinals. Similarly, in a tree $x$ of a large rank, we can always find a comb: an infinite branch – a trunk – such that from infinitely many nodes on the side of this trunk we can reach a node labelled by $1$ , below which the rank is again large (but slightly smaller). In these places we can repeat this process, that is, again find an analogous comb, and so on, obtaining a tree of nested combs that is well-formed but itself has a large rank. Obviously the converse holds as well: such a tree of nested combs having large rank can exist inside $x$ only if $x$ has a large rank. Let us also remark that in the case of a finite-memory strategy of $\forall$ we obtain that such combs in $x$ can be nested at most $N\in\mathbb{N}$ times, which itself implies that the rank of $x$ is at most $\omega\cdot N$ .

Thus, in order to show that the constructed tree $t$ allows only witnesses $x$ of large rank, $\exists$ shows a nested comb structure. But this has to be done for every $x$ such that $(t,x)\in\Gamma$ , so, in a sense, for every run of $\mathcal{A}$ over $(t,x)$ for some $x$ . As usual, we cannot require from $\forall$ to choose a run on the fly, during the game; an interesting (even an accepting) run of $\mathcal{A}$ can only be fixed after the whole tree (i.e., the whole future of the play) is fixed. This means that during the game we have to trace all possible runs of $\mathcal{A}$ . However, there are infinitely many runs, so we cannot do that. To deal with that, we keep track of all “interesting” states in the sets $T_{n}$ , $R_{n}$ , and we consider all possible transitions from them in step 3. This makes the situation of $\exists$ a bit worse: she has to make decisions based only on the current state, not knowing the past of the run (the same state may emerge after two different run prefixes). But it turns out that $\exists$ can handle that; in our proof this corresponds to positionality of strategies in an auxiliary game considered in Section 7.

Now, how exactly does $\exists$ show the nested comb structure? This is done via selectors proposed in the sets $F_{n}$ . For states in $T_{n}$ (i.e., on the “trunk” side) $\exists$ has to show in which direction the trunk continues. Moreover, $\exists$ has to show places where on side of the trunk we can reach label $1$ followed by a nested comb; in these places $\exists$ plays mode (“branch”). If $\forall$ chooses a direction in which the trunk (as declared by $\exists$ ) continues, we trace the resulting state again on the $\mathsf{T}$ side. If he chooses the opposite direction, and the mode is (no branching here), we just stop tracing this run. But if $\forall$ chooses the non-trunk direction while the mode is , the resulting state ends up on the $\mathsf{R}$ (“reach”) side. The role of $\exists$ is now to show a direction in which we can reach a node with label $1$ . If $\forall$ follows this direction, and the label of $x$ is $0$ , we continue searching for label $1$ on the $\mathsf{R}$ side. When label $1$ is found, we put the resulting state on the $\mathsf{T}$ side; $\exists$ has to show a next comb. The B) part of the winning condition ensures for every accepting run that the trunk of each comb has infinitely many branching points (i.e., points with mode ) and that on the $\mathsf{R}$ side we stay only for finitely many steps (as mode does not occur there). Note that by arbitrarily composing transitions we may obtain also rejecting runs; the B) condition does not require anything for them.

There is one more issue taken into account in the design of the game: $\exists$ should be obliged to produce the combs nested arbitrarily many times, but not infinitely many times. The number of nestings (i.e., of switches between sides $\mathsf{T}$ and $\mathsf{R}$ ) is controlled by $\forall$ . When he is satisfied with the nesting depth provided by $\exists$ for runs ending in some state, he can remove this step from the position in step 1, and let $\exists$ provide appropriate comb structures only from remaining states (we allow this removal only on the $\mathsf{T}$ side, but we could equally well allow it on the $\mathsf{R}$ side, or on both sides). The A) part of the winning condition obliges $\forall$ to indeed remove a state after seeing finitely many nestings. To see the usefulness of back-marking used to formulate this condition, consider a situation with two runs leading to some state: one with already many nestings of combs provided by $\exists$ , and other where we are still on the trunk of the first comb. Because $\exists$ should provide many nested combs for all runs, in such a situation $\forall$ should still be able to analyse the latter run. To this end, he can select the latter run as the back-marked history of the considered state, and continue waiting for further nested combs, without worrying that he will lose by the A) part of the winning condition due to the former run.

Example 5.1.

Let us see how the game $\mathcal{G}_{\mathcal{A}}$ behaves for the automaton $\mathcal{A}$ from Example 3.2. Recall that the closure ordinal of $\mathcal{A}$ is $\omega_{1}$ , so $\exists$ should be able to win.

The strategy of $\exists$ from a position $\llparenthesis T_{n}^{\prime},R_{n}\rrparenthesis$ is as follows. If $T_{n}^{\prime}\cup R_{n}$ contains a state $r_{i}$ , then $\exists$ plays letter $\mathsf{b}$ , otherwise letter $\mathsf{c}$ . Then $\exists$ proposes selectors: transitions $\delta$ originating from states $q_{j}$ are handled by selectors $(\delta,s,m,d)$ with mode $m=\mathbf{\text{\leavevmode\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\hbox{\lower 1.826% 9pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p069-Niwinski.la% texml-figure33.pdf}}}}}}$ and with direction $d$ being such that $\delta$ sends state $p_{0}$ to the opposite direction $\bar{d}$ (i.e., $d=\mathtt{{\scriptstyle L}}$ for $\delta=(q_{j},(a,0),q_{2},p_{0})$ , etc.); transitions originating from $r_{i}$ are handled by direction $d=\mathtt{{\scriptstyle R}}$ , and by mode $m=\mathbf{\text{\leavevmode\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\hbox{\lower 2.651% pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p069-Niwinski.lat% exml-figure34.pdf}}}}}}$ on the $\mathsf{T}$ side and mode $m=\mathbf{\text{\leavevmode\immediate\immediate\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\hbox{\lower 3.231% 69pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-tikzpictures/p069-Niwinski.l% atexml-figure35.pdf}}}}}}$ on the $\mathsf{R}$ side. As we argue below, $p_{0}$ never becomes an element of $T_{n}\cup R_{n}$ , so transitions from $p_{0}$ need not to be handled.

The initial position is $\llparenthesis\{q_{1}\},\emptyset\rrparenthesis$ . Here $\exists$ plays letter $\mathsf{c}$ and some selectors with mode , and $\forall$ chooses a direction. There are two selectors $(\delta,s,m,d)$ that agree with this direction, and they send there states $q_{3}$ and $r_{0}$ . Thus the next position is $\llparenthesis\{q_{3},r_{0}\},\emptyset\rrparenthesis$ , reached by the flow $\{((q_{1},\mathsf{T}),\mathbf{\text{\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{\lower 1.8269pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-% tikzpictures/p069-Niwinski.latexml-figure37.pdf}}}}}},(q_{3},\mathsf{T})),((q_% {1},\mathsf{T}),\mathbf{\text{\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{\lower 2.651pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-% tikzpictures/p069-Niwinski.latexml-figure38.pdf}}}}}},(r_{0},\mathsf{T}))\}$ . This time $\exists$ plays letter $\mathsf{b}$ . If $\forall$ goes right, the new position is $\llparenthesis\{q_{1},r_{0}\},\emptyset\rrparenthesis$ , reached by the flow $\{((q_{3},\mathsf{T}),\mathbf{\text{\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{\lower 3.23169pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-% tikzpictures/p069-Niwinski.latexml-figure39.pdf}}}}}},(q_{1},\mathsf{T})),((r_% {0},\mathsf{T}),\mathbf{\text{\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{\lower 1.8269pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-% tikzpictures/p069-Niwinski.latexml-figure40.pdf}}}}}},(r_{0},\mathsf{T}))\}$ ; this position behaves identically to the previous one, as from $q_{1}$ and $q_{3}$ we have the same transitions. If $\forall$ goes left, the new position is $\llparenthesis\{q_{2}\},\{r_{1}\}\rrparenthesis$ , reached by the flow $\{((q_{3},\mathsf{T}),\mathbf{\text{\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{\lower 1.8269pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-% tikzpictures/p069-Niwinski.latexml-figure41.pdf}}}}}},(q_{2},\mathsf{T})),((r_% {0},\mathsf{T}),\mathbf{\text{\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{\lower 2.651pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-% tikzpictures/p069-Niwinski.latexml-figure42.pdf}}}}}},(r_{1},\mathsf{R}))\}$ . From $\llparenthesis\{q_{2}\},\{r_{1}\}\rrparenthesis$ once again letter $\mathsf{b}$ is played. Note that the only transition from $r_{1}$ reading letter $\mathsf{b}$ on the first coordinate, reads $1$ on the second coordinate. So, if $\forall$ goes right, the new position is back to $\llparenthesis\{q_{1},r_{0}\},\emptyset\rrparenthesis$ , reached by the flow $\{((q_{2},\mathsf{T}),\mathbf{\text{\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{\lower 3.23169pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-% tikzpictures/p069-Niwinski.latexml-figure43.pdf}}}}}},(q_{1},\mathsf{T})),((r_% {1},\mathsf{R}),\mathbf{\text{\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{\lower 1.8269pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-% tikzpictures/p069-Niwinski.latexml-figure44.pdf}}}}}},(r_{0},\mathsf{T}))\}$ ; if he goes left, he reaches $\llparenthesis\{q_{2}\},\emptyset\rrparenthesis$ , which behaves like the initial position.

It is also possible that $\forall$ erases a state from the $\mathsf{T}$ side (i.e., plays $T_{n}^{\prime}$ being a proper subset of $T_{n}$ ). If state $r_{0}$ is erased, we end up in a position $\llparenthesis\{q_{j}\},\emptyset\rrparenthesis$ , being like the initial position. We may also have positions $\llparenthesis\{r_{0}\},\emptyset\rrparenthesis$ and $\llparenthesis\emptyset,\{r_{1}\}\rrparenthesis$ , and flows $\{((r_{0},\mathsf{T}),\mathbf{\text{\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{\lower 1.8269pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-% tikzpictures/p069-Niwinski.latexml-figure45.pdf}}}}}},(r_{0},\mathsf{T}))\}$ , $\{((r_{0},\mathsf{T}),\mathbf{\text{\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{\lower 2.651pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-% tikzpictures/p069-Niwinski.latexml-figure46.pdf}}}}}},(r_{1},\mathsf{R}))\}$ , $\{((r_{1},\mathsf{R}),\mathbf{\text{\leavevmode\immediate\immediate\immediate% \immediate\immediate\immediate\immediate\immediate\immediate\immediate% \immediate\hbox{\lower 3.23169pt\hbox{{\leavevmode\includegraphics{}{}{dagpub-% tikzpictures/p069-Niwinski.latexml-figure47.pdf}}}}}},(r_{0},\mathsf{T}))\}$ between them. Finally, we may also reach $\llparenthesis\emptyset,\emptyset\rrparenthesis$ .

Note that in our example there is always only one state-flow leading to every pair $(q,s)$ ; in consequence, every state-flow is back-marked.

Let us now check the winning condition. One possibility is that infinitely many letters $\mathsf{c}$ were played. In these moments no state $r_{i}$ was present in the position, so the only infinite path in the composition of flows is the path going through appropriate $q_{j}$ states. But after seeing every $\mathsf{c}$ this state was $q_{3}$ , so the path is rejecting; part B) of the winning condition is satisfied (we may also have no infinite path, if the $q_{j}$ state was removed by $\forall$ , but then condition B) holds even more). The opposite case is that from some moment on, only letter $\mathsf{b}$ was played. We then also have an infinite path going, from some moment, through the $r_{i}$ states (this path really exists: if $\forall$ removes the state $r_{0}$ , then letter $\mathsf{c}$ is played). Note that whenever $\forall$ goes left, this path changes sides from $\mathsf{T}$ to $\mathsf{R}$ , and in the next round returns back to the $\mathsf{T}$ side. If this happens infinitely often, $\exists$ wins by condition A). Otherwise, from some moment on $\forall$ constantly goes right. After that, the path going through the $r_{i}$ states has all state-flows of mode , and the other path (if exists) remains in state $q_{1}$ , so it is rejecting; condition B) is satisfied.

6 Soundness

We begin by proving Item 1 of Proposition 4.2: if $\exists$ wins $\mathcal{G}_{\mathcal{A}}$ then $\eta_{\Gamma}=\omega_{1}$ . To this end, assume that $\exists$ wins the game and fix any winning strategy for her. For every countable ordinal $\eta>0$ , our goal is to construct a tree $t$ such that $\mathrm{rank}(x)\geq\eta$ whenever $(t,x)\in\Gamma$ . We do this by inductively unravelling the fixed strategy of $\exists$ . During this process, we keep track of

$\blacksquare$

the current node $v\in\{\mathtt{{\scriptstyle L}},\mathtt{{\scriptstyle R}}\}^{\ast}$ ,
$\blacksquare$

the current position $\llparenthesis T_{v},R_{v}\rrparenthesis$ of the game,
$\blacksquare$

a mapping $\kappa_{v}$ , which assigns some ordinals $\leq\eta$ to all elements of the set $\llparenthesis T_{v},R_{v}\rrparenthesis$ .

Initially $v=\varepsilon$ , the position $\llparenthesis T_{\varepsilon},R_{\varepsilon}\rrparenthesis$ is the initial position of the game (i.e., $\llparenthesis\{q_{\mathrm{I}}\},\emptyset\rrparenthesis$ ), and $\kappa_{\varepsilon}=\{(q_{\mathrm{I}},\mathsf{T})\mapsto\eta\}$ . Then, in every node $v$ , the letter declared by $\exists$ provides a label of this node in $t$ , and while moving to a child $v d$ of $v$ we trace a play in which $\forall$ declares the respective direction $d$ . What remains is to declare the remaining choices of $\forall$ and say how the mapping $\kappa_{v}$ is updated. The role of the ordinal $\kappa_{v}(q,s)$ is to provide a lower bound for ranks of witnesses $x$ such that $(t{\upharpoonright}_{v},x)$ can be accepted by $\mathcal{A}$ from the state $q$ . While going down the tree, this ordinal decreases whenever we change the side from $\mathsf{T}$ to $\mathsf{R}$ ; when it becomes $0$ , $\forall$ removes the respective state from the set $T_{v}$ in his move. The back-markings are declared by $\forall$ in a way that maximises the ordinals $\kappa_{v}(q,s)$ of the respective state-flows.

It remains to show that if $(t,x)\in\Gamma$ then $\mathrm{rank}(x)\geq\eta$ . This is achieved by considering any accepting run $\rho$ of $\mathcal{A}$ over $(t,x)$ . Since all possible transitions of $\mathcal{A}$ are taken into account in each round of $\mathcal{G}_{\mathcal{A}}$ , one can trace the run $\rho$ in the simulated plays of $\mathcal{G}_{\mathcal{A}}$ . The policy of updating the mapping $\kappa_{v}$ inductively assures that for every node $v$ and currently traced side $s_{v}$ we have $(\rho(v),s_{v})\in\llparenthesis T_{v},R_{v}\rrparenthesis$ and $\mathrm{rank}(x{\upharpoonright}_{v})\geq\kappa_{v}(\rho(v),s_{v})$ . Moreover, this policy guarantees that condition A) is never satisfied in these plays. Thus, condition B) must hold, inductively guaranteeing the inequality on $\mathrm{rank}(x{\upharpoonright}_{v})$ .

7 Auxiliary game

Before moving towards a proof of the other implication, we need to be able to construct reasonable strategies of $\exists$ in $\mathcal{G}_{\mathcal{A}}$ . This is achieved by considering an auxiliary game, based directly on $\mathcal{G}_{\mathcal{A}}$ , when considering a single transition of $\mathcal{A}$ at each round. The players of the game are called Automaton (responsible for choosing transitions and choices of $\forall$ in $\mathcal{G}_{\mathcal{A}}$ ) and Pathfinder (responsible for choices of $\exists$ in $\mathcal{G}_{\mathcal{A}}$ ). The game is denoted $\mathcal{H}_{\mathcal{A},t,N}$ and depends on the fixed automaton $\mathcal{A}$ , a tree $t\in\mathrm{Tr}_{A}$ , and a number $N\in\mathbb{N}$ . Positions of $\mathcal{H}_{\mathcal{A},t,N}$ are triples $(v,q,s)\in\{\mathtt{{\scriptstyle L}},\mathtt{{\scriptstyle R}}\}^{\ast}\times Q% \times\{\mathsf{T},\mathsf{R}\}$ , plus some additional auxiliary positions, to which we do not refer explicitly.

For a node $v\in\mathrm{dom}(t)$ and a state $q\in Q$ define

\mathrm{val}_{t}(v,q)=\inf\big{\{}\mathrm{rank}(x)\mid\text{$(t{% \upharpoonright}_{v},x)$ can be accepted from $q$}\big{\}}.

We assume $\inf\emptyset=\infty$ (which is greater than all ordinals).

In positions $(v,q,s)$ such that $\mathrm{val}_{t}(v,q)=0$ the game reaches an immediate victory in which Pathfinder wins. A round from a position $(v,q,s)$ such that $\mathrm{val}_{t}(v,q)>0$ consists of the following steps:

1.

Automaton declares a transition $\delta=(q,(t(v),i),q_{\mathtt{{\scriptstyle L}}},q_{\mathtt{{\scriptstyle R}}})$ from the current state $q$ over $(t(v),i)$ for some $i\in\{0,1\}$ .
2.

Pathfinder declares a selector $(\delta,s,m,d)$ for $(\delta,s)$ .
3.

Automaton declares a direction $d^{\prime}$ that agrees with the selector.

Let $v^{\prime}=vd^{\prime}$ , $q^{\prime}=q_{d^{\prime}}$ , and let $s^{\prime}$ be the output side of the selector in the direction $d^{\prime}$ . Now, for every possible number $k\leq N$ , the following four conditions of immediate victory may end the game, making Automaton win:

$\displaystyle s=\mathsf{T}$	$\displaystyle\ \land\ \mathrm{val}_{t}(v,q)\geq\omega\cdot k$	$\displaystyle\ \land\ s^{\prime}=\mathsf{T}$	$\displaystyle\ \land\$	$\displaystyle\mathrm{val}_{t}(v^{\prime},q^{\prime})<\omega\cdot k,$
$\displaystyle s=\mathsf{T}$	$\displaystyle\ \land\ \mathrm{val}_{t}(v,q)\geq\omega\cdot k$	$\displaystyle\ \land\ s^{\prime}=\mathsf{R}$	$\displaystyle\ \land\$	$\displaystyle\mathrm{val}_{t}(v^{\prime},q^{\prime})\leq\omega\cdot(k{-}1),$
$\displaystyle s=\mathsf{R}$	$\displaystyle\ \land\ \mathrm{val}_{t}(v,q)>\omega\cdot k$	$\displaystyle\ \land\ s^{\prime}=\mathsf{R}$	$\displaystyle\ \land\$	$\displaystyle\mathrm{val}_{t}(v^{\prime},q^{\prime})\leq\omega\cdot k,$
$\displaystyle s=\mathsf{R}$	$\displaystyle\ \land\ \mathrm{val}_{t}(v,q)>\omega\cdot k$	$\displaystyle\ \land\ s^{\prime}=\mathsf{T}$	$\displaystyle\ \land\$	$\displaystyle\mathrm{val}_{t}(v^{\prime},q^{\prime})<\omega\cdot k.$

If no immediate victory happened, the game proceeds to the new position which is $(v^{\prime},q^{\prime},s^{\prime})$ . Note that the conditions of immediate victory depend only on $(v,q,s)$ and $(v^{\prime},q^{\prime},s^{\prime})$ , so can be directly hardwired in the structure of the game.

An infinite play (i.e., without any immediate victory) of $\mathcal{H}_{\mathcal{A},t,N}$ is won by Pathfinder if the sequence of visited states is rejecting or a selector with mode is played infinitely often.

The main result about $\mathcal{H}_{\mathcal{A},t,N}$ is the following lemma. First, the winning condition of $\mathcal{H}_{\mathcal{A},t,N}$ guarantees that if Pathfinder wins the game then he wins it positionally. To prove that he wins, one assumes that Automaton wins from some position, which leads to a contradiction.

Lemma 7.1.

Pathfinder has a positional strategy in $\mathcal{H}_{\mathcal{A},t,N}$ that is winning from every position of the game (we call such a strategy uniform).

8 Completeness

We now move to the proof of Item 2 of Proposition 4.2: if $\forall$ wins $\mathcal{G}_{\mathcal{A}}$ then $\eta_{\Gamma}<\omega\cdot N$ for some computable $N\in\mathbb{N}$ . First observe the following important consequence of the winning condition of the game.

Proposition 8.1.

There exists a computable bound $N\in\mathbb{N}$ such that if $\forall$ wins $\mathcal{G}_{\mathcal{A}}$ then he has a winning strategy that guarantees the following. In every play $\Pi$ (either finite or infinite) consistent with this strategy, every path in the graph obtained as the composition of back-markings $\bar{\mu}_{1},\bar{\mu}_{2},\dots$ contains less than $N$ changes of sides from $\mathsf{T}$ to $\mathsf{R}$ .

Compute the bound $N$ as above. Assume that $\forall$ wins the game $\mathcal{G}_{\mathcal{A}}$ and fix his winning strategy satisfying the thesis of the above Proposition. We claim that then the closure ordinal of the automaton is bounded by $\omega\cdot N$ . Assume for the sake of contradiction that there exists a tree $t$ which does not have a witnessing tree $x$ of rank smaller than $\omega\cdot N$ . The above assumption about $t$ implies that $\mathrm{val}_{t}(\varepsilon,q_{\mathrm{I}})\geq\omega\cdot N$ .

Based on the tree $t$ , we now construct a play that is consistent with the fixed $\forall$ ’s strategy, but is won be $\exists$ , leading to a contradiction. Together with the current position of the game, $\llparenthesis T_{n},R_{n}\rrparenthesis$ , we store some node $v_{n}$ of the tree, starting with $v_{0}=\varepsilon$ . In order to construct the play, we need to provide choices of $\exists$ : she declares a letter based on the label of $v_{n}$ in the fixed tree $t$ , and a set of selectors based on a fixed uniform positional strategy $\pi_{0}$ of Pathfinder in $\mathcal{H}_{\mathcal{A},t,N}$ , given by Lemma 7.1. The current node $v_{n}$ is then updated according to the direction declared by $\forall$ in $\mathcal{G}_{\mathcal{A}}$ .

For a pair $(q,s)\in\llparenthesis T_{n},R_{n}\rrparenthesis$ denote by $\mathrm{hist}_{n}(q,s)$ the number of switches from the side $\mathsf{T}$ to the side $\mathsf{R}$ on the back-marked history of $(q,s)$ . We keep a val-preserving invariant saying that for every pair $(q,s)\in\llparenthesis T_{n},R_{n}\rrparenthesis$ with $k=N-\mathrm{hist}_{n}(q,s)$ either

1.

$s=\mathsf{T}$ and $\mathrm{val}_{t}(v_{n},q)\geq\omega\cdot k$ , or
2.

$s=\mathsf{R}$ and $\mathrm{val}_{t}(v_{n},q)>\omega\cdot k$ .

Note that the val-preserving invariant is initially met, because $\mathrm{val}_{t}(\varepsilon,q_{\mathrm{I}})\geq\omega\cdot N$ . Note also that always $k>0$ because Proposition 8.1 implies that $\mathrm{hist}_{n}(q,s)<N$ . The fact that the Pathfinder’s strategy $\pi_{0}$ is winning in $\mathcal{H}_{\mathcal{A},t,N}$ can be used to deduce that the constructed play is won by $\exists$ in $\mathcal{G}_{\mathcal{A}}$ . This concludes the proof of Proposition 4.2, hence also of Theorem 1.1.

9 Definability of ranks in MSO

We now move to a study of definability of particular rank bounds in MSO.

With some analogy to the cardinality quantifier by Bárány et al. [3], one can propose a quantifier $\exists^{\leq\eta}X.\,\varphi(\vec{Y},X)$ , expressing that there exists a well-founded set $X$ of rank at most $\eta$ such that $\varphi(\vec{Y},X)$ holds. Note that this can be equivalently rewritten using the predicate $\mathrm{rank}(X)\leq\eta$ , defined by $\exists^{\leq\eta}Z.\,X=Z$ . Below we show that the predicate $\mathrm{rank}(X)\leq\eta$ , and consequently the respective quantifier, cannot be expressed in MSO except for the basic case of natural numbers (or $\omega_{1}$ ). Definability of this predicate in MSO boils down to checking if the following language is regular:

L_{\leq\eta}\stackrel{{\scriptstyle\text{def}}}{{=}}\big{\{}x\in\mathrm{Tr}_{% \{0,1\}}\mid\mathrm{rank}(x)\leq\eta\big{\}}.

Clearly, $\mathrm{rank}(x)<\omega_{1}$ holds for every well-founded tree, thus it remains to consider $\eta<\omega_{1}$ .

We first show that these languages are regular for $\eta<\omega$ .

Fact 9.1.

For every $l<\omega$ the language $L_{\leq l}$ is regular.

Going beyond $\omega$ , the languages stop being regular. First, a simple pumping argument shows the following.

Lemma 9.2.

For all ordinals $\eta<\omega_{1}$ and all $l<\omega$ the language $L_{\leq\eta+\omega+l}$ is not regular.

The argument from Lemma 9.2 applies in particular to all ordinals $\eta$ such that $\omega\leq\eta<\omega^{2}$ , whereas the ordinals $\eta\geq\omega^{2}$ are covered by Theorem 1.1. Thus we may conclude.

Corollary 9.3.

For an ordinal $\eta<\omega_{1}$ the language $L_{\leq\eta}$ is regular if and only if $\eta<\omega$ .

The above Corollary does not exclude the possibility that a higher ordinal $\eta$ may be a supremum of a regular subset of $L_{\leq\eta}$ .

Lemma 9.4.

For each pair of natural numbers $k$ , $l$ there exists a regular language $L\subseteq\mathrm{WF}$ such that $\sup_{x\in L}\mathrm{rank}(x)=\omega\cdot k+l$ .

$\blacktriangleright$ Remark 9.5.

Clearly no countable formalism can define all the languages $L_{\leq\eta}$ for $\eta<\omega_{1}$ . However, certain formalisms can go beyond MSO. For instance, the logic WMSO+U (for which the satisfiability problem is known to be decidable [4]) is capable of defining the language $L_{\leq\omega}$ : a tree $x$ has rank at most $\omega$ if below every node $u$ labelled by $1$ there is a bound $K$ on the number of nodes labelled by $1$ that can appear on branches of $x$ passing through $u$ . This construction can be iterated to define the languages $L_{\leq\omega\cdot k+l}$ and possibly even beyond that.

10 Closure ordinals

In this section we show how a negative answer to Czarnecki’s question on closure ordinals can be derived from the present result. We use the standard syntax and semantics of modal $\mu$ -calculus [7], with its formulae constructed using the following grammar:

F::=a\mid X\mid\mu X.\,F\mid\nu X.\,F\mid F_{1}\lor F_{2}\mid F_{1}\land F_{2}% \mid\Diamond F\mid\Box F,

where $a\in A$ is a letter from a fixed alphabet, $X$ is a variable from some fixed set of variables, $\mu$ and $\nu$ are the least and the greatest fixed-point operators, and $\Diamond$ and $\Box$ are the standard modalities (“exists a successor” and “for all successors”). For technical convenience we make an assumption that, in each point of our model, exactly one proposition (letter in $A$ ) is satisfied. For the sake of readability we often identify a formula with its semantics, that is, we read a closed formula as a subset of the domain, and a formula with $k$ free variables as a $k$ -ary function over its powerset.

Given an ordinal number $\eta$ , we use the standard notation $\mu^{\eta}X.\,F(X)$ for the $\eta$ -approximation of the fixed point in a given model (which amounts to the $\eta$ ’s iteration $F^{\eta}(\emptyset)$ ). Given a model $\tau$ , we define the closure ordinal of $\mu X.\,F(X)$ in $\tau$ as the least ordinal $\eta$ such that $\mu X.\,F(X)=\mu^{\eta}X.\,F(X)$ . Then, the closure ordinal of $\mu X.\,F(X)$ (as considered in 1.2) is the supremum of these ordinals over all models $\tau$ (or $\infty$ if the supremum does not exist). We aim at providing an (alternative to Afshari, Barlucchi, and Leigh [1]) proof of the following Theorem.

Theorem 10.1.

Let $F(X)$ be a $\mu$ -calculus formula in which the variable $X$ does not occur in scope of any fixed-point operator. Then, the closure ordinal of $\mu X.\,F(X)$ is either strictly smaller than $\omega^{2}$ , or at least $\omega_{1}$ and it can be effectively decided which of the cases holds.

Note that we allow arbitrary closed formulae of $\mu$ -calculus to be nested in $F$ ; however, we do not cover the whole $\mu$ -calculus, because of the restriction on occurrences of $X$ . This stays in line with the fragment considered by Afshari, Barlucchi, and Leigh [1] (as explained in Section 1), but we additionally provide a decision procedure that makes the dichotomy effective.

Towards a proof of Theorem 10.1, as a first step, we eliminate from $F$ all occurrences of $X$ that are not in scope of any modal operator; this can be done without changing the closure ordinal. Next, using standard techniques we obtain the following Lemma.

Lemma 10.2.

Let $F(X)$ be a formula as in Theorem 10.1, with all occurrences of $X$ being in scope of a modal operator. The following three conditions are equivalent for every countable limit ordinal $\eta$ :

1.

the closure ordinal of $\mu X.\,F(X)$ is bounded by $\eta$ ;
2.

for every model $\tau$ that is a countable tree with its root in $\mu X.\,F(X)$ , this root belongs to $\mu^{\eta}X.\,F(X)$ ;
3.

for every model $\tau$ that is a countable tree with its root in $\mu X.\,F(X)$ , there exists a well-founded set $Z\subseteq\mathrm{dom}(\tau)$ containing the root, such that $F(Z)\supseteq Z$ and $\mathrm{rank}(Z)\leq\eta$ .

A countable tree $\tau$ , occurring in Items 2 and 3 above, can be seen as a function $\tau\colon X\to A$ from a prefix-closed subset $X\subseteq\mathbb{N}^{\ast}$ to a finite alphabet $A$ . Now, recall a natural encoding $(n_{1},n_{2},\ldots,n_{k})\mapsto\mathtt{{\scriptstyle R}}^{n_{1}}\mathtt{{% \scriptstyle L}}\mathtt{{\scriptstyle R}}^{n_{2}}\mathtt{{\scriptstyle L}}% \cdots\mathtt{{\scriptstyle R}}^{n_{k}}\mathtt{{\scriptstyle L}}$ of $\mathbb{N}^{\ast}$ into $\{\mathtt{{\scriptstyle L}},\mathtt{{\scriptstyle R}}\}^{\ast}$ . This encoding preserves the prefix order on $\mathbb{N}^{\ast}$ and moreover preserves ranks of well-founded sets. Take the relation $\Gamma_{F}$ that contains $(t,x)\in\mathrm{Tr}_{A}\times\mathrm{Tr}_{\{0,1\}}$ if:

$\blacksquare$

$t$ encodes a model $\tau$ ,
$\blacksquare$

$x$ encodes a set $Z\subseteq\mathrm{dom}(\tau)$ ,
$\blacksquare$

the root of $\tau$ belongs to $\mu X.\,F(X)$ ,
$\blacksquare$

the root of $\tau$ belongs to $Z$ , and $F(Z)\supseteq Z$ .

The $\mu$ -calculus formulae $F(Z)$ and $\mu X.\,F(X)$ can be rewritten into MSO [7] and then modified to read the above encoding of $\tau$ in the binary tree, instead of $\tau$ itself. It follows that the relation $\Gamma_{F}$ is MSO-definable.

Observe that Item 3 of Lemma 10.2 can be rephrased by saying that the closure ordinal of $\Gamma_{F}$ is bounded by $\eta$ . Applying Theorem 1.1 to $\Gamma_{F}$ , and then Lemma 10.2, we have one of two possibilities: If the closure ordinal of $\Gamma_{F}$ is smaller than $\omega^{2}$ , then it is bounded by $\omega\cdot N$ for some $N\in\mathbb{N}$ ; then also the closure ordinal of $\mu X.\,F(X)$ is bounded by $\omega\cdot N<\omega^{2}$ . Otherwise, the closure ordinal of $\Gamma_{F}$ is $\omega_{1}$ , so it is not bounded by any countable limit ordinal; then also the closure ordinal of $\mu X.\,F(X)$ is not bounded by any countable limit ordinal, hence it is at least $\omega_{1}$ . This concludes the proof of Theorem 10.1.

$\blacktriangleright$ Remark 10.3.

One may ask if Theorem 10.1 is merely a consequence or it is in some sense equivalent to our main result Theorem 1.1. To the best of our understanding, Theorem 10.1 does not transfer back to the general realm of MSO-definable relations, as in Theorem 1.1. One of the reasons is that the iterations of fixed points are required to proceed in a monotone fashion, driven by the internal formula $F$ ; while in full MSO one can express arbitrary correspondence between the parameters $\vec{Y}$ and a well-founded witness $X$ .

11 Conclusions

This work contributes to the study of expressive power of the MSO theory of binary tree. We investigate to what extent this theory can express properties of well-founded trees, and in particular distinguish between their ordinal ranks. We observe that the ability of explicit expression of properties of ranks is practically limited to statements of the form: all trees $X$ satisfying $\varphi(X)$ have $\mathrm{rank}(X)<N$ , for a fixed $N\in\mathbb{N}$ (cf. Corollary 9.3 above). However the implicit expressive power of MSO logic goes much higher. In particular, our main result (Theorem 1.1) allows us to decide whether the property

\exists X.\,\varphi(\vec{Y},X)\;\wedge\;X\mbox{ is well\nobreak\hbox{-}% \nobreak\thinspace\ignorespaces founded with }\mathrm{rank}(X)<\omega^{2},

is generally true (for all $\vec{Y}$ ), although the property itself is not expressible in MSO.

There is, however, a number of questions that remain to be answered. As ordinals smaller than $\omega^{2}$ can be effectively represented, we would like to have an effective procedure that, given a formula $\varphi$ , computes the exact bound, that is, (a representation of) the least ordinal $\eta_{\varphi}$ that can be substituted for $\omega^{2}$ in the construction above. Even more elementarily, given an MSO-definable set $L$ of well-founded trees, we would like to compute the supremum of ranks of trees in $L$ . These questions are subjects of ongoing research.

A more far-reaching direction is to relate the techniques of the present paper to the open problem of computing the Mostowski index, mentioned in Introduction. The parity condition itself imposes well-foundedness restriction on the occurrences of each odd label $m$ in the fragments of tree where this label is the highest. Colcombet and Löding [11] have approached the index problem (still unsolved) by reducing it to the boundedness problem for distance automata (see also Idir and Lehtinen [20] for a simplified version of this reduction). One may consider an alternative approach towards the index problem by studying the ordinal ranks which arise from the well-foundedness restriction of the parity condition.

References

[1] Bahareh Afshari, Giacomo Barlucchi, and Graham E. Leigh. The limit of recursion in state-based systems. In FICS, 2024. URL: https://www.irif.fr/_media/users/saurin/fics2024/pre-proceedings/fics-2024-afshari-etal.pdf.
[2] Bahareh Afshari and Graham E. Leigh. On closure ordinals for the modal mu-calculus. In CSL, volume 23 of LIPIcs, pages 30–44. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2013. doi:10.4230/LIPICS.CSL.2013.30.
[3] Vince Bárány, Łukasz Kaiser, and Alexander M. Rabinovich. Expressing cardinality quantifiers in monadic second-order logic over trees. Fundam. Inform., 100(1-4):1–17, 2010. doi:10.3233/FI-2010-260.
[4] Mikołaj Bojańczyk. Weak MSO+U with path quantifiers over infinite trees. In ICALP (2), volume 8573 of Lecture Notes in Computer Science, pages 38–49. Springer, 2014. doi:10.1007/978-3-662-43951-7_4.
[5] Julian C. Bradfield. Simplifying the modal mu-calculus alternation hierarchy. In STACS, volume 1373 of Lecture Notes in Computer Science, pages 39–49. Springer, 1998. doi:10.1007/BFB0028547.
[6] Julian C. Bradfield, Jacques Duparc, and Sandra Quickert. Transfinite extension of the mu-calculus. In CSL, volume 3634 of Lecture Notes in Computer Science, pages 384–396. Springer, 2005. doi:10.1007/11538363_27.
[7] Julian C. Bradfield and Igor Walukiewicz. The mu-calculus and model checking. In Handbook of Model Checking, pages 871–919. Springer, 2018. doi:10.1007/978-3-319-10575-8_26.
[8] Julius R. Büchi and Lawrence H. Landweber. Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society, 138:295–311, 1969.
[9] Lorenzo Clemente and Michał Skrzypczak. Deterministic and game separability for regular languages of infinite trees. In ICALP, volume 198 of LIPIcs, pages 126:1–126:15. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPICS.ICALP.2021.126.
[10] Thomas Colcombet, Denis Kuperberg, Christof Löding, and Michael Vanden Boom. Deciding the weak definability of Büchi definable tree languages. In CSL, volume 23 of LIPIcs, pages 215–230. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2013. doi:10.4230/LIPICS.CSL.2013.215.
[11] Thomas Colcombet and Christof Löding. The non-deterministic Mostowski hierarchy and distance-parity automata. In ICALP (2), volume 5126 of Lecture Notes in Computer Science, pages 398–409. Springer, 2008. doi:10.1007/978-3-540-70583-3_33.
[12] Marek Czarnecki. How fast can the fixpoints in modal mu-calculus be reached? In FICS, pages 35–39. Laboratoire d’Informatique Fondamentale de Marseille, 2010. URL: https://hal.archives-ouvertes.fr/hal-00512377/document#page=36.
[13] Christian Delhommé. Automaticité des ordinaux et des graphes homogènes. Comptes Rendus de L’Académie des Sciences, Mathématiques, 339(1):5–10, 2004.
[14] Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Derivation tree analysis for accelerated fixed-point computation. Theor. Comput. Sci., 412(28):3226–3241, 2011. doi:10.1016/J.TCS.2011.03.020.
[15] Alessandro Facchini, Filip Murlak, and Michał Skrzypczak. Rabin-Mostowski index problem: A step beyond deterministic automata. In LICS, pages 499–508. IEEE Computer Society, 2013. doi:10.1109/LICS.2013.56.
[16] 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. Games on graphs. CoRR, abs/2305.10546, 2023. doi:10.48550/arXiv.2305.10546.
[17] Olivier Finkel and Stevo Todorcevic. Automatic ordinals. Int. J. Unconv. Comput., 9(1-2):61–70, 2013. URL: http://www.oldcitypublishing.com/journals/ijuc-home/ijuc-issue-contents/ijuc-volume-9-number-1-2-2013/ijuc-9-1-2-p-61-70/.
[18] Gaëlle Fontaine. Continuous fragment of the mu-calculus. In CSL, volume 5213 of Lecture Notes in Computer Science, pages 139–153. Springer, 2008. doi:10.1007/978-3-540-87531-4_12.
[19] Maria J. Gouveia and Luigi Santocanale. $\aleph$ ${}_{\mbox{1}}$ and the modal $\mu$ -calculus. Log. Methods Comput. Sci., 15(4), 2019. doi:10.23638/LMCS-15(4:1)2019.
[20] Olivier Idir and Karoliina Lehtinen. Mostowski index via extended register games. CoRR, abs/2412.16793, 2024. doi:10.48550/arXiv.2412.16793.
[21] Alexander Kechris. Classical descriptive set theory. Springer-Verlag, New York, 1995.
[22] Damian Niwiński. On the cardinality of sets of infinite trees recognizable by finite automata. In MFCS, volume 520 of Lecture Notes in Computer Science, pages 367–376. Springer, 1991. doi:10.1007/3-540-54345-7_80.
[23] Damian Niwiński and Igor Walukiewicz. A gap property of deterministic tree languages. Theor. Comput. Sci., 1(303):215–231, 2003. doi:10.1016/S0304-3975(02)00452-8.
[24] C.-H. Luke Ong. On model-checking trees generated by higher-order recursion schemes. In LICS, pages 81–90. IEEE Computer Society, 2006. doi:10.1109/LICS.2006.38.
[25] Michael O. Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society, 141:1–35, 1969.
[26] Sylvain Schmitz. Algorithmic Complexity of Well-Quasi-Orders. (Complexité algorithmique des beaux pré-ordres). École normale supérieure Paris-Saclay, 2017. URL: https://tel.archives-ouvertes.fr/tel-01663266.
[27] Michał Skrzypczak. Descriptive Set Theoretic Methods in Automata Theory – Decidability and Topological Complexity, volume 9802 of Lecture Notes in Computer Science. Springer, 2016. doi:10.1007/978-3-662-52947-8.
[28] Michał Skrzypczak and Igor Walukiewicz. Deciding the topological complexity of Büchi languages. In ICALP, volume 55 of LIPIcs, pages 99:1–99:13. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2016. doi:10.4230/LIPICS.ICALP.2016.99.
[29] Wolfgang Thomas. Languages, automata, and logic. In Handbook of Formal Languages (3), pages 389–455. Springer, 1997. doi:10.1007/978-3-642-59126-6_7.

[bib.bib1] [1] Bahareh Afshari, Giacomo Barlucchi, and Graham E. Leigh. The limit of recursion in state-based systems. In FICS, 2024. URL: https://www.irif.fr/_media/users/saurin/fics2024/pre-proceedings/fics-2024-afshari-etal.pdf.

[bib.bib2] [2] Bahareh Afshari and Graham E. Leigh. On closure ordinals for the modal mu-calculus. In CSL, volume 23 of LIPIcs, pages 30–44. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2013. doi:10.4230/LIPICS.CSL.2013.30.

[bib.bib3] [3] Vince Bárány, Łukasz Kaiser, and Alexander M. Rabinovich. Expressing cardinality quantifiers in monadic second-order logic over trees. Fundam. Inform., 100(1-4):1–17, 2010. doi:10.3233/FI-2010-260.

[bib.bib4] [4] Mikołaj Bojańczyk. Weak MSO+U with path quantifiers over infinite trees. In ICALP (2), volume 8573 of Lecture Notes in Computer Science, pages 38–49. Springer, 2014. doi:10.1007/978-3-662-43951-7_4.

[bib.bib5] [5] Julian C. Bradfield. Simplifying the modal mu-calculus alternation hierarchy. In STACS, volume 1373 of Lecture Notes in Computer Science, pages 39–49. Springer, 1998. doi:10.1007/BFB0028547.

[bib.bib6] [6] Julian C. Bradfield, Jacques Duparc, and Sandra Quickert. Transfinite extension of the mu-calculus. In CSL, volume 3634 of Lecture Notes in Computer Science, pages 384–396. Springer, 2005. doi:10.1007/11538363_27.

[bib.bib7] [7] Julian C. Bradfield and Igor Walukiewicz. The mu-calculus and model checking. In Handbook of Model Checking, pages 871–919. Springer, 2018. doi:10.1007/978-3-319-10575-8_26.

[bib.bib8] [8] Julius R. Büchi and Lawrence H. Landweber. Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society, 138:295–311, 1969.

[bib.bib9] [9] Lorenzo Clemente and Michał Skrzypczak. Deterministic and game separability for regular languages of infinite trees. In ICALP, volume 198 of LIPIcs, pages 126:1–126:15. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPICS.ICALP.2021.126.

[bib.bib10] [10] Thomas Colcombet, Denis Kuperberg, Christof Löding, and Michael Vanden Boom. Deciding the weak definability of Büchi definable tree languages. In CSL, volume 23 of LIPIcs, pages 215–230. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2013. doi:10.4230/LIPICS.CSL.2013.215.

[bib.bib11] [11] Thomas Colcombet and Christof Löding. The non-deterministic Mostowski hierarchy and distance-parity automata. In ICALP (2), volume 5126 of Lecture Notes in Computer Science, pages 398–409. Springer, 2008. doi:10.1007/978-3-540-70583-3_33.

[bib.bib12] [12] Marek Czarnecki. How fast can the fixpoints in modal mu-calculus be reached? In FICS, pages 35–39. Laboratoire d’Informatique Fondamentale de Marseille, 2010. URL: https://hal.archives-ouvertes.fr/hal-00512377/document#page=36.

[bib.bib13] [13] Christian Delhommé. Automaticité des ordinaux et des graphes homogènes. Comptes Rendus de L’Académie des Sciences, Mathématiques, 339(1):5–10, 2004.

[bib.bib14] [14] Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Derivation tree analysis for accelerated fixed-point computation. Theor. Comput. Sci., 412(28):3226–3241, 2011. doi:10.1016/J.TCS.2011.03.020.

[bib.bib15] [15] Alessandro Facchini, Filip Murlak, and Michał Skrzypczak. Rabin-Mostowski index problem: A step beyond deterministic automata. In LICS, pages 499–508. IEEE Computer Society, 2013. doi:10.1109/LICS.2013.56.

[bib.bib16] [16] 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. Games on graphs. CoRR, abs/2305.10546, 2023. doi:10.48550/arXiv.2305.10546.

[bib.bib17] [17] Olivier Finkel and Stevo Todorcevic. Automatic ordinals. Int. J. Unconv. Comput., 9(1-2):61–70, 2013. URL: http://www.oldcitypublishing.com/journals/ijuc-home/ijuc-issue-contents/ijuc-volume-9-number-1-2-2013/ijuc-9-1-2-p-61-70/.

[bib.bib18] [18] Gaëlle Fontaine. Continuous fragment of the mu-calculus. In CSL, volume 5213 of Lecture Notes in Computer Science, pages 139–153. Springer, 2008. doi:10.1007/978-3-540-87531-4_12.

[bib.bib19] [19] Maria J. Gouveia and Luigi Santocanale. $\aleph$ ${}_{\mbox{1}}$ and the modal $\mu$ -calculus. Log. Methods Comput. Sci., 15(4), 2019. doi:10.23638/LMCS-15(4:1)2019.

[bib.bib20] [20] Olivier Idir and Karoliina Lehtinen. Mostowski index via extended register games. CoRR, abs/2412.16793, 2024. doi:10.48550/arXiv.2412.16793.

[bib.bib21] [21] Alexander Kechris. Classical descriptive set theory. Springer-Verlag, New York, 1995.

[bib.bib22] [22] Damian Niwiński. On the cardinality of sets of infinite trees recognizable by finite automata. In MFCS, volume 520 of Lecture Notes in Computer Science, pages 367–376. Springer, 1991. doi:10.1007/3-540-54345-7_80.

[bib.bib23] [23] Damian Niwiński and Igor Walukiewicz. A gap property of deterministic tree languages. Theor. Comput. Sci., 1(303):215–231, 2003. doi:10.1016/S0304-3975(02)00452-8.

[bib.bib24] [24] C.-H. Luke Ong. On model-checking trees generated by higher-order recursion schemes. In LICS, pages 81–90. IEEE Computer Society, 2006. doi:10.1109/LICS.2006.38.

[bib.bib25] [25] Michael O. Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society, 141:1–35, 1969.

[bib.bib26] [26] Sylvain Schmitz. Algorithmic Complexity of Well-Quasi-Orders. (Complexité algorithmique des beaux pré-ordres). École normale supérieure Paris-Saclay, 2017. URL: https://tel.archives-ouvertes.fr/tel-01663266.

[bib.bib27] [27] Michał Skrzypczak. Descriptive Set Theoretic Methods in Automata Theory – Decidability and Topological Complexity, volume 9802 of Lecture Notes in Computer Science. Springer, 2016. doi:10.1007/978-3-662-52947-8.

[bib.bib28] [28] Michał Skrzypczak and Igor Walukiewicz. Deciding the topological complexity of Büchi languages. In ICALP, volume 55 of LIPIcs, pages 99:1–99:13. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2016. doi:10.4230/LIPICS.ICALP.2016.99.

[bib.bib29] [29] Wolfgang Thomas. Languages, automata, and logic. In Handbook of Formal Languages (3), pages 389–455. Springer, 1997. doi:10.1007/978-3-642-59126-6_7.

A Dichotomy Theorem for Ordinal Ranks in MSO

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

Related Version:

Acknowledgements:

Funding:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

Theorem 1.1.

Related work

Question 1.2 (Czarnecki [12]).

2 Basic notions

Words.

Trees.

Automata.

Theorem 2.1 ([25], see also [29]).

Games.

Ranks.

Example 2.2.

3 Problem formulation

Definition 3.1.

Example 3.2.

4 The dichotomy game

▶ Remark 4.1.

Proposition 4.2.

Depiction of a round of 𝓖𝓐.

5 Intuitions

Example 5.1.

6 Soundness

7 Auxiliary game

Lemma 7.1.

8 Completeness

Proposition 8.1.

9 Definability of ranks in MSO

Fact 9.1.

Lemma 9.2.

Corollary 9.3.

Lemma 9.4.

▶ Remark 9.5.

10 Closure ordinals

Theorem 10.1.

Lemma 10.2.

▶ Remark 10.3.

11 Conclusions

References

$\blacktriangleright$ Remark 4.1.

Depiction of a round of $\mathcal{G}_{\mathcal{A}}$ .

$\blacktriangleright$ Remark 9.5.

$\blacktriangleright$ Remark 10.3.