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

M Hague

A Meyer

C.-H L Ong

¶ O Serre

Winning regions of higher-order pushdown games *

In this paper we consider parity games defined by higher-order pushdown automata. These automata generalise pushdown automata by the use of higher-order stacks, which are nested "stack of stacks" structures. Representing higher-order stacks as well-bracketed words in the usual way, we show that the winning regions of these games are regular sets of words. Moreover a finite automaton recognising this region can be effectively computed.

A novelty of our work are abstract pushdown processes which can be seen as (ordinary) pushdown automata but with an infinite stack alphabet. We use the device to give a uniform presentation of our results.

From our main result on winning regions of parity games we derive a solution to the Modal Mu-Calculus Global Model-Checking Problem for higher-order pushdown graphs as well as for ranked trees generated by higher-order safe recursion schemes.

Introduction

Higher-order pushdown automata were introduced by Maslov [START_REF] Maslov | Multi-level stack automata[END_REF] as a generalisation of pushdown automata and nested pushdown automata to extend the indexed languages introduced by Aho [START_REF] Aho | Indexed grammars, an extension of contextfree grammars[END_REF]. Whereas an ordinary (i.e. order-1) pushdown automaton works with a stack of symbols (i.e. order-1 stack), a pushdown automaton of order 2 works with a stack of (order-1) stacks. In addition to pushing a symbol onto and popping a symbol from the top-most order-1 stack, an order-2 pushdown automaton can duplicate or remove the entire top-most (order-1) stack. Pushdown automata of higher orders are defined in a similar way and have been extensively studied as language acceptors [START_REF] Damm | The IO-and OI-hierarchies[END_REF][START_REF] Engelfriet | Iterated stack automata and complexity classes[END_REF].

Recently, the infinite structures defined by these automata have received a lot of attention. In [START_REF] Knapik | Higherorder pushdown trees are easy[END_REF], the families of infinite terms defined by higher-order pushdown automata were shown to correspond to the solutions of safe higher-order recursion schemes. Subsequently, in [START_REF]On infinite terms having a decidable monadic theory[END_REF][START_REF] Carayol | The Caucal hierarchy of infinite graphs in terms of logic and higher-order pushdown automata[END_REF], the ε-closure of their configuration graphs were shown to be exactly those constructible from finite graphs using natural graph transformations (see [START_REF] Thomas | Constructing infinite graphs with a decidable MSO-theory[END_REF] for a survey).

A remarkable property of these graphs is that we can decide the validity of any formula of monadic second-order (MSO) logic. Unfortunately the decision procedure is nonelementary (in the size of the formula) and this is already so in the case of pushdown graphs. In order to obtain an elementary decision procedure, we consider the µ-calculus: a weaker modal logic equi-expressive with MSO over trees [START_REF] Janin | On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic[END_REF]. The two main algorithmic problems in this setting are the (local) model-checking problem (i.e. to decide if a particular configuration satisfies a given µ-calculus formula) and the global model-checking problem (i.e. to compute a finite description of the set of configurations satisfying a given formula). To solve these problems, we consider the associated two-player parity game, whose size is polynomial in both the size of the automaton and of the formula [START_REF] Emerson | Tree automata, mucalculus and determinacy (extended abstract)[END_REF]. The two versions of the model-checking problem above are respectively equivalent to deciding which player wins from a given configuration and to giving a finite description of the winning region for each player.

For parity games defined by pushdown automata, Walukiewicz has given an EXPTIME decision procedure to compute the winner from a given configuration [START_REF] Walukiewicz | Pushdown processes: games and model checking[END_REF]. In [START_REF] Cachat | Uniform solution of parity games on prefixrecognizable graphs[END_REF][START_REF] Serre | Note on winning positions on pushdown games with omega-regular winning conditions[END_REF], the winning region is shown to be regular when a configuration (q, w) is represented by the word qw. Note that this result can easily be derived from the results by Vardi [START_REF] Vardi | Reasoning about the past with two-way automata[END_REF]. For order-n pushdown automata, an n-EXPTIME decision procedure for the local version of the problem was given by Cachat [START_REF] Cachat | Higher order pushdown automata, the Caucal hierarchy of graphs and parity games[END_REF] using techniques from [START_REF] Vardi | Reasoning about the past with two-way automata[END_REF]. In this article, we shall consider the global version of the problem i.e. the computation of a finite representation of the winning region, and we obtain, as a by-product, a new proof of Cachat's result.

To give a finite description of a set of higher-order stacks, we represent these stacks as well-bracketed words. Note that the depth of the bracketing is bounded by the order of the stack. By extension, we say that a set of higherorder stacks is regular if the set of associated well-bracketed words is regular. Our main result is that the winning regions of parity games over higher-order pushdown graphs are regular. Moreover we can construct in n-EXPTIME a finite deterministic automaton accepting it.

To simplify the presentation, we consider a more general notion of pushdown automata, called abstract pushdown automata, which work with a possibly infinite stack alphabet. Standard pushdown automata are abstract pushdown automata with a finite stack alphabet; order-(k + 1) pushdown automata are abstract pushdown automata whose stack alphabet is the (infinite) set of order-k stacks. Our main technical result concerns parity games over the configuration graphs of abstract pushdown automata. From an abstract pushdown parity game, we construct a reduced parity game based on the stack alphabet (i.e. which does not make use of a stack structure) and we show that a finite description of the winning region of the original game can be derived from a finite description of the winning region of the reduced game. Applied to higher-order pushdown automata, this result allows us to reduce the problem of computing the winning region of an order-(k + 1) pushdown parity game to that of computing the winning region of an order-k pushdown parity game. We also show that starting from a winning strategy in the reduced parity game one can effectively build an abstract pushdown automaton that realises a winning strategy in the original game and whose stack is synchronised with the one used in the game. Applied to higher-order pushdown parity games, this result allows us to prove that any such game always admits an effective winning strategy realised by a higher-order pushdown automata of the same order and whose stack is synchronised with the one used in the game.

As an application of these results, we solve the µcalculus global model-checking problem for higher-order pushdown graphs, and for ranked trees generated by safe higher-order recursion schemes.

Related work.

In [START_REF] Bouajjani | Symbolic reachability analysis of higher-order context-free processes[END_REF], Bouajjani and Meyer considered simpler reachability games over higher-order pushdown automata with a single control state. They showed that the winning regions in these games are regular. In [START_REF] Hague | Symbolic backwardsreachability analysis for higher-order pushdown systems[END_REF], Hague and Ong extended the result to arbitrary higher-order pushdown automata. The results presented here have been obtained by Hague and Ong, and also (separately and independently) by the other co-authors. The present article follows the latter approach whereas the proof in [START_REF] Hague | Global Model Checking of Higher-Order Pushdown Systems[END_REF] generalises the saturation method developed in [START_REF] Hague | Symbolic backwardsreachability analysis for higher-order pushdown systems[END_REF].

