Arnaud Carayol
email: arnaud.carayol@univ-mlv.fr

Olivier Serre
email: olivier.serre@cnrs.fr

Counting Branches in Trees Using Games

Keywords: Automata on Infinite Trees, Two-Player Games, Cardinality Constraints, Topologically Large Sets ˚Corresponding

We study finite automata running over infinite binary trees. A run of such an automaton is usually said to be accepting if all its branches are accepting. In this article, we relax the notion of accepting run by allowing a certain quantity of rejecting branches. More precisely we study the following criteria for a run to be accepting: (i) it contains at most finitely (resp. countably) many rejecting branches;

(ii) it contains infinitely (resp. uncountably) many accepting branches;

(iii) the set of accepting branches is topologically "big".

In all situations we provide a simple acceptance game that later permits to prove that the languages accepted by automata with cardinality constraints are always ω-regular. In the case (ii) where one counts accepting branches it leads to new proofs (without appealing to logic) of a result of Beauquier and Niwiński.

Introduction

There are several natural ways of describing sets of infinite trees. One is logic where, with any formula, one associates the set of all trees for which the formula holds. Another option is using finite automata. Finite automata on infinite trees (that extends both automata on infinite words and on finite trees) were originally introduced by Rabin in [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF] to prove the decidability of the monadic second order logic (MSOL) over the full binary tree. Indeed, Rabin proved that for any MSOL formula, one can construct a tree automaton such that it accepts a non empty language if and only if the original formula holds at the root of the full binary tree. These automata were also successfully used by Rabin in [START_REF] Rabin | Automata on infinite objects and Church's problem[END_REF] to solve Church's synthesis problem [START_REF] Church | Logic, arithmetic and automata[END_REF], that asks for constructing a circuit based on a formal specification (typically expressed in MSOL) describing the desired input/output behaviour. His approach was to represent the set of all possible behaviours of a circuit by an infinite tree (directions code the inputs while node labels along a branch code the outputs) and to reduce the synthesis problem to emptiness of a tree automaton accepting all those trees coding circuits satisfying the specification. Since then, automata on infinite trees and their variants have been intensively studied and found many applications, in particular in logic. Connections between automata on infinite trees and logic are discussed e.g. in the excellent surveys [START_REF] Thomas | Languages, automata, and logic[END_REF][START_REF] Vardi | Automata: from logics to algorithms[END_REF].

Roughly speaking a finite automaton on infinite trees is a finite memory machine that takes as input an infinite node-labelled binary tree and processes it in a top-down fashion as follows. It starts at the root of the tree in its initial state, and picks (possibly nondeterministically) two successor states, one per child, according to the current control state, the letter at the current node and the transition relation. Then the computation proceeds in parallel from both children, and so on. Hence, a run of the automaton on an input tree is a labelling of this tree by control states of the automaton, that should satisfy the local constraints imposed by the transition relation. A branch in a run is accepting if the ω-word obtained by reading the states along the branch satisfies some acceptance condition (typically an ω-regular condition such as a Büchi or a parity condition). Finally, a tree is accepted by the automaton if there exists a run over this tree in which every branch is accepting. An ω-regular tree language is a tree language accepted by some tree automaton equipped with a parity condition.

A fundamental result of Rabin is that ω-regular tree languages form a Boolean algebra [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF]. The main technical difficulty in establishing this result is to show the closure under complementation. Since the publication of this result in 1969, it has been a challenging problem to simplify this proof. A much simpler one was obtained by Gurevich and Harrington in [START_REF] Gurevich | Trees, automata, and games[END_REF] making use of two-player perfect information games for checking membership of a tree in the language accepted by the automaton3 : Éloïse (a.k.a. Automaton) builds a run on the input tree while Abélard (a.k.a. Pathfinder ) tries to exhibit a rejecting branch in the run. Another fruitful connection between automata and games is for emptiness checking. In a nutshell the emptiness problem for an automaton on infinite trees can be modelled as a game where Éloïse builds an input tree together with a run while Abélard tries to exhibit a rejecting branch in the run. Hence, the emptiness problem for tree automata can be reduced to solving a two-player parity game played on a finite graph. Beyond these results, the tight connection between automata and games is one of the main tools in automata theory [START_REF] Thomas | Languages, automata, and logic[END_REF][START_REF]Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar[END_REF][START_REF] Löding | Infinite games and automata theory[END_REF].

There are several levers on which one can act to define alternative families of tree automata / classes of tree languages. A first lever is local with respect to the run: it is the condition required for a branch to be accepting, the reasonable options here being all classical ω-regular conditions (reachability, Büchi, parity. . . ).

A second one has to do with the set of runs. The usual definition is existential: a tree is accepted if there exists an accepting run on that tree. Other popular approaches are universality, alternation or probabilistic transition functions. A third lever is global with respect to the run: it is the condition required for a run to be accepting. The usual definition is that all branches must be accepting for the run to be accepting but one could relax this condition by specifying how many branches should be accepting/rejecting. One can do this either by counting the number of accepting branches (e.g. infinitely many, uncountably many) or by counting the number of rejecting branches (e.g. finitely many, at most countably many): this leads to the notion of automata with cardinality constraints [START_REF] Beauquier | About the effect of the number of successful paths in an infinite tree on the recognizability by a finite automaton with Büchi conditions[END_REF][START_REF] Beauquier | Automata on infinite trees with path counting constraints[END_REF]. As these properties can be expressed in MSOL [START_REF] Bárány | Expressing cardinality quantifiers in monadic second-order logic over trees[END_REF], the classes of languages accepted under these various restrictions are always ω-regular. However, this logical approach does not give a tractable transformation to standard parity or Büchi automata. Another option is to use a notion of topological "bigness" and to require for a run to be accepting that the set of accepting branches is big [START_REF] Völzer | Defining fairness[END_REF][START_REF] Asarin | Fair adversaries and randomization in two-player games[END_REF]. Yet another option considered in [START_REF] Carayol | Qualitative tree languages[END_REF][START_REF] Carayol | Randomisation in automata on infinite trees[END_REF][START_REF] Fijalkow | Emptiness of alternating tree automata using games with imperfect information[END_REF] is to measure (in the usual sense of measure theory) the set of accepting branches and to put a constraint on this measure (e.g. positive, equal to one).

The idea of allowing a certain amount of rejecting branches in a run was first considered by Beauquier, Nivat and Niwiński in [START_REF] Beauquier | About the effect of the number of successful paths in an infinite tree on the recognizability by a finite automaton with Büchi conditions[END_REF][START_REF] Beauquier | Automata on infinite trees with path counting constraints[END_REF], where it was required that the number of accepting branches in a run belongs to a specified set of cardinals Γ. In particular, they proved that if Γ consists of all cardinals greater than some γ, then one obtains an ω-regular tree language. Their approach was based on logic (actually they proved that a tree language defined by such an automaton can be defined by a Σ 1 1 formula hence, can also be defined by a Büchi tree automaton) while the one we develop here is based on designing acceptance games. There is also work on the logical side with decidability results but that do not lead to efficient algorithms [START_REF] Bárány | Expressing cardinality quantifiers in monadic second-order logic over trees[END_REF].

Our main contributions are to introduce (automata with cardinality constraints on the number of rejecting branches; automata with topological bigness constraints) or revisit (automata with cardinality constraints on the number of accepting branches) variants of tree automata where acceptance for a run allows a somehow negligible set of rejecting branches. For each model, we provide a game counterpart by means of an equivalent acceptance game and this permits to retrieve the classical (and fruitful) connection between automata and game. It also permit to argue that languages defined by those classes are always ω-regular. Moreover, in the case where one counts accepting branches we show that the languages that we obtain are always accepted by a Büchi automaton, which contrasts with the case where one counts rejecting branches where we exhibit a counter-example for that property.

The paper is organised as follows. Section 2 recalls classical concepts while Section 3 introduces the main notions studied in the paper, namely automata with cardinality constraints and automata with topological bigness constraints. Then, Section 4 studies those languages obtained by automata with cardinality constraints on the number of rejecting branches while Section 5 is devoted to those languages obtained by automata with cardinality constraints on the number of accepting branches. Finally, Section 6 considers automata with topological bigness constraints.

Preliminaries

Words and Trees

An alphabet A is a (possibly infinite) set of letters. In the sequel A ˚denotes the set of finite words over A, and A ω the set of infinite words (or ω-words) over A. The empty word is written ε. The length of a word u P A ˚is denoted by |u|. For any k ě 0, we let A k " tu | |u| " ku, A ďk " tu | |u| ď ku and A ěk " tu | |u| ě ku. We let A `" A ˚ztεu.

Let u be a finite word and v be a (possibly infinite) word. Then u ¨v (or simply uv) denotes the concatenation of u and v; the word u is a prefix of v, denoted u Ď v, if there exists a word w such that v " u ¨w. We denote by u Ă v the fact that u is a strict prefix of v (i.e. u Ď v and u " v). When u is a prefix of v we let u ´1v denote the unique word w such that v " uw. For some finite word u and some integer k ě 0, we denote by u k the word obtained by concatenating k copies of u (with the convention that u 0 " ε).

In this paper we consider full binary node-labelled trees. Let A be an alphabet, then an A-labelled tree t is a (total) function from t0, 1u ˚to A. In this context, an element u P t0, 1u ˚is called a node, and the node u ¨0 (resp. u ¨1) is the left child (resp. right child ) of u. The node ε is called the root. The letter tpuq is called the label of u in t.

A branch is an infinite word π P t0, 1u ω and a node u belongs to a branch π if u is a prefix of π. For an A-labelled tree t and a branch π " π 0 π 1 ¨¨¨we define the label of π as the ω-word tpπq " tpεqtpπ 0 qtpπ 0 π 1 qtpπ 0 π 1 π 2 q ¨¨¨.

Two-Player Perfect Information Turn-Based Games on Graphs

A graph is a pair G " pV, Eq where V is a (possibly infinite) set of vertices and E Ď V ˆV is a set of edges. For a vertex v, we denote by Epvq " tv 1 | pv, v 1 q P Eu the set of successors of v in G. In the rest of the paper (hence, this is implicit from now on), we only consider graphs that have no dead-end, i.e. such that Epvq ‰ H for all v.

An arena is a triple G " pG, V E , V A q where G " pV, Eq is a graph and V " V E Z V A is a partition of the vertices among two players, Éloïse and Abélard.

Éloïse and Abélard play in G by moving a pebble along edges. A play from an initial vertex v 0 proceeds as follows: the player owning v 0 (i.e. Éloïse if v 0 P V E , Abélard otherwise) moves the pebble to a vertex v 1 P Epv 0 q. Then the player owning v 1 chooses a successor v 2 P Epv 1 q and so on. As we assumed that there is no dead-end, a play is an infinite word v 0 v 1 v 2 ¨¨¨P V ω such that for all i ě 0 one has v i`1 P Epv i q. A partial play is a prefix of a play, i.e., it is a finite word v 0 v 1 ¨¨¨v P V ˚such that for all 0 ď i ă one has v i`1 P Epv i q.

A strategy for Éloïse is a function ϕ : V ˚VE Ñ V assigning, to every partial play ending in some vertex v P V E , a vertex v 1 P Epvq. Strategies of Abélard are defined likewise, and usually denoted ψ. In a given play λ " v 0 v 1 ¨¨¨we say that Éloïse (resp. Abélard) respects a strategy ϕ (resp. ψ) if whenever v i P V E (resp.

v i P V A ) one has v i`1 " ϕpv 0 ¨¨¨v i q (resp. v i`1 " ψpv 0 ¨¨¨v i q).
A winning condition is a subset Ω Ď V ω and a (two-player perfect information) game is a pair G " pG, Ωq consisting of an arena and a winning condition.

A play λ is won by Éloïse if and only if λ P Ω; otherwise λ is won by Abélard. A strategy ϕ is winning for Éloïse in G from a vertex v 0 if any play starting from v 0 where Éloïse respects ϕ is won by her. Finally, a vertex v 0 is winning for Éloïse in G if she has a winning strategy ϕ from v 0 . Winning strategies and winning vertices for Abélard are defined likewise.

