Didier Caucal
email: caucal@irisa.fr

SYNCHRONIZATION OF PUSHDOWN AUTOMATA

We introduce the synchronization of a pushdown automaton by a sequential transducer associating an integer to each input word. The visibly pushdown automata are the automata synchronized by an one state transducer whose output labels are -1, 0, 1. For each transducer, we can decide whether a pushdown automaton is synchronized. The pushdown automata synchronized by a given transducer accept languages which form an effective boolean algebra containing the regular languages and included in the deterministic real-time context-free languages.

Introduction

It is well-known that the context-free languages are not closed under intersection and complementation, and that the deterministic context-free languages are not closed under intersection and union. Alur and Madhusudan have shown that the languages accepted by the visibly pushdown automata form a boolean algebra included in the deterministic real-time context-free languages [AM 04]. The notion of visibly pushdown automaton is based on the synchronization between the input symbols and the actions performed on the stack: this enforces that the variation of the stack height is entirely characterized by the input word. It appears that the closure results for the languages accepted by the visibly pushdown automata are based on a geometrical property of their graphs with regard to the stack height. This geometrical property which holds for every pushdown graph (not only visibly) was discovered by Muller and Schupp [MS 85]. A simple adaptation of their result shows that the graph of every pushdown automaton is regularly generated by increasing stack height [Ca 95]. This regularity is described by a finite deterministic graph grammar which in n steps of parallel rewritings, generates the graph restricted to the configurations with stack height at most n. In this article, we generalize the notion of synchronization to abstract from the stack height. Towards this goal, we introduce a sequential transducer associating an integer to each input word. Provided that this transducer defines a weight for the vertices of the pushdown graph, we show that we can decide whether the graph can be generated regularly with regard to that weight. This is the notion of synchronization by a transducer. For any fixed transducer, the languages accepted by the pushdown automata synchronized by this transducer, are deterministic real-time context-free languages and form an effective boolean algebra containing the regular languages.

Graphs and finite automata

By allowing labels not only on arcs but also on vertices, we define graphs as a simple extension of automata: the vertex labelling is not restricted to indicate initial and final vertices but it also permits to add information on vertices (e.g. the vertices accessible from a given colour, more generally the vertices defined by a µ-formula, . . .). First we give some notations. Let IN be the set of non-negative integers and Z Z be the set of integers. For any set E, we denote |E| its cardinality. For every n ≥ 0, E n is the set of n tuples of elements of E, and E * = n≥0 E n is the free monoid generated by E for the concatenation : (e 1 , . . ., e n )•(e ′ 1 , . . ., e ′ n ) = (e 1 , . . ., e n , e ′ 1 , . . ., e ′ n ). A finite set E of symbols is an alphabet of letters, and E * is the set of words over E. Any word u ∈ E n is of length |u| = n and is represented by the juxtaposition of its letters: u = u(1). . .u(|u|). The word of length 0 is the empty word ε. We denote Now we present our notion of graph which generalizes the notion of automaton. Let L and C be disjoint countable sets of symbols for respectively labelling arcs and labelling vertices. Here a graph is simple, oriented, arc labelled in a finite subset of L and vertex labelled in a finite subset of C. Precisely, a graph G is a subset of V ×L×V ∪ C×V where V is an arbitrary set such that its vertex set

|u| P := |{ 1 ≤ i ≤ |u| | u(i) ∈ P }| the number of occurrences of P ⊆ E in u ∈ E * .
V G := { p | ∃ a, q, (p, a, q) ∈ G ∨ (q, a, p) ∈ G } ∪ { p | ∃ c, (c, p) ∈ G } is finite or countable, with its vertex label set or colour set C G := { c ∈ C | ∃ p, (c, p) ∈ G } is finite, and its arc label set or label set L G := { a ∈ L | ∃ p, q, (p, a, q) ∈ G } is finite. Any (p, a, q) of
G is a labelled arc of source p, of goal q, with label a, and is identified with the labelled transition p

a -→ G q or directly p a -→ q if G is under- stood. Any (c, p) of G is a vertex p labelled by c and is also written c p if G is understood. We denote V G,i := { p | i p ∈ G } the set of vertices of G labelled by the colour i ∈ C.
A graph is deterministic if distinct arcs with the same source have distinct labels:

r a -→ p ∧ r a -→ q =⇒ p = q . Note that a graph G is finite if and only if it has a finite vertex set V G . For instance {r b -→ p , p a -→ s , p b -→ q , q a -→ p , q b
-→ s , i r , g p , h p , f s , f t} is a finite graph of vertices p, q, r, s, t, of colours i, f, g, h, and of (arc) labels a, b. It is represented below.

G := sup{ d(p) | p ∈ V G } is the degree of G. A graph
G |P := { p a -→ G q | p, q ∈ P } ∪ { c p ∈ G | p ∈ P }.
Any tuple (p 0 , a 1 , p 1 , . . ., a n , p n ) such that n ≥ 0 and p 0 a1 -→ p 1 . . . p n-1 an -→ p n , denoted also by the word p 0 a 1 p 1 . . .a n p n (which have a sense if V G ∩ L * G = ∅), is a path from p 0 to p n labelled by u = a 1 . . .a n , and we write p

0 u =⇒ G p n or directly p 0 u =⇒ p n if G is understood; for n = 0, the path p 0 ε =⇒ G p 0 is reduced to p 0 ∈ V G . For any U ⊆ L * , we write p U =⇒ q if p u =⇒ q for some u ∈ U . We also write p =⇒ G * q if p L * =⇒ G q.
We say that a vertex r is a root of G if every vertex p is accessible from r : r =⇒ * p. The accessible subgraph G /p := G |{ q | p =⇒ * q } of a graph G from a vertex p is the restriction of G to the vertices accessible from p. Given a graph G and vertex sets P, Q ⊆ V G , we denote L(G, P, Q) the language of path labels from vertices in P to vertices in Q :

L(G, P, Q) := { u | ∃ p ∈ P ∃ q ∈ Q p u =⇒ G q } . Given colours i, f ∈ C, we define L(G, i, f ) := L(G, V G,i , V G,f
) the path labels from the set V G,i of vertices labelled by i to the set V G,f of vertices labelled by f . For instance taking the previous graph, its path labels from i to f is b(ba) * (a+bb). So a finite graph G with two colours i and f is a finite automaton recognizing the language L(G, i, f ). The family

Rat(T * ) := { L(G, i, f ) | |G| < ω ∧ i, f ∈ C } of
languages over T recognized by the finite automata coincides with the family of rational languages (or regular languages). So the finite graphs describe the structures of the rational languages and permit to derive properties on these languages. For the context-free languages which are the languages recognized by the pushdown automata, their graphs are generated by the deterministic graph grammars which are also really powerful to get properties on these languages. Our purpose is to use the deterministic graph grammars in order to describe geometrically the notion of visibly pushdown automata and to get in this way a natural generalization.

Graph grammars and pushdown automata

A pushdown automaton is a particular case of a word rewriting system where the rules are only applied by prefix. By restriction to rational vertex sets, the pushdown automata and the word rewriting systems define the same (prefix) graphs which are the graphs of bounded degree and regular in the sense that they can be generated by a deterministic grammar [Ca 90]. We extend this result to the pushdown automata which are in a weak form used by the visibly pushdown automata (cf. Theorem 3.1). We recall that the graphs of the pushdown automata are regular by increasing length (cf. Proposition 3.2).

We fix an alphabet T of terminals. Recall that a labelled word rewriting system R is a finite subset of N * ×T ×N * for some alphabet N of non-terminals i.e. is a finite uncoloured graph of (arc) labels in T and whose vertices are words over N . The graph:

G•P := { uw a -→ vw | u a -→ G v ∧ w ∈ P } is the right concatenation of any graph G ⊆ N * ×T
×N * by any language P ⊆ N * . Rewritings of a system are generally defined as applications of rewriting rules in every context. On the contrary, we are here concerned with prefix rewriting [Bü 64]. The prefix transition graph of R is the uncoloured graph R•N * which is of bounded degree and has a finite number of non isomorphic connected components. A subclass of labelled word rewriting systems is the standard model of real-time pushdown automata. A pushdown automaton R (without ε-rule) is a finite set of rules of the form: pA a -→ qU with p, q ∈ Q, A ∈ P, U ∈ P * , a ∈ T where P and Q are disjoint alphabets of respectively pushdown letters and states.

The transition graph of R is R•P * = { pAV a -→ qU V | pA a -→ R qU ∧ V ∈ P * } the restriction of the prefix transition graph R•(P ∪ Q) * of R to the rational set QP * of configurations.
A strong way to normalize the rules of pushdown automata is given by a weak pushdown automaton R which is a finite set of rules of the following form: p a -→ q or p a -→ qA or pA a -→ q with p, q ∈ Q, A ∈ P, a ∈ T . Its transition graph R•P * is isomorphic to S•P * ⊥ where ⊥ is a new pushdown letter (the bottom of the stack) and S is the following pushdown automaton:

S = { pA a -→ qA | p a -→ R q ∧ A ∈ P ∪ {⊥} } ∪ { pB a -→ qAB | p a -→ R qA ∧ B ∈ P ∪ {⊥} } ∪ { pA a -→ q | pA a -→ R q }.
The labelled word rewriting systems and the weak pushdown automata define the same prefix transition graphs, hence also for the pushdown automata which are intermediate devices.

Theorem 3.1 The transition graphs of weak pushdown automata, the transition graphs of pushdown automata, the prefix transition graphs of labelled word rewriting systems, have up to isomorphism the same accessible subgraphs: the rooted regular graphs of bounded degree, connected components: the connected regular graphs of bounded degree, rational restrictions: the regular graphs of bounded degree.

F n := { f ∈ F | ̺(f ) = n } is countable for every n ≥ 0, with F 1 = C and F 2 = L. A hypergraph G is a subset of n≥0 F n V n where V is an arbitrary set such that its vertex set V G := { p ∈ V | F V * pV * ∩ G = ∅ } is finite or countable, its label set F G := { f ∈ F | f V * ∩ G = ∅ } is finite. Any f v 1 . . .v ̺(f ) ∈ G is
a hyperarc labelled by f and of successive vertices v 1 , . . ., v ̺(f ) ; it is depicted for ̺(f ) ≥ 2 as an arrow labelled f and successively linking v 1 , . . ., v ̺(f ) :

f (v 1 ) (v 2 ) (v ̺(f ) )
The transformation of a hypergraph G by a function h from V G into any set

V is the graph h(G) := { f h(v 1 ). . .h(v ̺(f ) ) | f v 1 . . .v ̺(f ) ∈ G }.
Note that the graphs are the hypergraphs whose any label is of arity 1 or 2 : any arc p a -→ q corresponds to the hyperarc apq. A graph grammar R is a finite set of rules of the form f x 1 . . .x ̺(f ) -→ H where f x 1 . . .x ̺(f ) is a hyperarc joining pairwise distinct vertices x 1 = . . . = x ̺(f ) and H is a finite hypergraph. The labels of the left hand sides form the set N R of non-terminals of R :

N R := { X(1) | X ∈ Dom(R) }, and the labels of R which are not non-terminals form the set T R of terminals :

T

R := { X(1) ∈ N R | ∃ P ∈ Im(R), X ∈ P }.
Any graph grammar R is used to generate graphs of arc labels in T hence we assume that T R ⊂ T ∪ C. We will use capital letters for the non-terminals and small letters for the terminals. Starting from any non-terminal hyperarc, we want to generate by a graph grammar a unique graph up to isomorphism. So we restrict any graph grammar to be deterministic : there is only one rule per non-terminal. For instance taking A ∈ F 0 , B ∈ F 3 , a, b, c ∈ T and i, f ∈ C, the following two rules:

A -→ {ip , f r , Bpqr} ; Bxyz -→ {axp , bxy , cqy , byz , crz , Bpqr} constitute a deterministic graph grammar which is represented below:

; a c c i f A B B B b b (x) (x) (y) (y) (z) (z)
For any (deterministic graph) grammar R, the rewriting -→ R is the binary relation between hypergraphs defined by M -→ R N if we can choose a non-terminal hyperarc X = As 1 . . .s p in M and a rule Ax 1 . . .x p -→ H in R to replace X by H in M : N = (M -X) + h(H) for some function h mapping x i to s i , and the other vertices of H injectively to vertices outside of M ; this rewriting is denoted by

M -→ R, X N . The rewriting -→ R, X
of a hyperarc X is extended in an obvious way to the rewriting -→ R, E of any set E of non-terminal hyperarcs. A complete parallel rewriting =⇒ R is the rewriting according to the set of all non-terminal hyperarcs:

M =⇒ R N if M -→ R, E
N where E is the set of all non-terminal hyperarcs of M . For instance, the first three steps of the parallel derivation from the hypergraph {A} according to the above grammar are depicted in the figure below. A regular graph, also called a hyperedge replacement equational graph [Co 90], is a graph G generated by a hypergraph grammar R from a non-terminal hyperarc X. More formally, G is isomorphic to a graph in the following set R ω (X) of isomorphic graphs:

=⇒ =⇒ =⇒

R ω (X) := { n≥0 [H n ] | H 0 = X ∧ ∀ n ≥ 0, H n =⇒ R H n+1 } .
For instance by continuing infinitely the previous derivation, we get the infinite graph: In particular any regular graph of finite degree is of bounded degree. The regular graphs trace the context-free languages: for any regular graph G (not necessarily bounded) and for any colours i, f ∈ C, L(G, i, f ) is a contextfree language and by Theorem 3.1, the converse is true. Graph grammars are suitable to deduce the pumping lemma, or to prove the Parikh lemma. Here we will use graph grammars to describe geometrically the notion of visibly pushdown automaton and to extend it.

A regular graph can be generated by several grammars. For instance instead of generating the previous graph by 'vertical slides', we can generate it by 'diagonal slides' using the following grammar:

; ; A C b a b c f B b i a B a c c C b b C (x) (x) (x) (x) (z) (z) (y) (y) (y) (y)
We specify the regularity of a graph G according to a mapping g from V G into IN. Precisely for every n ≥ 0, we define the graph G g,n of the first n levels of G according to g by

G g,n := { p a -→ G q | g(p) < n ∨ g(q) < n } ∪ { c p ∈ G | g(p) < n } .
We say that a graph G is regular by g if there exists a grammar R and a nonterminal hyperarc I such that for any parallel derivation

I =⇒ R n H, the set of terminal arcs of H is [H] = G g,n and its vertex set of its non-terminal hyperarcs is V H-[H] which is included in { p ∈ V G | g(p) = n } ∪ { p ∈ V G | g(p) > n ∧ ∃ q (p -q ∧ g(q) < n) }
with the notation pq for ∃ a, p a -→ q ∨ q a -→ p. So any graph regular by some mapping is of bounded degree. We consider the regularity of the transition graph R•P * of any pushdown automaton R according to the stack height |U | of any configuration pU where p ∈ Q is a state and U ∈ P * is a pushdown word. When R is weak then R•P * is regular by stack height with the grammar reduced to this unique rule: Zq 1 . . .q n -→ R ∪ { Z(q 1 A). . .(q n A) | A ∈ P } for {q 1 , . . . , q n } = Q. By synchronisation product of this rule with any finite automaton, we deduce that any rational restriction of the transition graph of any weak pushdown automaton is regular by stack height (or by length). This result is extended to any pushdown automaton. Proposition 3.2 The rational restrictions of the prefix transition graphs of labelled word rewriting systems are regular by length.

This proposition has been established for any morphism [Ca 95].

We can now present a geometrical description of the visibly pushdown automata, and its extension by synchronization with a sequential transducer with integer output.

We present the visibly pushdown automata defined in [AM 04] with the main result (cf. Theorem 4.1), and we consider the regularity of their transition graphs by stack height.

The visibly pushdown automata are given according to a splitting of the alphabet T of terminals into three disjoint alphabets T -1 , T 0 , T 1 to indicate respectively the letters allowed to pop the topmost stack symbol, to unchange the stack, and to push a symbol on the stack. A visibly pushdown automaton R is a finite set of rules of the following form:

pA a -→ q or p b -→ q or p c -→ qA or p⊥ a -→ q⊥ with p, q ∈ Q, A ∈ P, a ∈ T -1 , b ∈ T 0 , c ∈ T 1
, where P, Q, {⊥} are disjoint alphabets of respectively pushdown letters, of states and of the bottom of the stack. The transition graph of R is R•P * ⊥ and the language L(R•P * ⊥ , I⊥ , F P * ⊥) recognized from a set I ⊆ Q of initial states to a set F ⊆ Q of final states is a visibly pushdown language. For instance taking a ∈ T 1 , c ∈ T 0 , b ∈ T -1 , the language { a n cb n | n ≥ 0 } is a visibly pushdown language and the Lukasiewicz language i.e. the language L(G, A) generated by the context-free grammar G = {A -→ aAA , A -→ b}, is also a visibly pushdown language. But the language { a n ba n | n ≥ 0 } and the language L(G, A) generated by the grammar G = {A -→ aAAA , A -→ b} are not visibly pushdown languages for any partition of T in T -1 , T 0 and T 1 . So the visibly pushdown languages are not preserved in general by morphism and inverse morphism. Any rational language over T is a visibly pushdown language according to any partition T = T -1 ∪ T 0 ∪ T 1 : for any finite T -graph H and any I, F ⊆ V H , the rational language L(H, I, F ) = L(R•P * ⊥ , I⊥ , F P * ⊥) for P = {A} reduced to a unique pushdown letter A and for the following visibly pushdown automaton:

R = { p a -→ qA | p a -→ H q ∧ a ∈ T 1 } ∪ { p a -→ q | p a -→ H q ∧ a ∈ T 0 } ∪ { pA a -→ q | p a -→ H q ∧ a ∈ T -1 } ∪ { p⊥ a -→ q⊥ | p a -→ H q ∧ a ∈ T -1 }.
The family of visibly pushdown languages is an extension of the regular languages with same basic closure properties.

Theorem 4.1 [AM 04] For any partition of the input letters, the class of visibly pushdown languages is a subfamily of deterministic real-time contextfree languages, and is an effective boolean algebra closed by concatenation and its transitive closure.

In particular the universality problem and the inclusion problem are decidable for the visibly pushdown languages. For any visibly pushdown automaton R and by discarding the rules p⊥

a -→ q⊥ (for a ∈ T -1 ), note that pU u =⇒ R•P * qV =⇒ |V | -|U | = |u| T 1 -|u| T -1
which implies the following first key point:

|u| T 1 -|u| T -1 = |v| T 1 -|v| T -1 = |U | for any u, v ∈ L(R•P * , I, pU ).
A second key point is given by Proposition 3.2 : any rational restriction of R•P * can be generated by a graph grammar S by stack height. We will see that these two key points are sufficient to establish Theorem 4.1 (without the closure by concatenation and its transitive closure). These two key points indicate that the weak form of a visibly pushdown automaton is inessential. We need that the transition graph G restricted to the configurations accessible from a given set I, satisfies the property that for every vertex s, any label u of a path from I to s has the same value |u| T 1 -|u| T -1 (first key point) called the weight of s, and that G is regular by weight (second key point). Note that the weight of a vertex can be negative which allows to discard the rules of the form p⊥ a -→ q⊥ . Finally we will generalize the visibility defined by the partition T = T -1 ∪ T 0 ∪ T 1 to any sequential transducer from T * into Z Z.

Synchronized pushdown automata

The synchronization of pushdown automata over T is done according to a sequential transducer A from T * into Z Z. The synchronization by A is defined for the regular graphs of bounded degree which are by Theorem 3.1 the rational restrictions of the transition graphs of pushdown automata. It is decidable whether a regular graph is synchronized by A (cf. Proposition 5.4), and the traces of the graphs synchronized by A form an effective boolean algebra of deterministic realtime context-free languages containing the rational languages (cf. Theorem 5.8).

We fix a colour i ∈ C to indicate initial vertices. A sequential transducer (or generalized sequential machine) from the free monoid T * into the additive monoid Z Z is a finite graph A of label set L A ⊂ T ×Z Z and of colour set C A = {i} such that A is input deterministic:

p (a,x) -→ A q ∧ p (a,y) -→ A r =⇒ x = y ∧ q = r i p , i q ∈ A =⇒ p = q
(a unique state is coloured by i). A (sequential) transducer A realizes the transduction

L(A, i, V A ) = { (u, m) | ∃ s, t, i s ∈ A ∧ s (u,m) =⇒ A t }
of the label set of the paths from the vertex coloured by i to any vertex, for the operation (u, m).(v, n) := (uv, m + n) for every u, v ∈ T * and m, n ∈ Z Z.

For instance taking a unique state r, the transducer {i r , r For any (sequential) transducer A, we denote L(A):=Dom(L(A, i, V A )) its first projection, and we say that A is complete if L(A) = T * . For any word u ∈ L(A), there is a unique integer u A called the weight of u in A such that (u, u A ) ∈ L(A, i, V A ). A transducer A is visible if it has a unique state, is complete and the value of any arc can be only -1, 0, 1 :

|V A | = 1 , L A ⊆ T ×{-1, 0, 1} and Dom(L A ) = T ; in that case for any i ∈ {-1, 0, 1}, T i = { a | (a, i) ∈ L A }.
We say that a graph G is compatible with a transducer A if for any vertex s of G, there is a path from (a vertex coloured by) i to s and the labels of the paths from i to s are in L(A) and have the same weight:

∅ = L(G, i, s) ⊆ L(A) ∧ u, v ∈ L(G, i, s) =⇒ u A = v A ;
in that case we denote s A := u A for any u ∈ L(G, i, s). In the next figure,

G A := { s (a,x) -→ t | s a -→ G t ∧ ∃ p, q, p (a,x) -→ A q ∧ i Dom(L(A,i,p)) =⇒ G s } ∪ G ∩ CV G
is a regular graph, and we can decide whether G is compatible with A.

Here are represented by increasing weight two regular graphs of finite degree which are compatible with the previous visible transducer. give by intersection the language { a n b n a n | n ≥ 0 } which is not context-free, hence is not the language between colours of a regular graph. We now discard the graph H because we cannot generate it by increasing weight: we would need non-terminal hyperarcs having an infinite number of vertices. We say that a graph is synchronized by a transducer A if it is compatible with A and regular by the absolute value of the weight A . The graph above Lemma 5.1 is generated by increasing weight with the following grammar:

; ; ; A f i B B a b C a b D C a b C D a b D (x) (x) (x) (x) (x) (x)
Let us give a graph synchronized by A with the same path labels.

Lemma 5.2 For any transducer A, the following graph:

-→ A := { (p, n) a -→ (q, n + x) | p (a,x) -→ A q ∧ n ∈ Z Z } ∪ { i (p, 0) | i p ∈ A } is synchronized by A and L(G, i, V G ) = L(A).
Let us give a simple characterization of the regular graphs which are synchronized. We say that any graph G compatible with a transducer A is finitely compatible with A if for every integer n ∈ Z Z, the vertex set { s ∈ V G | s A = n } is finite. By definition, any synchronized graph by A is regular and finitely compatible with A ; the converse is true.

Proposition 5.3 For any transducer A, G is synchronized by A ⇐⇒ G is regular and finitely compatible with A.

This permits to extend the decidability of Lemma 5.1 to the synchronization problem.

Proposition 5.4 For any transducer A, we can decide whether a regular graph G is synchronized by A, and in the affirmative, we can construct a graph grammar generating G by increasing weight A .

In particular we can decide whether a regular graph is visibly synchronized (we have only a finite number of visible transducers). We fix another colour -→ q , q (a,-1) -→ q , q (b,-1) -→ q }. Such a language cannot be synchronized by an one state transducer: we need several integers for the labels a and b (here 1 and -1).

  For any binary relation R ⊆ E×F from E into a set F , we write also e R f for (e, f ) ∈ R, and we denote Dom(R) := { e | ∃ f, e R f } the domain of R, and Im(R) := { f | ∃ e, e R f } the image (or the range) of R.

  Note that a vertex r is depicted by a dot named by (r) where parentheses are used to differentiate a vertex name with a vertex label (a colour). For any p ∈ V G , d + (p) := |{ (a, q) | p a -→ q }| and d -(p) := |{ (q, a) | q a -→ p }| are respectively the out-degree and the in-degree of p ; d(p) := d + (p) + d -(p) is the degree of p and d

  ] := H ∩ (CV H ∪ T V H V H ) be the set of terminal arcs and of coloured vertices of any hypergraph H.

  represented in the next figure, realizes { (u , |u| a -|u| b ) | u ∈ {a, b} * }.

  we have a graph G compatible with a visible transducer for T = {a, b} ; note that L(G, i, f) = { u ∈ T * | |u| a = |u| b } is not a visibly pushdown language.For G compatible with A and H ⊆ G, H is compatible with A. Let us give another fact.Lemma 5.1 For any regular graph G and any transducer A,

  Their languages L(G, i, f ) = { a n b n | n ≥ 0 }a * and L(H, i, f ) = a * { b n a n | n ≥ 0 }

  f ∈ C to indicate final vertices. The visibly pushdown languages are extended to any transducer A : a synchronized language by A is L(G, i, f ) for some graph G synchronized by A. Let us give basic examples of synchronized languages. Example 5.5 The languages synchronized by a transducer A such that L A ⊆ T ×{0} are all the rational languages included in L(A). Example 5.6 Taking m ≥ 0, the language L m := L(G, X) generated by the context-free grammar G = {X -→ aX m , X -→ b} is synchronized by the transducer A = { i p , p (a,m-1) -→ p , p (b,-1) -→ p }. This transducer has a unique state, and it is visible for m = 0 (L 0 = {a, b}), for m = 1 (L 1 = a * b) and for m = 2 (L 2 is the Lukasiewicz language). For m > 2, L m is not a visibly pushdown language. The language { u ∈ {a, b} * | |u| b = (m -1)|u| a } is also synchronized by A. More generally for m, n ≥ 0, L m,n := { u ∈ {a, b} * | m |u| a = n |u| b } is a language synchronized by { i p , p (a,m) -→ p , p (b,-n) -→ p }. For m, n > 0, L m,n is not a visibly pushdown language in the sense of [AM 04]. Example 5.7 The linear language { uc u | u ∈ {a, b} * } for u the mirror of u, is synchronized by { i p , p

  is of finite degree (or locally finite) if d(p) < ω for any vertex p ; a graph G is of bounded degree (or locally bounded) if d G < ω . A graph G without vertex label i.e. C G = ∅ is called an uncoloured graph. The restriction (or the induced subgraph) of a graph G to a vertex subset P is

  This theorem has been first established in [Ca 90] and completed in [Ca 95] but without considering the weak pushdown automata. It remains to recall what is a regular graph and more exactly to reintroduce the notion of a deterministic graph grammar to generate a graph. Such a generation needs to use non-terminal arcs linking several vertices and called hyperarcs.

Let F be a set of symbols called functions, graded by a mapping ̺ : F -→ IN associating to each function f its arity ̺(f ), and such that

We establish effective closure properties of the synchronized languages by A as for the rational languages: we apply the classical constructions on finite automata to the graph grammars generating by A . By synchronization product of -→ A by any finite automaton, we deduce that any rational language included in L(A) is synchronized by A. By disjoint union of two graph grammars generating by A , we deduce that the union of two synchronized languages by A remains synchronized. By synchronization product of two graph grammars generating by

A , we obtain that the intersection of two synchronized languages by A remains synchronized. Finally by a determinization of any graph grammar generating by A , we show that any synchronized language is deterministic context-free, and its complement with respect to L(A) remains synchronized.

Theorem 5.8 For any transducer A, the class of synchronized languages contains all the rational languages in L(A), is a subfamily of deterministic real-time context-free languages, and is an effective boolean algebra with respect to L(A).

This generalization of the visibly pushdown automata has permitted to work with unrestricted pushdown automata (the synchronization is independent of the length of the words in the rules), and by allowing any integer and several states (instead of -1, 0, 1 and a unique state). This paper also indicates that the deterministic graph grammars can be a powerful tool to investigate properties of context-free languages. Thanks to Christof Löding for a survey on the visibly pushdown automata which has been at the origin of this paper. The first half part of this paper has been done during a stay in Udine; many thanks to Angelo Montanari for his invitation. The second half part of this paper has been done during a stay in Aachen; many thanks to Wolfgang Thomas for his support. Thanks to Arnaud Carayol for his help in the drafting of this paper.


Arnaud Carayol

Christof Löding

MSO on the Infinite Binary Tree: Choice and Order

We give a new proof showing that it is not possible to define in monadic second-order logic (MSO) a choice function on the infinite binary tree. This result was first obtained by Gurevich and Shelah using set theoretical arguments. Our proof is much simpler and only uses basic tools from automata theory. We discuss some applications of the result concerning unambiguous tree automata and definability of winning strategies in infinite games. In a second part we strengthen the result of the non-existence of an MSO-definable well-founded order on the infinite binary tree by showing that every infinite binary tree with a well-founded order has an undecidable MSO-theory.

Introduction

Our main purpose is to present a simple proof for the fact (first shown by Gurevich and Shelah in [START_REF] Gurevich | Rabin's uniformization problem[END_REF]) that on the infinite binary tree there is no choice function that can be defined in monadic second-order logic (MSO), i.e., in the extension of first-order logic by quantification over sets of elements. A choice function on the infinite binary tree is a mapping assigning to each nonempty set of nodes one element from this set, i.e., the function chooses for each set one of its elements. Such a function is MSO-definable if there is an MSO-formula with one free set variable X and one free element variable x such that for each nonempty set U of nodes there is exactly one element u ∈ U such that the formula is satisfied if X is interpreted as U and x is interpreted as u.

The question of the existence of an MSO-definable choice function over the infinite binary tree can be seen as a special instance of the more general uniformization problem, which asks, given a relation that is defined by a formula with free variables, whether it is possible to define by another formula a function that is compatible with this relation. More precisely, given a formula φ( X, Ȳ ) with vectors Ȳ , X of free variables, such that ∀ X∃ Ȳ φ( X, Ȳ ) is satisfiable, uniformization asks for a formula φ * ( X, Ȳ ) such that 1. φ * implies φ (each interpretation of Ȳ , X making φ * true also makes φ true), 2. and φ * defines a function in the sense that for each interpretation of X there is exactly one interpretation of Ȳ making φ * true.

The question of the existence of a choice function is the uniformization problem for the formula φ(X, y) = X = ∅ → y ∈ X.

The infinite line, i.e., the structure (ω, succ) of the naturals with the successor function is known to have the uniformization property for MSO [START_REF] Siefkes | The recursive sets in certain monadic second order fragments of arithmetic[END_REF]. On the infinite binary tree MSO is known to be decidable [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF] but it does not have the uniformization property. This was conjectured in [START_REF] Siefkes | The recursive sets in certain monadic second order fragments of arithmetic[END_REF] and proved in [START_REF] Gurevich | Rabin's uniformization problem[END_REF] where it is shown that there is no MSO-definable choice function on the infinite binary tree.

The reason for the present paper is that the proof in [START_REF] Gurevich | Rabin's uniformization problem[END_REF] uses complex set theoretical arguments, whereas it appears that the result can be obtained by much more basic techniques. We show that this is indeed true and present a proof that only relies on the equivalence of MSO and automata over infinite trees and otherwise only uses basic techniques from automata theory. Besides its simplicity, another advantage of the proof is that we provide a concrete family of sets (parameterized by natural numbers) such that each formula will fail to make a choice for those sets with the parameters chosen big enough. We use this fact when we discuss two applications of the result concerning unambiguous tree automata (as presented in [NW]) and the definability of strategies in infinite games.

The subject of MSO-definability of choice functions on trees has been studied in more depth in [START_REF] Lifsches | Uniformization, choice functions and well orders in the class of trees[END_REF], where the authors consider more general trees not only the infinite binary tree. They show the following dichotomy: for a tree it is either not possible to define a choice function in MSO, or it is possible to define a well-ordering on the domain of the tree.

We strengthen this result by showing that extending the infinite binary tree by any well-ordering leads to a structure with undecidable MSO-theory. As a consequence we obtain that each structure in which we can MSO-define a wellordering and MSO-interpret the infinite binary tree must have an undecidable MSO-theory.

The article is structured as follows. In the next section we introduce some notations and basic terminology. In Section 3 we give the proof that there is no MSO-definable choice function on the infinite binary tree and discuss applications of the result. In Section 4 the undecidability of the MSO-theory of the infinite binary tree augmented by any well-ordering is shown.

Preliminaries

Words. For a finite alphabet Σ, we write Σ * for the set of all words over Σ. The length of a word u ∈ Σ * is denoted by |u| and ε is the empty word. For all words u, v

∈ Σ * , u is a prefix of v (written u ⊑ v) if there exists w ∈ Σ * such that v = uw. If w ∈ Σ + then u is a strict prefix of v (written u ⊏ v).
The greatest common prefix of two words u and v (written u ∧ v) is the longest word which is a prefix of u and v.

Relational structures. A signature is a ranked set of symbol S, where for all R ∈ S, |R| denotes the arity (which is ≥ 1) of the symbol R. A relational structure R over the signature S is given by a tuple (U, (R R ) R∈S ) where U is the universe of R and where for all R ∈ S, R R (which is also called the interpretation of R in R) is a subset of U |R| . When R is clear from the context, we will simply write R instead of R R .

Monadic second-order logic. We adopt the definition of monadic second-order logic (MSO) over relational structures with the standard syntax and semantics (see e.g. [START_REF] Ebbinghaus | Finite Model Theory[END_REF] for a detailed presentation). We write ϕ(X 1 , . . . , X n , y 1 , . . . , y m ) to denote that the free variables of the formula ϕ are among X 1 , . . . , X n (monadic second-order) and y 1 , . . . , y m (first-order) respectively. A formula without free variables is called a sentence.

For a relational structure R and a sentence ϕ, we write R |= ϕ if R satisfies the formula ϕ. The MSO-theory of R is the set of sentences satisfied by R. For every formula ϕ(X 1 , . . . , X n , y 1 , . . . , y m ), all subsets U 1 , . . . , U n of the universe of R and all elements v 1 , . . . , v m of the universe of R, we write R |= ϕ[U 1 , . . . , U n , v 1 , . . . , v m ] to express that ϕ holds in R when X i is interpreted as U i for all i ∈ [1, n] and y j is interpreted as v j for all j ∈ [1, m].

Infinite binary labelled trees. An (infinite binary) tree labeled by a finite alphabet Σ is a mapping t : {0, 1} * → Σ. We denote by T Σ the set of all trees labeled by Σ. For a set U ⊆ {0, 1} * , we write t(U ) ∈ T {0,1} for the characteristic tree of U , i.e., the tree which labels all nodes in U with 1 and all the other nodes with 0. This notation is extended to the case of several sets. The characteristic tree of U 1 , . . . , U n ⊆ {0, 1} * is the tree labeled by {0, 1} n written t(U 1 , . . . , U n ) and defined for all u ∈ {0,

1} * by t(U 1 , . . . , U n )(u) := (b 1 , . . . , b n ) where for all i ∈ [1, n], b i = 1 if u ∈ U i and b i = 0 otherwise.
To every tree t labeled by Σ = {a 1 , . . . , a n }, we associate a canonical structure over the signature {E 0 , E 1 , P a1 , . . . , P an } where E 0 and E 1 are binary symbols and the P ai are predicates. The universe of this structure is {0, 1} * . The symbols E 0 and E 1 are respectively interpreted as {(w, w0) | w ∈ {0, 1} * } and {(w, w1) | w ∈ {0, 1} * }. Finally for all i ∈ [1, n], P ai is interpreted as {u ∈ Σ * | t(u) = a i }. In the following, we will not distinguish between a tree and its canonical relational structure.

In particular, for a formula ϕ(X 1 , . . . , X n ) and sets U 1 , . . . , U n ⊆ {0, 1} * , we write t(U 1 , . . . , U n ) |= ϕ to indicate that the infinite binary tree satisfies ϕ when X i is interpreted by U i .

Choice

As described in the introduction, an MSO-definable choice function is given by an MSO-formula φ(X, x) such that

∀X∃x. X = ∅ → (x ∈ X ∧ φ(X, x) ∧ ∀y. φ(X, y) → x = y)
is true over the infinite binary tree. This section is mainly devoted to the proof of the following theorem of Gurevich and Shelah.

Theorem 1 ([GS83]

). There is no MSO-definable choice function on the infinite binary tree.

The technical formulation of the result we prove is given in Theorem 3, where we concretely provide counter examples for which a given formula cannot choose a unique element. As a machinery for the proof we use tree automata, which are easier to manipulate (at least for our purpose) than formulas. In the following we give some basic definitions. More details on automata for infinite trees can be found in [START_REF] Thomas | Languages, automata, and logic[END_REF].

In this section we take the view of labeled trees as mappings from {0, 1} * to the label alphabet (which usually is {0, 1} n for some number n).

A parity automaton on Σ-labeled trees is a tuple

A = (Q, Σ, q 0 , ∆, Ω) with a finite set Q of states, initial state q 0 ∈ Q, transition relation ∆ ⊆ Q × Σ × Q × Q, and a priority function Ω : Q → N. A run of A on a tree t ∈ T Σ from a state q ∈ Q is a tree ρ ∈ T Q such that ρ(ε) = q,
and for each u ∈ {0, 1} * we have (ρ(u), t(u), ρ(u0), ρ(u1)) ∈ ∆. We say that ρ is accepting if on each path the minimal priority appearing infinitely often is even. If we only speak of a run of A without specifying the state at the root, we implicitly refer to a run from q 0 . We extend this model to automata that do not only accept or reject trees but also mark some of the nodes with special marking states. A marking parity automaton (MPA) is a tuple A = (Q, Σ, q 0 , ∆, Ω, P ) with an additional set of marking states P ⊆ Q. A run ρ of such an automaton defines a set U ρ ⊆ {0, 1} * as the set of those nodes that are labeled by a marking state, i.e., U ρ = ρ -1 (P ).

Given a set U ⊆ {0, 1} * and an MPA A on {0, 1}-labeled trees, we define

T (A, U ) = {U ρ | ρ is an accepting run of A on t(U )}.
That is, the set of all sets that are marked by A in an accepting run on t(U ).

Theorem 2 ([Rab69]

). For each MSO-formula φ(X, Y ) there is an MPA A φ such that

T (A φ , U ) = {U ′ ⊆ {0, 1} * | t(U, U ′ ) |= φ} for each U ⊆ {0, 1} * .
For a set U ⊆ {0, 1} * we say that A marks an element u of U if u ∈ U and there is an accepting run ρ of A on t(U ) such that U ρ = {u}. Note that with other runs A might mark other elements or sets of elements. For two trees t, t ′ we say that they are A-equivalent, written as t ≡ A t ′ , if for each state q of A there is an accepting run from q on t iff there is an accepting run from q on t ′ . Intuitively, this means that A cannot distinguish the two trees.

Undefinability of choice functions

We now define a family (U M,N ) M,N of sets such that for each MPA we can find M and N such that this MPA cannot mark a unique element of U M,N . To achieve this, we "hide" the elements from the set very deep in the tree such that MPAs up to a certain size are not able to uniquely choose an element that they can mark.

For M, N ∈ N the set U M,N ⊆ {0, 1} * is defined by the following regular expression U M,N = {0, 1} * (0 N 0 * 1) M {0, 1} * . Let t M,N = t(U M,N ). This tree can be obtained by unfolding the finite graph G M,N depicted in Figure 1 from x M . In this picture, the dashed arrows represent 1-labeled edges leading back to the node x M . The chains of 0-edges between x k+1 and x k have length N . All nodes in this graph are labeled 0 except x 0 , which is labeled by 1. It is easy to verify that x 0 is reachable from x M by exactly those paths whose sequence of edge labels is in the set U M,N . So G M,N can be viewed as the minimal DFA accepting the language U M,N where x 0 is the only final state. Let t k,M,N denote the tree that we obtain by unfolding the graph G M,N from the node x k .

xM 1 • 0 • 0 • • • • • 0 0 xM-1 1 • 0 • • • • • 0 0 xM-2 1 . . . • 0 x1 1 • 0 • 0 • • • • • 0 0 x0 1 0,1
We now fix an MPA A = (Q, {0, 1}, q 0 , ∆, Ω, P ) on {0, 1}-labeled trees and take M = 2 |Q| + 1 and N = |Q| + 1. For these fixed parameters we simplify the notation by letting

t k = t k,M,N . In particular, t M = t M,M,N = t M,N .
We say that a subtree (of some tree t) that is isomorphic to t k for some k is of type t k .

Our aim is to trick the automaton A to show that it cannot choose a unique element from the set U M,N . This is done by modifying a run that marks an element u of U M,N such that we obtain another run marking something different.

To understand the general idea, consider the path between x k+1 and x k for some k. If we take a 1-edge before having reached the end of the 0-chain, i.e., if we take a dashed edge in the picture, then we reach a subtree of type t M . But if we walk to the end of the 0-chain and then move to the right using a 1-edge, then we arrive at a subtree of type t k . If we show that there is ℓ < M such that t M and t ℓ are A-equivalent, then this means that A has no means to identify when it enters the part where taking a 1-edge leads to subtree of type t ℓ . We then exploit this fact by pumping the run on this part of the tree such that we obtain another run marking something different.

Lemma 1. There exists ℓ < M such that t M ≡ A t ℓ .

Proof. We consider for each tree t ∈ T {0,1} the function f t : Q → {a, r} with f t (q) = a if there is an accepting run from q on t, and f t (q) = r otherwise. By definition, two trees t, t ′ are A-equivalent if f t = f t ′ . There are at most 2 |Q| different such functions. By the choice of M there are 1

≤ k 1 < k 2 ≤ M such that t k1 ≡ A t k2 . Let k = k 2 -k 1 and ℓ = M -k.
We show that we can obtain t ℓ from t M by substituting some of the subtrees of type t k2 in t M by subtrees of type t k1 . As we have seen that t k1 and t k2 are A-equivalent, this suffices to show that t M and t ℓ are also A-equivalent.

We know that t M is obtained by unraveling the graph G M,N (Figure 1) from x M . One way to obtain t ℓ is the following. We take a second copy of G M,N and denote in this copy the vertices corresponding to x 0 , . . . , x M by x ′ 0 , . . . , x ′ M . Now we redirect the edge leading to x k2 in the first copy to point to x ′ k1 in the second copy. It is easy to verify that unravelling this new graph from x M (in the first copy) yields the tree t ℓ . And furthermore, this shows that t ℓ can be obtained by replacing some subtrees of type t k2 in t M by subtrees of type t k1 . Hence, t M ≡ A t ℓ .

⊓ ⊔

The following lemma states that it is impossible for A to distinguish a unique element of U M,N , i.e., it is not possible that T (A, U M,N ) = {{u}} for some

u ∈ U M,N . Lemma 2. If A marks an element of U M,N , then |T (A, U M,N )| > 1
Proof. Assume that that there is an accepting run ρ of A on t M = t M,N such that U ρ = {u} with u ∈ U M,N . From ρ we construct another accepting run marking a different set of nodes. For 0 ≤ k ≤ M let u k denote the maximal prefix of u such that the subtree at u k is of type t k . Let ℓ be as in Lemma 1. For i ≥ 0 we let v i = u ℓ+1 0 i and v ′ i = v i 1. Note that v 0 = u ℓ+1 and that for 0 ≤ i < N the subtrees at v ′ i are of type t M , and for i ≥ N the subtrees at v ′ i are of type t ℓ . From Lemma 1 we know that t ℓ ≡ A t M . Hence, for each accepting run ρ q of A from q on t M we can pick an accepting run ρ ′ q of A from q on t ℓ . By the choice of N there are 0 ≤ j < j ′ < N such that ρ(v j ) = ρ(v j ′ ). For the moment, consider only the transitions taken in ρ on the sequence v 0 , v 1 , . . ., i.e., on the infinite branch to the left starting from v 0 . We now simply repeat the part of the run between v j and v j ′ once. The effect is that some of the states that were at a node v ′ i for i < N are pushed to nodes v ′ i for i ≥ N , i.e., the states are moved from subtrees of type t M to subtrees of type t ℓ . But for those states q we can simply plug the runs ρ ′ q that we have chosen above. More formally, we define the new run ρ ′ of A on t M as follows. On the part that is not in the subtree below v 0 the run ρ ′ corresponds to ρ. In the subtree at v 0 we make the following definitions, where h = j ′j.

-For i < j ′ let ρ ′ (v i ) = ρ(v i ) and ρ ′ (v ′ i ) = ρ(v ′ i ). -For i ≥ j ′ let ρ ′ (v i ) = ρ(v i-h ) and ρ ′ (v ′ i ) = ρ(v ′ i-h ).
-For the subtrees at v ′ i for i < j ′ we take the subrun of ρ at v ′ i . -For the subtrees at v ′ i for j ′ ≤ i < N or i ≥ N + h we take the subrun of

ρ at v ′ i-h . This is justified because in these cases ρ ′ (v ′ i ) = ρ(v ′ i-h
) and the subtrees at v ′ i and v ′ i-h are of the same type (both of type t M or both of type t ℓ ).

-For the subtrees at v ′ i for N ≤ i < N + h we take the runs ρ ′ qi for q i = ρ ′ (v ′ i ). This is justified as follows. From q i = ρ ′ (v ′ i ) and the definition of ρ ′ we know that ρ(v ′ i-h ) = q i . Hence, there is an accepting run of A from q i on t M . Thus, ρ ′ qi as chosen above is an accepting run of A from q i on t ℓ . This run ρ ′ is accepting. Furthermore, the state marking u in the run ρ has been moved to another subtree: There are n ≥ N and w ∈ {0, 1} * such that u = u ℓ+1 0 n w. In ρ ′ the state marking u is at u ′ = u ℓ+1 0 n+h w. Hence, we have constructed an accepting run marking a set different from {u}.

⊓ ⊔

Of course, the statement is also true if we increase the value of M or N , e.g., if we let N = M = 2 |Q|+1 . Thus, combining Theorem 2 and Lemma 2 we obtain the following.

Theorem 3. Let φ * (X, x) by an MSO-formula. There exists n ∈ N such that for each u ∈ U n,n with t(U n,n , u) |= φ * there is u ′ = u with t(U n,n , u ′ ) |= φ * .

A direct consequence is the theorem of Gurevich and Shelah. The advantage of our proof is that we obtain a rather simple family of counter examples (the sets U M,N ). An easy reduction allows us to extend the non-existence of an MSO-definable choice function to the case where we allow a finite number of fixed predicates as parameters. This result has already been shown in [START_REF] Lifsches | Uniformization and skolem functions in the class of trees[END_REF] in an even more general context, but again relying on the methods employed in [START_REF] Gurevich | Rabin's uniformization problem[END_REF].

Corollary 1. Let P 1 , . . . , P n ⊆ {0, 1} * be arbitrary predicates. There is no MSOformula φ * (X 1 , . . . , X n , X, x) such that for each nonempty set U there is exactly one u ∈ U with t(P 1 , . . . , P n , U, u) |= φ * . Proof. Assume that there are P 1 , . . . , P n ⊆ {0, 1} * and φ * (X 1 , . . . , X n , X, x) such that for each set U there is exactly one u ∈ U with t(P 1 , . . . , P n , U, u) |= φ * . Then the formula ∃X 1 , . . . , X n ∀X∃x φ * (X 1 , . . . , X n , X, x) ∧ ∀y φ * (X 1 , . . . , X n , X, y) → x = y is satisfiable. Hence, by the Rabin Basis Theorem (cf. [START_REF] Thomas | Languages, automata, and logic[END_REF]), there are regular predicates P 1 , . . . , P n such that t(P 1 , . . . , P n ) |= ∀X∃x φ * (X 1 , . . . , X n , X, x) ∧ ∀y φ * (X 1 , . . . , X n , X, y) → x = y.

Regular predicates are MSO-definable, so let ψ 1 (X 1 ), . . . , ψ n (X n ) be formulas defining P 1 , . . . , P n , respectively. Then the formula φ ′ (X, x) defined as

∃X 1 , . . . , X n φ * (X 1 , . . . , X n , X, y) ∧ n i=1 ψ i (X i )
describes a choice function, contradicting Theorem 3.

⊓ ⊔

We point out here that this method only relies on the fact that the property of being a choice function is MSO-definable. So this way of reducing the case with parameters to the parameter free case can be applied whenever the properties of the object under consideration are MSO-definable (at the end of the last section we briefly mention another application of this technique).

Applications of the result and its proof

We now discuss a few applications of the results presented so far in this section. One immediate application concerns the non-definability of well-founded orders over the infinite binary tree. We skip this subject here because it is treated in detail in the next section. The first application is about unambiguous tree automata. It is well known that parity automata on infinite trees cannot be determinized. A weaker requirement than determinism is unambiguity. An automaton is called unambiguous if for each object that it accepts there is exactly one accepting run. For example, it is known that all regular languages of infinite words can be accepted by an unambiguous Büchi automaton [START_REF] Carton | Unambiguous büchi automata[END_REF] (and deterministic Büchi automata do not suffice to accept all regular ω-languages).

In an unpublished note [NW] Niwiński and Walukiewicz have shown that not every parity tree automaton is equivalent to an unambiguous one.

Theorem 4 ([NW]

). There is no unambiguous parity automaton accepting exactly those {0, 1}-labeled trees in which at least one node is labeled 1.

The underlying idea is that the set of 1-labeled nodes represents the set from which an element has to be chosen. Now we assume that A is a parity automaton accepting the language used in Theorem 4. Using a game that is similar to the emptiness game for tree automata (cf. [START_REF] Thomas | Languages, automata, and logic[END_REF]) one can show that each accepting run on a tree allows us to pick a unique 1-labeled node from the accepted tree in an MSO-definable way. If A is unambiguous, then this means that for each accepted tree there is a unique run and hence we can build an MSO-formula picking exactly one 1-labeled node for each accepted tree. This yields an MSOdefinable choice function.

In fact, the proof in [NW] yields a more general result: Assume that A is a parity tree automaton (over the alphabet {0, 1}) that does not accept the tree that is completely labeled by 0, i.e., the tree t(∅). Then there is a formula φ A (X, x) such that for each U ⊆ {0, 1} * for which there is a unique accepting run of A on t(U ), there is a unique element u ∈ U such that t(U, u) |= φ A .

We can use this fact to show the following result.

Theorem 5. There is a regular language T ⊆ T {0,1} and a tree t ∈ T such that there is no parity automaton accepting T that has a unique accepting run for t.

Proof. Consider the language T of trees with the property that each subtree rooted at a node of the form 1 * 0 contains a node labeled 1. The tree t is defined to have all nodes of the form 1 * labeled 0, and as the subtree rooted at the nodes 1 n 0 we plug the trees t n,n . As each t n,n contains a node labeled 1, we have t ∈ T . Assume that there is parity automaton A accepting T that has a unique run on t. Let q be a state of A that occurs at infinitely many nodes of the form 1 * 0 in this run. Let A ′ be the automaton A with initial state q. As A accepts T it is clear that A ′ does not accept the tree t(∅). Furthermore, as the run of A on t is unique, there are infinitely many n such that A ′ has a unique run on t n,n . In combination with the result from [NW] that we discussed above, this gives a contradiction to Theorem 3.

⊓ ⊔

Another application of Theorem 1 concerns the definability of winning strategies in infinite games. In the following we show that there exist game trees that do not admit the definition of winning strategies in MSO.

A game tree is a tuple Γ = (U 1 , U 2 , Ω, W ) where U 1 , U 2 ⊆ {0, 1} * form a partition of {0, 1} * , Ω : {0, 1} * → {0, . . . , n} maps the nodes to a finite set of natural numbers, and W ⊆ {0, . . . , n} ω is the winning condition. A play of Γ starts in ε. If the play is currently in u ∈ {0, 1} * , then Player 1 or Player 2, depending on whether u ∈ U 1 or u ∈ U 2 , chooses b ∈ {0, 1} and the next game position is ub. In the limit, such a play forms an infinite word in {0, 1} ω . This infinite word corresponds to an infinite sequence over {0, . . . , n} by applying Ω to each prefix. If this sequence is in W , then Player 1 wins, and otherwise Player 2 wins. We identify a play with the corresponding infinite word in {0, 1} ω .

A strategy for Player i is a function f i : U i → {0, 1} and a play γ is played according to f i if for each prefix u ∈ U i of γ, Player 1 uses the strategy to determine the next move, i.e., if uf i (u) is a prefix of γ. A strategy f i is winning for Player i if each play γ that is played according to f i is winning for Player i.

If W ⊆ {0, . . . , n} ω is a regular ω-language (i.e. MSO-definable), then for each game tree Γ = (U 1 , U 2 , Ω, W ) one of the players has a winning strategy ( [START_REF] Büchi | Solving sequential conditions by finite-state strategies[END_REF]). If we represent the mapping Ω by sets Ω 0 , . . . , Ω n ⊆ {0, 1} * , each Ω i corresponding to the set of nodes mapped to i by Ω, the set of all trees t(U 1 , U 2 , Ω 0 , . . . , Ω n ) such that Player 1 has a winning strategy in

Γ = (U 1 , U 2 , Ω, W ) is MSO- definable.
This raises the question whether it is also possible to define winning strategies in MSO. Note that we can represent a strategy for Player 1 by a subset of nodes that contains ε, for each u ∈ U 1 one successor u0 or u1, and for each u ∈ U 2 both successors u0 and u1. The plays according to this strategy are exactly the infinite paths contained in this set. If the winning condition is MSO-definable, then the set of all winning strategies for Player 1 is also MSO-definable, i.e., there is a formula φ(X 1 , X 2 , Y 0 , . . . , Y n , X) such that t(U 1 , U 2 , Ω 0 , . . . , Ω n , U ) |= φ iff U is a winning strategy for Player 1 (for the fixed winning condition W ).

We now look at the case where we want to select a single strategy, i.e., we are interested in a formula that defines exactly one strategy. We show in the following that there is even a fixed game tree on which no formula can define a single winning strategy (this tree is similar to the one used in the proof of Theorem 5). Theorem 6. There is a game tree Γ = (U 1 , U 2 , Ω, W ) with an MSO-definable winning condition W such that Player 1 has a winning strategy for Γ but there is no MSO-definable winning strategy for Player 1.

Proof. Consider the following {0, 1, 2}-labeled tree t such that for each n ∈ N the subtree at the node 1 n 0 is isomorphic to t n,n , and all nodes of the form 1 n are labeled by 2. The labeling of t defines the mapping Ω, i.e., Ω(u) = t(u). We let U 2 = {1 n | n ∈ N} and U 1 = {0, 1} * \ U 2 . The winning condition W contains all infinite words over {0, 1, 2} that do not contain 0 or that contain a 1.

Intuitively, Player 2 can move along the right branch of the game tree. If he continues like this forever, then he loses because only nodes labeled 2 are visited during the play. Otherwise, he moves to the left at some position, that is, to the root of a subtree t n,n . Now Player 1 chooses all the following moves and wins if a node labeled 1 is reached eventually. As each subtree t n,n contains a node labeled 1 it is obvious that Player 1 has a winning strategy.

Assume that there is a winning strategy on t that is MSO-definable by a formula φ(X) (as the game tree is fixed we omit the other free variables). This formula is equivalent to a parity automaton A that accepts exactly one strategy labeling of t, corresponding to the winning strategy defined by φ.

Using A we can construct a formula φ * (X, x) that chooses exactly one u ∈ U n,n for each n ∈ N, contradicting Theorem 3. For this we fix an arbitrary order on the states of A. For each n there is at least one state q of A such that A accepts exactly one winning strategy on the subtree t n,n of t (namely the state assumed at the root of the subtree t n,n in an accepting run for the unique winning strategy on Γ that is accepted by A). The formula φ * picks the smallest state q with this property and then chooses the element of U n,n that is described by the unique winning strategy accepted by A from q on t n,n . It is not difficult to verify that this is indeed possible in MSO.

⊓ ⊔

One should note here that the tree constructed in the proof of Theorem 6 (and also the one from Theorem 5) is not too complicated: it belongs to the Caucal hierarchy1 ( [START_REF]On infinite terms having a decidable monadic theory[END_REF]). This means that it can be obtained from a regular tree by a finite number of applications of MSO-interpretations and unfoldings, or equivalently, it is the transition graph of a higher-order pushdown automaton ([CW03]).

Order

A direct consequence of Theorem 1 is that there exists no MSO-definable wellfounded order on the nodes of the infinite binary tree. In fact from an MSOformula ϕ ≤ (x, y) defining a well-founded order on the nodes of the infinite binary tree, a choice function ϕ choice (x, X) := x ∈ X ∧ ∀y, y ∈ X → x ≤ y is easily defined by taking the smallest element of the set. In this section, we prove the following stronger result.

Theorem 7. The MSO-theory of the full-binary tree together with any wellfounded order is undecidable.

As the infinite binary tree has a decidable MSO-theory [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF], the existence of an MSO-definable well-order would contradict Theorem 7. In the particular case of t llex , the infinite binary tree with length-lexicographic order (formally defined below), this result is well-known [START_REF] Blumensath | Automatic structures[END_REF]. We show that t llex can be MSO-interpreted in the infinite binary tree with any well-founded order. Theorem 8. There exists an MSO-interpretation I such that for every wellordered infinite binary tree t, I(t) is isomorphic to t llex As MSO-interpretations preserve the decidability of MSO, Theorem 7 follows from the undecidability of the MSO-theory of t llex . The rest of this section is dedicated to the proof of Theorem 8.

Well-ordered trees

We consider structures over the binary signature S = {E 0 , E 1 , ≤}. We say that an S-structure t is a well-ordered (infinite binary) tree if it is isomorphic to a wellordered tree with universe {0, 1} * where E 0 and E 1 are respectively interpreted as {(u, u0) | u ∈ {0, 1} * } and {(u, u1) | u ∈ {0, 1} * }, and ≤ is interpreted as a well-founded order on {0, 1} * . Such an S-structure will be referred to as a canonical well-ordered tree. Up to isomorphism, a well-ordered tree is entirely characterized by the well-founded order on the set of words over {0, 1}.

For example, consider the length-lexicographic order ≤ llex defined by: u ≤ llex v ⇔ |u| < |v| or (|u| = |v| and u ≤ lex v) where ≤ lex refers to the standard lexicographic order. This order is well-founded and we write t llex the canonical well-ordered tree associated to ≤ llex . The key property of t llex is that it is MSOdefinable (up to isomorphism) in the class of well-ordered trees 2 . Proposition 1. There exists an MSO-formula ϕ llex such that for every wellordered tree t, t |= ϕ llex ⇔ t ∼ = t llex . Succ 1 (v) which belongs to U 1 . Remarking that U 1 is equal to (U 1 ) <u ∪ (U 1 ) ≥u = (U 0 ) ≤v ∪ (U 1 ) ≥u and using the fact that t |= ψ[U 0 ], we obtain that Succ 0 (v) ≤ u. Similarly U 0 is equal to (U 0 ) <Succ0(v) ∪ (U 0 ) ≥Succ0(v) = (U 1 ) ≤v ∪ (U 0 ) ≥Succ0(v) and using the fact that t |= ψ[U 1 ], we obtain that u = Succ 1 (v) ≤ Succ 0 (v). It follows that u = Succ 0 (v) which brings the contradiction.

⊓ ⊔ Theorem 8 directly follows from Proposition 3. An immediate consequence of this result is that the infinite binary tree cannot be MSO-interpreted in (ω, succ), i.e., the natural numbers with successor. As a well-founded order can be defined in MSO on (ω, succ), one could interpret the full binary tree with a wellfounded order. From Theorem 7, this structure has an undecidable MSO-theory which would contradict the fact that the MSO-theory of (ω, succ) is decidable [START_REF] Büchi | On a decision method in restricted second order arithmetic[END_REF]. More generally, we obtain that the infinite binary tree cannot be MSOinterpreted in any structure having both a decidable MSO-theory and an MSOdefinable well-founded order. Combining the result that the infinite binary tree cannot be interpreted in (ω, succ) with the same technique as in the proof of Corollary 1, we can also show that the infinite binary tree cannot be interpreted in (ω, succ, P 1 , . . . , P n ) for arbitrary fixed predicates P i .

Fig. 1 .

 1 Fig. 1. A representation of the regular tree tM,N by the graph GM,N

In particular, as all graphs in the Caucal hierarchy have a decidable MSO-theory, the tree constructed in the proof of Theorem 6 also has a decidable MSO-theory.

The class of well-ordered trees is itself MSO-definable in the class of S-structures.

Proof. Consider the MSO-formula ϕ llex over S expressing that: the root ε is the smallest element for ≤, for all nodes u ∈ {0, 1} * and v ∈ 1 * , the successor of the node u0v is the smallest element for the prefix order of the set u10 * \ {Succ(u0v ′ ) | v ′ ⊏ v} where Succ(u) the successor of u for the order ≤ and for all nodes u ∈ 1 * , the successor of u is the smallest element for the prefix order of the set 0 + \ {Succ(u ′ ) | u ′ ⊏ u}.

It is easy to see that t llex satisfies the formula ϕ llex . It remains to show that for every well-ordered tree t, if t satisfies ϕ llex then t is isomorphic to t llex .

Let t be a well-founded tree satisfying ϕ llex . We can assume w.l.o.g that t is a canonical well-ordered tree. It is therefore enough to show that t = t llex .

For all nodes u ∈ {0, 1}, we write Succ llex (u) for the successor of u for the order ≤ llex . As by condition 1 the root ε of t is the minimal element of ≤, it is enough to establish that for all u ∈ {0, 1} * , Succ(u) = Succ llex (u).

Assume by contradiction that this property is not satisfied. Let u 0 be the smallest node u for the order ≤ llex such that Succ(u) = Succ llex (u) We distinguish two cases depending whether u 0 contains an occurrence of 0 or not.

If u 0 contains an occurrence of 0 then u 0 can be uniquely written as u0v with u ∈ {0, 1} * and v ∈ 1 * . The successor of u 0 in the order ≤ llex is Succ llex (u 0 ) = u10 |v| . By condition 2 of the definition of ϕ llex , Succ(u 0 ) is the smallest element for the prefix order of the set u10 * \ {Succ(u0v

By minimality (for the order ≤ llex ) of u 0 , we have for all v ′ ⊏ v that Succ(u0v ′ ) = Succ llex (u0v ′ ) = u10 |v ′ | . Therefore, Succ(u 0 ) is the minimal element for the prefix order of the set u10 * \ {u10 |v ′ | | v ′ ⊏ v}. This implies that Succ(u 0 ) = u10 |v| = Succ llex (u 0 ) which contradicts the definition of u 0 .

If u 0 does not contain an occurrence of 0 then u 0 ∈ 1 * . The successor of u 0 for the order ≤ llex is 0 |u0|+1 . By condition 3 of the definition of ϕ llex , Succ(u 0 ) is the smallest element for the prefix order of the set 0 + \ {Succ(u) | u ⊏ u 0 }.

By minimality (for the order ≤ llex ) of u 0 , we have for all u ⊏ u 0 that Succ(u) = Succ llex (u) = 0 |u|+1 . Therefore, Succ(u 0 ) is the minimal element for the prefix order of the set 0 + \ {0 |u|+1 | u ⊏ u 0 }. This implies that Succ(u 0 ) = 0 |u0|+1 = Succ llex (u 0 ) which contradicts the choice of u 0 .

⊓ ⊔

Interpreting t llex

We now define the notion of induced well-ordered tree. Consider a canonical well-ordered tree t and a set U ⊆ {0, 1} * of nodes which is closed under greatest common prefix (i.e.

The well-ordered tree t| U induced by U in t has universe U and its signature is interpreted as

Lemma 3. For every MSO-formula ϕ over S, there exists a formula ϕ * (X) such that for every canonical well-ordered tree t and set U , t |= ϕ * [U ] if and only if the set U induces a well-ordered tree t| U on t and t| U |= ϕ.

Proof. Consider an MSO-formula ϕ over S. Let ϕ ind (X) be an S-formula expressing that X satisfies the conditions to induce a full binary tree and let ϕ ′ (X) be the formula obtained from ϕ by relativizing the quantifications to X and by replacing

It is easy to check that the formula ϕ * (X) := ϕ ind (X) ∧ ϕ ′ (X) satisfies the property stated in the lemma.

⊓ ⊔

We first show that for every canonical well-ordered tree t, there exists a subset U ⊆ {0, 1} * such that t| U is isomorphic to t llex . To construct such a set we need the following technical definition. A node u ∈ {0, 1} * of a canonical well-ordered tree t is mixed if for all v ⊒ u, v ′ ⊒ u ∈ {0, 1} * there exists a w ∈ {0, 1} * such that v < v ′ w.

Lemma 4. For every canonical well-ordered tree t, there exists a mixed node.

Proof. Let t be a canonical well-ordered tree. Assume by contradiction that t does not have any mixed nodes. We construct by induction two sequences of nodes (u i ) i∈N and (v i ) i∈N such that for all i ≥ 0, u i > u i+1 and u i ≥ v i w for all w ∈ {0, 1} * .

As ε is not mixed there exist two nodes u and v such that u ≥ vw for all w ∈ {0, 1} * . We take u 0 = u and to ensure that u 0 > v 0 w for all w ∈ {0, 1} * , we pick as v 0 an element of v{0,

Assume that both sequences are constructed up to rank i ≥ 0, we define u i+1 and v i+1 . As v i is not mixed, there exists two nodes u ⊒ v i and v ⊒ v i such that u ≥ vw for all w ∈ {0, 1} * . We take u i+1 equal to u and v i+1 an element of v{0, 1} * \ {u ′ | u ′ ⊑ u i+1 } thus ensuring that for all w ∈ {0, 1} * , u i+1 > v i+1 w. By induction hypothesis, we have that u i > u i+1 .

The sequence (u i ) i∈N is an infinite strictly decreasing sequence which contradicts the fact that ≤ is a well-founded order.

⊓ ⊔ Proposition 2. For every canonical well-ordered tree t, there exists a set of nodes U inducing a well-ordered tree t| U isomorphic to t llex .

Proof. Let t be a canonical well-ordered tree. We construct a sequence of nodes (u w ) w∈{0,1} * indexed by the set of words over {0, 1} * such that: for all w, w ′ ∈ {0, 1} * , w ≤ llex w ′ implies u w ≤ u w ′ , and for all w ∈ {0, 1} * and i ∈ {0, 1}, u wi ∈ u w i{0, 1} * . If we assume that this sequence has been constructed and we take U := {u w | w ∈ {0, 1} * }, it is easy to check that U is closed by greatest common prefix and hence U induces a full binary tree on t. Furthermore the mapping from {0, 1} * to U associating w to u w is an isomorphism from t llex to t| U .

We now construct the sequence (u w ) w∈{0,1} * by induction on the lengthlexicographic order ≤ llex . By Lemma 4, the tree t has a mixed node. We take u ε to be a mixed node of t. Assume that the sequence has been constructed up to w 0 ∈ {0, 1} * , we construct the element u w1 where w 1 is the successor of w 0 for the length-lexicographic order. From the definition of ≤ llex , it follows that the element w 1 is equal to w 2 i for some i ∈ {0, 1} and w 2 ≤ llex w 0 . As u ε is mixed, there exists a v such that u w0 < u w2 iv. We take u w1 = u w2 iv. By induction hypothesis, for all w ≤ llex w 1 , we have u w ≤ u w1 .

⊓ ⊔ Note that Theorem 7 can already be derived from the above proposition. For every formula ϕ over S, consider the formula ϕ * (X) obtained from ϕ by Lemma 3 and ϕ * llex (X) obtained from the formula ϕ llex of Proposition 1. By Proposition 2, for every well-ordered tree t, t |= ∃X, ϕ * llex (X) ∧ ϕ * (X) if and only if t llex |= ϕ. As the formula ϕ * (X) can be effectively constructed from the formula ϕ, it follows that the MSO-theory of t llex is recursive in the MSO-theory of any well-ordered tree t.

We now strengthen the result of Proposition 2 by showing that in every wellordered tree t there exists an MSO-definable set of nodes inducing a well-ordered tree isomorphic to t llex . Proposition 3. For every canonical well-ordered tree, there exists an MSOdefinable set of nodes U 0 inducing a well-ordered tree isomorphic t llex .

Proof. Consider the following MSO-formula ψ(X) defined by:

x < y and min Z designates the smallest element of the set Z for the order ≤.

Let t be a well-ordered tree. We claim that t |= ∃ =1 X, ψ(X) (where ∃ =1 stands for there exists a unique), which establishes the MSO-definability of a set of nodes U 0 inducing on t a well-ordered tree isomorphic to t llex .

The first step is to show that t |= ∃X, ψ(X). For this, we define a sequence of nodes (u w ) w∈{0,1} * of t by induction on the order ≤ llex . The node u ε is the smallest element of {min Z | Z ⊆ {0, 1} * ∧t |= ϕ * llex [Z]}. Proposition 2 guarantees that this set is not empty. Assume that the sequence has been constructed up to the element u w0 . We define u w1 where w 1 is the successor of w 0 for the order ≤ llex . We take u w1 as the smallest element for ≤ of the set {min Z | w 0 < Z ∧ ϕ * llex ({u w | w ≤ w 0 } ∪ Z})}. This set is not empty by definition of u w0 . Consider the set U 0 := {u w | w ∈ {0, 1} * }. It is straightforward to show that U 0 induces a well-ordered tree on t isomorphic to t llex . It follows that t |= ψ[U 0 ]. Hence t |= ∃X, ψ(X).

We now show that t |= ∃ =1 X, ψ(X). It is enough to show that for all U 1 ⊆ {0, 1} * , t |= ψ[U 1 ] implies U 1 = U 0 . For all u ∈ U 0 (resp. u ∈ U 1 ), we write Succ 0 (u) (resp. Succ 1 (u)) the smallest element of U 0 (resp. of U 1 ) strictly greater than u.

By induction on w for the order ≤ llex , it is easy to show that u w ∈ U 1 for all w ∈ {0, 1} and hence U 0 ⊆ U 1 . Assume by contradiction that U 0 U 1 . Let u be the smallest element of U 1 \ U 0 . It is easy to see that both sets have the same minimal element and therefore u = min U 1 . As U 1 induces a well-ordered tree isomorphic to t llex and since u = min U 1 , there exists v ∈ U 1 such that u = Succ 1 (v). By minimality of u, v belongs to U 0 and for all v ′ ≤ v, v ′ ∈ U 1 implies v ′ ∈ U 0 . Furthermore Succ 0 (v) which belongs to U 0 is different from