A similar result was obtained in [START_REF] Carayol | Positional Strategies for Higher-Order Pushdown Parity Games[END_REF] for a stronger notion of regularity (introduced in [START_REF] Carayol | Regular sets of higher-order pushdown stacks[END_REF][START_REF] Fratani | Automates à pile de piles[END_REF]) which coincides with MSO-definable sets of configurations. In contrast, the simpler notion presented here can only capture properties definable in µ-calculus. In particular, owing to the higherorder push operations, the set of configurations reachable from a given configuration is not regular in the sense of the present paper. (To our knowledge the results presented here do not appear to be derivable from Carayol's work [START_REF] Carayol | Regular sets of higher-order pushdown stacks[END_REF].)

Definitions

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 over A. The empty word is denoted by ε.

Infinite two-player games. Let G = (V, E) be a (possibly infinite) graph with vertex-set V and edge-set

E ⊆ V × V . Let V E ∪ V A be a partition of V between two players, Éloïse and Abelard. A game graph is a tuple G = (V E , V A , E). An infinite two-player game on a game graph G is a pair G = (G, Ω), where Ω ⊆ V ω is a winning condition.
Éloïse and Abelard play in G by moving a token between vertices. A play from some initial vertex v 0 proceeds as follows: the player owning v 0 moves the token to a vertex v 1 such that (v 0 , v 1 ) ∈ E. Then the player owning v 1 chooses a successor v 2 and so on. If at some point one of the players cannot move, she/he loses the play. Otherwise, the play is an infinite word Λ ∈ V ω and is won by Éloïse if and only if Λ ∈ Ω. Nevertheless, for all game graphs considered in this article one can always assume without loss of generality that they have no dead-ends. A partial play is any prefix of a play.

A strategy for Éloïse is a function assigning, to any partial play ending in some vertex v ∈ V E , a vertex v such that (v, v ) ∈ E. Éloïse respects a strategy Φ during some play

Λ = v 0 v 1 v 2 • • • if v i+1 = Φ(v 0 • • • v i ), for all i ≥ 0 such that v i ∈ V E .
A strategy Φ for Éloïse is winning from some position v ∈ V if she wins every play that starts from v and respects Φ. Finally, a vertex v ∈ V is winning for Éloïse if she has a winning strategy from v, and the winning region for Éloïse consists of all winning vertices for her. Symmetrically, one defines the corresponding notions for Abelard.

A game G is determined if, from any position, either Éloïse or Abelard has a winning strategy. Determinacy of all games considered here follows from Martin's Theorem [START_REF] Martin | Borel determinacy[END_REF].

For more details and basic results on games, we refer the reader to [START_REF] Thomas | On the synthesis of strategies in infinite games[END_REF][START_REF] Zielonka | Infinite games on finitely coloured graphs with applications to automata on infinite trees[END_REF][START_REF] Grädel | Automata, Logics, and Infinite Games[END_REF][START_REF] Walukiewicz | A landscape with games in the backgroung[END_REF].

Higher-order pushdown processes. An order-n pushdown process is a tuple P = Q, Σ, ⊥, δ where Q is a finite set of control states, Σ is a finite stack alphabet containing a bottom-of-stack symbol ⊥ ∈ Σ, and ∆ is a transition function (to be defined below). Let Op

1 = {pop 1 , push 1 (σ) | σ ∈ Σ \ {⊥}} (resp. Op k = {pop k , push k }) be the set of order-1 (resp. order-k with 2 ≤ k ≤ n) stack operations. Then ∆ : Q × Σ → 2 Q×Op ≤n where Op ≤i = 1≤k≤i Op i .
An order-0 stack over Σ is an element of Σ, and for k > 0 an order-k stack over Σ is a finite sequence s 1 , • • • , s of order-(k -1) stacks. Moreover we require that an order-k stack be non-empty whenever k ≥ 2. Let k > 0 and take an order-k stack s = s 1 , • • • , s , we define the following partial functions:

top 1 (s) = s if = 0 and k = 1, top 1 (s ) if k > 1. pop i (s) = s 1 , • • • , s -1 if > 1 and k = i, s 1 , • • • , s -1 , pop i (s ) if k > i. push i (s) = s 1 , s 2 , • • • , s , s if k = i, s 1 , s 2 • • • , s -1 , push i (s ), if k > i.
A configuration of P is a pair (q, s) where q ∈ Q and s is an order-n stack. At a configuration (q, s), P can apply any transition (q , op) ∈ ∆(q, top 1 (s)), leading to the configuration (q , op(s)). The configuration graph of P is defined to be the graph whose vertices are the configurations and whose edges are given by the transitions of P.

In order to define a notion of regularity over higher-order stacks, we associate to each order-k stack a well-bracketed word of depth k as follows. Let

s = s 1 , • • • , s be an order- k stack. We define s ∈ (Σ ∪ {[, ]}) * as s = [ s 1 • • • s ] if k ≥ 1 s if k = 0 (i.e. s ∈ Σ)
A set S of order-k stacks is said to be regular if the language S = { s | s ∈ S} is a regular subset of (Σ ∪ {[, ]}) * . By extension, a set C of configurations of an order-k pushdown automaton is said to be regular if the set

C = { sq | (q, s) ∈ C} is a regular subset of (Σ ∪ {[, ]}) * Q. For ex- ample {[ [a a] • • • [a a] n ] | n ≥ 0} is a regular set of order-2 stacks, but {[ [a • • • a n ] [a • • • a n ] ] | n ≥ 0} is not.
In particular, the set of configurations reachable from a given configuration is not in general regular. Consider for example an order-2 pushdown automaton with two states q 0 and q 1 and two transitions ∆(q 0 , a) = {(q 0 , push(a)), (q 1 , push 2 )}. The language of words representing the configurations reachable from

(q 0 , [[a]]) is the context-free language {[[a n ]]q 0 | n ≥ 1} ∪ {[[a n ][a n ]]q 1 | n ≥ 1}.
When considering higher-order pushdown automata as acceptors of finite-word languages over a finite alphabet Σ, we attach to each transition a symbol in Σ ∪ {ε} and fix an initial state q 0 together with a set F of final states. We use the symbol ε to label silent transitions. We call such automata labelled higher-order pushdown automata.

A word w ∈ Σ * is accepted by the automaton if there exists a sequence of configurations c 0 a1 -→ . . . an -→ c n where c 0 is the initial configuration (q 0 , [ n ⊥] n ), c n contains a final state in F ⊆ Q and w is the word obtained by removing all occurrences of ε in a 1 . . . a n . (We say that w is the word traced out by the configuration sequence c 0 a1 -→ . . . an -→ c n .) Proposition 1. Take an (resp. deterministic) order-k pushdown automaton. The set of words traced out by configuration sequences from the initial configuration c 0 to a configuration c, where c ranges over a regular set of configurations, is accepted by an (resp. deterministic) order-k pushdown automaton.

Abstract Pushdown Processes. We situate the techniques developed here in a general and abstract framework of (order-1) pushdown processes whose stack alphabet is a possibly infinite set.

An abstract pushdown process is a tuple P = Q, Γ, ∆ where Q is a finite set of states, Γ is a (possibly infinite) set called an abstract pushdown alphabet and containing a bottom-of-stack symbol denoted ⊥ ∈ Γ, and

∆ : Q × Γ → 2 Q×{rew(γ),pop,push(γ) | γ∈Γ}
is the transition relation. We additionally require that for all γ = ⊥, ∆(q, γ) does not contain any element of the form (q, push(⊥)) or (q , rew(⊥)), and that ∆(q, ⊥) does not contain any element of the form (q , pop) or (q , rew(γ)) with γ = ⊥, i.e. the bottom-of-stack symbol can only occur at the bottom of the stack, and is never popped or rewritten.

An abstract pushdown content is a word in St = ⊥(Γ \ {⊥}) * . A configuration of P is a pair (q, σ) with q ∈ Q and σ ∈ St. Note that the top stack symbol in some configuration (q, σ) is the rightmost symbol of σ.

Remark 1.

In general an abstract pushdown process is not finitely describable, as the domain of ∆ is infinite and no further assumption is made on ∆.

Example 1.

A pushdown process is an abstract pushdown process whose stack alphabet is finite.

A abstract pushdown process P induces a possibly infinite graph, called an abstract pushdown graph, denoted G = (V, E), whose vertices are the configurations of P (i.e. pairs from Q × St), and edges are defined by the transition relation ∆, i.e., from a vertex (p, σγ) one has edges to:

• (q, σγ ) whenever (q, rew(γ )) ∈ ∆(p, γ).

• (q, σ) whenever (q, pop) ∈ ∆(p, γ).

• (q, σγγ ) whenever (q, push(γ )) ∈ ∆(p, γ).

Example 2. Higher-order pushdown processes are special cases of abstract pushdown processes. Let n > 1 and consider an order-n pushdown process P = Q, Σ, ∆ . Set Γ to be the set of all order-(n-1) stacks over Σ, and for every p ∈ Q and γ ∈ Γ with σ = top 1 (γ), we define ∆ (p, γ) by • (q, pop) ∈ ∆ (p, γ) iff (q, pop n ) ∈ ∆(q, σ);

• (q, push(γ)) ∈ ∆ (p, γ) iff (q, push n ) ∈ ∆(q, σ);

• (q, rew(op(γ))) ∈ ∆ (p, γ) iff (q, op) ∈ ∆(q, σ)
where k < n and op is an order-k action.

It follows that the abstract pushdown process Q, Γ, ∆ and P have isomorphic transition graphs.

Abstract Pushdown Parity Game. Consider a partition

Q E ∪ Q A of Q between Éloïse and Abelard. It induces a natural partition V E ∪ V A of V by setting V E = Q E × St and V A = Q A × St. The resulting game graph G = (V E , V A , E
) is called an abstract pushdown game graph.

Finally, an abstract pushdown game is a game played on such a game graph. Let ρ be a colouring function from Q to a finite set of colours C ⊂ N. This function is easily extended to a function from V to C by setting ρ((q, σ)) = ρ(q). The parity condition is the winning condition defined by:

Ω par = {v 0 v 1 • • • | lim inf((ρ(v i )) i≥0 ) is even}
For an abstract pushdown parity game, the main questions are the following:

1. For a given vertex, decide who wins from it.

2. For a given vertex, compute a winning strategy for the winning player.

3. Compute a finite representation of the winning regions.

These three problems are polynomially equivalent to the following problems respectively: model-checking for µcalculus, controller synthesis against µ-calculus specifications, and global model-checking for µ-calculus.

Automata with oracles. We now define a class of automata to accept the winning positions in an abstract pushdown game. An automaton with oracles is a tuple

A = (S, Q, Γ, δ, s in , O 1 • • • O n , Acc)
where S is a finite set of control states, Q is a set of input states, Γ is a (possibly infinite) input alphabet, s in ∈ S is the initial state, O i are subsets of Γ (called oracles) and δ : S × {0, 1} n → S is the transition function. Finally Acc is a function from S to 2 Q . Such an automaton is designed to accept in a deterministic way configurations of an abstract pushdown process whose abstract pushdown content alphabet is Γ and whose control states are Q.

Let A = (S, Q, Γ, δ, s in , O 1 • • • O n , Acc
) be such an automaton. With every γ ∈ Γ we associate a Boolean vector

π(γ) = (b 1 , • • • b n ) where b i = 1 if γ ∈ O i 0 otherwise.
The automaton reads a configuration C = (q, γ 1 γ 2 • • • γ ) from left to right. A run over C is the sequence s 0 , • • • , s +1 such that s 0 = s in and s i+1 = δ(s i , π(γ i )) for every i = 0, • • • , . Finally the run is accepting if and only if q ∈ Acc(s +1 ).

Remark 2. When the input alphabet is finite, it is easily seen that automata with oracles behave as (standard) deterministic finite automata.

In this article, we are going to use automata with oracles to accept sets of configurations of higher-order pushdown automata. As seen in Example 2 for an order-(k + 1) pushdown automaton, we take Γ to be the set of all orderk stacks. The sets of regular configurations of an order-(k + 1) pushdown automaton are naturally captured by automata using, as oracles, regular sets of order-k stacks.

Preliminary results

From now on, let us fix an abstract pushdown process P = Q, Γ, ∆ together with a partition Q E ∪ Q A of Q and a colouring function ρ using a finite set of colours C. Denote respectively by G = (V, E) and G the associated abstract pushdown game graph and abstract pushdown parity game.

We can define an automaton with oracles that accepts Éloïse's winning region of the game G. The oracles of this automaton are defined using conditional games. For every subset R of Q the game G(R) played over G is the conditional game induced by R over G. A play Λ in G(R) is winning for Éloïse iff one of the following happens:

• In Λ no configuration with an empty stack (i.e. of the form (q, ⊥)) is visited, and Λ satisfies the parity condition.

• In Λ a configuration with an empty stack is visited and the control state in the first such configuration belongs to R.

More formally, the winning condition in G(R) is

[Ω par \ V * (Q × {⊥})V ω ] ∪ V * (R × {⊥})V ω
For any state q, any stack letter γ = ⊥, and any subset R ⊆ Q it follows from Martin's Determinacy theorem that either Éloïse or Abelard has a winning strategy from (q, ⊥γ) in G(R). We denote by R(q, γ) the set of subsets R for which Éloïse wins in G(R) from (q, ⊥γ):

R(q, γ) = {R ⊆ Q | (q, ⊥γ) is winning for Éloïse in G(R)} Proposition 3. Let σ ∈ (Γ\{⊥}) * , q ∈ Q and γ ∈ Γ\{⊥}.
Then Éloïse has a winning strategy in G from (q, ⊥σγ) if and only if there exists some R ∈ R(q, γ) such that (r, ⊥σ) is winning for Éloïse in G for every r ∈ R.

Proof (sketch)

. Assume Éloïse has a winning strategy from (q, ⊥σγ) in G and call it ϕ. Define R to be the set of all r ∈ Q such that there is a play

v 0 • • • v k (r, ⊥σ)v k+1 • • •
where Éloïse respects ϕ and each v i for 0 ≤ i ≤ k is of the form (p, ⊥σσ ) for some σ = ε. Mimicking ϕ, Éloïse wins in G(R) from (q, γ) and hence R ∈ R(q, γ). Finally, for every r ∈ R there is a partial play λ r that starts from (q, ⊥σγ), where Éloïse respects ϕ, and that ends in (r, ⊥σ). Hence (r, ⊥σ) is also winning for Éloïse in G.

Conversely, let us assume that there is some R ∈ R(q, γ) such that (r, ⊥σ) is winning for Éloïse in G for every r ∈ R. For every r ∈ R, let us denote by ϕ r a winning strategy for Éloïse from (r, ⊥σ) in G. Let ϕ R be a winning strategy for Éloïse in G(R) from (q, ⊥γ). In order to win in G from (q, ⊥σγ), Éloïse first mimics ϕ R and, if eventually some configuration (r, ⊥σ) is reached she follows, ϕ r from that point onward. Proposition 3 easily implies the following result.

Theorem 1. Let G be an abstract pushdown parity game induced by an abstract pushdown process

P = Q, Γ, ∆ .

Then the set of winning positions in G for Éloïse (respectively for Abelard) is accepted by an automaton with oracles

A = (S, Q, Γ, δ, s i , O 1 • • • O n , Acc) such that • S = 2 Q ; • s i = ∅. • There is an oracle O p,R for every p ∈ Q and R ⊆ Q, and γ ∈ O p,R iff R ∈ R(p, γ) and γ = ⊥.
• There is an oracle O ⊥ and γ ∈ O ⊥ iff γ = ⊥

• Using the oracles, δ is designed such that:

-From state ∅ on reading ⊥, A goes to {p | (p, ⊥) is winning for Éloïse in G}. -From state S on reading γ, A goes to {p | S ∈ R(p, γ)}.
• Acc is the identity function.

We will later use Theorem 1 in combination with Remark 2 to prove that the set of winning positions in any higher-order pushdown parity games is regular (see Theorem 4).

Reducing the conditional games

The main purpose of this section is to build a new game whose winning region embeds all the information needed to determine the sets R(q, γ). Moreover the underlying game graph no longer uses a stack.

For an infinite play

Λ = v 0 v 1 • • • , let
Steps Λ be the set of indices of positions where no configuration of strictly smaller stack height is visited later in the play. More formally,

Steps Λ = {i ∈ N | ∀j ≥ i sh(v j ) ≥ sh(v i )}, where sh((q, ⊥γ 1 • • • γ n )) = n + 1.
Note that Steps Λ is always infinite and hence induces a factorisation of the play Λ into finite pieces.

In the factorisation induced by Steps Λ , a factor

v i • • • v j is called a bump if sh(v j ) = sh(v i ), called a Stair otherwise (that is, if sh(v j ) = sh(v i ) + 1).
For any play Λ with

Steps Λ = {n 0 < n 1 < • • • }, we can define the sequence (mcol Λ i ) i≥0 ∈ N N by setting mcol Λ i = min{ρ(v k ) | n i ≤ k ≤ n i+1 }.
This sequence fully characterises the parity condition.

Proposition 4. For a play

Λ, Λ ∈ Ω par iff lim inf((mcol Λ i ) i≥0
) is even. In the sequel, we build a new parity game G over a new game graph G = ( V , E). This new game simulates the abstract pushdown graph, in the sense that the sequence of visited colours during a correct simulation of some play Λ in G is exactly the sequence (mcol Λ i ) i≥0 . Moreover, a play in which a player does not correctly simulate the abstract pushdown game is losing for that player. We shall see that the winning regions in G allow us to compute the sets {γ ∈

Γ | R ∈ R(q, γ)}.
Before providing a description of the game graph G, let us consider the following informal description of this simulation game. We aim at simulating a play in the abstract pushdown game from some initial vertex (p in , ⊥). In G we keep track of only the control state and the top stack symbol of the simulated configuration.

The interesting case is when it is in a control state p with top stack symbol α, and the player owning p wants to push a symbol β onto the stack and change the control state to q.

(q, β, -→ R , min(θ, ρ(q))) tt ff (p, α, - → R , θ) (p, α, -→ R , θ, q, β) (p, α, -→ R , θ, q, β, - → S ) (q, β, - → S , ρ(q)) (s, α, -→ R , min(θ, i, ρ(s))) i If ∃ (r, pop) ∈ ∆(p, α) s.t. r ∈ Rθ If ∃ (r, pop) ∈ ∆(p, α) s.t. r / ∈ R ∀ (q, rew(β)) ∈ ∆(p, α) ∀ (q, push(β)) ∈ ∆(p, α) ∀ - → S ∈ P(Q) d+1 ∀ s ∈ Si Figure 1. Local structure of G.
For every strategy of Éloïse, there is a certain set of possible (finite) continuations of the play that will end with popping β (or actually a symbol into which β was rewritten in the meantime) from the stack. We require Éloïse to declare a vector -→ S = (S 0 , . . . , S d ) of (d + 1) subsets of Q, where S i is the set of all states the game can be in after popping (possibly a rewriting of) β along those plays where in addition the smallest visited colour while (possibly a rewriting of) β was on the stack is i.

Abelard has two choices. He can continue the game by pushing β onto the stack and updating the state (we call this a pursue move). Otherwise, he can pick a set S i and a state s ∈ S i , and continue the simulation from that state s (we call this a jump move). If he does a pursue move, then he remembers the vector -→ S claimed by Éloïse; if later on, a pop transition is simulated, the play stops and Éloïse wins if and only if the resulting state is in S θ where θ is the smallest colour seen in the current level (this information is encoded in the control state, reset after each pursue move and updated after each jump move). If Abelard does a jump move to a state s in S i , the currently stored value for θ is updated to min(θ, i, ρ(s)), which is the smallest colour seen since the current stack level was reached.

There are extra moves to simulate rew rules where the top stack element and the value of θ are updated.

Therefore the main vertices of this new game graph are of the form (p, α, -→ R , θ), which are controlled by the player who controls p. Intermediate vertices are used to handle the previously described intermediate steps. The local structure is given in Figure 1 (circled vertices are those controlled by Éloïse). Two special vertices tt and ff are used to simulate pop moves. This game graph is equipped with a colouring function on the vertices and on the edges: vertices of the form (p, α, -→ R , θ) have colour ρ(p), an edge leaving from a vertex (p, α, -→ R , θ, q, β, -→ S ) has colour i where i is the colour of the simulated bump. Note that intermediate vertices could be introduced in order to have only colours on vertices. A precise description of the graph is given in the full proof of the following main result.

For every

q ∈ Q, γ ∈ Γ and R ⊆ Q, R ∈ R(q, γ)
if and only if (q, γ, (R, . . . , R), ρ(q)) is winning for Éloïse in G.

Proof (sketch).

We concentrate here on the first point, as the second is actually a part of the proof of the first one. For the direct implication, assume that the configuration (p in , ⊥) is winning for Éloïse in G, and let Φ be a corresponding strategy for her.

Using Φ, we define a strategy ϕ for Éloïse in G from (p in , ⊥, (∅, . . . , ∅), ρ(p in )). This strategy stores a partial play Λ in G, that is an element in V * (where V denotes the set of vertices of G). At the beginning Λ is initialised to the vertex (p in , ⊥).

By a round we mean a factor of a play between two visits through vertices of the form (p, α, -→ R , θ). Both the strategy ϕ and the update of Λ, are described for a round. When Éloïse has to play from some vertex (p, α, -→ R , θ) she considers the value of Φ(Λ). If it is a pop move then she goes to tt (one proves that this move is always possible). If it equals (q, rew(β)), she goes to (q, β, -→ R , min(θ, ρ(q))). Finally, if it is equal to (q, push(β)), she goes to (p, α, -→ R , θ, β). From some vertex (p, α, -→ R , θ, q, β), Éloïse has to provide a vector -→ S ∈ P(Q) d+1 that describes which states can be reached if β (or one of its successors by top rewriting) is popped, depending on the smallest visited colour in the meantime. In order to define -→ S , Éloïse considers the set of all possible continuations of Λ • (q, σαβ) (where (p, σα) denotes the last vertex of Λ) where she respects her strategy Φ. For each such play, she checks whether some configuration of the form (s, σα) is visited after Λ • (q, σαβ), that is if the β is eventually popped. If it is the case, she considers the first such configuration and the smallest colour i seen in the meantime. For every i ∈ {0, . . . d}, S i , is exactly the set of states s ∈ Q such that the preceding case happens.

Let (p, σα) be the last vertex in Λ. The memory Λ is updated after each visit to a vertex of the form (p, α, -→ R , θ),

we have three cases depending on the kind of the round. If it was simulating a (q, rew(β)) action then the updated memory is Λ • (q, βσ). If it was simulating a bump of colour i starting with some action (q, push(β)) and ending in a state s ∈ S i then the memory becomes Λ extended by (q, σαβ) followed by a sequence of moves, where Éloïse respects Φ, that ends by popping β and reaches (s, σα) while having i as smallest colour. Finally, if it was simulating a stair starting with a (q, push(β)) action, then the updated memory is Λ • (q, σαβ). Therefore, any partial play λ in G -in which Eloise respects her strategy ϕ -is associated with a partial play Λ in G. One shows that Éloïse respects Φ in Λ. The same arguments work for an infinite play λ, and the corresponding play Λ is infinite, starts from (p in , ⊥) and Éloïse respects Φ in that play. Therefore it is a winning play. Relying on that fact one concludes that ϕ is winning.

For the converse implication one can reason in a rather similar way by constructing a winning strategy for Abelard in G from one in G.

From a more constructive proof of Theorem 2 one can construct natural strategies in G from strategies in G.

Theorem 3. Assume Éloïse has a winning strategy ϕ in G that uses a memory ranging from some set M . Then one can construct an abstract pushdown process T with output that realises a winning strategy Φ for Éloïse in G. Moreover the abstract pushdown alphabet used by T is V × M and, at any moment in a play where Éloïse respects Φ, the abstract pushdown content of T has exactly the same height as the one in the current position of the game graph. Finally, if ϕ is effective the same holds for Φ. Remark 3. In the special case of pushdown games, since Γ is finite so is G. Hence in the previous statement, ϕ can be chosen to be memoryless. Therefore one concludes that for pushdown games one can construct a deterministic pushdown automaton that realises a winning strategy and whose stack is synchronised with the one in the game [START_REF] Walukiewicz | Pushdown processes: games and model checking[END_REF].

Uniform solution of higher-order pushdown parity games and strategies

In this section we prove that the winning regions in higher-order pushdown games are regular. The first step is to note the following property. Property 1. Let G be a higher-order pushdown parity game of order-n and let G be as in Theorem 2. Then G is a higherorder pushdown parity game of order-(n -1).

Proof. One simply needs to consider how the game graph G is defined. It suffices to make the following observations concerning the local structure given in Figure 1 when G is played on the transition graph of a pushdown automaton of order-n.

For every vertex of the form

(p, α, - → R , θ), (p, α, - → R , θ, q, β) or (p, α, - → R , θ, q, β, - → S ), α is an order-(n -1) stack. 2. For every vertex of the form (p, α, - → R , θ, q, β) or (p, α, - → R , θ, q, β, - → S ), it holds that α = β.
This implies that any vertex in G can be seen as a pair formed by a state in a finite set and an order-(n -1) stack.

Then one concludes the proof by checking that the edge relation is the one of an order-(n -1) pushdown automaton (for the transition to vertices tt and ff one can introduce vertices (tt, α) and (ff, α) for any order-(n -1) stack α).

Remark 4. The number states of the higher-order pushdown automaton describing G is exponential in the number of states of the pushdown automaton describing G but both games have the same number of colours.

Consider the order-1 case. As G is finite one can solve it and therefore effectively construct the automaton with oracles as in Theorem 1. As this automaton has a finite input alphabet, using Remark 2, we deduce the following result.

Property 2. [START_REF] Cachat | Higher order pushdown automata, the Caucal hierarchy of graphs and parity games[END_REF][START_REF] Serre | Note on winning positions on pushdown games with omega-regular winning conditions[END_REF] The set of winning position in a pushdown parity game is regular. Now, one can iterate this reasoning: applying inductively Property 1 together with Proposition 2 and Theorem 2 easily leads to the desired result.

Theorem 4. The sets of winning positions in a higher-order pushdown parity game are regular and can be effectively computed. Computing these regions is an n-EXPTIMEcomplete problem for an order-n pushdown parity game.

Starting with an order-n pushdown parity game, and applying n times the reduction of Proposition 1, one ends up with a parity game using the same number of colours over a finite game graph whose size, using Remark 4, is n times exponential in the size of the original order-n pushdown automaton. As solving this latter game is exponential only on the number of colours [START_REF] Grädel | Automata, Logics, and Infinite Games[END_REF] the global procedure is in n-EXPTIME. The lower bound follows from the fact that deciding the winner in two-player reachability games over order-n pushdown is already n-EXPTIME-hard. A self-contained proof can be found in [START_REF] Cachat | The complexity of games on higher order pushdown automata[END_REF]. The next remark sketches a much simpler proof of this result.

Remark 5. Note that using the reduction of Theorem 2, we can deduce n-EXPTIME-hardness by reduction to the (n -1)-EXPTIME-hardness of the emptiness problem for order-n pushdown automata [START_REF] Engelfriet | Iterated stack automata and complexity classes[END_REF]. Consider an order-(n+1) pushdown automaton P over a one-letter input alphabet. The emptiness problem for P is polynomially equivalent to deciding the winner in the associated one-player reachability game. In the case of a one-player game, the reduction of Theorem 2 can be tailored to yield a reduced game G which is a two-player game of polynomial size w.r.t to P. Hence we establish that the emptiness problem for order-(n + 1) pushdown automata can be polynomially reduced to deciding the winner of two-player order-n game. This proves the n-EXPTIME-hardness of the latter problem. Remark 6. Theorem 4 generalises the result obtained by Hague and Ong [START_REF] Hague | Symbolic backwardsreachability analysis for higher-order pushdown systems[END_REF] for higher-order pushdown reachability games.

Concerning strategies, we already noted in Remark 3 that a winning strategy can be realised by a pushdown automaton whose stack is synchronised with the one from the game. Reasoning by induction and relying on Theorem 3, one can obtain a similar result for the general case. More precisely, if one defines the shape of an order-k stack to be the stack of obtained by rewriting the stack symbols by a fixed symbol , we get the following result.

Theorem 5. Consider an order-k pushdown parity game.

Then one can construct, for any player, a deterministic order-k pushdown automaton that realises a winning strategy and whose stack has always the same shape as the one in the game. Remark 7. Theorem 5 means that the memory needed to win a higher-order pushdown parity game can actually be implemented in the underlying higher-order pushdown automaton defining the game by enriching its stack alphabet.

Global µ-calculus model-checking

Given a vertex (state) s in a state-transition graph K and a formula ϕ, the model-checking problem asks whether K, s |= ϕ holds (in words, whether the formula ϕ holds at s in the structure K). The global model-checking problem is the task of computing (if possible) a finite representation of the set ||K|| ϕ = {s | K, s |= ϕ} of vertices in K that satisfy a given formula ϕ.

In the following we tackle the global model checking problem when ϕ is a formula of the modal µ-calculus [START_REF] Kozen | Results on the propositional mu-calculus[END_REF][START_REF] Arnold | Rudiments of mucalculus[END_REF]. We consider two kinds of structures for K: configuration graphs of higher-order pushdown automata, and trees generated by higher-order safe recursion schemes.

Global model-checking of configuration graphs of higher-order pushdown automata

The µ-calculus global model-checking problem for families of graphs closed under Cartesian product with finite graphs is well-known to be equivalent to the solvability of parity games over the same class. Hence Theorem 4 implies the following characterisation of µ-calculus definable sets over higher-order pushdown graphs: Theorem 6. The µ-calculus definable sets over configuration graphs of higher-order pushdown automata are exactly the regular sets of configurations.

Remark 8. The preceding Theorem generalises a result of Bouajjani and Meyer in [START_REF] Bouajjani | Symbolic reachability analysis of higher-order context-free processes[END_REF] for a weaker logic (i.e. the E(U, X) fragment of CTL) over weaker structures (i.e. higher-order pushdown automata with a single control state).

Global model-checking of trees generated by higher-order safe recursion schemes

Fix a (ranked) alphabet Σ. Types are generated from a base type using the arrow constructor →. A higher-order (deterministic) recursion scheme is a finite set of equations of the form F x 1 • • • x n = e, where F is a typed nonterminal, each x i is a typed variable, and e is an applicative term constructed from the non-terminals, terminals (which are the Σ-symbols), and variables x 1 , • • • , x n . The scheme is said to be order-k if the highest order of the non-terminals is k. We use recursion schemes here as generators of possibly infinite term-trees. The ranked tree generated by a recursion scheme is defined to be the (possibly infinite) term-tree built up from the terminal symbols by applying the equations qua rewrite rules, replacing the formal parameters by the actual parameters, starting from the initial non-terminal. We refer the reader to [START_REF] Knapik | Higherorder pushdown trees are easy[END_REF] for a precise description of the preceding, and for the meaning of safety which is a syntactic constraint; here we rely on the following characterisation: Theorem 7. [START_REF] Knapik | Higherorder pushdown trees are easy[END_REF] For each k ≥ 0, the ranked trees generated by safe order-k recursion schemes coincide with the ε-closure of the unravelling of the configuration graphs of deterministic order-k pushdown automata.

Consider a higher-order deterministic pushdown automaton labelled by Σ ∪ {ε}. After unravelling its configuration graph from the initial configuration, the operation of ε-closure (see [START_REF] Stirling | Decidability of bisimulation equivalence for pushdown processes[END_REF]) first adds an a-labelled edge from c 1 to c 2 whenever there is a path from c 1 to c 2 that traces out the word aε * and c 2 is not the source-vertex of an εlabelled edge, and then removes the source-vertex of every ε-labelled edge. The resultant graph is a tree.

A node in this tree is naturally represented by the word over Σ labelling the path from the root to this node. Hence, every µ-calculus formula over such a tree induces a language in Σ * i.e. the set of words labelling a path from the root to a node satisfying the formula. These languages can be characterised as follows: Theorem 8. Let k ≥ 0 and let T be the ranked tree generated by a given order-k safe recursion scheme. The µcalculus definable sets of T -nodes are recognisable by a deterministic order-k pushdown automaton. Proof (sketch). Let C be the configuration graph of a deterministic order-k Σ ∪ {ε}-labelled pushdown automaton P, and let U be the unravelling of C from the initial configuration c 0 , such that the ε-closure of U is isomorphic to T . Let ϕ be a µ-calculus formula. A node in U satisfies ϕ if and only if it corresponds to a path ending in a vertex of C that satisfies ϕ. By Theorem 6, the set F of configurations of C satisfying ϕ in C is regular. Moreover it is easy to see that the set E of configurations of C which are not the sourcevertex of a ε-labelled edge in C is also regular. A node in T at the end of a path from the root labelled by w satisfies ϕ in T if and only if w is accepted by the labelled pushdown automaton P from the initial configuration to the regular set E ∩ F . By Proposition 1, the language consisting of such w is accepted by an order-k pushdown automaton.

Discussions

There are a number of further directions:

• Can the quite general class of stack data games together with Theorem 2 be used to prove the decidability of games over new structures (e.g. allowing arithmetic on the stack)?

• Regular stack properties allow assertions over the stack contents. Since information regarding regular tests may be encoded in the control states and stack of an abstract pushdown process, the definable sets are again regular. Properties of this kind have been shown to have applications in inter-procedural data-flow analysis [START_REF] Esparza | Modelchecking LTL with regular valuations for pushdown systems[END_REF] and security [START_REF] Jensen | Verification of control flow based security properties[END_REF] for the case of order-1 pushdown systems. One such security property, implemented in Java and .Net [START_REF] Gong | Inside Java 2 platform security architecture, API design, and implementation[END_REF][START_REF] Box | Essential .NET: The Common Language Runtime[END_REF], allows the programmer to decorate code with permission checks. These checks require that all callers on the stack have sufficient privileges to proceed. Do regular stack properties have similar applications for other structures encodable as abstract pushdown processes?

• The notion of regularity used in this article can capture the µ-calculus definable sets of configurations. As mentioned previously, MSO-definable sets can be captured by a stronger notion of regularity introduced in [START_REF] Carayol | Regular sets of higher-order pushdown stacks[END_REF][START_REF] Fratani | Automates à pile de piles[END_REF]. Hence a natural question is the decidability of the following problem: given a strong regular set (in the sense of [START_REF] Carayol | Regular sets of higher-order pushdown stacks[END_REF][START_REF] Fratani | Automates à pile de piles[END_REF]), decide whether it is regular (in the sense of this article). Moreover, it is known from [START_REF] Fratani | Automates à pile de piles[END_REF] that positional winning strategies of higher-order pushdown parity game can be described using strong regular sets (i.e. for each transition, the set of configurations from which the strategy plays the transition is a strong regular set) and a k-Exptime algorithm was recently given in [START_REF] Carayol | Positional Strategies for Higher-Order Pushdown Parity Games[END_REF]. Is it possible to describe positional winning strategies using the weak notion of regularity of this article?

• Order-k collapsible pushdown automata (CPDA) are a generalisation of order-k pushdown automata in which each symbol in the k-stack has a link to a stack below it. As generators of ranked trees, they are equi-expressive with (arbitrary) order-k recursion schemes [START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF]. A natural question is to consider configuration graphs of CPDA, and compute a finite representation of the µ-calculus definable vertex-sets thereof.

An alternative method for computing the winning regions of a higher-order pushdown parity game develops the order-1 saturation techniques introduced by Bouajjani et al. [START_REF] Bouajjani | Reachability analysis of pushdown automata: Application to model-checking[END_REF] and Finkel et al. [START_REF] Finkel | A direct symbolic approach to model checking pushdown systems[END_REF] and generalised to Büchi games by Cachat [8]. This algorithm uses a characterisation of a game's winning regions as a series of greatest and least fixed points. Following this characterisation, a small initial automaton, accepting higher-order stacks, is expanded until the winning region has been computed. Because this technique does not require an n-exponential reduction to a finite state game, it is possible that the state-explosion problem may be avoided in some, low-order, cases.

δ B (q B 0 , π) = p for b 0 = 1 and δ A ((q B 0 , 0), [) = (p, 1) δ B (q i , π) = q j for b ρ(i,j) = 1 finally, we take Acc(p) = {q ∈ Q | δ A ((p, 1), ]q) ∈ F A } for all p ∈ Q A .

C Proof of Proposition 3

Proposition 3. Let σ ∈ (Γ\{⊥}) * , q ∈ Q and γ ∈ Γ\{⊥}. Then Éloïse has a winning strategy in G from (q, ⊥σγ) if and only if there exists some R ∈ R(q, γ) such that (r, ⊥σ) is winning for Éloïse in G for every r ∈ R.

Proof. Assume Éloïse has a winning strategy from (q, ⊥σγ) in G and call it ϕ. Consider the set L of all plays in G that starts from (q, ⊥σγ) and where Éloïse respects ϕ. Define R to be the (possibly empty) set that consists of all r ∈ Q such that there is a play in L of the form

v 0 • • • v k (r, ⊥σ)v k+1 • • • where each v i for 0 ≤ i ≤ k is of the form (p i , ⊥σσ i ) for some σ i = ε.
In other words, R consists of all states that can be reached on popping (possibly a rewriting of) γ for the first time in a play where Éloïse respects ϕ. Define a (partial) function τ as τ ((q, ⊥σσ )) = (q, ⊥σ ) for every q ∈ Q and set τ -1 ((q, ⊥σ )) = (q, ⊥σσ ). Then τ -1 is extended as a morphism over V * . It is easily shown that R ∈ R(q, γ). Indeed a winning strategy for Éloïse in G(R) is defined as follows:

• if some empty stack configuration has already been visited play any move,

• otherwise goes to τ (ϕ(τ -1 (λ)), where λ is the partial play seen so far.

By definition of L and R it easily follows that the previous strategy is winning for Éloïse in G(R), and therefore R ∈ R(p, γ). Finally, for every r ∈ R there is, by definition of L a partial play λ r that starts from (q, ⊥σγ), where Éloïse respects ϕ and that ends in (r, ⊥σ). A winning strategy for Éloïse in G from (r, ⊥σ) is given by ψ(λ) = ϕ(λ r • λ), where λ r denotes the partial play obtained from λ r by removing its last vertex (r, ⊥σ).

Conversely, let us assume that there is some R ∈ R(q, γ) such that (r, ⊥σ) is winning for Éloïse in G for every r ∈ R. For every r ∈ R, let us denote by ϕ r a winning strategy for Éloïse from (r, ⊥σ) in G. Let ϕ R be a winning strategy for Éloïse in G(R) from (q, ⊥γ). Let us define τ and τ -1 as in the direct implication and extend them as (partial) morphism over V * . Define the following strategy for Éloïse in G for plays starting from (q, ⊥σγ). For any partial play λ,

• if λ does not contain a configuration of the form (p, ⊥σ) then ϕ(λ) = τ -1 (ϕ R (τ (λ)));

• otherwise let λ = λ • (r, ⊥σ) • λ where λ does not contain any configuration of the form (p, ⊥σ). From how ϕ is defined in the previous case, it is follows that r ∈ R. One finally sets ϕ(λ) = ϕ r (λ • (r, ⊥σ)).

It is then easy to prove that ϕ is a winning strategy for Éloïse in G from (q, ⊥σγ).

D Proof of Theorem 2

Theorem 2 The following holds.

For every

q ∈ Q, γ ∈ Γ and R ⊆ Q, R ∈ R(q, γ)
if and only if (q, γ, (R, . . . , R), ρ(q)) is winning for Éloïse in G.

D.1 The game graph G

Let us first precisely describe the game graph G. We refer the reader to Figure 1.

• The main vertices of G are those of the form

(p, α, - → R , θ), where p ∈ Q, α ∈ Γ, - → R = (R 0 , . . . , R d ) ∈ P(Q) d+1 and θ ∈ {0, . . . , d}. A ver- tex (p, α, - → R , θ
) is reached when simulating a partial play Λ in G such that:

-The last vertex in Λ is (p, ⊥σα) for some σ ∈ Γ * .

-Éloïse claims that she has a strategy to continue Λ in such a way that if α (or a rewriting of it) is eventually popped, the control state reached after popping belongs to R m , where m is the smallest colour visited since the stack height was at least |⊥σα|. -The colour θ is the smallest one since the current stack level was reached from a lower stack level.

A vertex (p, α, -→ R , θ) is controlled by Éloïse if and only if p ∈ Q E .
• The vertices tt and ff are here to ensure that the vectors -→ R encoded in the main vertices are correct. Vertex tt is controlled by Abelard, whereas vertex ff belongs to Éloïse. As these vertices are dead-ends, a play reaching tt is won by Éloïse whereas a play reaching ff is won by Abelard (recall that the player controlling the dead-end loses).

There is a transition from some vertex (p, α, -→ R , θ) to tt, if and only if there exists a transition rule (r, pop) ∈ ∆(p, α), such that r ∈ R θ (this means that -→ R is correct with respect to this transition rule). Dually, there is a transition from a vertex (p, α, -→ R , θ) to ff if and only if there exists a transition rule (r, pop) ∈ ∆(p, α) such that r / ∈ R θ (this means that -→ R is not correct with respect to this transition rule).

• To simulate a transition rule (q, rew(β)) ∈ ∆(p, α), the player that controls (p, α, -→ R , θ) moves to (q, β, -→ R , min(θ, ρ(q))). Note that the last component has to be updated as the smallest colour seen since the current stack level was reached is now min(θ, ρ(q)).

• To simulate a transition rule (q, push(β)) ∈ ∆(p, α), the player that controls (p, α, -→ R , θ) moves to (p, α, -→ R , θ, q, β). This vertex is controlled by Éloïse who has to give a vector -→ S = (S 0 , . . . , S d ) ∈ P(Q) d+1 that describes the control states that can be reached if β (or a symbol that rewrites it later by applying rew rules) is eventually popped. To describe this vector, she goes to the corresponding vertex

(p, α, - → R , θ, q, β, - → S ). Any vertex (p, α, - → R , θ, q, β, - → S
) is controlled by Abelard who chooses either to simulate a bump or a stair. In the first case, he additionally has to pick the minimal colour of the bump. To simulate a bump with minimal colour i, he goes to a vertex (s, α, -→ R , min(θ, i, ρ(s))), for some s ∈ S i , through an edge coloured by i.

To simulate a stair, Abelard goes to the vertex (q, β, -→ S , ρ(q)).

The last component of the vertex (that stores the smallest colour seen since the currently simulated stack level was reached) has to be updated in all those cases. After simulating a bump of minimal colour i, the minimal colour is min(θ, i, ρ(s)). After simulating a stair, this colour has to be initialized (since a new stack level is simulated). Its value, is therefore ρ(q), which is the unique colour since the (new) stack level was reached.

The only vertices that are coloured are those of the form

(p, α, - → R , θ
) and the colour of such a vertex is ρ(p). Some edges are also coloured. See Figure 1 for details.

Remark 9. In the definition of parity games we were required a total colouring function working only on vertices. One can add extra intermediate states to remove colouring on edges and assign the largest colour d to all uncoloured vertices.

D.2 Proof of Theorem 2

This subsection is devoted to the proof of Theorem 2. We only prove the first part of it, the proof of the second one being a subpart of it.

Factorisation of a play in G.

Recall that for an infinite play

Λ = v 0 v 1 • • • in G Steps Λ
denote the set of indices of positions where no configuration of strictly smaller stack height is visited later in the play. More formally,

Steps Λ = {i ∈ N | ∀j ≥ i sh(v j ) ≥ sh(v i )}, where sh((q, ⊥γ 1 • • • γ n )) = n + 1. Note that
Steps Λ is always infinite and hence induces a factorisation of the play Λ into finite pieces.

Indeed, for any play Λ with

Steps Λ = {n 0 < n 1 < • • • }, one can define the sequence (Λ i ) i≥0 by setting Λ i = v ni • • • v ni+1 .
Note that each of the Λ i is either a bump or a stair. In the later we designate (Λ i ) i≥0 as the rounds factorisation of Λ.

Factorisation of a play in G.

Recall that in G some edges are coloured. Hence, to represent a play, we have to encode this information on edge colouring. We only need to encode the colours in {0, . . . , d} that appears when simulating a bump: a play will be represented as a sequence of vertices together with colours in {0, . . . , d} that correspond to colours appearing on edges.

For any play in G, a round is a factor between two visits through vertices of the form (p, α, -→ R , θ). We have the following possible forms for a round:

• The round is of the form (p, α, -→ R , θ)(q, β, -→ R , θ) and corresponds therefore to the simulation of a rew rule. We designate it as a top rewriting bump.

• The round is of the form (p, α, - → R , θ)(p, α, -→ R , θ, q, β)(p, α, -→ R , θ, q, β, - → S )i (s, α, - → R , min (θ, i, ρ(s)
)) and corresponds therefore to the simulation of a rule pushing β followed by a sequence of moves that ends by popping β (or a rewriting of it). Moreover i is the smallest colour encountered while β (or other top stack symbol obtained by applying rew rules successively) was on the stack.

• The round is of the form (p, α, - → R , θ)(p, α, -→ R , θ, q, β)(p, α, -→ R , θ, q, β, - → S ) (q, β, - → S , ρ(q)
) and corresponds therefore to the simulation of a rule pushing a symbol β leading to a new stack level below which the play will never go. We designate it as a stair.

For any play

λ = v 0 v 1 v 2 • • • in G,
we consider the subset of indices corresponding to vertices of the form (p, α, -→ R , θ). More precisely:

Rounds λ = {n | v n = (p, α, - → R , θ), p ∈ Q, α ∈ Γ, - → R ∈ P(Q) d+1 , 0 ≤ θ ≤ d}
Therefore, the set Rounds λ induces a natural factorisation of λ into rounds.

Definition 1 (Rounds factorisation). For a (possibly partial) play

λ = v 0 v 1 v 2 • • • , we call rounds factorisation of λ, the (possibly finite) sequence (λ i ) i≥0 of rounds defined as follows. Let Rounds λ = {n 0 < n 1 < n 2 < • • • }, then for all 0 ≤ i < |Rounds λ |, λ i = v ni • • • v ni+1 .
Therefore, for every i ≥ 0, the first vertex in λ i+1 equals the last one in λ i . Moreover, λ = λ 1 λ 2 λ 3 • • • , where λ i λ i+1 denotes the concatenation of λ i with λ i+1 without its first vertex.

Finally, the colour of a round is the smallest colour in {0, . . . , d} appearing in the round.

In order to prove both implications of Theorem 2, we build from a winning strategy for Éloïse in one game a winning strategy for her in the other game. The main argument to prove that the new strategy is winning is to prove a correspondence between the factorisations of plays in both games.

Direct implication.

Assume that the configuration (p in , ⊥) is winning for Éloïse in G, and let Φ be a corresponding winning strategy for her.

Using Φ, we define a strategy ϕ for Éloïse in G from (p in , ⊥, (∅, . . . , ∅), ρ(p in )). This strategy stores a partial play in G, that is an element in V * (where V denotes the set of vertices of G). This memory will be denoted Λ. At the beginning Λ is initialized to the vertex (p in , ⊥). We first describe ϕ, and then we explain how Λ is updated. Both the strategy ϕ and the update of Λ, are described for a round.

Choice of the move. Assume that the play is in some vertex

(p, α, - → R , θ) for p ∈ Q E .
The move given by ϕ depends on Φ(Λ):

• If Φ(Λ) = (r, pop), then Éloïse goes to tt (Proposition 5 will prove that this move is always possible).

• If Φ(Λ) = (q, rew(β)), then Éloïse goes to (q, β, -→ R , min(θ, ρ(q))).

• If Φ(Λ) = (q, push(β)), then Éloïse goes to (p, α, -→ R , θ, q, β).

In this last case, or in the case where p ∈ Q A and Abelard goes to (p, α, -→ R , θ, q, β), we also have to explain how Éloïse behaves from (p, α, -→ R , θ, q, β). She has to provide a vector -→ S ∈ P(Q) d+1 that describes which states can be reached if β (or its successors by top rewriting) is popped, depending on the smallest visited colour in the meantime. In order to define -→ S , Éloïse considers the set of all possible continuations of Λ • (q, σαβ) (where (p, σα) denotes the last vertex of Λ) where she respects her strategy Φ. For each such play, she checks whether some configuration of the form (s, σα) is visited after Λ • (q, σαβ), that is if the stack level of β is eventually left. If it is the case, she considers the first configuration (s, σα) appearing after Λ • (q, σαβ) and the smallest colour i since β and (possibly) its successors by top rewriting were on the stack. For every i ∈ {0, . . . d}, S i , is exactly the set of states s ∈ Q such that the preceding case happens. More formally,

S i = {s | ∃ Λ • (q, σαβ)v 0 • • • v k (s, σα) • • • play in G
where Éloïse respects Φ and s.t. |v j | > |σα|, ∀j = 0, . . . , k and min({ρ(v j ) | j = 0, . . . , k} ∪ {ρ(q)}) = i} Finally, we set -→ S = (S 0 , . . . , S d ) and Éloïse moves to

(p, α, - → R , θ, q, β, - → S )
. Update of Λ. The memory Λ is updated after each visit to a vertex of the form (p, α, -→ R , θ). We have three cases depending on the kind of the last round:

• The round is a top rewriting bump and therefore a (q, rew(β)) action was simulated. Let (p, σα) be the last vertex in Λ, then the updated memory is Λ•(q, σβ).

• The round is a bump, and therefore a bump of colour i (where i is the colour of the round) starting with some action (q, push(β)) and ending in a state s ∈ S i was simulated. Let (p, σα) be the last vertex in Λ. Then the memory becomes Λ extended by (q, σαβ) followed by a sequence of moves, where Éloïse respects Φ, that ends by popping β and reach (s, σα) while having i as smallest colour. By definition of S i such a sequence of moves always exists.

• The round is a stair and therefore we have simulated a (q, push(β)) action. If (p, σα) denotes the last vertex in Λ, then the updated memory is Λ • (q, σαβ).

Therefore, with any partial play λ in G in which Éloïse respects her strategy ϕ, is associated a partial play Λ in G. An immediate induction shows that Éloïse respects Φ in Λ. The same arguments works for an infinite play λ, and the corresponding play Λ is therefore infinite, starts from (p in , ⊥) and Éloïse respects Φ in that play. Therefore it is a winning play.

The following proposition is a direct consequence of how ϕ was defined. Proposition 5. Let λ be a partial play in G that starts from (p in , ⊥, (∅, . . . , ∅), ρ(p in )), ends in a vertex of the form (p, α, -→ R , θ), and where Éloïse respects ϕ. Let Λ be the play associated with λ built by the strategy ϕ. Then the following holds:

1. Λ ends in a vertex of the form (p, σα) for some σ ∈ Γ * . 2. θ is the smallest visited colour in Λ since α (or a symbol that was later rewritten as α) has been pushed.

3. Assume that Λ is extended, that Éloïse keeps respecting Φ and that the next move after (p, σα) is to some vertex (r, σ). Then r ∈ R θ .

Remark 10. Proposition 5 implies that the strategy ϕ is well defined when it provides a move to tt. Moreover, one can deduce that, if Éloïse respects ϕ, ff is never reached.

The preceding remark shows in particular that any finite play ends in some vertex tt and is therefore won by Éloïse. For infinite plays, using the definitions of G and ϕ, we easily deduce the following proposition. Proposition 6. Let λ be an infinite play in G that starts from (p in , ⊥, (∅, . . . , ∅), ρ(p in )), and where Éloïse respects ϕ. Let Λ be the associated play built by the strategy ϕ, and let (Λ i ) i≥0 be its rounds factorisation. Let (λ i ) i≥0 be the rounds factorisation of λ. Then, for every i ≥ 1 the following hold:

1. λ i is a bump if and only if Λ i is a bump 2. λ i has colour mcol Λ i . Proposition 6 implies that for any infinite play λ in G starting from (p in , ⊥, (∅, . . . , ∅), ρ(p in )) where Éloïse respects ϕ, the sequence of visited colours in λ is (mcol Λ i ) i≥0 for the corresponding play Λ in G. Hence, using Proposition 4 we conclude that λ is winning if and only if Λ is winning. As Λ is winning for Éloïse, it follows that λ is also winning for her.

Converse implication 1

Assume now that Éloïse has a winning strategy ϕ in G from (p in , ⊥, (∅, . . . , ∅), ρ(p in )). Using ϕ, we build a strategy Φ for Éloïse in G for plays starting from (p in , ⊥).

1 Note that in order to prove the converse implication one could follow the direct implication and consider the point of view of Abelard. Nevertheless the proof we give here starts from a winning strategy for Éloïse in e G and deduces a strategy for her in G: this induces a more involved proof but has the advantage to lead to an effective construction of a winning strategy for Éloïse in G if one has an effective strategy for her in e G

The strategy Φ uses, as memory, an abstract pushdown content Π, to store the complete description of a play in G. Recall here that a play in G is represented as a sequence of vertices together with colours in {0, . . . d}.

Therefore the abstract pushdown content alphabet of Π is the set of vertices of G together with {0, . . . , d}. In the following, top(Π) will denote the top stack symbol of Π while StCont(Π) will be the word obtained by reading Π from bottom to top (without considering the bottomof-stack symbol of Π). In any play where Éloïse respects Φ, StCont(Π) will be a play in G that starts from (p in , ⊥, (∅, . . . , ∅), ρ(p in )) and where Éloïse respects her winning strategy ϕ. Moreover, for any play Λ where Éloïse respects Φ, we will always have that top(Π) = (p, α, -→ R , θ) if and only if the current configuration in Λ is of the form (p, σα). Finally, if Éloïse keeps respecting Φ, and if α (or a symbol that rewrite it later) is eventually popped the configuration reached will be of the form (r, σ) for some r ∈ R i , where i is the smallest visited colour since α (or some symbol that was later rewritten as α) was on the stack. Initially, Π only contains (p in , ⊥, (∅, . . . , ∅), ρ(p in )).

In order to describe Φ, we assume that we are in some configuration (p, σα) and that top(Π) = (p, α, -→ R , θ). We first describe how Éloïse plays if p ∈ Q E , and then we explain how the stack is updated.

• Choice of the move. Assume that p ∈ Q E and that Éloïse has to play from some vertex (p, σα). For this, she considers the value of ϕ on StCont(Π).

If it is a move to tt, Éloïse plays an action (r, pop) for some state r ∈ R θ . Lemma 1 will prove that such an r always exists.

If the move given by ϕ is to go to some vertex (q, β, -→ R , min(θ, ρ(q))), Éloïse applies the transition (q, rew(β)). If the move given by ϕ is to go to some vertex (p, α, -→ R , θ, q, β), then Éloïse applies the transition (q, push(β)).

• Update of Π. Assume that the last move, played by Éloïse or Abelard, was to go from (p, σα) to some configuration (r, σ). The update of Π is illustrated by figure 2 and explained in what follows. Éloïse pops in Π until she finds some configuration of the form (p , α , -→ R , θ , p , α , -→ R ) that is not preceded by a colour in {0, . . . , d}. This configuration is therefore in the stair that simulates the pushing of α onto the stack (here if α = α then α was later rewritten as α). Éloïse updates Π by pushing θ in Π followed by (r, α , -→ R , min(θ , θ, ρ(r))). Assume that the last move, played by Éloïse or Abelard, was to go from (p, σα) to some configu-ration (q, σα ). Then Éloïse update Π by pushing (q, α , -→ R , min(θ, ρ(q))). Assume that the last move, played by Éloïse or Abelard, was to go from (p, σα) to some configuration

(q, σαβ), let (p, α, -→ R , θ, q, β, - → S ) = ϕ(StCont(Π) • (p, α, - → R , θ, q, β)).
Intuitively, -→ S describes which states Éloïse can force play to reach if β is eventually popped. Éloïse updates Π by successively pushing (p, α, -→ R , θ, q, β), (p, α, -→ R , θ, q, β, -→ S ), and (q, β, -→ S , ρ(q)).

The following lemma gives the meaning of the information stored in Π.

Lemma 1. Let Λ be a partial play in G, where Éloïse respects Φ, that starts from (p in , ⊥) and that ends in a configuration (p, σα). We have the following facts:

1. top(Π) = (p, α, - → R , θ) with - → R ∈ P(Q) d+1 and 0 ≤ θ ≤ d.

StCont(Π) is a partial play in G that starts from

(p in , ⊥, (∅, . . . , ∅), ρ(p in )), that ends with (p, α, -→ R , θ) and where Éloïse respects ϕ.

3. θ is the smallest colour visited since α (or some symbol that was later rewritten as α) was pushed.

4. If Λ is extended by some move that pops α, the configuration (r, σ) that is reached is such that r ∈ R θ .

Proof. The proof goes by induction on Λ. We first show that the last point is a consequence of the second and third points. To aid readability, one can refer to Figure 2. Assume that the next move after (p, σα) is to apply an action (r, pop) ∈ ∆(p, α). The second point implies that

(p, α, - → R , θ) is winning for Éloïse in G. If p ∈ Q E ,
by definition of Φ, there is some edge from that vertex to tt, which means that r ∈ R θ and allows us to conclude. If p ∈ Q A , note that there is no edge from (p, α, -→ R , θ) (winning position for Éloïse) to the losing vertex ff . Hence we conclude the same way.

Let us now prove the other points. For this, assume that the result is proved for some play Λ, and let Λ be an extension of Λ. We have two cases, depending on how Λ extends Λ:

• Λ is obtained by applying a rule of type rew or push.

The result is trivial in that case.

• Λ is obtained by applying a pop rule. Let (p, σα) be the last configuration in Λ, and let -→ R be the last vector component in top(Π) when in configuration (p, σα).

By the induction hypothesis, it follows that

Λ = Λ • (p , σ) (p , σα ) (p, σα) σ = σ α Π • • • (p , α , -→ R , θ ) (p , α , -→ R , θ , p , α) (p , α , -→ R , θ , p , α , - → R ) (p , α , - → R , ρ(p )) (p, α, - → R , θ) • • • (p, σα) min. col. = θ min. col. = θ (p , σ) (r, σ) σ = σ α Π • • • (p , α , -→ R , θ ) (p , α , -→ R , θ , p , α ) (p , α , -→ R , θ , p , α , - → R ) θ (r, α , -→ R , min(θ , θ, ρ(r)))
min. col.= min(θ , θ, ρ(r)) Actually, we easily deduce a more precise result.

Lemma 2. Let Λ be a partial play in G starting from (p in , ⊥) and where Éloïse respects Φ. Let (Λ i ) i≥0 be its rounds factorisation. Let λ = StCont(Π), where Π denotes the strategy's stack in the last vertex of Λ. Let (λ i ) i=0,...,k be the rounds factorisation of λ. Then the following holds:

• λ i is a bump if and only if Λ i is a bump.

• λ i has colour mcol Λ i . Both lemmas 1 and 2 are for partial plays. A version for infinite plays would allow us to conclude. Let Λ be an infinite play in G. We define an infinite version of λ by considering the limit of the stack contents (StCont(Π i )) i≥0 where Π i is the strategy's stack after the first i moves in Λ. See [START_REF] Serre | Games with winning conditions of high borel complexity[END_REF] for similar constructions. It is easily seen that such a limit always exists, is infinite and corresponds to a play won by Éloïse in G. Moreover the results of Lemma 2 apply.

Let Λ be a play in G with initial vertex (p in , ⊥), and where Éloïse respects Φ, and let λ be the associated infinite play in G. Therefore λ is won by Éloïse. Using Lemma 2 and Proposition 4, we conclude, as in the direct implication that Λ is winning.

E Proof of Theorem 3

Theorem 3. Assume Éloïse has a winning strategy ϕ in G that uses a memory ranging from some set M . Then one can construct an abstract pushdown process T with output that realises a winning strategy Φ for Éloïse in G. Moreover the abstract pushdown alphabet used by T is V × M and, at any moment in a play where Éloïse respects Φ, the abstract pushdown content of T has exactly the same height as the one in the current position of the game graph. Finally, if ϕ is effective the same holds for Φ.

Proof (sketch). The proof strongly relies on the converse implication of the proof of Theorem 2. Hence we assume that the reader read Section D.2 where the following was proved. Starting from a winning strategy for Éloïse in G from (p in , ⊥, (∅, . . . , ∅), ρ(p in )) we built a winning strategy Φ for Éloïse in G that is winning from (p in , ⊥). Moreover Φ uses an abstract pushdown content Π as a memory and the stack alphabet of Φ is the set of vertices in G augmented by the set of colours {0, . . . , d}. Assume now that ϕ is a strategy with memory ranging from some set M . Then, it is fairly easy to note that Π can be modified (and denoted Π ) so that it is now over a larger alphabet (namely the Cartesian product of the previous one with M ) and that its M component is exactly the value of the memory over StCont(Π). Hence the move given by ϕ over StCont(Π ) only depends on top(Π ).

At that point we have the desired result except that Π is not synchronised (i.e. always has the same height) with the abstract pushdown content of the game graph. Indeed Π stores for instance all bumps on a given level which can arbitrarily increases its height. Nevertheless we can note that the only case where we really use the fact that Π is a stack is when we simulate a pop action and have to remove a lot of symbols from Π (until finding the step that reached the currently left stack level). When doing this we always go back to the last moment where some stack level was visited. Hence instead of collecting information on bumps in Π we can forget about it and only recall the information on the last configuration of each stack level. Therefore, if we denote by Π this new stack, it contains exactly one element per stack level in the game and therefore always has the same height than the stack in the game. Hence we have the desired result.

So far we have only considered the case where we start from a configuration with an empty stack. In order to deal with the general case, we only have to explain how to initialise Π . This can be done by following the idea behind Theorem 1. Indeed, consider some (winning) position (p, σ)

with σ = ⊥σ 1 • • • σ n . Let ∅ • R 0 , • • • R n be the run of the automaton A from Theorem 1 on ⊥σ 1 • • • σ n . Then set v i = (p, σ i , (R i , • • • , R i ), ρ(p)
) and initialise Π as ⊥v 0 • • • v n . Now if one defines the winning strategy as in the previous case with this initial value, it leads to a winning strategy from (p, σ). This is immediate if σ n (and its possibly rewritings) is never popped. Otherwise, it mainly follows from the fact that Éloïse wins from (r, ⊥σ 1 • • • σ n-1 ) for any r ∈ R n (and by induction).

F Proof of Theorem 4

Theorem 4. The sets of winning positions in a higherorder pushdown parity game are regular and can be effectively computed. Computing these regions is an n-EXPTIME-complete problem for an order-n pushdown parity game.

Proof. Regularity of the wining region is directly obtained by combining Property 1 together with Proposition 2 and Theorem 2. Hence, we only discuss the complexity issue. The upper bound comes from two facts:

• The description (by means of a higher-order pushdown automaton) of G is exponentially larger than the one of G (the control state space is exponentially larger).

• Both G and G use the same number of colours

Starting with an order-n parity pushdown game, and applying n time the reduction of Theorem 2, one ends up with a parity game using (d + 1) colours over a finite game graph whose size is n times exponential in the size of the original order-n pushdown automaton. As solving this latter game is exponential only on the number of colours [START_REF] Grädel | Automata, Logics, and Infinite Games[END_REF] the global procedure is in n-EXPTIME.

For the lower bound, it follows from the fact that deciding the winner in an order-n pushdown two-player reachability game is already n-EXPTIME-hard. Indeed, checking emptiness of a nondeterministic higher-order pushdown automaton of order-n is an (n -1)-EXPTIME complete problem [START_REF] Engelfriet | Iterated stack automata and complexity classes[END_REF]. Trivially this result is still true if we assume that the input alphabet is reduced to a single letter. Now consider an order-(n + 1) nondeterministic higher order pushdown automaton A whose input alphabet is reduced to a single letter. The language accepted by A is non-empty if and only if there is a path from the initial configuration of A to a final configuration of A in the transition graph G of A. Equivalently the language accepted by A is non-empty if and only if Éloïse wins the reachability game G over G where she controls all vertices (and where the play starts from the initial configuration of A and where final vertices are those corresponding to final configurations of A). Now consider the reduction used to prove Theorem 2 and apply it to G (and adapt it to the -simpler -reachability winning condition): it leads to an equivalent reachability game G that is now played on the transition graph of an order-n pushdown automaton. In the new game graph, the main vertices are of the form (p, s, R): here R is a subset of Q as we no longer need to deal with colours and we no longer need to use the θ component to store information on the smallest colour. The important fact is that R can be forced to be a singleton: this follows from the fact that all vertices in G are controlled by Éloïse (and from the proof's details). Therefore, one concludes that the size of the game graph associated with G is polynomial in the size of A. Hence, one has shown the following: checking emptiness for an order-(n + 1) nondeterministic higher order pushdown automaton whose input alphabet is reduced to a single letter can be polynomially reduced to solve a reachability game over the transition graph of an order-n higher order pushdown automaton. In conclusion, this last problem is n-EXPTIME hard (and actually n-EXPTIME-complete).

G Proof of Theorem 5

Theorem 5. Consider an order-k parity pushdown game. Then one can construct, for any player, a deterministic order-k pushdown automaton that realises a winning strategy and whose stack has always the same shape as the one in the game.

Proof (sketch). The order 1 case was noted in Remark 3. For the general case, we reason by induction using Theorem 3 together with the base case (order 1).

Assume the result is proved at order k and consider some order-(k + 1) game G. Then using Property 1 we get that G is a game of order k. Hence we conclude on the existence of a strategy realised by a deterministic order-k pushdown automaton whose stack has always the same shape as the one in G. Now apply Theorem 3: it leads to a strategy in G realised by an abstract pushdown process whose abstract pushdown content is the product of the vertices in G together with the memory used to win in G, that is the product of two order-k stacks having the same shape. Hence, this product can be though as a single order-k stack, and therefore the resulting strategy in G is realised by an order-(k+1) automaton. Finally, the fact that this latter automaton always has the same shape as the current configuration in the game, easily follows by construction (and induction).

H Proof of Theorem 6

Theorem 6. The µ-calculus definable sets over transition graphs of higher-order pushdown automata are regular sets of configurations. Proof (sketch). Given some µ-calculus formula ϕ a classical construction [START_REF] Emerson | Tree automata, mucalculus and determinacy (extended abstract)[END_REF] leads a finite game graph G ϕ whose vertices are all possible subformulas of ϕ together with a colouring function ρ. Then for any structure K and any vertex v in K, the following holds: K, v |= ϕ iff Éloïse wins from (v, ϕ) in the parity game induced by K × G ϕ . The underlying graph of this game is the cartesian product of K and G ϕ , the partition of its vertices as well as the associated colouring function being inherited from the ones for G ϕ . Then, it follows that ||K|| ϕ = {v | (v, ϕ) ∈ W E } where W E denotes the winning region for Éloïse in the previous game.

The previous construction does not rely on K being finite and can be used for instance to solve the µ-calculus modelchecking problem against pushdown processes [START_REF] Walukiewicz | Pushdown processes: games and model checking[END_REF]. In the case where K is the transition graph of some higher-order pushdown process, the game graph K×G ϕ is also the transition graph of some higher-order pushdown process and the partition of its vertices as well as its associated colouring function only depend on the control states. Hence, the solution of the global µ-calculus model-checking problem for such a graph can be deduced from the (regular) winning region of a higher-order parity pushdown game by a simple operation that preserves regularity. Hence µ-calculus definable sets are regular.

Proposition 2 .

 2 Fix an order-(k + 1) pushdown automaton P and consider an automaton A with oracles O 1 , . . . , O n respectively accepted by deterministic word automata A 1 , . . . , A n . Let C be the set of configurations of P accepted by A. Then we can construct a deterministic finite automaton, of size O(|A||A 1 | • • • |A n |), accepting the set C.

Figure 2 .

 2 Figure 2. Updating the strategy's stack Π

Theorem 2 .

 2 The following holds. 1. A configuration (p in , ⊥) is winning for Éloïse in G if and only if (p in , ⊥, (∅, . . . , ∅), ρ(p in )) is winning for Éloïse in G.

  1. A configuration (p in , ⊥) is winning for Éloïse in G if and only if (p in , ⊥, (∅, . . . , ∅), ρ(p in )) is winning for Éloïse in G.

Appendix

A Proof of Proposition 1

Proposition 1. Take an (resp. deterministic) order-k pushdown automaton. The set of words traced out by configuration sequences from the initial configuration c 0 to a configuration c, where c ranges over a regular set of configurations, is accepted by an (resp. deterministic) order-k pushdown automaton.

Proof. Let P = (Q, Σ, ∆ P ) be an order-(k + 1) pushdown automaton. Let Γ be the set of all order-k stacks over Σ.

Let A = (Q A , δ A , q A 0 , F A ) be a deterministic automaton over the alphabet Σ ∪ Q ∪ {[, ]} accepting words of the form wq with w a well-bracketed word of depth k + 1 over Σ ∪ {[, ]} and q ∈ Q.

Let Θ be the set of partial functions from Q A to Q A . Moreover with every word w ∈ Σ ∪ {[, ]}, we associate the partial function θ w ∈ Θ defined by θ w (q) = δ A (q, w) for q ∈ Q A .

For an order-k stack s = (s 1 , . . . , s |s| ), we take for all i ∈ [1, |s|], θ s i ∈ Θ to be θ s1••• si . With every order-k stack s over Σ we associate an orderk stack [[s]] over Σ ∪ Θ as follows.

For an order-1 stack s = (γ 1 , . . . , γ ), we take

where s i is obtained by pushing the symbol θ s i on top of

The idea of the construction is to simulate a configuration (q, s) of the original automaton by the configuration ((q, γ, θ 1 , . . . , θ k ), [[s]]) where γ is the top-most symbol of s and where for all i ∈ [1, k], θ i = θ ti |ti|-1 where t i is the top-most order-i stack of s.

It is easy to check that a transition of the original automaton can be similuated in a deterministic fashion by a finite sequence of operations. To process sequences of operations, we naturally introduce intermediate states and label the corresponding transition by the silent symbol ε.

Finally a state (q, γ, θ 1 , . . . , θ k ) is final if Proof. Let P = (Q, Σ, ∆ P ) be an order-(k + 1) pushdown automaton and let Γ be the set of all order-k stacks over Σ.

B Proof of Proposition 2

For the direct implication, consider an automaton with oracles A = (S, Q, Γ, δ, s in , O 1 , . . . , O n , Acc). For i ∈ [1, n], we assumme that O i \ {⊥} is accepted by the deterministic finite automaton

We construct a determistic finite automaton

} such that for every order-(k + 1) stack (γ 1 , . . . , γ ) and every state q ∈ Q, ((⊥, γ 1 , . . . , γ ), q) is accepted by A if and only if the word

The set of states

Intuitvely, B is a synchronized product of A together with the automata A 1 , . . . , A n . An extra componant is needed to keep track of the bracketing depth. The transition function is defined by: δ B (q B 0 , [) = (δ A (s in , π(⊥)), q 1 0 , . . . , q n 0 , 1) δ B ((s, q 1 , . . . , q n , ), σ) = (s, δ 1 (q 1 , σ), . . . , δ n (q n , σ), ) δ B ((s, q 1 , . . . , q n , ), [) = (s, δ 1 (q 1 , [), . . . , δ n (q n , [), + 1) δ B ((s, q 1 , . . . , q n , ), ]) = (s, δ 1 (q 1 , ]), . . . , δ n (q n , ]), -1) δ B ((s, q 1 , . . . , q n , 2), ]) = (δ(s, π ), q 0 1 , . . . , q 0 n , 1) δ B ((s, q 1 , . . . , q n , 1), ]) = (s, q 0 1 , . . . , q 0 n , 0) δ B ((s, q 1 , . . . , q n , 0), q) = q f for q ∈ Acc(s)

and b i = 0 otherwise and similarly π is the boolean vector (b 1 , . . . , b n ) where for i ∈ [1, n], b i is equal to 1 if δ(q i , ]) ∈ F i and 0 otherwise.