We now define three classical winning conditions.

• A Büchi winning condition is of the form pV ˚F q ω for a set F Ď V of final vertices, i.e. winning plays are those that infinitely often visit vertices in F .

• A co-Büchi condition is of the form V ˚pV zF q ω for a set F Ď V of forbidden vertices, i.e. winning plays are those that visit only finitely often forbidden vertices.

• A parity winning condition is defined by a colouring function Col that is a mapping Col : V Ñ C Ă N where C is a finite set of colours. The parity winning condition associated with Col is the set

Ω Col " tv 0 v 1 ¨¨¨P V ω | lim infpColpv i qq iě0 is evenu
i.e. a play is winning if and only if the smallest colour infinitely often visited is even.

Finally, a Büchi (resp. co-Büchi, parity) game is one equipped with a Büchi (resp. co-Büchi, parity) winning condition. For notation of such games we often replace the winning condition by the object that is used to defined it (i.e. F or Col).

Tree Automata, Regular Tree Languages and Acceptance Game

A tree automaton A is a tuple xA, Q, q ini , ∆, Accy where A is the input alphabet, Q is the finite set of states, q ini P Q is the initial state, ∆ Ď Q ˆA ˆQ ˆQ is the transition relation and Acc Ď Q ω is the acceptance condition. An automaton is complete if, for all q P Q and a P A there is at least one pair pq 0 , q 1 q P Q 2 such that pq, a, q 0 , q 1 q P ∆. In this work we always assume that the automata are complete and this is implicit from now. Note that we will discuss the impact of this restriction in the conclusion.

Given an A-labelled tree t, a run of A over t is a Q-labelled tree ρ such that (i) the root is labelled by the initial state, i.e. ρpεq " q ini ;

(ii) for all nodes u, pρpuq, tpuq, ρpu ¨0q, ρpu ¨1qq P ∆.

A branch π P t0, 1u ω is accepting in the run ρ if ρpπq P Acc, otherwise it is rejecting. A run ρ is accepting if all its branches are accepting. Finally, a tree t is accepted if there exists an accepting run of A over t. The set of all trees accepted by A (or the language recognised by A) is denoted LpAq.

In this work we consider the following three classical acceptance conditions:

• A Büchi condition is given by a subset F Ď Q of final states by letting Acc " BuchipF q " pQ ˚F q ω , i.e. a branch is accepting if it contains infinitely many final states.

• A co-Büchi condition is given by a subset F Ď Q of forbidden states by letting coBuchipF q " Q ˚pQzF q ω , i.e. a branch is accepting if it contains finitely many forbidden states.

• A parity condition is given by a colouring mapping Col : Q Ñ N by letting

Acc " P arity " tq 0 q 1 q 2 ¨¨¨| lim infpColpq i qq i is evenu

i.e. a branch is accepting if the smallest colour appearing infinitely often is even.

These conditions are all examples of ω-regular acceptance conditions, i.e. Acc is an ω-regular set of ω-words over the alphabet Q (see e.g. [START_REF] Perrin | Infinite Words[END_REF] for a reference book on languages of infinite words).

Remark 1. The parity condition is expressive enough to capture the general case of an arbitrary ω-regular condition Acc. Indeed, it is well known that Acc, when it is ω-regular, is accepted by a deterministic parity word automaton. By taking the synchronised product of this automaton with the tree automaton, we obtain a parity tree automaton accepting the same language (see e.g. [START_REF] Perrin | Infinite Words[END_REF]).

When it is clear from the context, we may replace, in the description of A, Acc by F for Büchi/co-Büchi condition (resp. Col for a parity condition), and we shall refer to the automaton as a Büchi/co-Büchi (resp. parity) tree automaton. A set L of infinite trees is an ω-regular tree language if there exists a parity tree automaton A such that L " LpAq. The class of ω-regular tree languages is robust, as illustrated by the following famous statement [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF].

Theorem 1. The class of ω-regular tree languages is a Boolean algebra. q, u q, u, q 0 , q 1 q 0 , u0 q 1 , u1 for any pq, tpuq, q 0 , q 1 q P ∆ Fix an automaton A " xA, Q, q ini , ∆, Accy and a tree t and define an acceptance game G A,t , i.e. a game where Éloïse wins if and only if there exists an accepting run of A on t, as follows.

Intuitively, a play in G A,t consists in moving a pebble along a branch of t in a top-down manner: to the pebble is attached a state, and in a node u with state q, Éloïse picks a transition pq, tpuq, q 0 , q 1 q P ∆, and then Abélard chooses to move down the pebble either to u ¨0 (and update the state to q 0 ) or to u ¨1 (and update the state to q 1 ).

Formally (see Figure 1 for an illustration4 ), let

G A,t " pV E Z V A , Eq with V E " Q ˆt0, 1u ˚,
V A " tpq, u, q 0 , q 1 q | u P t0, 1u ˚and pq, tpuq, q 0 , q 1 q P ∆u Ď Q ˆt0, 1u ˚ˆQ ˆQ and E " tppq, uq, pq, u, q 0 , q 1 qq | pq, u, q 0 , q 1 q P V A qu Y tppq, u, q 0 , q 1 q, pu ¨x, q x qq | x P t0, 1u and pq, u, q 0 , q 1 q P V A qu Then let G A,t " pG A,t , V E , V A q and extend Col on V E Y V A by letting Colppq, uqq " Colppq, u, q 0 , q 1 qq " Colpqq. Finally define G A,t as the parity game pG A,t , Colq.

The next theorem is well-known (see e.g. [START_REF] Gurevich | Trees, automata, and games[END_REF][START_REF]Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar[END_REF]) and its proof is obtained by remarking that strategies for Éloïse in G A,t are in bijection with runs of A on t (with the winning strategies corresponding to the accepting runs).

Theorem 2. One has t P LpAq if and only if Éloïse wins in G A,t from pq ini , εq.

Automata with Cardinality Constraints and Automata with Topological Bigness Constraints

We now introduce the main notions studied in the paper, namely automata with cardinality constraints (studied in Section 4 and Section 5) and automata with topological bigness constraints (studied in Section 6).

Automata with Cardinality Constraints

We now relax the criterion for a run to be accepting. Recall that classically, a run is accepting if every branch in it is accepting. For a given automaton A, we define the following four criteria (two for the case where one counts the number of accepting branches and two for the case where one counts the number of rejecting branches) for a run to be accepting. Note that the case where one counts accepting branches was already considered in [START_REF] Beauquier | About the effect of the number of successful paths in an infinite tree on the recognizability by a finite automaton with Büchi conditions[END_REF][START_REF] Beauquier | Automata on infinite trees with path counting constraints[END_REF].

• There are finitely many rejecting branches in the run. A tree t is in L Rej Fin pAq if and only if there is a run of A on t satisfying the previous condition.

• There are at most countably many rejecting branches in the run. A tree t is in L Rej ďCount pAq if and only if there is a run of A on t satisfying the previous condition.

• There are infinitely many accepting branches in the run. A tree t is in L Acc 8 pAq if and only if there is a run of A on t satisfying the previous condition.

• There are uncountably many accepting branches in the run. A tree t is in L Acc U ncount pAq if and only if there is a run of A on t satisfying the previous condition. q, u q, u, q 0 , q 1 q 0 , u0 q 1 , u1 q, u, q 0 , q 1 for any pq, tpuq, q 0 , q 1 q P ∆

Automata with Topological Bigness Constraints

A notion of topological "bigness" and "smallness" is given by large and meager sets respectively (see [START_REF] Völzer | Defining fairness in reactive and concurrent systems[END_REF][START_REF] Grädel | Banach-Mazur Games on Graphs[END_REF] for a survey of the notion). The idea is to see the set of branches in a tree as a topological space by taking as basic open sets the cones. For a node u P t0, 1u ˚, the cone Conepuq is defined as tπ P t0, 1u ω | u Ď πu. A set of branches B Ď t0, 1u ω is nowhere dense if for all nodes u, there exists v P t0, 1u ˚such that no branch of B has uv as a prefix. It is meagre if it is the countable union of nowhere dense sets. Finally it is large if it is the complement of a meagre set.

For a given automaton A, we define the following acceptance criterion: a run is accepting if and only if its set of accepting branches is large. Note that this is equivalent to require that the set of rejecting branches is meagre.

Finally, a tree t is in L Acc Large pAq if and only if there is a run of A on t satisfying the previous condition.

Counting Rejecting Branches

For the classes of automata where acceptance is defined by a constraint on the number of rejecting branches we show that the associated languages are ω-regular. For this, we adopt the following roadmap: first we design an acceptance game and then we note that it can be transformed into another equivalent game that turns out to be the (usual) acceptance game for some tree automaton.

Fix, for this section, a parity tree automaton A " xA, Q, q ini , ∆, Coly and recall that a tree t is in L Rej ďCount pAq (resp. in L Rej Fin pAq) if and only if there is a run of A on t in which there are at most countably (resp. finitely) many rejecting branches.

The Case of Languages L Rej

ďCount pAq Fix a tree t and define an acceptance game for L Rej ďCount pAq as follows. In this game the two players move a pebble along a branch of t in a top-down manner: to the pebble is attached a state whose colour gives the colour of the configuration. Hence, (Éloïse's main) configurations in the game are elements of Q ˆt0, 1u ˚. See Figure 2 for the local structure of the arena. In a node u with state q Éloïse picks a transition pq, tpuq, q 0 , q 1 q P ∆, and then Abélard has two possible options: (i) he chooses a direction 0 or 1; or (ii) he lets Éloïse choose a direction 0 or 1.

Once the direction i P t0, 1u is chosen, the pebble is moved down to u ¨i and the state is updated to q i . A play is won by Éloïse if one of the following two situations occurs: either the parity condition is satisfied or Abélard has not let Éloïse infinitely often choose the direction. Call this game G RejďCount A,t . The next theorem states that it is an acceptance game for the language L Rej ďCount pAq. from pq ini , εq. With ϕ we associate a run ρ of A on t as follows. We inductively associate with any node u a partial play λ u where Éloïse respects ϕ and that ends in a vertex of Éloïse of the form pq, uq. For this we let λ ε " pq ini , εq. Now assume that we have defined λ u for some node u and let ϕpλ u q "pq, tpuq, q 0 , q 1 q be the transition Éloïse plays from λ u when she respects ϕ. Then let i be the direction Éloïse would choose (again playing according to ϕ) if Abélard lets her pick the direction right after she played pq, tpuq, q 0 , q 1 q: one defines λ ui as the partial play obtained by extending λ u by Éloïse choosing transition pq, tpuq, q 0 , q 1 q, followed by Abélard letting her choose the direction and Éloïse choosing direction i; and one defines λ up1´iq as the partial play obtained by extending λ u by Éloïse choosing transition pq, tpuq, q 0 , q 1 q, followed by Abélard choosing direction p1 ´iq. Note that for j P t0, 1u, λ uj ends with the pebble on uj with the state q j attached to it, equivalently in configuration pq j , ujq. We also refer to the node ui (i.e. the node that Éloïse has picked) as marked : note that any node has exactly one child that is marked (by convention the root is marked).

The run ρ is defined by letting ρpuq be the state attached to the pebble in the last configuration of λ u . By construction, ρ is a valid run of A on t and moreover with any branch π in ρ one can associate a play λ π in G RejďCount A,t from pq ini , εq where Éloïse respects ϕ (one simply considers the limit of the increasing sequence of partial plays λ u where u ranges over those nodes along branch π).

It remains to show that the number of rejecting branches is at most countable. Now consider a rejecting branch π. By construction π is rejecting if and only if λ π does not fulfil the parity condition. As ϕ is winning so does λ π hence, it means that in λ π Abélard does not let Éloïse choose infinitely often the direction (indeed, this is the only way for λ π to be winning as we assumed π is rejecting, which implies that λ π does not satisfy the parity condition). Equivalently, π contains finitely many marked nodes (marked nodes corresponding precisely to those steps where Éloïse chooses the direction). Hence, with any rejecting branch π, one can associate the last marked node u π in it. And if π ‰ π 1 one has u π ‰ u π 1 : indeed, at the point where π and π 1 first differ, one of the node is marked from the property that every node has exactly one child that is marked. Hence, the number of rejecting branches is countable as the map π Þ Ñ u π is injective and as the number of nodes in a tree is countable. This permits to conclude that ρ is an accepting run -in the sense of L Rej ďCount pAq -of A on t.

Conversely, assume that Éloïse has no winning strategy. It follows from Borel determinacy [START_REF] Martin | Borel determinacy[END_REF] that Abélard has a winning strategy ψ in G RejďCount A,t from pq ini , εq. Let us prove that any run ρ of A on t contains uncountably many rejecting branches. For this, fix a run ρ of A on t. With any sequence α " α 1 α 2 ¨¨¨P t0, 1u ω we associate a strategy ϕ α of Éloïse in G RejďCount A,t

. The strategy ϕ α of Éloïse consists in describing the run ρ and to propose direction α i when it is the i-th time that Abélard lets her choose the direction. More formally, when the pebble is on node u with state q (we will trivially have q " ρpuq as an invariant) she picks the transition pρpuq, tpuq, ρpu0q, ρpu1qq; moreover if Abélard lets her choose the direction, she picks α i`1 where i is the number of times Abélard let her choose the direction since the beginning of the play.

As we assumed that ψ is winning, the (unique) play obtained when she plays ϕ α and when he plays ψ is loosing for Éloïse: such a play defines a branch π α in ρ, and this branch is a rejecting one. Now, for any α ‰ α 1 one has π α ‰ π α 1 : indeed, at some point α and α 1 differs and, as infinitely often Abélard lets Éloïse choose the directions, the branches π α and π α 1 will differ as well. But as there are uncountably many different sequences α, it leads an uncountable number of rejecting branches in ρ. Hence, ρ is rejecting.

Consider the game G RejďCount

A,t and modify it so that Éloïse is now announcing in advance which direction she would choose if Abélard let her do so. This new game is equivalent to the previous one (meaning that she has a winning strategy in one game if and only if she also has one in the other game). As this new game can easily be modified to obtain an equivalent acceptance game for the classical acceptance condition (as described in Section 2.3) one concludes that the languages of the form L Rej ďCount pAq are always ω-regular. Theorem 4. Let A " xA, Q, q ini , ∆, Coly be a parity tree automaton using d colours. Then there exists a parity tree automaton

A 1 " xA, Q 1 , q 1 ini , ∆ 1 , Col 1 y such that L Rej ďCount pAq " LpA 1 q. Moreover |Q 1 | " Opd|Q|q and A 1 uses d `1 colours. Proof. Define G 1RejďCount A,t
as the game obtained from G RejďCount A,t by asking Éloïse to say which direction she would choose before Abélard possibly lets her this option. Éloïse has a winning strategy in G RejďCount A,t if and only if she has a winning strategy in G 1RejďCount A,t (strategies being essentially the same in both games). The way she indicates the direction can be encoded in the control state: just duplicate the control states (with a classical version and a starred version of each state) and when she wants to pick a transition e.g. pq, tpuq, q 0 , q 1 q and direction 1, she just moves to configuration pq, u, q 0 , q 1 q in the new game. Now the winning condition can be rephrased as either the parity condition is satisfied or finitely many configuration of the form pq ˚, uq are visited. Now this later game can be transformed into a standard acceptance game for ω-regular language (as defined in Section 2.3) by the following trick. One adds to states an integer where one stores the smallest colour seen since the last starred state was visited (this colour is easily updated); whenever a starred state is visited the colour is reset to the colour of the state. Now unstarred states are given an even colour that is greater than all colour previously used (hence, it ensures that if finitely many starred states are visited Éloïse wins) and starred states are given the colour that was stored (hence, if infinitely many starred states are visited we retrieve the previous parity condition). It should then be clear that the later game is a classical acceptance game, showing that L Rej ďCount pAq is ω-regular. The construction of A 1 is immediate from the final game and the size is linear in d|Q| due to the fact that one needs to compute the smallest colour visited between two starred states.

More formally 5 , we assume that A uses colours 0, 1, . . . , d ´1 and we let

A 1 " xA, Q 1 , q 1 ini , ∆ 1 , Col 1 y where: • Q 1 " tq i , q i | q P Q and 0 ď i ď d ´1u;
• q 1 ini " q ini,Colpqiniq ;

• for any q P Q and any 0 ď i ď d ´1 one lets Col 1 pq i q " i and Colpq i q " d `1 if d `1 is even and Colpq i q " d otherwise; and

• ∆ 1 consists of the following tuples for every pq, a, r, sq P ∆ and every

0 ď i ď d ´1 -pq i , a, r minti,Colprqu , s minti,Colpsqu q, -pq i , a, r minti,Colprqu , s minti,Colpsqu q,
pq i , a, r Colprq , s Colpsq q, and pq i , a, r Colprq , s Colpsq q.

It is then easily seen that the acceptance game G A 1 ,t of A 1 as defined in Section 2.3 is essentially the same as the above game G 1RejďCount A,t .

The Case of Languages L Rej

Fin pAq The following lemma (whose proof is straightforward) characterises finite sets of branches by noting that for such a set there is a finite number of nodes belonging to at least two branches in the set.

Lemma 1. Let Π be a set of branches. Then Π is finite if and only if the set W " tu P t0, 1u ˚| Dπ 0 ‰ π 1 P Π s.t. u Ď π 0 and u Ď π 1 u is finite. Equivalently, Π is finite if and only if there exists some ě 0 such that for all u P t0, 1u ě there is at most one π P Π such that u Ď π. Now, fix a tree t and define an acceptance game for L Rej Fin pAq as follows. In this game (we refer the reader to Figure 3 for the local structure of the arena for game G RejFin A,t

) the two players move a pebble along a branch of t in a top-down manner: as in the classical case the players first select a transition and then a direction. The colour of the current state gives the colour of the configuration. There are three modes in this game: wait mode, path mode and check mode and the game starts in wait mode. Hence, (Éloïse's main) configurations in the game are elements of Q ˆt0, 1u ˚ˆtwait, path, checku.

Regardless of the mode, in a node u with state q Éloïse picks a transition pq, tpuq, q 0 , q 1 q P ∆, and for each direction in i P t0, 1u she proposes the next mode m i in twait, path, checku (we describe below what are the possible options depending on the current mode). Then Abélard chooses a direction j P t0, 1u, the pebble is moved down to u ¨j, the state is updated to q j and the mode changes to m j . The possible modes that Éloïse can propose depend on the current mode in the following manner.

• In wait mode she can propose any modes m i in twait, path, checku but if one proposed mode m i is path then the other mode m 1´i must be check.

q, u q, u, q w 0 , q c 1 , 0 q, u, q c 0 , q w 1 , 0 q, u, q w 0 , q w 1 , 0 q, u, q c 0 , q p 1 , 0 q, u, q p 0 , q c 1 , 0

q, u, q c 0 , q c 1 , 0 q0, u0 q1, u1
for any pq, tpuq, q0, q1q

P ∆ wait mode q, u q, u, q c 0 , q c 1 , 0 q0, u0 q1, u1
for any pq, tpuq, q0, q1q P ∆ check mode q, u q, u, q p 0 , q c 1 , 0 q, u, q c 0 , q p 1 , 0 q0, u0 q1, u1

for any pq, tpuq, q0, q1q P ∆ path mode . We use superscripts to indicate which modes have been proposed by Éloïse.

• In check mode the proposed modes must be check (i.e. once the mode is check it no longer changes).

• In path mode one proposed mode must be path and the other must be check.

A play is won by Éloïse if one of the two following situations occurs.

• The wait mode is eventually left and the parity condition is satisfied.

• The mode is eventually always equal to path.

In particular a play in which the mode is wait forever is lost by Éloïse. Note that the latter winning condition can easily be reformulated as a parity condition. Call this game G RejFin A,t . The next theorem states that it is an acceptance game for the language L Rej Fin pAq.

Theorem 5. One has t P L Rej Fin pAq if and only if Éloïse wins in G RejFin A,t from pq ini , ε, waitq.

Proof. Assume that Éloïse has a winning strategy ϕ in G RejFin A,t from pq ini , ε, waitq. With ϕ we associate a run ρ of A on t as follows. We inductively define for any node u P t0, 1u ˚a partial play λ u where Éloïse respects ϕ. For this we let λ ε " pq ini , ε, waitq. Now assume that we defined λ u for some node u P t0, 1u ˚and let pq, tpuq, q 0 , q 1 q be the transition Éloïse plays from λ u when she respects ϕ. Then for each i P t0, 1u one defines λ u¨i as the partial play obtained by extending λ u by Éloïse choosing transition pq, tpuq, q 0 , q 1 q, followed by Abélard choosing direction i (we update the mode accordingly to the choice of Éloïse when respecting ϕ in λ u ).

The run ρ is defined by letting, for any u P t0, 1u ˚, ρpuq be the state attached to the pebble in the last configuration of λ u . By construction, ρ is a run of A on t. Moreover with any branch π one can associate a play λ π in G RejFin A,t from pq ini , εq where Éloïse respects ϕ (one simply considers the limit of the increasing sequence of partial plays λ u where u ranges over nodes along branch π).

First, note that there exists some ě 0 such that, for all u P t0, 1u ě , λ u ends in a vertex where the mode is not wait. Indeed, if this was not the case, one could construct an infinite branch π such that, for all nodes u in π, λ u ends with a vertex in mode wait (recall that the only way to be in wait mode is to be in that mode from the very beginning) and therefore the corresponding play λ π would be loosing, which contradicts the fact that Éloïse respects her winning strategy ϕ in play λ π . Now, consider some node u P t0, 1u . If the final vertex in λ u is in mode check one easily verifies that any branch that goes through u is accepting (because the corresponding play is winning hence, satisfies the parity condition). If the final vertex in λ u is in mode path one easily checks that among all branches that go through u, there is exactly one branch π such that λ π eventually stays in mode path forever (and this branch may not satisfy the parity condition) while all other branches eventually stay in mode check forever (and satisfy the parity condition). Therefore, the number of rejecting branches is finite.

Conversely, assume that there is a run ρ of A on t that contains finitely many rejecting branches. Call this set of branches Π. Thanks to Lemma 1, there exists some ě 0 such that for all w P t0, 1u ě there is at most one π P Π such that w Ď π. Using ρ we define a strategy ϕ for Éloïse in G RejFin A,t as follows. In any configuration pq, uq (regardless of the mode) the strategy is to play the transition pq, tpuq, ρpu0q, ρpu1qq. Then there are several cases for determining how the mode is updated.

• In some configuration pq, uq with u of length strictly smaller than the mode remains in wait.

• In some configuration pq, uq with u of length equal to the strategy proposes to update the mode to path for direction i P t0, 1u such that u ¨i Ď π for some branch π P Π, and to check otherwise. Note that due to the definition of , there is at most one direction i in which the mode becomes path.

• In some configuration pq, uq with u of length strictly greater than if the mode is check it will remain to check in both direction. Otherwise (i.e. the mode is path) the strategy proposes to update the mode to path for direction i P t0, 1u such u ¨i Ď π for some branch π P Π, and to check otherwise. Note that in the latter case, there is exactly one direction i in which the mode is path.

Remark that no play where Éloïse respects ϕ stays in wait mode forever. Moreover, with any λ where Éloïse respects ϕ one can associate a branch in the run ρ and this branch is rejecting if and only if λ stays eventually in mode path forever. Hence, any play where the mode is not infinitely often path satisfies the parity condition (because the corresponding branch in ρ does so). Hence, ϕ is winning.

From Theorem 5 and the local structure of the arena of game G RejFin A,t one easily concludes that any language of the form L Rej Fin pAq is ω-regular. Theorem 6. Let A " xA, Q, q ini , ∆, Coly be a parity tree automaton using d colours. Then, there exists a parity tree automaton A 1 " xA, Q 1 , q 1 ini , ∆ 1 , Col 1 y such that L Rej Fin pAq " LpA 1 q. Moreover, |Q 1 | " Op|Q|q and A 1 uses d colours.

Proof. Consider the local structure of game G RejFin A,t as described in Figure 3. The way one defines A 1 is fairly simple: for any state on A and any mode, one gets a new state in A 1 , and the transition function ∆ 1 directly follows from the way we update the modes. The states in wait mode all get the same odd minimal colour (hence, if they are never left Éloïse looses), the states in path mode all get the same even minimal colour (hence, if they are never left Éloïse wins), and the states in check mode get the colour they had in A. Hence, we do not need to add any extra colour (except in the case where A uses only one colour but in this very degenerated case one can simply take A 1 " A).

Languages L Rej

ďCount pAq and L Rej Fin pAq vs. Büchi Tree Languages One can wonder, as it will be later the case (see Section 5) for languages of the form L Acc 8 pAq or L Acc U ncount pAq , whether a Büchi condition is enough to accept (with the classical semantics) a language of the form L Rej ďCount pAq (resp. L Rej Fin pAq). The next Proposition answers negatively. Proposition 1. There is a co-Büchi deterministic tree automaton A such that for any Büchi tree automaton A 1 , L Rej ďCount pAq ‰ LpA 1 q and L Rej Fin pAq ‰ LpA 1 q. Proof. We choose for A the same automaton that was used by Rabin in [START_REF] Rabin | Automata on infinite objects and Church's problem[END_REF] to derive a similar statement where one replaces L Rej ďCount pAq by LpAq and we generalise the proof of this result as given in [START_REF] Thomas | Languages, automata, and logic[END_REF]Example 6.3]. Let L be the set of ta, bu-labelled trees such that the number of branches that contain infinitely many b's is at most countable. Obviously there is a deterministic co-Büchi automaton A such that L " L Rej ďCount pAq. Indeed, consider an automaton A with two states, one forbidden and the other one non-forbidden, and that from any state, goes (for both children) in the forbidden state whenever he was in a b-labelled node and otherwise goes (for both children) in the non-forbidden state. Assume, by contradiction, that there is some Büchi tree automaton A 1 " xta, bu, Q, q ini , ∆, F y such that L Rej ďCount pAq " LpA 1 q. Note that we will not treat the case where L Rej Fin pAq " LpA 1 q as it is identical. Let n " |Q| and let t be the ta, bu-labelled tree such that tpuq " b if and only if u P p0 `1q k for some 1 ď k ď n, i.e. label b occurs when a right successor is taken after a sequence of left successors, however allowing at most n right turns. Clearly, t P L as every branch contains finitely many b-labelled nodes. Let ρ be an accepting run of A 1 on t.

The goal is to exhibit three nodes u, v and w such that:

1. u is a strict prefix of both v and w.

2. v is not a prefix of w and vice versa;

3. ρpuq " ρpvq " ρpwq is a final state; 4. tpuq " tpvq " tpwq " a;

5. on the path segment from u to v there is at least one node labelled b;

6. on the path segment from u to w there is at least one node labelled b.

Once this is done we can form a new tree t 1 (and an associated run ρ 1 of A 1 on t 1 ) by iterating the finite path segment from u (inclusive) to v (exclusive) and from u (inclusive) to w (exclusive) indefinitely, copying also the subtrees which have their roots on these path segments. More formally, consider the two-hole context C t r', 's (resp. C ρ r', 's) obtained by placing holes at v and w in t (resp. in ρ) and the two-hole context D t r', 's (resp. D ρ r', 's) obtained by placing holes at u ´1v and u ´1w in the subtree t {u of t rooted at u (resp. ρ {u ) . The tree t 1 is equal to C t rt 2 , t 2 s where t 2 is the unique tree satisfying the equation t 2 " D t rt 2 , t 2 s. Similarly ρ 1 is equal to C ρ rρ 2 , ρ 2 s where ρ 2 is the unique tree satisfying the equation ρ 2 " D ρ rρ 2 , ρ 2 s.

This process exhibits a binary tree like structure6 inside t 1 (resp. ρ 1 ) such that any branch in t 1 contains infinitely many b-labelled nodes, hence t 1 R L (indeed, there will be uncountably many branches in this binary tree like structure). But this leads to a contradiction as ρ 1 is easily seen to be accepting while being a run on t 1 .

We now explain why we can find nodes u, v and w as above. We first claim that for any node u P 0 `p10 `qk , for some 0 ď k ă n, there are two nodes v u , w u P u0 `10 `such that (i) u is a strict prefix of v u and w u ; (ii) v u is not a prefix of w u and vice versa; and (iii) ρpv u q " ρpw u q is a final state. Indeed, for any i ą 0, the branch u0 i 10 ω is accepting in ρ and therefore there exists some index k i ą 0 such that ρpu0 i 10 ki q P F ; thus, by the pigeon hole principle, there exists i ‰ j such that ρpu0 i 10 ki q " ρpu0 j 10 kj q P F and therefore one can choose v u " u0 i 10 ki and w u " u0 j 10 kj . Now define a sequence of nodes u 0 Ă u 1 Ă u 2 Ă ¨¨¨Ă u n as follows: we let u 0 P 0 `to be such that ρpu 0 q P F (such a node exists as the branch 0 ω is accepting in ρ); and for all 1 ď i ď n, u i " v ui´1 . In particular, one has ρpu i q P F for all 0 ď i ď n and therefore, by the pigeon hole principle there exists 0 ď i ă j ď n such that ρpu i q " ρpu j q. Now, to finish our construction, we simply let u " u i , v " u j and w " w uj´1 . This concludes the proof.

Counting Accepting Branches

We now consider the case where acceptance is defined by a constraint on the number of accepting branches and we show that the associated languages are ω-regular. It leads to new proofs, that rely on games rather than on logic, of the results in [START_REF] Beauquier | Automata on infinite trees with path counting constraints[END_REF].

Fix, for this section, a parity tree automaton A " xA, Q, q ini , ∆, Coly and recall that a tree t is in L Acc 8 pAq (resp. L Acc U ncount pAq) if and only if there is a run of A on t that contains infinitely (resp. uncountably) many accepting branches.

The Case of Languages L Acc 8 pAq

The key idea behind defining an acceptance game for L Acc 8 pAq for some tree t is to exhibit a pseudo comb in a run of A over t. In a nutshell, a pseudo comb consists of an infinite branch U and a collection V of accepting branches each of them sharing some prefix with U . One easily proves that a run contains infinitely many accepting branches if and only if it contains a pseudo comb. More formally, a pseudo comb (see Figure 4 for an illustration) is a pair of subset pU, V q of nodes with U, V Ď t0, 1u ˚such that:

• U and V are disjoint.

• U is a branch: ε P U , for all u P U one has |tu0, u1u X U | " 1 and if u ‰ ε its parent is in U as well.

• V is a set of nodes such that (i) for all v P V , one has |tv0, v1u X V | " 1;

(ii) for all v P V , v P pU Y V q ¨t0, 1u.

• For infinitely many u P U there exists some v P V such that either v " u0 or v " u1.

The following folklore lemma characterises infinite sets of branches in the full binary tree (recall that we say that a node w belongs to a branch π if and only if w Ă π).

Lemma 2. Let Π be a set of branches. Then Π is infinite if and only if the set W " tw | Dπ P Π s.t. w belongs to πu contains a pseudo comb pU, V q, i.e. U Y V Ď W .

Proof. If W contains a pseudo comb it directly implies that Π is infinite, so we focus on the other implication.

There exists an increasing sequence (for the prefix relation Ď) pu i q iě0 of nodes such that for all i ě 0 infinitely many branches in Π go through u i and for both directions j " 0 and j " 1, at least one branch in Π goes through u i ¨j. The existence of this sequence is by an immediate induction.

Define U as the set of prefixes of elements in the sequence pu i q iě0 : U is a branch as the sequence pu i q iě0 is increasing.

For all i, pick a branch V i that goes through u i but not through u i`1 (it exists by definition of u i ). Then to obtain a pseudo comb pU,

V q such that U Y V Ď W , it suffices to define V " p Ť iě0 V i qzU .
Now, fix a tree t and define an acceptance game for L Acc 8 pAq. There are two modes in the game (See Figure 5 for the local structure of the arena): path mode and check mode and the game starts in path mode. Hence, (Éloïse's) configurations in the game are elements of Q ˆt0, 1u ˚ˆtpath, checku. In path mode, in a node u with state q Éloïse picks a transition pq, tpuq, q 0 , q 1 q P ∆, and she chooses a direction i P t0, 1u. Then Éloïse has two options. Either she moves down the pebble to u ¨i and updates the state to be q i . Or she proposes Abélard to change to check mode: if he accepts, the pebble is moved down to u ¨p1 ´iq and the state is updated to q p1´iq ; if he refuses, the pebble is moved down to u ¨i and the state is updated to q i (and the game stays in path mode).

In check mode Éloïse plays alone: in a node u with state q she picks a transition pq, tpuq, q 0 , q 1 q P ∆, and she chooses a direction i P t0, 1u; then the pebble is moved down to u ¨i and the state is updated to q i . Note that it is not possible to switch from check mode back to path mode.

A play is won by Éloïse if one of the two following situations occurs.

q, u q, u, q 0 , q 1 , 0 q, u, q 0 , q 1 , 1 q 0 , u0 q 1 , u1 q, u, q 0 , q 1 , 0 q, u, q 0 , q 1 , 1 q 1 , u1 q 0 , u0 q, u q, u, q 0 , q 1 , 0 for any pq, tpuq, q 0 , q 1 q P ∆ path mode check mode for any pq, tpuq, q 0 , q 1 q P ∆ • Eventually the players have switched to check mode and the parity condition is satisfied.

• Éloïse proposed infinitely often Abélard to switch the mode but he always refused.

Call this game G Acc 8 A,t . Intuitively path mode is used to define the U part of the pseudo-comb pU, V q and each of the branches in V is inspected in check mode. Note that in check mode, Éloïse plays alone and hence only checks the existence of an accepting branch. However, as the automata we consider are assumed to be complete hence, there always exists some run containing this accepting branch.

The next theorem states that it is an acceptance game for the language L Acc 8 pAq. from configuration pq ini , ε, pathq. With ϕ we associate a run ρ of A on t and a pseudo comb pU, V q as follows. We inductively associate with any node u P U a partial play λ u where Éloïse respects ϕ and that is always in path mode; and we inductively associate with any node v P V a partial play λ v where Éloïse respects ϕ and where the mode has eventually been switched to check mode. For this we let ε P U and λ ε " pq ini , ε, pathq. Now assume that we defined λ u for some node u P U and let pq, tpuq, q 0 , q 1 q be the transition and let i be the direction Éloïse plays from λ u when she respects ϕ. Then we have two possible situations depending whether, right after playing pq, tpuq, q 0 , q 1 q and still respecting ϕ, Éloïse proposes Abélard to switch to check mode.

• If she does so we let u¨p1´iq belong to V and we define λ u¨p1´iq as the partial play obtained by extending λ u by Éloïse choosing transition pq, tpuq, q 0 , q 1 q and direction i, followed by Éloïse proposing Abélard to switch the mode and Abélard accepting (hence, moving down the pebble in direction p1 ´iq and attaching state q p1´iq to it). We let u ¨i belong to U and we define λ u¨i as the partial play obtained by extending λ u by Éloïse choosing transition pq, tpuq, q 0 , q 1 q and direction i, followed by Éloïse proposing Abélard to switch the mode and Abélard refusing (hence, moving down the pebble in direction i and attaching state q i to it).

• If Éloïse does not propose Abélard to switch the mode we do not let u ¨p1 ´iq belong to V . And we let u ¨i belong to U and we define λ u¨i as the partial play obtained by extending λ u by Éloïse choosing transition pq, tpuq, q 0 , q 1 q and direction i, followed by Éloïse not proposing Abélard to switch the mode (hence, moving down the pebble in direction i and attaching state q i to it).

The run ρ is defined by letting, for any w P U Y V , ρpwq be the state attached to the pebble in the last configuration of λ w . For those w R U Y V we define ρpwq so that the resulting run is valid, which is always possible as we only consider complete automata. By construction, ρ is a run of A on t and pU, V q is a pseudo comb. Moreover with any branch π that can be built as an initial sequence of nodes in U followed by an infinite sequence of nodes in V one can associate a play λ π in G Acc 8 A,t from pq ini , ε, pathq where Éloïse respects ϕ (one simply considers the limit of the increasing sequence of partial plays λ v where v ranges those nodes nodes in V along branch π). By construction π is accepting as λ π fulfils the parity condition. Hence, by Lemma 2 we conclude that ρ contains infinitely many accepting branches, meaning that t P L Acc 8 pAq. Conversely, assume that Éloïse does not have a winning strategy in G Acc 8 A,t from pq ini , ε, pathq. By Borel determinacy, Abélard has a winning strategy ψ in G Acc 8 A,t from pq ini , ε, pathq. By contradiction, assume that there is a run ρ of A on t that contains infinitely many accepting branches. By Lemma 2, it follows that ρ contains a pseudo comb pU, V q such that any branch that can be built as an initial sequence of nodes in U followed by an infinite sequence of nodes in V is an accepting branch. From ρ and pU, V q we define a strategy ϕ of Éloïse in G Acc 8 A,t from pq ini , ε, pathq as follows. Strategy ϕ uses as a memory either a node u P U if the play is in path mode or a node v P V if the play is in check mode; initially the memory is u " ε. Now assume that the pebble is in some node u P U with state q attached to it (one will inductively check that ρpuq " q). Then there are two possibilities.

• Both u0 and u1 belong to U YV : the strategy ϕ indicates that Éloïse chooses transition pq, tpuq, ρpu0q, ρpu1qq and direction i where ui P U and proposes Abélard to switch to check mode. Then the memory is updated to u ¨j where j " i if the mode is unchanged and j " 1 ´i otherwise.

• If u0 (resp. u1) belongs to U but u1 (resp. u0) does not belong to V : strategy ϕ indicates that Éloïse chooses the transition pq, tpuq, ρpu0q, ρpu1qq and chooses the direction 0 (resp. 1) and does not propose Abélard to switch to check mode. Then the memory is updated to u0 (resp. u1).

Now assume that the pebble is in some node v P V with state q attached to it: one will inductively check that ρpvq " q and that the mode is check. Call i the (unique) direction such that vi belongs to V : then the strategy ϕ indicates that Éloïse chooses transition pq, tpvq, ρpv0q, ρpv1qq and then moves down the pebble to direction vi. In particular, once a node in V is reached, strategy ϕ ensures that the pebble always stays in V for the rest of the play. Now consider the (unique) play λ where Éloïse respects her strategy ϕ while Abélard respects his strategy ψ. As we assumed ψ to be a winning strategy for Abélard, λ is won by him. Now, as pU, V q is a pseudo comb and by definition of ϕ, it follows that λ only goes through nodes in U Y V , and if λ only goes through nodes in U then Éloïse proposes infinitely often to Abélard to switch to check mode. Hence, as λ is winning for Abélard one concludes that eventually the mode is switched in λ and that the resulting play does not fulfil the parity condition. Now, it is easily seen that with λ one associates a branch π in the run ρ and that this branch can be built as an initial sequence of nodes in U followed by an infinite sequence of nodes in V (indeed, at some point the mode is switched to check and from that point the play stays in nodes from V forever). Now, by definition of a pseudo comb, it follows that the branch π is accepting in ρ which means that it satisfies the parity condition, and therefore so does λ, which brings a contradiction with the fact that it is won by Abélard.

One can modify G Acc 8

A,t so that to obtain an equivalent game that has the form of a classical acceptance game. From this follows the fact that the languages of the form L Acc 8 pAq are indeed ω-regular. As the new game can be seen to be obtained from a Büchi automaton, this also permits to lower the acceptance condition. Theorem 8. Let A " xA, Q, q ini , ∆, Coly be a parity tree automaton using d colours. Then there exists a Büchi tree automaton

A 1 " xA, Q 1 , q 1 ini , ∆ 1 , Col 1 y such that L Acc 8 pAq " LpA 1 q. Moreover |Q 1 | " Opd|Q|q. Proof. Start from game G Acc 8 A,t
and observe that if one duplicates the control states (with a classical version and a starred version of each state) and add a Boolean flag Éloïse can indicate the direction she wants to follow and whether she proposes to switch to check mode: e.g. if she wants to choose transition pq, tpuq, q 0 , q 1 q and direction 1 and not change the mode, she just moves to configuration pq, u, q 0 , q 1 , Kq in the new game; if she wants to choose transition pq, tpuq, q 0 , q 1 q and direction 0 and offer Abélard the option to switch to check mode she moves to configuration pq, u, q 0 , q 1 , Jq. Now, we allow Abélard to choose any direction but if the corresponding state is not starred then either one goes to a dummy winning configuration for Éloïse if the Boolean was K and otherwise one changes the mode to check. We indicate the check mode in the control state and we use the same trick to let Éloïse impose the choice of the branch (if Abélard does not follow her choice one ends up in the previous dummy configuration). It should be clear that the resulting game is an equivalent acceptance game when equipped with the following winning condition: Éloïse wins if either the dummy configuration is reached, or infinitely many configuration with Boolean J are visited but the play is always in path mode or the play is eventually in check mode and the parity condition holds. Now, the two first criteria are Büchi criteria while the third one is a priori a parity condition. But as Éloïse plays alone in check mode, she can indicate at some point that the smallest infinitely visited colour will be some (even) integer and that no other smaller colour will latter be visited: hence, if one stores the colour, go to a final state whenever it is visited and to a rejecting state if some smaller colour occurs, then one obtains a Büchi condition. All together (combining the Büchi conditions in the usual way) one obtains an equivalent Büchi classical acceptance game, showing that L Rej ďCount pAq is ω-regular and accepted by a Büchi automaton. The construction of A 1 is immediate from the final game and the size is linear in d|Q| due to the fact that one needs to remember the smallest colour for the check mode.

The Case of Languages L Acc

U ncount pAq We now discuss the case of languages of the form L Acc U ncount pAq. For this we with some key objects (accepting pseudo binary trees and k-pseudo binary trees) that are used to characterise runs with uncountably many accepting branches. Then, we describe two acceptance games: the first one is very simple while the second one is more involved but later permits to lower the acceptance condition to Büchi when showing that the languages L Acc U ncount pAq are accepted by tree automata with the classical semantics.

Accepting-Pseudo Binary Tree & k-Pseudo Binary Tree

The key idea behind defining an acceptance game for L Acc U ncount pAq for some tree t is to exhibit an accepting pseudo binary tree in a run of A over t. In a nutshell, an accepting pseudo binary tree is an infinite set U of nodes with a tree-like structure between them and such that any branch that has infinitely many prefixes in U is accepting.

We now formally define accepting-pseudo binary trees and k-pseudo binary trees that characterise those runs that contains uncountably many accepting branches (Lemma 3 and Lemma 4 below). Let A " xA, Q, q ini , ∆, Coly be a parity tree automaton and let ρ be a run of A on some tree t. An accepting-pseudo binary tree in ρ (see Figure 6 for an illustration) is a subset U Ď t0, 1u ˚of nodes such that (i) for all u P U there are v, w P U such that v " u0v 1 and w " u1w 1 for some v 1 and w 1 P t0, 1u ˚;

(ii) for all v, w P U the longest common prefix u of v and w belongs to U ;

(iii) any branch π that goes through infinitely many nodes in U is accepting.

We now give a stronger notion than accepting-pseudo binary tree. For this, let k be some even colour. A k-pseudo binary tree in ρ (see Figure 7 for an illustration) is a subset U Ď t0, 1u ˚of nodes such that (i) for all u P U there are v, w P U such that v " u0v 1 and w " u1w 1 for some v 1 and w 1 P t0, 1u (ii) for all v, w P U the largest common prefix u of v and w belongs to U ;

˚; ' ' ' ' ' ' min " k
(iii) for all u, v P U such that u Ă v, one has mintColpρpwqq | u Ď w Ď vu " k.

The following lemma characterises runs that contain an uncountable sets of accepting branches. Its proof is a direct consequence of [START_REF] Beauquier | Automata on infinite trees with path counting constraints[END_REF]Lemma 2]. But for the sake of completeness, we give a proof here. Lemma 3. Let ρ be a run. Then ρ contains uncountably many accepting branches if and only if it contains a k-pseudo binary tree for some even colour k.

Proof. Clearly if ρ contains a k-pseudo binary tree for some even colour k, ρ contains uncountably many accepting branches. It remains to prove the converse.

Let ρ be a run with uncountably many accepting branches. For an even colour k and a node u in ρ, we denote by Π k,u the set of branches π of ρ such that:

• π goes through u (i.e. u Ď π),

• the smallest colour appearing infinitely often in π is k,

• no colour strictly smaller than k appears below u (i.e. for all u Ď v Ď π, ρpvq ě k).

As the set of all accepting branches in ρ is equal to the (countable) union of all the Π k,u , there exists an even colour k 0 and a node u 0 such that Π k0,u0 is uncountable. In the following, we write Π for Π k0,u0 .

Claim. For all nodes u Ě u 0 such that uncountably many branches of Π go through u, there exists a node w u such that:

• w u is a strict descendant of u (i.e. u Ă w u ), • mintColpρpvqq | u Ď v Ď w u u " k 0 ,
• there are uncountably many branches of Π going though w u 0 and through w u 1.

If we assume that the claim holds, we can construct a k 0 -pseudo binary tree by considering the smallest set U such that w u0 belongs to U and such that for all v, v P U implies w v0 P U and w v1 P U .

Hence, it remains to show that the claim holds. Let u Ě u 0 be a node such that uncountably many branches of Π go through u. Consider the sets:

X :" tv Ě u | mintColpρpvqq | u Ď w Ď vu " k 0 and uncountably many branches of Π go through v u Y :" tv Ě u | mintColpρpvqq | u Ď w Ď vu " k 0
and countably many branches of Π go through v u A branch π P Π that goes through u must contain a node in X Y Y . There are two cases:

1. either it contains a node in Y , 2. or after some position all nodes in π belong to X.

As there are at most countably many branches satisfying Case 1, there must be uncountably many branches satisfying Case 2. In turn this implies that there exists v P X such that both v0 and v1 also belong to X and we can simply take w u to be such a v. Indeed if it was not the case, there would be exactly one branch of Π satisfying Case 2 and going through any given vertex in X: the set of branches satisfying Case 2 would be at most countable.

As any k-pseudo binary tree is an accepting-pseudo binary tree, we directly have the following Lemma from Lemma 3. Lemma 4. Let ρ be a run. Then ρ contains uncountably many accepting branches if and only if it contains an accepting-pseudo binary tree.

The Acceptance Game G Acc Uncount

A,t q, u q, u, q 0 , q 1 q 0 , u0 q 1 , u1 q, u, q 0 , q 1 for any pq, tpuq, q 0 , q 1 q P ∆ Fix a tree t and define an acceptance game for L Acc U ncount pAq. In this game (see Figure 8 for the local structure of the arena) the two players move a pebble along a branch of t in a top-down manner: to the pebble is attached a state, and the colour of the state gives the colour of the configuration. Hence, (Éloïse's main) configurations in the game are elements of Q ˆt0, 1u ˚. In a node u with state q Éloïse picks a transition pq, tpuq, q 0 , q 1 q P ∆, and then Éloïse has two options. Either she chooses a direction 0 or 1 or she lets Abélard choose a direction 0 or 1. Once the direction i P t0, 1u is chosen, the pebble is moved down to u ¨i and the state is updated to q i . A play is won by Éloïse if and only if (1) the parity condition is satisfied and

(2) Éloïse lets Abélard infinitely often choose the direction during the play.

Call this game G Acc Uncount

A,t . The next theorem states that it is an acceptance game for the language L Acc U ncount pAq.

Theorem 9. Éloïse wins in G Acc Uncount

A,t from pq ini , εq if and only if t P L Acc U ncount pAq.

Proof. In the following proof for a set X Ď t0, 1u ˚we denote by P ref pXq the set of prefixes of elements in X, i.e. PrefpXq " tu | Dv P X s.t. u Ď vu.

Assume that Éloïse has a winning strategy ϕ in G Acc Uncount A,t from pq ini , εq. With ϕ we associate a run ρ of A on t and an accepting-pseudo binary tree U as follows. We inductively define U and PrefpU q and associate with any node u P PrefpU q a partial play λ u where Éloïse respects ϕ. Remark that even if PrefpU q is uniquely determined by U we independently define them, making sure that they are indeed compatible. For this we let ε P PrefpU q and we set λ ε " pq ini , εq.

Now assume that we have defined λ u for some node u P PrefpU q. Then let pq, tpuq, q 0 , q 1 q be the transition Éloïse plays from λ u when she respects ϕ. Then we have two possible situations depending whether, right after playing pq, tpuq, q 0 , q 1 q and still respecting ϕ, Éloïse chooses the direction or lets Abélard make that choice. If she chooses the direction, let i be this direction: then one lets ui P PrefpU q and defines λ u¨i as the partial play obtained by extending λ u by Éloïse choosing transition pq, tpuq, q 0 , q 1 q, followed by Éloïse choosing direction i. If she lets Abélard choose the direction, one lets u belong to U and lets both u0 and u1 belongs to PrefpU q and defines λ u¨i for i P t0, 1u as the partial play obtained by extending λ u by Éloïse choosing transition pq, tpuq, q 0 , q 1 q, followed by Éloïse letting Abélard choose the direction and Abélard picking direction i. Note that for any ui P PrefpU q, λ u¨i ends with the pebble on u ¨i with state q i attached to it, equivalently in configuration pq i , uiq.

The run ρ is defined by letting, for any u P PrefpU q, ρpuq be the state attached to the pebble in the last configuration of λ u . For those u R PrefpU q we define ρpuq so that the resulting run is valid, which is always possible as we only consider complete automata. By construction, ρ is a run of A on t. Moreover, with any branch π consisting only of nodes in PrefpU q, one can associate a play λ π in G Acc Uncount A,t from pq ini , εq where Éloïse respects ϕ (one simply considers the limit of the increasing sequence of partial plays λ u where u ranges over nodes along branch π). As λ π is winning it follows easily that U is a pseudo binary tree (indeed, condition piq and piiq from the definition of an accepting-pseudo binary tree are immediate, while condition piiiq follows from the fact that λ π is winning). Hence, from Lemma 4 we conclude that ρ contains uncountably many accepting branches, meaning that t P L Acc U ncount pAq. Conversely, assume that there is a run ρ of A on t that contains uncountably many accepting branches. By Lemma 4, it follows that ρ contains an accepting-pseudo binary tree U .

From ρ and U we define a strategy ϕ of Éloïse in G Acc Uncount A,t from pq ini , εq as follows. Strategy ϕ uses as a memory a node v P PrefpU q, and initially v " ε. Now assume that the pebble is on some node v with state q attached to it (one will inductively check that v P PrefpU q and that ρpvq " q). Then we have two possibilities.

• Assume v P U . Both v0 and v1 belong to PrefpU q: strategy ϕ indicates that Éloïse chooses transition pq, tpvq, ρpv0q, ρpv1qq and let Abélard choose the direction, say i. Then the memory is updated to v ¨i.

• Assume v R U . Hence, v ¨i belong to PrefpU q for only one i P t0, 1u: strategy ϕ indicates that Éloïse chooses transition pq, tpvq, ρpv0q, ρpv1qq and chooses direction i. Then the memory is updated to v ¨i.

Now consider a play λ where Éloïse respects her strategy ϕ. It is easily seen that with λ one associates a branch π in the run ρ and that this branch goes only through nodes in PrefpU q. From this observation and from the definition of an accepting-pseudo binary tree, we conclude that λ is winning for Éloïse (it satisfies the parity condition as π does and in λ Éloïse lets Abélard choose the direction infinitely often, namely whenever her memory v belongs to U ). Hence, we conclude that strategy ϕ is winning from pq ini , εq.

The Acceptance Game r G Acc Uncount

A,t

One can modify G Acc Uncount A,t

to obtain an equivalent game that has the form of a classical acceptance game. From this follows the fact that the languages of the form L Acc U ncount pAq are indeed ω-regular. Nevertheless, using a more involved game than G Acc Uncount A,t one can obtain a stronger result where the acceptance condition is lowered to a Büchi condition. We now describe this game.

Fix a tree t and define an acceptance game for L Acc U ncount pAq. There are two modes in the game (See Figure 9 for the local structure of the arena): wait mode and check mode and the game starts in wait mode. Moreover the check mode is parametrised by a colour k. Again, the two players move a pebble along a branch of t in a top-down manner. Hence, (main) configurations in the game are elements of Q ˆt0, 1u ˚ˆtwait, check 0 , . . . , check 2 u where t0, . . . , 2 u are the even colours used by A. In wait mode Éloïse plays alone: in a node u with state q she picks a transition pq, tpuq, q 0 , q 1 q P ∆, and she chooses a direction i P t0, 1u; then the pebble is moved down to u ¨i and the state is updated to q i . When moving the pebble down she can decide to switch the mode to some check k (for any even colour k). Once entered check k mode the play stays in that mode forever and goes as follows. In a node u with state q Éloïse picks a transition pq, tpuq, q 0 , q 1 q P ∆, and then she has two possible options. Either she chooses a direction 0 or 1 or she lets Abélard choose a direction 0 or 1. Once the direction i P t0, 1u is chosen, the pebble is moved down to u ¨i and the state is updated to q i . A play is won by Éloïse if and only if (1) it eventually enters some check k mode and

(2) it goes infinitely often through configurations in tpq, u, check k q | Colpqq " ku,

(3) it never visits a configuration in tpq, u, check k q | Colpqq ă ku, q 1 , u1 q 0 , u0 q, u q, u, q 0 , q 1 , 0 wait mode for any pq, tpuq, q 0 , q 1 q P ∆ for any even colour k q, u q, u, q 0 , q 1 q 0 , u0 q 1 , u1 q, u, q 0 , q 1 for any pq, tpuq, q 0 , q 1 q P ∆ check k mode (4) Éloïse lets Abélard infinitely often choose the direction during the play, and between two such situations the smallest colour visited is always k.

The next theorem states that it is an acceptance game for the language L Acc U ncount pAq. Note that its proof is a refinement of the one of Theorem 9. Proof. In the following proof for a set X Ď t0, 1u ˚we denote by P ref pXq the set of prefixes of elements in X, i.e. PrefpXq " tu | Dv P X s.t. u Ď vu.

Assume that Éloïse has a winning strategy ϕ in r G Acc Uncount A,t from pq ini , ε, waitq. With ϕ we associate a run ρ of A on t and a k-pseudo binary tree U (for some k to be defined later) as follows. We inductively define U and PrefpU q (even if PrefpU q is uniquely determined by U we independently define them, making sure that they are indeed compatible) and associate with any node u P PrefpU q a partial play λ u where Éloïse respects ϕ. For this we let ε P PrefpU q and we let λ ε " pq ini , ε, waitq.

Now assume that we have defined λ u for some node u P PrefpU q and that the mode in λ u is always wait. Then let pq, tpuq, q 0 , q 1 q be the transition and let i be the direction Éloïse plays from λ u when she respects ϕ. If she does not change the mode, then one lets ui P PrefpU q and defines λ u¨i as the partial play obtained by extending λ u by Éloïse choosing transition pq, tpuq, q 0 , q 1 q, followed by Éloïse choosing direction i and keeping the mode to wait. If she changes the mode to check k , then one lets ui P PrefpU q and defines λ u¨i as the partial play obtained by extending λ u by Éloïse choosing transition pq, tpuq, q 0 , q 1 q, followed by Éloïse choosing direction i and changing the mode to check k (this k is the one such that U is a k-pseudo binary tree U ). Now assume that we have defined λ u for some node u P PrefpU q and that the mode in λ u has been switched from wait to check k . Then let pq, tpuq, q 0 , q 1 q be the transition Éloïse plays from λ u when she respects ϕ. Then we have two possible situations depending whether, right after playing pq, tpuq, q 0 , q 1 q and still respecting ϕ, Éloïse chooses the direction or lets Abélard make that choice. If she chooses the direction, let i be this direction: then one lets ui P PrefpU q and defines λ u¨i as the partial play obtained by extending λ u by Éloïse choosing transition pq, tpuq, q 0 , q 1 q, followed by Éloïse choosing direction i. If she lets Abélard choose the direction, one lets u belongs to U and lets both u0 and u1 belongs to PrefpU q and defines λ u¨i for i P t0, 1u as the partial play obtained by extending λ u by Éloïse choosing transition pq, tpuq, q 0 , q 1 q, followed by Éloïse letting Abélard choose the direction and Abélard picking direction i. Note that for any ui P PrefpU q, λ u¨i ends with the pebble on u ¨i with state q i attached to it, equivalently in configuration pq i , uiq.

The run ρ is defined by letting, for any u P PrefpU q, ρpuq be the state attached to the pebble in the last configuration of λ u . For those u R PrefpU q we define ρpuq so that the resulting run is valid, which is always possible as we only consider complete automata. By construction, ρ is a run of A on t. Moreover with any branch π consisting only of nodes in PrefpU q one can associate a play λ π in r G Acc Uncount A,t from pq ini , ε, waitq where Éloïse respects ϕ (one simply considers the limit of the increasing sequence of partial plays λ u where u ranges over nodes along branch π). As λ π is winning it follows easily that U is a k-pseudo binary tree (indeed, condition piq and piiq from the definition of a k-pseudo binary tree are immediate, while condition piiiq follows from the definition of the winning condition and of the fact that λ π is winning). Moreover π is accepting as the smallest colour infinitely often visited is k. As there are uncountably many branches π consisting only of nodes in PrefpU q we conclude that ρ contains uncountably many accepting branches, meaning that t P L Acc U ncount pAq. Conversely, assume that there is a run ρ of A on t that contains uncountably many accepting branches. By Lemma 3, it follows that ρ contains a k-pseudo binary tree U . Let X " tx P PrefpU q | ρpxq ą ku: then by definition of a k-pseudo binary tree we conclude that X is finite and has a minimal element for the prefix relation (with the convention that if X is empty this minimum is set to be the root ε); call r this minimum. Note that there is also a minimum element u 0 in U (for the prefix relation) and that r Ă u 0 .

From ρ and U we define a strategy ϕ of Éloïse in r G Acc Uncount A,t from pq ini , ε, waitq as follows. Strategy ϕ uses as a memory a node v P PrefpU q and initially v " ε; moreover as long as v Ď r the play will be in wait mode. Now assume that the pebble is on some node v with state q attached to it (one will inductively check that v P PrefpU q and that ρpvq " q). Then we have several possibilities.

• The mode is wait (i.e. v Ď r Ă u 0 ): strategy ϕ indicates that Éloïse chooses transition pq, tpvq, ρpv0q, ρpv1qq, goes to direction i where i is such that vi Ď u 0 , and stay in mode wait except if v " r where the mode is switched to check k .

• The mode is check k and v P U . Both v0 and v1 belong to PrefpU q: strategy ϕ indicates that Éloïse chooses transition pq, tpvq, ρpv0q, ρpv1qq and let Abélard choose the direction, say i. Then the memory is updated to v ¨i.

• The mode is check k and v R U . Hence, v ¨i belong to PrefpU q for only one i P t0, 1u: strategy ϕ indicates that Éloïse chooses transition pq, tpvq, ρpv0q, ρpv1qq and chooses direction i. Then the memory is updated to v ¨i.

Now consider a play λ where Éloïse respects her strategy ϕ. It is easily seen that with λ one associates a branch π in the run ρ and that this branch goes only through nodes in PrefpU q. From this observation and from the definition of a k-pseudo binary tree, we conclude that λ is winning for Éloïse hence, that strategy ϕ is winning from pq ini , ε, waitq.

Remark 2. In the winning condition we can remark the following (the first two points are obvious, the third one requires to adapt the proof of Theorem 10 that then can simplify the construction of a Büchi automaton accepting L Acc U ncount pAq (see Theorem 11 below). Condition ( 1) is in fact implied by Condition [START_REF] Rabin | Automata on infinite objects and Church's problem[END_REF]. Condition (3) can be enforced by removing the edges of the game graph that violate it. Condition (4) can be replaced by:

(5) Éloïse lets Abélard infinitely often choose the direction during the play. while preserving the validity of Theorem 10. Indeed, one can remark that if we require condition (5) instead of Condition (4) and follows the same lines as in the proof of Theorem 10 in the direct implication (the converse implication is unchanged) the pseudo binary tree we build from a winning strategy ϕ for Éloïse may no longer be a k-pseudo binary tree; however, thanks to Condition (2), one can easily extract a k-pseudo binary tree from it.

Languages of the Form L Acc

U ncount pAq Are Büchi Regular Thanks to Theorem 10 we can easily prove that any language of the form L Acc U ncount pAq can be accepted by a Büchi automaton. Theorem 11. Let A " xA, Q, q ini , ∆, Coly be a parity tree automaton using d colours. Then there exists a Büchi tree automaton A 1 " xA, Q 1 , q 1 ini , ∆ 1 , Col 1 y such that L Acc U ncount pAq " LpA 1 q. Moreover |Q 1 | " Opd|Q|q.

Proof. One can easily transform game r G Acc Uncount A,t

to obtain an equivalent game that is the acceptance game of some tree automaton A 1 with the classical semantics. The construction is very similar to the one we had for the other cases and we omit the details here. It simply suffices to notice that the winning condition in r G Acc Uncount A,t is a conjunction of Büchi conditions, hence can be rephrased as a Büchi condition (up to adding some flags).

Checking Topological Largeness of Accepting Branches

We now consider the case of automata with topological bigness constraints and we prove that languages of the form L Acc Large pAq are always ω-regular (Theorem 13). This acceptance condition is referred to as the best model of a fair adversary in [START_REF] Völzer | Defining fairness[END_REF], and finite games where Éloïse plays against such an adversary have been studied and solved in [START_REF] Asarin | Fair adversaries and randomization in two-player games[END_REF]. We first characterise large set of branches (Lemma 5), then based on this, we define an acceptance game for L Acc Large pAq and finally we transform it to obtain an equivalent game that has the form of a classical acceptance game from which we extract an equivalent automaton with a classical semantic.

The Banach-Mazur theorem gives a game characterisation of large and meager sets of branches (see for instance [START_REF] Kechris | Classical Descriptive Set Theory[END_REF][START_REF] Grädel | Banach-Mazur Games on Graphs[END_REF]). The Banach-Mazur game on a tree t, is a two-player game where Abélard and Éloïse choose alternatively a node in the tree, forming a branch: Abélard chooses first a node and then Éloïse chooses a descendant of the previous node and Abélard chooses a descendant of the previous node and so on forever. In this game it is always Abélard that starts a play.

Formally a play is an infinite sequence u 1 , u 2 , . . . of words in t0, 1u `, and the branch associated with this play is u 1 u 2 ¨¨¨. A strategy for Éloïse is a mapping ϕ : pt0, 1u `q`Ñ t0, 1u `that takes as input a finite sequence of words, and outputs a word. A play u 1 , u 2 , . . . respects ϕ if for all i ě 1, u 2i " ϕpu 1 , . . . , u 2i´1 q. We define Outcomespϕq as the set of plays that respect ϕ and Bpϕq as the set branches associated with the plays in Outcomespϕq.

The Banach-Mazur theorem (see7 e.g. [START_REF] Grädel | Banach-Mazur Games on Graphs[END_REF]Theorem 4]) states that a set of branches B is large if and only if there exists a strategy ϕ for Éloïse such that Bpϕq Ď B.

Furthermore a folk result (see e.g. [START_REF] Grädel | Banach-Mazur Games on Graphs[END_REF]Theorem 9]) about Banach-Mazur games states that when B is Borel8 one can look only at "simple" strategies, defined as follows. A decomposition-invariant strategy is a mapping f : t0, 1u ˚Ñ t0, 1u `and we associate with f the strategy ϕ f defined by ϕ f pu 1 , . . . , u k q " f pu 1 ¨¨¨u k q. Finally, we define Outcomespf q " Outcomespϕ f q and Bpf q " Bpϕ f q. The folk result states that for any Borel set of branches B, there exists a strategy ϕ such that Outcomespϕq Ď B if and only if there exists a decomposition-invariant strategy f such that Bpf q Ď B.

Call a set of nodes W Ď t0, 1u ˚dense if @u P t0, 1u ˚, Dw P W such that u Ď w. Given a dense set of nodes W , the set of branches supported by W , BpW q is the set of branches π that have infinitely many prefixes in W . Using the existence of decomposition-invariant winning strategies in Banach-Mazur games, the following lemma characterises large sets of branches. Lemma 5. A Borel subset of branches B Ď t0, 1u ω is large if and only if there exists a dense set of nodes W Ď t0, 1u ˚such that BpW q Ď B.

Proof. Assume that B is large and let f be a decomposition-invariant strategy for Éloïse in the associated Banach-Mazur game (recall that we assumed B to be Borel). Consider the set:

W " tvf pvq | v P t0, 1u ˚u.
The set W is dense (as for all v P t0, 1u ˚, v Ă vf pvq P W ). We claim that BpW q is included in B. Let π be a branch in BpW q. As π has infinitely many prefixes in W , there exists a sequence of words u 1 , u 2 , ¨¨¨such that u 1 f pu 1 q Ă u 2 f pu 2 q Ă ¨¨¨Ă π. As the lengths of the u i are strictly increasing, there exists a sub-sequence pv i q iě1 of pu i q iě1 such that for all i ě 1, v i f pv i q Ă v i`1 . Now, consider the play in the Banach-Mazur game where Abélard first moves to v 1 and then Éloïse responds by going to v 1 f pv 1 q. Then Abélard moves to v 2 (which is possible as v 1 f pv 1 q Ă v 2 ) and Éloïse moves to v 2 f pv 2 q. And so on. In this play Éloïse respects the strategy f and therefore wins. Hence, the branch π associated to this play belongs to B.

Conversely let W be a dense set of nodes such that BpW q Ď B. To show that B is large, we define a decomposition-invariant strategy f for Éloïse in the associated Banach-Mazur game. For all nodes u we pick v of W such that u is a strict prefix of v (since W is dense there must always exist such a v). Let v " uu 1 and fix f puq " u 1 . A play where Éloïse respects f goes through infinitely many nodes in W (as f always points to an element in W ). Hence, the branch associated with the play belongs to BpW q Ď B which shows that f is winning for Éloïse.

We aim to define, for a given tree an acceptance game witnessing membership into L Acc Large pAq. In this game, Éloïse describes a run ρ together with a dense set U of nodes while Abélard tries either to prove that U is not dense or that there is a rejecting branch in BpU q. The way Éloïse describes a run is as usual (she proposes valid transitions); the way she describes U is by (1) indicating explicitly when a node is in U and;

(2) at each node giving a direction i that should lead (by iteratively following the directions) to a node in U . Abélard chooses the direction: if it does not select i and does not go to a node in U the colour is a large even one (preventing him not to follow Éloïse forever); if he chooses i but does not go to a node in U the colour is a large odd one (forcing Éloïse to describe a dense set U ); and if he chooses i and goes to a node in U the colour is the smallest one seen since the last visit to a node in U (and it is computed in the game).

Before formally constructing the game we need the following lemma. A direction mapping is a mapping d : t0, 1u ˚Ñ t0, 1u, and given a set of nodes U , we say that d points to U if for every node v there exists i 1 , . . . , i k P t0, 1u such that vi 1 ¨¨¨i k P U and for all 1 ď j ď k, i j " dpvi 1 ¨¨¨i j´1 q. Lemma 6. A set of nodes U is dense if and only if there exists a direction mapping that points to U .

Proof. Assume that U is dense. We define dpvq by induction on v as follows. Let v such that dpvq is not yet defined, we pick a node vi 1 ¨¨¨i k P U (there must exists one since U is dense), and for all j ď k we define dpvi 1 ¨¨¨i j´1 q " i j .

The mapping is defined on every node and satisfies the requirement by definition. The other implication is straightforward (for all nodes v, there exists vi 1 ¨¨¨i k P U ).

Fix a tree t and define an acceptance game G Acc Large A,t for L Acc Large pAq as follows. The game is played along a tree, Éloïse chooses the transitions of the automaton and Abélard chooses the directions. Furthermore, at each node Éloïse proposes a direction that Abélard may or may not follow, and possibly marks some of the children of the current state. In Éloïse's vertices, we keep track of informations about the choice of Abélard in his previous move differentiating three possible situations: (‹) Abélard has picked a child that Éloïse has marked, (˝) Abélard has not picked a marked child, but he has followed the direction that Éloïse has given, (˝) Abélard has not picked a marked child and has not followed the direction given by Éloïse. Therefore Éloïse's vertices will be of the form pq, u, symbq with q a state, u a node, and symb P t‹, ˝, ˝u, and we define the colour of this vertex as the colour of q, and Abélard's state will be of the form pq, u, q 0 , q 1 , i, Sq where pq, tpuq, q 0 , q 1 q is a transition of the automaton, i P t0, 1u is the direction that Éloïse has proposed in the previous turn and S Ď t0, 1u describes which children of u she marked (see Figure 10 for the local structure of the game).

The acceptance condition for Éloïse is described as follows. She wins a play if and only if one of the following occurs.

• There are infinitely many ‹-vertices and the smallest colour appearing infinitely often is even

• Eventually there are no more ‹-vertices but there are infinitely often ˝-vertices, i.e. Abélard stop visiting marked nodes and avoids infinitely often the directions given by Éloïse.

q, u, symb q, u, q 0 , q 1 , i, S q j , u ¨j, ‹ q i , u ¨i, qj , u ¨j, for any symb P t‹, ˝, ˝u for any pq, tpuq, q 0 , q 1 q P ∆, any i P t0, 1u and any S Ď t0, 1u

for any j P t0, 1u s.t. j P S for any j P t0, 1u s.t. j ‰ i and j R S if i R S Call G Acc Large A,t this game. Intuitively a strategy of Éloïse is a run of the automaton over the tree, along with a set U of marked nodes and directions on each of the nodes, and Abélard chooses a branch along the tree. If at some point Abélard follows forever the directions given by Éloïse without going through a marked node, then Abélard wins. If Abélard goes infinitely often through a marked node, then the smallest colour seen infinitely often is the one of the branch in the run of Éloïse, therefore Éloïse wins if this branch is accepting. These two remarks intuitively mean that if Éloïse has a winning strategy, then the set U of marked nodes implied by this strategy must be a dense set and BpU q must consist only of accepting branches of the run, therefore the set of accepting branches of the run is large.

On the other hand, if there exists a run whose set of accepting branches is large, there exists a dense set of nodes U such that all branches in BpU q are accepting (Lemma 5), and directions on each nodes that leads to nodes in U (Lemma 6). If Éloïse plays according to them, she wins the game. Indeed, if Abélard follows infinitely often the nodes in U , then the branch is an accepting branch and therefore Éloïse wins the game. His only option to avoid the nodes of U is to infinitely often go in the opposite direction than the one given by Éloïse, in which case Éloïse also wins.

The next theorem states that G from pq ini , ε, ˝q. With ϕ we associate a run ρ of A on t as follows. We inductively associate with any node u a partial play λ u where Éloïse respects ϕ. For this we let λ ε " pq ini , ε, ˝q. Now assume that we defined λ u for some node u and let pq, tpuq, q 0 , q 1 , i, Sq be the transition Éloïse plays from λ u when she respects ϕ.

For j P t0, 1u, one defines λ u¨j as the partial play obtained by extending λ u by Éloïse choosing transition pq, tpuq, q 0 , q 1 , i, Sq, followed by Abélard choosing direction j (i.e. we extend λ u by the unique successor that respects ϕ and then let we Abélard choose direction j). Note that for j P t0, 1u, λ u¨j ends in configuration pq j , uj, symbq for some symb P t‹, ˝, ˝u.

The run ρ is defined by letting ρpuq be the state q in the last configuration pq, u, symbq of λ u . By construction, ρ is a valid run of A on t and moreover with any branch π in ρ one can associate a play λ π in G Acc Large A,t from pq ini , ε, ˝q where Éloïse respects ϕ (one simply considers the limit of the increasing sequence of partial plays λ u where u ranges over those nodes along branch π). By construction π is accepting if and only if λ π fulfils the parity condition.

We define spuq as the symbol symb in the last configuration pq, u, symbq of λ u . Furthermore, we define a direction mapping d and a set of nodes U as follows: for all u, dpuq " i with ϕpλ u q " pq, u, q 0 , q 1 , i, Sq; and for all u, u P U if and only if spuq " ‹. Notice that if dpuq " i then spu ¨iq " ˝or spu ¨iq " ‹.

Given a branch π " i 1 i 2 ¨¨¨we define spπq as the infinite sequence of spεqspi 1 qspi 1 i 2 q ¨¨¨, and Colpπq as the smallest colours appearing infinitely often in ρpπq. Note that since Éloïse wins the play λ π , ‹ appears infinitely often in spπq and Colpπq is even, or ‹ does not appear infinitely often in spπq but ˝does.

First let us show that d points to U . Suppose by contradiction that this is not the case, i.e. there exists a branch π " ui 1 i 2 ¨¨¨, with i j " dpui 1 ¨¨¨i j´1 q for all j ě 1, such that for all k ě 1, ui 1 ¨¨¨i k R U . Then for all k ě 1, spui 1 ¨¨¨i k q " ˝, therefore λ π is loosing. This raises a contradiction since ϕ is a winning strategy. Now, let us show that all branches in BpU q are winning in ρ. Let π P BpU q. Then by definition, ‹ appears infinitely often in spπq. Then since λ π is winning we have that Colpπq is even, then π is an accepting branch in ρ.

Conversely let ρ be a run whose set of accepting branches is large. From Lemma 6 there exist a direction mapping d and a set of nodes U such that d points to U , and every branch π P BpU q is accepting in ρ. Define the strategy ϕ of Éloïse as follows. For all partial play λ ending in pρpuq, u, symbq ϕpλq " pρpuq, u, ρpu0q, ρpu1q, dpuq, tj | uj P U uq, and for all other plays, we do not give any restriction on ϕpλq (assuming that the automaton is complete, Éloïse can always play something). Let us show that ϕ is a winning strategy for Éloïse.

As for the other direction, we inductively associate with any node u a partial play λ u where Éloïse respects ϕ. For this we let λ ε " pq ini , ε, ˝q. Now assume that we defined λ u for some node u and let pq, tpuq, q 0 , q 1 , i, Sq be the transition Éloïse plays from λ u when she respects ϕ. For j P t0, 1u, one defines λ u¨j as the partial play obtained by extending λ u by Éloïse choosing transition pq, tpuq, q 0 , q 1 , i, Sq, followed by Abélard choosing direction j. Note that for j P t0, 1u, λ u¨j ends in configuration pq j , uj, symbq for some symb P t‹, ˝, ˝u.

Moreover with any branch π in ρ one can associate a play λ π in G Acc Large A,t from pq ini , ε, ˝q where Éloïse respects ϕ (one simply considers the limit of the increasing sequence of partial plays λ u where u ranges over those nodes along branch π). By construction π is accepting in ρ if and only if λ π fulfils the parity condition. Furthermore observe that any play that respects ϕ is equal to λ π for some branch π. Again, we define spuq as the symbol symb in the last configuration pq, u, symbq of λ u . Observe that if spu ¨iq " ˝for some node u and i P t0, 1u then i " dpuq.

Let λ π be a play that respects ϕ. Note that Éloïse wins the play λ π if and only if ‹ appears infinitely often in spπq and Colpπq is even, or ‹ does not appear infinitely often in spπq but ˝does. First observe that u P U if and only if spuq " ‹. If ‹ appears infinitely often in spπq then π is in BpU q therefore it is accepting, thus λ π is winning. If ‹ does not appear infinitely often in spπq let u and i 1 , i 2 , . . . be such that π " ui 1 i 2 ¨¨¨and for all k, spui 1 ¨¨¨i k q ‰ ‹. Assume by contradiction that ˝does not appears infinitely often in spπq. Therefore there exists such that for all k ě , spui 1 ¨¨¨i k q " ˝, thus i k " dpui 1 ¨¨¨i k´1 q. Thus π is a branch where at some point d is followed, but no node in U is eventually reached, which means that d does not point to U hence, raises a contradiction.

Therefore λ π is a winning play, thus ϕ is a winning strategy.

Thanks to Theorem 12 we can now easily prove that languages of the form L Acc Large pAq are always ω-regular. Theorem 13. Let A " xA, Q, q ini , ∆, Coly be a parity tree automaton using d colours. Then there exists a parity tree automaton A 1 " xA, Q 1 , q 1 ini , ∆ 1 , Col 1 y such that L Acc Large pAq " LpA 1 q. Moreover |Q 1 | " Opd|Q|q and A 1 uses d `2 colours.

Proof. The game G Acc Large A,t can be transformed into a standard acceptance game for ω-regular language (as defined in Section 2.3) by the following trick (this is the same as the one for G 1RejďCount A,t

). One adds to states an integer where one stores the smallest colour seen since the last ‹-state was visited (this colour is easily updated); whenever a starred state is visited the colour is reset to the colour of the state. Now ˝-states are given an even colour e that is greater or equal than all colour previously used (hence, it ensures that if finitely many ‹-states but infinitely many ˝-states are visited then Éloïse wins), ˝-states are given the odd colour e `1 (hence it ensures that if at some points only ˝-states are visited, Éloïse looses) and starred states are given the colour that was stored (hence, if infinitely many starred states are visited we retrieve the previous parity condition). It should then be clear that the latter game is a classical acceptance game, showing that L Acc Large pAq is ω-regular. The construction of A 1 is immediate from the final game and the size is linear in d|Q| due to the fact that one needs to compute the smallest colour visited between to starred states.

Conclusion and Perspectives

In this paper we proved, using a game-theoretic approach, that the languages defined by automata with cardinality constraints as well as those defined by automata with topological bigness constraints are always ω-regular. Moreover, in the case where the cardinality constraint is on the number of accepting branches we showed that the languages collapse to those defined by classical Büchi tree automata, which contrasts with the case where the cardinality constraint is expressed on the number of rejecting branches.

One advantage of our approach is that it preserves the well-known connection between automata and games and that it permits to have tractable transformations (which might not be the case when using e.g. the more general logical approach of [START_REF] Bárány | Expressing cardinality quantifiers in monadic second-order logic over trees[END_REF]).

One technical restriction of our work is that we required our automata to be complete. This restriction was made for ease of presentation and can easily be removed thanks to the following trick (pointed to us by an anonymous reviewer). It suffices that we modify the various constructions of acceptance games we consider as follows. Every time Éloïse determines the direction in the acceptance game Abélard has now the option to either accept her choice or to challenge her. In the former case the play continues as usual. But if Abélard challenges Éloïse, we enter a new phase where she has to prove (in the same flavour as in the classical setting described in Section 2.3) that she can construct a run (not necessarily accepting) on the subtree: if she is able to do so she wins otherwise Abélard wins.

A first perspective has to do with applications. Indeed, while the present work is at the theoretical level only, it permits to observe that classical questions (membership, emptiness) for the classes of languages under consideration are tractable (at least not harder than for classical ω-regular languages). Hence, it would be interesting to find examples where automata with cardinality constraints or with topological bigness constraints are a relevant way to express properties of systems: in particular we believe that it can be an alternative to qualitative tree languages [START_REF] Carayol | Qualitative tree languages[END_REF][START_REF] Carayol | Randomisation in automata on infinite trees[END_REF] when specifying properties of non-deterministic system where one wants to allow a negligible set of bad executions.

A second perspective has to do with games played on graphs. A generalisation of two-player games is given by stochastic games (see e.g. [START_REF] Chatterjee | Stochastic ω-regular games[END_REF]) where a third, uncontrollable and unpredictable, player is added to the two usual antagonistic players. When the two first players aim to represent respectively a program and its (potentially malicious) environment, the third player can be seen as an abstraction of nature. Usually the nature player is equipped with a stochastic semantics and typical (qualitative) questions are whether the first player has a strategy that, against any strategy of the second player, almost-surely satisfies an objective (against all possible behaviours of the nature player). In other words, one seeks for a strategy that against any strategy of the second player produces a set of plays such that the losing plays form a negligible subset, negligible being understood in a measure theoretic sense (namely as being of measure 0). Following the ideas developed in this paper, one can consider qualitative questions on two-player games with a third nature player where one uses either counting or topology to define which sets of plays should be considered as being negligible. This seems a promising approach as we showed in our recent work [START_REF] Carayol | How good is a strategy in a game with nature?[END_REF].

A third perspective has to do with logic. One question is whether there is a natural logic that exactly captures the classes of automata studied in this paper. Obviously this should be a (strict) fragment of the monadic second order logic. A second question is to study how the automata models considered in the present work compare/can be combined with the quantifiers studied in the work of Bárány, Kaiser and Rabinovich [START_REF] Bárány | Expressing cardinality quantifiers in monadic second-order logic over trees[END_REF] and in the recent study initiated by Michalewski and Mio in [START_REF] Michalewski | Baire category quantifier in monadic second order logic[END_REF].

Figure 1 :

 1 Figure 1: Local structure of the arena of the acceptance game G A,t .

Figure 2 :

 2 Figure 2: Local structure of G RejďCount A,t

Figure 3 :

 3 Figure 3: Local structure of the arena of the acceptance game G RejFin A,t

Figure 4 :

 4 Figure 4: A pseudo comb pU, V q

Figure 5 :

 5 Figure 5: Local structure of the arena of the acceptance game G Acc 8 A,t .

Figure 6 :

 6 Figure 6: An accepting-pseudo binary tree U: nodes in U are marked by the symbol ' and all blue branches are accepting.

Figure 7 :

 7 Figure 7: A k-pseudo binary tree U : nodes in U are marked by symbol '.

Figure 8 :

 8 Figure 8: Local structure of the arena of the acceptance game G Acc Uncount A,t

Figure 9 :

 9 Figure 9: Local structure of the arena of the acceptance game r G Acc Uncount A,t

Theorem 10 .

 10 One has t P L Acc U ncount pAq if and only if Éloïse wins in r G Acc Uncount A,t from pq ini , ε, waitq.

Figure 10 :

 10 Figure 10: Local structure of the arena of the acceptance game G Acc Large A,t

  Theorem 3. One has t P L Rej ďCount pAq if and only if Éloïse wins in G RejďCount

	A,t	from pq ini , εq.
	Proof. Assume that Éloïse has a winning strategy ϕ in G RejďCount A,t

Note that the idea of using games to prove this result was already proposed by Büchi in[START_REF] Büchi | Using determinancy of games to eliminate quantifiers[END_REF].

In pictures, we always depict by circles (resp. squares) the vertices controlled by Éloïse (resp. Abélard).

We only give the formal construction of A 1 for this statement, and will keep it more informal later in similar proofs (namely the ones of theorems

6,8, 11 and 13).

Actually it is what we refer to as an accepting-pseudo binary tree in Section 5.2.1.

In[START_REF] Grädel | Banach-Mazur Games on Graphs[END_REF] the players of the Banach-Mazur game are called 0 and 1 and Player 0 corresponds to Abélard while player 1 corresponds to Éloïse. Hence, when using a statement from[START_REF] Grädel | Banach-Mazur Games on Graphs[END_REF] for our setting one has to keep this in mind as well as the fact that one must replace the winning condition by its complement (hence, replacing "meager" by "large").

This statement holds as soon as the Banach-Mazur games are determined and hence, in particular for Borel sets.

Acknowledgement

We would like to thanks the anonymous reviewers for their valuable comments, as well as Axel Haddad for his contributions on a preliminary version of this work.