Conversely, let A = (Q A , δ A , q A 0 , F A ) be a deterministic automaton over the alphabet Σ ∪ Q ∪ {[, ]} accepting words of the form wq with w being a well-bracketed word of depth k + 1 over Σ ∪ {[, ]} and q ∈ Q. We can assume without lost of generality that the set of states of A is of the form Q A × [0, k + 1] and that for all w ∈ (Σ ∪ {[, ]}) * , if δ A (q A 0 , w) = (q, ) then w] is a well-bracketed word of depth k + 1.

For each pair (p, q) of states in Q A , we define the language O p,q := {w | δ((p, 1), w) = (q, 1)} which is a regular set of well-bracketed words of depth k.

We can now define an automaton B with oracles accepting the configurations of P corresponding to words accepted by A. Assume that Q A is equal to {q 1 , . . . , q m }. We pick a bijection ρ from

The automaton B is formally defined as (Q B , Q, Γ, δ B , q B 0 , O 0 , . . . , O m 2 , Acc). We take Q B := Q A , Γ is the set of all level k stacks over Σ, q B 0 is such that q A 0 = (q B 0 , 0), O 0 = {⊥} and for all (i, j) ∈ [1, m] 2 , O ρ(i,j) = O qi,qj .

The transition function of δ B is defined for all boolean vector π = (b 0 , . . . , b m 2 ) by: