Florent Jacquemard
email: florent.jacquemard@inria.fr

Francis Klay
email: francis.klay@orange-ftgroup.com

Camille Vacher
email: vacher@lsv.ens-cachan.fr

Rigid Tree Automata and Applications 6

Keywords: Tree Automata, Symbol Constraints, Term Rewriting, Verification

We introduce the class of Rigid Tree Automata (RTA), an extension of standard bottom-up automata on ranked trees with distinguished states called rigid. Rigid states define a restriction on the computation of RTA on trees: RTA can test for equality in subtrees reaching the same rigid state. RTA are able to perform local and global tests of equality between subtrees, non-linear tree pattern matching, and some inequality and disequality tests as well. Properties like determinism, pumping lemma, Boolean closure, and several decision problems are studied in detail. In particular, the emptiness problem is shown decidable in linear time for RTA whereas membership of a given tree to the language of a given RTA is NP-complete. Our main result is the decidability of whether a given tree belongs to the rewrite closure of an RTA language under a restricted family of term rewriting systems, whereas this closure is not an RTA language. This result, one of the first on rewrite closure of languages of tree automata with constraints, is enabling the extension of model checking procedures based on finite tree automata techniques, in particular for the verification of communicating processes with several local non rewritable memories, like security protocols. Finally, a comparison of RTA with several classes of tree automata with local and global equality tests, with dag automata and Horn clause formalisms is also provided.

Introduction

Tree automata (TA) are finite representations of infinite sets of terms. In automated theorem proving, they allow to cut infinite computation branches by reduction to TA decision problems. In system and software verification, TA can be used to represent infinite sets of states of a system or a program (in the latter case, a term can represent the program itself), messages exchanged in a communication protocol, XML documents... In these settings, the closure properties of TA languages permit incremental constructions and verification problems can be reduced to TA problems decidable in polynomial time like emptiness (is the language recognized by a given TA empty) and membership (is a given term t recognized by a given TA).

Despite these nice properties, a big limitation of TA is their inability to test equalities between subterms during their computation: TA are able to detect linear patterns like fst(pair(x 1 , x 2 )) but not a pattern like pair(x, x). Several extensions of TA have been proposed to overcome this problem, by addition of equality and disequality tests in TA transition rules (the classes [START_REF] Bogaert | Equality and disequality constraints on direct subterms in tree automata[END_REF][START_REF] Dauchet | Automata for Reduction Properties Solving[END_REF] have a decidable emptiness problem), or an auxiliary memory containing a tree and memory comparison [START_REF] Comon | Tree automata with one memory, set constraints and cryptographic protocols[END_REF]. Pushdown tree automata [START_REF] Guessarian | Pushdown tree automata[END_REF][START_REF] Chabin | Visibly pushdown languages and term rewriting[END_REF] also permit such tests. However, they are all limited to local tests, at a bounded distance from the current position.

In this paper, we define the rigid tree automata (RTA) by the distinction of some states as rigid, and the condition that the subterms recognized in one rigid state during a computation are all equal. With such a formalism, it is possible to check local and global equality tests between subterms, and also the subterm relation or restricted disequalities. In Sections 2 to 6 we study issues like pattern matching, pumping lemmas, compare expressiveness with related classes of automata, determinism, closure of recognized languages under Boolean operations, and decision problems for RTA. RTA are a particular case of the more general class Tree Automata with General Equality and Disequality constraints (TAGED [START_REF] Filiot | Tree automata with global constraints[END_REF], see Section 3.1). The study of the class RTA alone is motivated by the complexity results and specific applications to verification mentioned below. But our most original contribution is the study of the rewrite closure of RTA languages in Section 7.

Term rewriting systems (TRS) is a general formalism for the symbolic evaluation of terms by replacement of some patterns by others, following rewrite rules. Combining tree automata and term rewriting techniques has been very successful in verification, see e.g. [START_REF] Bouajjani | On computing reachability sets of process rewrite systems[END_REF][START_REF] Genet | Rewriting for Cryptographic Protocol Verification[END_REF]. In this context, term rewriting systems (TRS) can describe the transitions of a system, the evaluation of a program [START_REF] Bouajjani | On computing reachability sets of process rewrite systems[END_REF], the specification of operators used to build protocol messages [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF] or also transformation of documents. If a TA A is used to finitely represent an infinite set L(A) of states of a system, the rewrite closure R * L(A) of the language L(A) using R represents the set of states reachable from states described by A. When R * L(A) is again a TA language, the verification of a safety property amounts to checking for the existence of an error state in R * L(A) (either a given term t or a term in a given regular language). This technique, sometimes referred as regular tree model checking, has driven a lot of attention to the rewrite closure of tree automata languages. However, there has been very few studies of this issue for constrained TA (see e.g. [START_REF] Jacquemard | Tree automata with equality constraints modulo equational theories[END_REF]). The reason is the difficulty to capture the behaviour of constraints after the application of rewrite rules.

In Section 7, we show that it is decidable whether a given term t belongs to the rewrite closure of a given RTA language for a restricted class of linear TRS called invisibly pushdown, whereas this closure is generally not an RTA language. Linear and invisibly pushdown TRS can typically specify cryptographic operators like decrypt(crypt(x, pk(A)), sk(A)) → x.

Using RTA instead of TA in a regular tree model checking procedure permits to handle processes with local and global memories taking their values in infinite domains and which can be written only once. We illustrate this idea in Section 8 with the description of a potential application of RTA to the verification of security protocols.

Preliminaries

A signature Σ is a finite set of function symbols with arity. We write Σ m for the subset of function symbols of Σ of arity m. Given an infinite set X of variables, the set of terms built over Σ and X is denoted T (Σ, X ), and the subset of ground terms (terms without variables) is denoted T (Σ). The set of variables occurring in a term t ∈ T (Σ, X ) is denoted vars(t). A term t ∈ T (Σ, X ) is called linear if every variable of vars(t) occurs at most once in t. A substitution σ is a mapping from a finite subset of X into T (Σ, X ). The application of a substitution σ to a term t is the homomorphic extension of σ to T (Σ, X ).

A term t can be seen as a function from its set of positions Pos(t) into function symbols or variables of Σ ∪ X . The positions of Pos(t) are sequences of positive integers (ε, the empty sequence, is the root position). Positions are compared wrt the prefix ordering: p 1 < p 2 iff there exists p = ε such that p 2 = p 1 • p (where p 1 • p denotes the concatenation of p 1 and p). In this case, p is denoted p 2p 1 . The subterm of t at position p is denoted t| p , and the replacement in t of the subterm at position p by u is denoted t[u] p . The depth d (t) of t is the length of its longest position. A n-context is a linear term of T (Σ, {x 1 , . . . , x n }). The application of a n-context C to n terms t 1 , . . . , t n , denoted by C[t 1 , . . . , t n ], is defined as the application to C of the substitution {x 1 → t 1 , . . . , x n → t n }.

Term Rewriting.

A term rewrite system (TRS) over a signature Σ is a finite set of rewrite rules ℓ → r, where ℓ ∈ T (Σ, X ) (it is called the left-hand side (lhs) of the rule) and r ∈ T (Σ, vars(ℓ)) (it is called right-hand-side (rhs)). A term t ∈ T (Σ, X ) rewrites to s ∈ T (Σ, X ) by a TRS R (denoted t --→ R s ) if there is a rewrite rule ℓ → r ∈ R, a position p ∈ Pos(t) and a substitution σ such that t| p = σ(ℓ) and s = t[σ(r)] p . In this case, t is called reducible. An irreducible term is also called an R-normal-form. The transitive and reflexive closure of --→ R is denoted --→ * R . Given L ⊆ T (Σ, X ), we denote R * (L) = {t ∃s ∈ L, s --→ * R t}. A TRS R is called linear if all the terms in its rules are linear and collapsing if every rhs of rules of R is a variable.

Tree automata.

Following definitions and notations of [START_REF] Comon | Tree Automata Techniques and Applications[END_REF], we consider tree automata which compute bottom-up (from leaves to root) on (finite) ground terms in T (Σ). At each stage of computation on a tree t, a tree automaton reads the function symbol f at the current position p in t and updates its current state, according to f and the respective states reached at the positions immediately under p in t. Definition 1. A tree automaton (TA) A on a signature Σ is a tuple Q, F, ∆ where Q is a finite set of nullary state symbols, disjoint from Σ, F ⊆ Q is the subset of final states and ∆ is a set of transition rules of the form: f (q 1 , . . . , q n ) → q where n ≥ 0, f ∈ Σ n , and q 1 , . . . , q n , q ∈ Q.

A run of the TA A on a term t ∈ T (Σ) is a relabelling of t with states of Q compatible with ∆. More formally, it is a function r : Pos(t) → Q such that for all p ∈ Pos(t) with t(p) = f ∈ Σ n (n ≥ 0), f r(p.1), . . . , r(p.n) → r(p) ∈ ∆. A run r is called successful if r(ε) ∈ F . We will sometimes use term-like notation for runs. For instance, a run {ε → q, 1 → q 1 , 2 → q 2 } will be denoted q(q 1 , q 2 ).

The language L(A, q) of a TA A in state q is the set of ground terms for which there exists a run r of A such that r(ε) = q. The language L(A) of A is q∈F L(A, q), and a set of ground terms is called regular if it is the language of a TA. The size of A, denoted |A|, is the number of symbols in ∆.

A TA A = Q, F, ∆ on Σ is deterministic (DTA), resp. complete, if for every f ∈ Σ n , and every q 1 , . . . , q n ∈ Q, there exists at most, resp. at least, one rule f (q 1 , . . . , q n ) → q ∈ ∆. In the deterministic (resp. complete) cases, given a tree t, there is at most (resp. at least) one run r of A on t.

RTA: Definition and Examples

We now introduce the class of rigid tree automata studied in this paper and show their expressiveness with some examples and first properties.

Definition and First Examples

Definition 2. A rigid tree automaton (RTA) A on a signature Σ is a tuple Q, R, F, ∆ where Q, F, ∆ is a tree automaton denoted ta(A) and R ⊆ Q is the subset of rigid states.

A run of the RTA A on a term t ∈ T (Σ) is a run r of the underlying TA ta(A) on t with the additional condition (called rigidity condition) stating that: for all positions

p 1 , p 2 ∈ Pos(t), if r(p 1 ) = r(p 2 ) ∈ R then t| p1 = t| p2 .
The languages L(A, q) and L(A) of RTA are defined the same way as for TA. Note that with these definitions, every regular language is an RTA language. We shall sometimes write below TA and RTA for the classes of TA and RTA languages. The size of an RTA A, denoted |A|, is the size |ta(A)| of its underlying TA.

Example 1. Let Σ = {a:0, b :0, f :2}. The set {f (t, t) | t ∈ T (Σ)} is recognized by the following RTA on Σ A = {q, q r , q f }, {q r }, {q f }, {a → q|q r , b → q|q r , f (q, q) → q|q r , f (q r , q r ) → q f } , where a → q|q r is an abbreviation for a → q, a → q r . An example of successful run of A on f (f (a, b), f (a, b)) is q f q r (q, q), q r (q, q) .3 Note that the above RTA language is not regular; this can be shown using a classical pumping argument.

Pattern Matching

TA are able to characterize languages of terms which embed a given pattern. However, they are limited to linear patterns for this purpose. For instance, as recalled above, the set of terms embedding the pattern f (x, x) is not a regular term language. The RTA permit to generalize this pattern matching ability to arbitrary patterns.

Example 2. Let us extend the RTA of Example 1 with the transitions rules f (q, q f ) → q f , f (q f , q) → q f ensuring the propagation of the final state q f up to the root. The RTA obtained recognizes the set of terms of T (Σ) containing the pattern f (x, x).

3

The principle of the construction of Examples 1 and 2 can be generalized into the following result.

Proposition 1. For all terms t ∈ T (Σ, X ), there exists an RTA of size linear in the size of t and constructed in linear time which recognizes the terms of T (Σ) having a ground instance of t as a subterm.

Proof. The proposition is obvious when t is a variable. Let us assume that t is not a variable and let us associate one state q s to every strict subterm s of t (including variables). The RTA for Proposition 1 has for set of states Q = {q s | s strict subterm of t} ∪ {q, q f }, the subset R of rigid states is the set of states of Q of the form q x such that x is a variable occurring at least twice in t, the subset of final states is F = {q f }, and its transition set is

∆ = {f (q, . . . , q) → q | f ∈ Σ n , n ≥ 0} ∪ {f (q, . . . , q) → q x | f ∈ Σ n , n ≥ 0, x ∈ vars(t)} ∪ {f (q s1 , . . . , q sn ) → q f (s1,...sn) | f ∈ Σ n , f (s 1 , . . . s n ) strict subterm of t} ∪ {f (q s1 , . . . , q sn ) → q f | f (s 1 , . . . s n ) = t} ∪ {f (q 1 , . . . , q n ) → q f | f ∈ Σ n , ∃i ≤ n, q i = q f }.
The transitions in the first four lines ensure the recognition of the pattern t into the final state q f and the transitions in the last line ensure the propagation of q f . The choice of rigid states ensure that the non linearities in t are respected.2

Other Examples: Disequalities, Inequalities, Global Equalities

In the above examples, the equalities tested by the RTA's are local, relatively to a position (e.g. the RTA tests that the subterms at the left and right child of some position p are equal). However, it is also possible to test equalities between subterms at arbitrary positions in a term.

Example 3. Let Σ = {a:0, g :1, f :2}. The set of terms t ∈ T (Σ) such that s 1 = s 2 for every two subterms g(s 1 ), g(s 2 ) of t is recognizable by the following RTA: A = {q, q r }, {q r }, {q, q r }, a → q, g(q ′ ) → q r , f (q ′ , q ′ ) → q | q ′ ∈ {q, q r } . 3 RTA are not limited to testing equalities. Using rigid states also permits to test some disequality and inequality as well, like the subterm relation.

Example 4. Let Σ = {a : 0, b : 0, f : 2, < : 2}. The set of terms <(s, t) such that s, t ∈ T Σ \ {<} and s is a strict subterm of t is recognized by the following RTA on Σ, {q, q r , q ′ , q f }, {q r }, {q f }, ∆ , with

∆ =    a → q|q r , b → q|q r , f (q, q) → q|q r , f (q, q r ) → q ′ , f (q r , q) → q ′ , f (q, q ′ ) → q ′ , f (q ′ , q) → q ′ , <(q r , q ′ ) → q f    .
For instance, a successful run on < a, f (a, b) is q f q r , q ′ (q r , q) . The idea is that in a successful run, the rigid state q r identifies (by a non-deterministic choice) the subterm s on the left side of <, and, on the right side t of <, the state q ′ is reached immediately above q r and propagated up to the root, in order to ensure that t is a strict superterm of s. 3

The RTA can also test disequalities between subterms built only with unary and constant symbols.

Example 5. Let Σ = {c : 0, a : 1, b : 1, = : 2}. The set of terms of T (Σ) of the form =(s, t), where s, t ∈ T Σ \ { =} and s is distinct from t is recognized by the following RTA on Σ, {q, q r , q a , q b , q f }, {q r }, {q f }, ∆ , with

∆ = {c → q|q r , a(q) → q|q r , b(q) → q|q r , a(q r ) → q a , b(q r ) → q b } ∪ a(q x ) → q x , b(q x ) → q x | q x ∈ {q a , q b } ∪ =(q 1 , q 2 ) → q f | q 1 , q 2 ∈ {q a , q b , q r }, q 1 = q 2 .
A successful run on = a(a(c)), b(a(c)) is q f q a (q r (q)), q b (q r (q)) . The rigid state q r will be placed at the position of the largest common postfix of s and t and q a or q b are used to memorize the letters immediately above this position, in order to check that s and t differ when reaching the top symbol = in =(s, t). 3

The construction of Example 4 cannot be generalized to the characterization of a maximal subterm amongst some subterms. This is shown in the following counter example, using a pumping argument. Example 6. Let Σ = {0 : 0, g : 1, h : 2}, and let L max be the set of terms of the form H g m (0), g n1 (0), . . . , g n k (0) where k is an arbitrary positive integer, m ≥ n 1 , . . . , n k , H is an k + 1-context made of the symbol h only, and g n represents n nested symbols g. Fact 1. L max is not an RTA language.

Proof. Assume that L max is recognized by an RTA A with n states and d rigid states. We can assume wlog that d < n. Let t ∈ L max be of the form H[t 0 , . . . , t d+1 ] where for each 0 ≤ i ≤ d + 1, t i = g (d+2-i)(n+1) (0). Let r be a run of A on t. We show, by a pumping argument, that for one i ≥ 1, we can increase as much as we want the number of g's in t i , while keeping the term recognized by A (a contradiction).

First, note that the t i 's are pairwise distinct. It follows that there are no rigid states in r at the positions of the symbols h in t, except rigid states which occur only once in r (such rigid states are not affected by a modification of some t i ). Second, a rigid state of A cannot occur twice in some t i . By a pigeonhole principle, it follows that there exists some i > 0 such that the n + 1 smaller (wrt prefix ordering) positions of t i are not labelled by a rigid state in r. Hence, there exists one non-rigid state of A labelling two of these n + 1 positions. Let k be the distance between these two positions. For all j ≥ 0, we can build from r a successful run of A on t ′ j := H[t 0 , . . . , t i-1 , g jk (t i ), t i+1 , . . . , t d+1 ]. But for a j sufficiently large, t ′ j / ∈ L max , a contradiction. 2 3

Pumping Lemma

Following some ideas developed in the proof of Fact 1 above, we propose a weak form, adapted to RTA, of the pumping (or iteration) lemma for TA. Pumping on runs of RTA is not as easy as for standard TA. Indeed, we must take care of the position of rigid states in order to preserve recognizability. For this reason, the transformation of a subterm must be performed in several branches in parallel (instead of one single branch for TA) in order to preserve the rigidity condition. Moreover, we cannot repeat a term containing a rigid state, because the same rigid state cannot label two different positions on the same branch.

Lemma 1. For all RTA A = Q, R, F, ∆ , for all terms t ∈ L(A) such that d (t) > (|Q| + 1)|R|, there exist a context C, two 1-contexts C ′ and D, with D non-trivial (non-variable), and a term u

such that t = C C ′ [D[u]], . . . , C ′ [D[u]] and for all n ≥ 0, C C ′ [D n [u]], . . . , C ′ [D n [u]] ∈ L(A).
Proof. Let t ∈ L(A) be such that d (t) > (|Q| + 1)|R|, let r be a successful run of A on t, and let p be a position in Pos(t) of length at least (|Q| + 1)|R|.

With the rigidity condition in the definition of successful runs, a rigid state can occur at most once on a path of r. Hence, there exist two positions p 0 < p ′ 0 < p such that |p ′ 0 | -|p 0 | > |Q| and no rigid state occurs between p 0 and p ′ 0 in r. By a pigeon-hole principle, there exist two positions p 1 , p 2 with p 0 ≤ p 1 < p 2 ≤ p ′ 0 labeled with the same state of Q \ R in r. We let u := t| p2 and D = (t| p1 )[x 1 ] p2-p1 . This situation is depicted in Figure 1.

In order to preserve the property of being a run while iterating D, we need to take care of rigid states above p 0 in r (rigid states below p ′ 0 and below D are not affected by iteration of D). Let π 1 be the maximal position of a rigid state in r smaller than p 0 wrt the prefix ordering. Let q r = r(π 1 ) and let π 2 , . . . , be the other positions of q r in r. Note that by definition of r being a run, the positions π 1 , . . . , π k are pairwise incomparable wrt the prefix ordering. We let

π k C π 1 C ′ p 1 D p 2 u π 2 . . . π n
C = t[x 1 ] π1 . . . [x k ] π k and C ′ = (t| π1 )[x 1 ] p1-π1 (
C C ′ [D n [u]], . . . , C ′ [D n [u]] ∈ L(A). 2
As usual, such a lemma can be used to show that a language is not in RTA.

Example 7. As a consequence of the above pumping lemma, we can show that the set B of balanced binary trees built over the signature {a : 0, f : 2} is not an RTA language. Assume indeed that it is recognized by an RTA A = Q, R, F, ∆ and let t ∈ L(A) such that d (t) > (|Q| + 1)|R| and C, C ′ , D, u be as in Lemma 1. By hypothesis,

C ′ [D[u]] is balanced, but for any n > 1, C ′ [D n [u]]
is not balanced since C ′ and D are not trivial. It contradicts the fact that

C C ′ [D n [u]], . . . , C ′ [D n [u]] ∈ L(A) by Lemma 1. 3

Related Classes of Tree Automata

We shall present below some other classes of automata strictly more expressive than the standard TA, and compare their expressiveness to RTA. The decidability and complexity results presented in Section 6 and summarized in Table 1 also offer a base of comparison.

TAGED

Tree Automata with General Equality and Disequality constraints [START_REF] Filiot | Tree automata with global constraints[END_REF] were introduced in the context of spatial logics for XML querying [START_REF] Filiot | Satisfiability of a spatial logic with tree variables[END_REF]. They are defined, like RTA, by an underlying TA, but instead of having simply a set of rigid state for testing equality, they have two binary relations on states: R = for testing equalities and R = for disequalities. More precisely, a run r of a TAGED on a term t is a run of the underlying TA on t with the additional condition that for all p 1 , p 2 ∈ Pos(t), if r(p 1 ), r(p 2 ) ∈ R = then t| p1 = t| p2 and if r(p 1 ), r(p 2 ) ∈ R = then t| p1 = t| p2 .

TAGED are strictly more general than RTA. The emptiness problem has been shown decidable for the class of negative TAGED (such that R = = ∅) [START_REF] Filiot | Tree automata with global constraints[END_REF], and a subclass of TAGED where the number of disequalities tested on every path is bounded [START_REF] Filiot | Satisfiability of a spatial logic with tree variables[END_REF]. More recently, emptiness was shown decidable for a class of TA with constraints strictly larger than TAGED [START_REF] Barguñó | The emptiness problem for tree automata with global constraints[END_REF].

The fragment of positive TAGED (with R = = ∅, denoted TAGED+) has the same expressiveness as RTA. This is shown in [START_REF] Filiot | Tree automata with global constraints[END_REF] where a construction is proposed for transforming any TAGED+ into an RTA (i.e. a TAGED with a reflexive relation R = ) recognizing the same language, at the price of an exponential blowup. The transformation of [START_REF] Filiot | Tree automata with global constraints[END_REF] was originally proposed in order to show the decidability of emptiness for TAGED+. This result is reused in the proof of Theorem 1 below.

Proposition 2 ([6]

). For all TAGED+ A, there exists an RTA A ′ of size exponential in the size of A, constructed in exponential time, and such that

L(A ′ ) = L(A).
The emptiness problem is EXPTIME-complete for TAGED+, and PTIME for RTA (see Section 6). To our knowledge, the rewrite closure of TAGED has not been studied so far.

TA with Equality Constraints

TA with equality constraints (TAC) are TA whose transitions can perform local equality and disequality tests on the subterms of the term in input (see e.g. [START_REF] Bogaert | Equality and disequality constraints on direct subterms in tree automata[END_REF][START_REF] Dauchet | Automata for Reduction Properties Solving[END_REF]). More precisely, a TAC Q, F, ∆ is defined by a finite set of states Q, a subset of final states F and a set ∆ of transitions of the form f (q 1 , . . . , q n ) -→ c q where f ∈ Σ n , q 1 , . . . , q n , q ∈ Q, and c is a conjunction of constraints of the form π = π ′ or π = π ′ where π and π ′ are positions (sequences of positive integers). A run of a TAC on a term t is a function r : Pos(t) → Q such that for all p ∈ Pos(t) with t(p) = f ∈ Σ n (n ≥ 0), there exists a transition f r(p • 1), . . . , r(p • n) -→ c r(p) ∈ ∆ such that for all constraints π = π ′ (resp.

π = π ′ ) in c, we have p • π, p • π ′ ∈ Pos(t) and t| p•π = t| p•π ′ (resp. t| p•π = t| p•π ′ ).
A TAC is called positive if all its transitions contain only equalities. The class of positive TAC is called TAC+. Note that the RTA language of Examples 1 and 2 are recognizable by TAC+:

A = {q, q f }, {q f }, {a → q, b → q, f (q, q) → q, f (q, q) ---→ 1=2 q f }
for Example 1, and the same extended with the transitions f (q, q f ) → q f , f (q f , q) → q f for Example 2.

The emptiness problem is undecidable in general [START_REF] Mongy | Transformation de noyaux reconnaissables d'arbres[END_REF] for TAC+. Two decidable subclasses of TAC have been identified: tree automata with equality and disequality tests between brother positions [START_REF] Bogaert | Equality and disequality constraints on direct subterms in tree automata[END_REF] (BTTA) and Reduction Automata [START_REF] Dauchet | Automata for Reduction Properties Solving[END_REF] (RA); the complexity of emptiness is at least EXPTIME for these subclasses.

The equality tests of TAC are performed locally, but can involve an unbounded number of subterms (yielding undecidability of emptiness). In contrast, the equality tests of RTA can be global, but can involve only a bounded number of subterms (the bound is the number of rigid states). Hence it is not surprising that the languages of these two classes of automata are incomparable. Proposition 3. The classes of languages of TAC+ and RTA are orthogonal.

Proof. The RTA languages of Examples 3 and 4 are not recognizable by a TAC. The language B of Example 7 is not recognizable by an RTA but it is recognizable by the TAC+: A = {q}, {q}, {a → q, f (q, q) ---→ 1=2 q} . 2

DAG Automata

DAG automata (DA) [START_REF] Charatonik | Automata on DAG Representations of Finite Trees[END_REF] are defined as TA computing on the representation of terms as directed acyclic graphs (DAG) with maximal sharing. In some sense, RTA are the dual of DA. Indeed, in the runs of DA, a unique state is associated to equal subtrees (which are rooted by the same node in the DAG representations) whereas for RTA, a unique subtree is associated to every occurrence of the same rigid state. However, for DA, the state condition for equal subtrees must be enforced for every state (since DAG-representation with maximal sharing are considered), whereas the "dual" rigidity condition of RTA must only be enforced for rigid states. Consequently, the languages defined are incomparable. Proof. On the one hand, one can observe that the language of the DAG representations of the terms of the RTA language of Example 1, L = {f (t, t) | t ∈ T (Σ)}, is not recognizable by a DA. Assume by contradiction that it is recognized by a DA A with n states and let t be a term of depth strictly greater than n. By hypothesis, there exists a run r of A on the DAG representation of the term f (t, t). Since there is a path in t of length strictly greater than n, there exists two different nodes v 1 and v 2 in the DAG representation of t that are labelled with the same state q in the run r. Let t 1 and t 2 be the subterms of t whose DAG representations are the subgraph rooted respectively in v 1 and v 2 , and let t ′ be the term obtained form t by replacement of every occurrence of t 1 by t 2 . Since both DAG representations of t 1 and t 2 are recognized by A in the same state q, any term containing some occurrences of t 1 recognized by A, is still recognized by A if you replace any number of occurrences of t 1 by t 2 . Then, the DAG representation of f (t, t ′ ) is recognized by A. Since t = t ′ , this is a contradiction and we conclude that there does not exist a DA recognizing the language of DAG representations of the terms of the RTA language L.

On the other hand, the language of DAG-representations of the terms of L max of Example 6 (which is not recognizable by an RTA), is recognized by the following DA (we admit that for the terms t = H[t 0 , . . . , t n ] of L max , the context H can be empty. In this case, t is reduced to t 0 ): A = {q, q ′ }, {q ′ }, {0 → q, s(q) → q|q ′ , h(q, q) → q, h(q ′ , q) → q ′ } With this DA, a term t = H[t 0 , . . . , t n ] is accepted in q ′ iff t 0 is accepted in q ′ and every t i , for i > 0 is accepted in q. Moreover, since t is put in DAG form with maximal sharing for the computation of A, and q ′ can only be reached through q, every t i , for i > 0 is a strict subterm of t 0 , meaning that t ∈ L max .2 Note also that the emptiness problem is PTIME for RTA and NP-complete for DA [START_REF] Charatonik | Automata on DAG Representations of Finite Trees[END_REF]. Moreover, deterministic DA coincide with DTA, and, as we show in Section 5.1, it is not the case for DRTA. Actually, DA and RTA are defined for different purposes: DA are proposed for computing on compressed trees, and not for checking equalities like RTA.

TA1M

Like pushdown tree automata [START_REF] Guessarian | Pushdown tree automata[END_REF], TA with one memory (TA1M) [START_REF] Comon | Tree automata with one memory, set constraints and cryptographic protocols[END_REF][START_REF] Comon-Lundh | Visibly tree automata with memory and constraints[END_REF] are TA extended in order to carry an unbounded amount of information along the states in computations. But instead of a stack, a TA1M stores this information in a memory with a tree structure. More precisely, this memory contains a ground term over a memory signature Γ. The memory is updated during the bottom-up computations. The general form of the transitions of TA1M is

f q 1 (m 1 ), . . . , q n (m n ) → q(m)
where f ∈ Σ n , q 1 , . . . , q n , q are states with an argument carrying the memories m 1 , . . . , m n , m ∈ T (Γ, X ). The new current memory m is built from the memories m 1 , . . . , m n which have been reached at the positions immediately below the current position of computation. For instance, in the following push transition, the new current memory m is built by pushing a symbol h ∈ Γ n at the top of memories m 1 , . . . , m n (which are variables x 1 , . . . , x n in this case):

f q 1 (x 1 ), . . . , q n (x n ) → q h(x 1 , . . . , x n ) . (push)
In a pop transition, the new current memory is a subterm of one of the memories reached so far:

f q 1 (x 1 ), . . . , q i (h(y 1 , . . . , y k )), . . . , q n (x n ) → q(y j ) (pop)
The top symbol h of m i is also read in the above pop transition. In an internal transition, the new current memory is one of the memories reached:

f q 1 (x 1 ), . . . , q n (x n ) → q(x i ) (internal) with 1 ≤ i ≤ n.
Moreover, TA1M can perform equality tests on the memory contents, with transitions like

f q 1 (x 1 ), . . . , q n (x n ) ----→ xi=xj q(x k ) (internal = )
where 1 ≤ i, j, k ≤ n. This ability makes possible the simulation of some tests of the TA with constraints (by storing some subterms in memory and comparing them), with a limitation to local tests (like for TAC).

Proposition 5. The classes of languages of TA1M and RTA are orthogonal.

Proof. Let Σ = {a : 0, g : 1, f : 2}. The language

L = {f (g n (f (s, t)), f (s, g n (f (s, t)))) | s, t ∈ T (Σ), n ≥ 1}
is recognized by the following RTA

A = {q, q s , q 1 , q r , q 2 , q f }, {q s , q r }, {q f },    a → q|q s , g(q) → q|q s , f (q, q) → q|q s , f (q s , q) → q 1 , g(q 1 ) → q 1 |q r , f (q s , q r ) → q 2 , f (q r , q 2 ) → q f   
The language L cannot be recognized by a TA1M. The reason is that, in order to recognize a term of the language, the automata needs to test equalities between i) the two subterms g n (f (s, t)) and ii) the two subterms s in the right side of every term of L. For i, it would need to store g n (f (s, t)) in its memory but for ii, it would also need to have s stored at the same time, which is not possible, since the memory can only store one term at a time.

Let us now consider Σ ′ = {a : 0, g : 1, h : 1, f : 2} and the language L ′ = {f (g n (a), h n (a)) | n ≥ 0}. This language is recognized by the TA1M with the following 4 push transitions and 1 test transition (q f is the only final state):

a → q g (a)|q h (a), g(q g (x 1 )) → q g (g(x 1 )), h(q h (x 1 )) → q h (g(x 1 )), f (q g (x 1 ), q h (x 2 )) -----→ x1=x2 q f (x 1 )
Note that the above transitions can only push the symbol g, whenever g or h is read. The states q g and q h permit to differentiate between g n (a) and h n (a). As a consequence of the pumping Lemma 1, the language L ′ is not recognized by an RTA. 2

Automatic Clauses with Rigid Variables

In this section, we show that the languages of rigid tree automata can alternatively be defined as finite set of Horn clauses with rigid variables [START_REF] Andrews | Theorem proving via general matings[END_REF]. This formalism was used in several related works [START_REF] Delaune | Protocol verification via rigid/flexible resolution[END_REF][START_REF] Affeldt | Verification of security protocols with a bounded number of sessions based on resolution for rigid variables[END_REF]. These papers do not mention the name of tree automata, but they are targeted at the same application as the one presented in Section 8: the static analysis of security protocols.

Following [START_REF] Frühwirth | Logic programs as types for logic programs[END_REF], it is a common approach to represent tree automata by Horn clause sets. A tree automata transition f (q 1 , . . . , q n ) → q can indeed be encoded into the following first order Horn clause (variables are implicitly universally quantified)

q 1 (y 1 ), . . . , q n (y n ) ⇒ q f (y 1 , . . . , y n ) (reg)
where y 1 , . . . , y n are distinct variables and q 1 , . . . , q n , q are unary predicate symbols. Let us call regular clauses the Horn clauses of the above form. Given a finite set C of regular clauses (an automaton in these settings) and a predicate q (a state), the language of C in q, denoted by L(C, q), is the set of terms t ∈ T (Σ) such that q(t) is a logical consequence of C (q(t) is in the smallest Herbrand model of C). This definition corresponds exactly to the language of the TA whose transitions are encoded by the clauses of C. One advantage of this presentation of tree automata by Horn clause sets is that it permits to use classical first-order theorem proving techniques in order to decide TA problems. For instance, if C is a finite set of regular clauses and t ∈ T (Σ), it holds that t ∈ L(C, q) iff C∪{q(t) ⇒} is inconsistent, and L(C, q) = ∅ iff C ∪ {q(x) ⇒} is inconsistent. These sets can be finitely saturated by a resolution calculus with appropriate strategies [START_REF] Goubault-Larrecq | Deciding H 1 by Resolution[END_REF], hence, the above decision problems can be solved using first order theorem provers.

This approach can also be suitable for studying RTA, by distinguishing, in regular clauses, some variables as so called rigid variables [START_REF] Andrews | Theorem proving via general matings[END_REF]. We use below uppercase letters X, Y... for rigid variables and lowercase x, y... for other variables, called flexible variables. Recently, in [START_REF] Delaune | Protocol verification via rigid/flexible resolution[END_REF][START_REF] Affeldt | Verification of security protocols with a bounded number of sessions based on resolution for rigid variables[END_REF], some models of Horn clauses with rigid variables (including regular clauses) have been studied in the context of the verification of security protocols. We recall the definitions and results of [START_REF] Affeldt | Verification of security protocols with a bounded number of sessions based on resolution for rigid variables[END_REF] in order to establish connections with RTA.

A set C of clauses with rigid variables X 1 , . . . , X n and flexible variables y 1 , . . . , y m is satisfiable if there exists a Σ-algebra A such that for all valuation σ : {X 1 , . . . , X n } → A, there exists a model S with domain A such that S, σ |= ∀y 1 , . . . , y m C. It is equivalent to say that for all valuation σ : {X 1 , . . . , X n } → T (Σ), there exists an Herbrand model L such that L |= ∀y 1 , . . . , y m σ(C).

This semantics permits to redefine the languages of RTA in term of models of regular clauses with rigid variables. Let us consider an RTA A = Q, R, F, ∆ and let us associate a rigid variable X q to each q ∈ R. We associate to A the set C of regular clauses with rigid variables

q 1 (α 1 ), . . . , q n (α n ) ⇒ q f (α 1 , . . . , α n ) (reg')
such that f (q 1 , . . . , q n ) → q ∈ ∆ and for all i ≤ n, α i = X qi if q i ∈ R and α i is a flexible variable y i otherwise. Then, we have (X = {X q | q ∈ R})

σ:X→T (Σ) L σ(C), q = L(A, q).
In [START_REF] Affeldt | Verification of security protocols with a bounded number of sessions based on resolution for rigid variables[END_REF], a translation of clauses with rigid variables into first order clauses (without rigid variables) preserving satisfiability is proposed. In the case of the above regular clause with rigid variables (reg'), the translation returns

q 1 (x, α ′ 1 ), . . . , q n (x, α ′ n ) ⇒ q x, f (α ′ 1 , . . . , α ′ n )
where x = (x q ) q∈R is a sequence of |R| flexible variables, one variable x q for each rigid state q ∈ R (hence one for each rigid variable X q ). Every variable α ′ i , i ≤ n, is either x qi if α i is the rigid variable X qi (i.e. if q i ∈ R) and α ′ i is the (flexible) variable α i = y i otherwise. Such clauses can alternatively be seen as transitions of tree automata extended with |R| auxiliary registers storing terms of T (Σ). For such an automaton, the values are stored in the registers once and for all at the beginning of the computation (in the variables of x) and during the application of a transition, the current subterm can be compared to the content of one register (in the case where α ′ i = y i ). It is shown in [START_REF] Affeldt | Verification of security protocols with a bounded number of sessions based on resolution for rigid variables[END_REF] that binary resolution with an appropriate ordered strategy terminates on clauses of the above form as long as there is only one unary predicate; [START_REF] Affeldt | Verification of security protocols with a bounded number of sessions based on resolution for rigid variables[END_REF] consider also other kinds of clauses; some of them can be seen as a generalisation of RTA to two way and alternating rigid tree automata.

Hence, in the result of [START_REF] Affeldt | Verification of security protocols with a bounded number of sessions based on resolution for rigid variables[END_REF], termination is limited to automata with one state. The resolution strategy of [START_REF] Affeldt | Verification of security protocols with a bounded number of sessions based on resolution for rigid variables[END_REF] does not terminate on automata with more than one state and a terminating resolution strategy for this case is not known. Some progress in this direction would enable the application of first order theorem proving techniques to decision problem for RTA. This could permit in particular to consider extensions of RTA with e.g. equational tests or language modulo equational theories, like what was done in [START_REF] Jacquemard | Tree automata with equality constraints modulo equational theories[END_REF] for standard tree automata using a Horn clauses approach and a paramodulation calculus. In particular, the latter extension (modulo equational theories) is related to the problem of Section 7.3, and in this context, first order theorem proving tools could provide an efficient alternative to the complicated decision algorithm described in Section 7.3.

Boolean Closure

We show below that the class of RTA languages is closed under union and intersection but not under complement. Proof.

Let A i = Q i , R i , F i , ∆ i with i = 1, 2. For L(A 1 ) ∪ L(A 2 )
, we do a classical disjoint union of automata. Let us assume wlog that the state sets Q 1 , Q 2 of A 1 and A 2 are disjoint. Like for the union of TA, the RTA A is obtained by disjoint union of the state sets, rigid state sets, final state sets and transitions sets.

For L(A 1 ) ∩ L(A 2 ), it is easy to construct a TAGED+ A ′ (see Section 3.1) recognizing L(A 1 ) ∩ L(A 2 ) by a Cartesian product operation like for standard TA. The state set of

A ′ is Q 1 × Q 2 , its final state set F 1 × F 2 and its set of transition rules is f q 11 , q 21 , . . . , q 1n , q 2n → q 1 , q 2 | q i1 . . . q in , q i ∈ Q i , | f (q i1 , . . . , q in ) → q i ∈ ∆ i , i = 1, 2 .
Moreover, the equality relation of

A ′ is R = = q r1 , q 2 , q r1 , q ′ 2 | q r1 ∈ R 1 , q 2 , q ′ 2 ∈ Q 2 ∪ q 1 , q r2 , q ′ 1 , q r2 | q 1 , q ′ 1 ∈ Q 1 , q r2 ∈ R 2 .
We can use Proposition 2 of [START_REF] Filiot | Tree automata with global constraints[END_REF] in order to transform this TAGED+ into an RTA recognizing the same language, at the price of an exponential blowup. Combining the two above steps results in an exponential construction for the intersection of RTA.

2

The following lemma shows that the exponential time complexity for the construction of the intersection automaton in Theorem 1 is a lower bound, with a reduction of the EXPTIME-complete problem of the non-emptiness of the intersection of n TA.

Lemma 2. Given n TA A 1 , . . . , A n on Σ, we can compute in polynomial time two RTA A × and A r , both of size O |A 1 | + . . . + |A n | , and such that L(A 1 ) ∩ . . . ∩ L(A n ) = ∅ iff L(A × ) ∩ L(A r ) = ∅. Proof. Let Σ d = Σ ⊎ {0 : 0, d : 2}. Both the RTA constructed will compute on Σ d . Let A r = {q, q r , q f }, {q r }, {q f }, {0 → q f , d(q r , q f ) → q f }∪{f (q, . . . , q) → q|q r | f ∈ Σ} . It recognizes the set of right combs of the form d(t, d(t, . . . d(t, 0))) with t ∈ T (Σ). Let A i = Q i , R i , F i , ∆ i for all 1 ≤ i ≤ n. We assume wlog that Q 1 , . . . , Q n are disjoint and that for each i ≤ n, F i = {q i }. Let A × = n i=1 Q i ⊎ {q 0 , q ′ 1 , . . . , q ′ n }, n i=1 R i , {q ′ 1 }, ∆ × , with ∆ × = n i=1 ∆ i ⊎ {0 → q 0 , d(q n , q 0 ) → q ′ n } ∪ n-1 i=1 d(q i , q ′ i+1 ) → q ′ i .
This RTA A × recognizes the set of right combs of the form d(t 1 , . . . d(t n , 0))) with t i ∈ L(A i ) for all i ≤ n. Hence L(A × ) ∩ L(A r ) is exactly the set of right combs d(t 1 , . . . d(t n , 0))) such that t i ∈ L(A i ) for all i ≤ n and t 1 = . . . = t n . Therefore, this intersection is empty iff L(A 1 ) ∩ . . . ∩ L(A n ) is empty as well. 2

Note that the above construction also works (hence Lemma 2 also holds) for n given RTA. With Lemma 2, we have a polynomial time reduction into the nonemptiness of the intersection of two RTA of the problem of the intersection nonemptiness for n TA (given n TA A 1 , . . . , A n , do we have

L(A 1 ) ∩ . . . ∩ L(A n ) = ∅?).
The latter problem is known to be EXPTIME-complete [START_REF] Seidl | Haskell overloading is dexptime-complete[END_REF]. Since by Theorem 1, the intersection of two RTA is an RTA, and the emptiness of RTA can be decided in linear time (Theorem 8 below), we conclude that EXPTIME is a lower bound for the construction of an RTA for the intersection. Moreover, in the above construction,

A × is a TA if every A i (1 ≤ i ≤ n) is a TA.
Hence the intersection of an RTA with a TA also leads to an exponential construction.

Complement

Theorem 2. The class of RTA languages is not closed under complement.

Proof. We have seen in Example 7 that the set B of balanced binary trees over Σ := {a : 0, f : 2} is not an RTA language. We show that its complement B in T (Σ) is an RTA language. The idea is similar to the construction for the subterm relation in Example 4: one rigid state q r is used to choose nondeterministically a subterm, and it is checked that the sibling of q r contains q r at depth more than one (such subterms are characterised by the state q ′ below). More precisely, the RTA for B is {q, q r , q ′ , q f }, {q r }, {q f }, ∆ with

∆ =        a → q|q r , f (q, q) → q|q r , f (q, q ′ ) → q ′ , f (q, q r ) → q ′ , f (q r , q) → q ′ , f (q ′ , q) → q ′ , f (q r , q ′ ) → q f , f (q ′ , q r ) → q f , f (q f , q) → q f , f (q, q f ) → q f       
.

The last two transition rules ensure the propagation of the final state q f up to the root, like in Example 2. 2

Deterministic and Visibly Rigid Tree Automata

Non-determinism is crucial for an RTA recognizing the terms of the form f (t, t) like in Example 1. Indeed, in a bottom-up computation, such an automaton needs to guess both positions of the two occurrences of t under the symbol f , and put one rigid state at these positions.

Example 8. Let us come back to Example 1, where Σ = {a:0, b:0, f :2} and the RTA A with transition set {a → q|q r , b → q|q r , f (q, q) → q|q r , f (q r , q r ) → q f } recognizing {f (t, t) | t ∈ T (Σ)}. Applying a classical subset construction to the transition set of A returns a deterministic set of transitions a → {q, q r }, b → {q, q r }, f {q, q r }, {q, q r } → {q, q r , q f }, f {q, q r , q f }, {q, q r , q f } → {q, q r , q f } .

However, it is not possible to choose a subset of rigid states amongst the two states obtained, in order to recognize the above language. 3

We show in this section that RTA can not be determinized in general, and propose a subclass for which a determinization is possible, though it is still not closed under complement.

Determinism and Completeness

Definition 3. A deterministic rigid tree automaton (DRTA) (resp. complete RTA) on a signature Σ is an RTA A whose underlying TA ta(A) is deterministic (resp. complete).

Like standard TA, every RTA can be completed into a complete RTA, by the addition of a trash state. Theorem 3. For every RTA A, a complete RTA A ′ of size polynomial in |A| and such that L(A ′ ) = L(A) can be constructed in PTIME from A.

Proof. Let A = Q, R, F, ∆ . We use the same construction as for standard TA, adding a state q ⊥ which is neither final nor rigid:

A ′ = Q∪{q ⊥ }, R, F, ∆ ⊥ with ∆ ⊥ = ∆ ∪ f (q 1 , . . . , q n ) → q ⊥ | f ∈ Σ n , q 1 , . . . , q n ∈ Q, ∀q ∈ Q, f (q 1 , . . . , q n ) → q / ∈ ∆ ∪ f (q 1 , . . . , q n ) → q ⊥ | f ∈ Σ n , q 1 , . . . , q n ∈ Q ∪ {q ⊥ }, ∃i ≤ n, q i = q ⊥ . 2
However, unlike standard TA, it is not true in general that for a complete RTA A, for every term t there exists at least one run of A on t. Indeed, a run of ta(A) on t might not be a run of A on t because of the rigidity condition.

Example 9. The RTA A = {q, q r }, {q r }, {q}, {a → q, g(q) → q r , g(q r ) → q} is deterministic and complete. The term t = g(g(g(a))) is in L ta(A), q r , it is accepted with a unique (TA) run r = q r (q(q r (q))). However, r is not a run of the RTA A, because the two subterms at the positions of q r are distinct.

3

It is well-known that DTA are as expressive as TA, and that every TA can effectively be determinized, at the price of an exponential blowup. We show below that it is not the case for RTA: the class of DRTA languages is strictly included in the class of RTA languages. We show now that L is not recognized by a DRTA. Assume that there is a DRTA A = Q, R, F, ∆ recognizing L. On any run r of A, on any tree, each rigid state can only appear once on a path; otherwise it would not respect the rigid condition. Hence there is at most |R| occurrences of rigid states on every path. Let t be a tree on which there exists a (unique) run r of A, and let p ∈ Pos(t) be a path from the root to a leaf which contains a maximal number of rigid states in r.

We build a tree t ′ such that there exists a position p ′ ∈ Pos(t ′ ), |p ′ | > |Q| -|R| and t ′ | p ′ = t. Since f (t ′ , t ′ ) is recognized by A, there exists a (unique) run r ′ on t ′ . Since A is deterministic, we know that r ′ | p ′ = r. Hence there exists a path in r ′ from the position p ′ to a leaf that contains the maximal number of rigid states. So for each strict prefix

p ′ 0 of p ′ , r ′ (p ′ 0 ) ∈ Q \ R. Since |p ′ | > |Q|-|R|, there exists two strict prefixes p ′ 1 , p ′ 2 of p ′ , such that p ′ 1 is a strict prefix of p ′ 2 and r ′ (p ′ 1 ) = r ′ (p ′ 2 ). Let t ′′ be the tree t ′ [t ′ p ′ 2 ] p ′ 1 .
This construction is illustrated in Figure 2.

Then

r ′′ = r ′ [r ′ p ′ 2 ] p ′
1 is a valid run of A on t ′′ : no rigid states occur between the root and p ′ 1 , and between p ′ 1 and p ′ 2 , so a position p ′ 3 of an occurrence of a rigid state was either • a position incomparable (wrt prefix ordering) with p ′ 1 , which still exists with the same subtree and the same rigid states in t ′′ ,

t ′ = t ′ 0 p ′ 1 t ′ 1 p ′ 2 t ′ 2 p ′ t t ′′ = t ′ 0 p ′ 1 t ′ 2 t Figure 2: Proof that DRTA RTA • a position p ′ 2 • π, π ∈ Pos(t ′ | p ′ 2 )
, and then the position p ′ 1 • π in t ′′ has the same subtree and the same rigid state,

• a position p ′ 1 • π, π ∈ Pos(t ′ | p ′ 1 )
, where π is not a suffix of p ′ 2 , and in this case, this occurrence of the rigid states disappears in t ′′ . Therefore, r ′′ satisfies the rigid condition on every rigid state of R. Since r ′′ (ε) = r ′ (ε), A recognizes the tree f (t ′′ , t ′ ) which is not in L.

2

Moreover, the class of regular tree languages is strictly included into the class of DRTA languages.

Theorem 5. TA DRTA.

Proof. The inclusion TA ⊂ DRTA is immediate since DTA ≡ TA and DTA are particular cases of DRTA.

Let Σ = {a : 0, g : 1, f : 2}. The language f (g(t), g(t)) | t ∈ T (Σ \ {g} is recognized by the DRTA A = {q, q r , q f }, {q r }, {q f }, a → q, f (q, q) → q, g(q) → q r , f (q r , q r ) → q f } .

But this language if not regular. 2

Visibly Rigid Tree Automata

We propose here a class of restricted RTA which can be determinized. The definition of the restriction is inspired by the theory of visibly pushdown automata (VPA) [START_REF] Alur | Visibly pushdown languages[END_REF]. VPA define a subset of context-free languages closed under intersection and complement. They were generalized to tree recognizers in [START_REF] Chabin | Visibly pushdown languages and term rewriting[END_REF][START_REF] Comon-Lundh | Visibly tree automata with memory and constraints[END_REF]. The idea in these works is that the signature Σ is partitioned into Σ = Σ c ⊎Σ r ⊎Σ ℓ and the operation performed by the VPA on the stack depends on the current symbol in the input: if it is a call symbol of Σ c , the VPA can only do a push, for a return symbol of Σ r it can do a pop and it must leave the stack untouched for a local symbol of Σ ℓ . The transitions of a VPA follow this discipline. There exists a determinization for this subclass of pushdown automata, and it is closed under intersection and complement.

The RTA use no auxiliary stack but they permit the comparison between subterms based on the rigid states. Hence, a natural way for defining a condition similar to the one of visibly pushdown automata, and enabling determinization for some RTA, is to restrict the rigid states that can be reached according to the function symbol in the input. In that sense, the rigidity of the states is made visible by the input signature. Definition 4. A visibly rigid tree automaton (VRTA) is an RTA A = Q, R, F, ∆ on a signature Σ such that there exists a partial function ν from Σ to R such that for every transition f (q 1 , . . . , q n ) → q ∈ ∆, q = ν(f ) if ν is defined on f and q ∈ Q \ R otherwise.

Example 10. The RTA of Example 3 is visibly rigid, with a function ν defined only on g by ν(g) = q r . The DRTA in the above proof of Theorem 5 is also visibly rigid, with the same function.

Conversely, the RTA of Example 1 (recognizing the terms f (t, t) with t ∈ T {a : 0, b : 0, f : 2} is not visibly rigid. Intuitively, some non-determinism is needed for the bottom-up recognition of this language (because t may contain the symbol f ), and it is not compatible with the visibly rigid condition. Indeed, the above language is not regular, hence at least one rigid state is necessary for the definition of a RTA recognizing it. Defining rigid states for ν(a) and ν(b), is pointless (it can be simulated by standard tree automata). Hence,ν(f ) must be defined in order to ensure the visibly rigid condition, but this would contradict the recognition a term such as e.g. f (f (a, a), f (a, a)).

3

With the visibly rigid condition, a determinization procedure can be applied to VRTA.

Theorem 6. Given a VRTA A on Σ, a deterministic VRTA A ′ on Σ of size exponential in |A| and such that L(A ′ ) = L(A) can be constructed in exponential time.

Proof. The RTA A ′ is obtained by a classical subset construction. Let A = Q, R, F, ∆ and let

A ′ = 2 Q , 2 R , {S ⊆ Q | S ∩ F = ∅}, ∆ ′ with ∆ ′ = f (S 1 , . . . , S n ) → S | S 1 , . . . S n , S ⊆ Q, S = {q ∈ Q | ∃q 1 ∈ S 1 , . . . , ∃q n ∈ S n , f (q 1 , . . . , q n ) → q ∈ ∆ .
The RTA A ′ is deterministic. Moreover, because of the visibly rigid condition for A, every state of A ′ occurring in ∆ (i.e. every state of A ′ with a non empty language) is either a subset of Q \ R (and it is not a rigid state of A ′ ) or is a singleton subset of R (and it is a rigid state of A ′ ). Hence, given a function ν associated to the VRTA A like in Definition 4, there exists a function ν ′ making A ′ a VRTA, defined by ν

′ (f ) = {q r } iff ν(f ) = q r ∈ R.
We can show by induction on t ∈ T (Σ) that there exists a run r of A on t iff there exists a run r ′ of A ′ on t such that for all p ∈ Pos(t), r(p) ∈ r ′ (p). The part of the proof which is specific to (V)RTA concerns the rigidity condition, and uses the above observation about the states of A ′ : all the rigid states in a run r ′ of A ′ are singleton subsets of R. Hence, for the if direction, given a run r ′ of A ′ on t, every relabeling r : Pos(t) → Q extracted from r ′ (i.e. such that r(p) ∈ r ′ (p), p ∈ Pos(t)) satisfies the rigidity condition. Similarly, for the only if direction, a relabeling r ′ : Pos(t) → 2 Q embedding a given run r of A on t also satisfies the rigidity condition. It follows that t ∈ L(A) iff t ∈ L(A ′ ).

2

Being able to determinize VRTA is not enough however to ensure the closure of this subclass of RTA under complement. Intuitively, the reason is that for the (unique) run r of a deterministic VRTA to be successful, a conjunction of two conditions must be realized: the top state of r must be final and the rigidity condition has to be enforced. In comparison, for a TA, only the first condition is necessary, and in order to construct the complement of a deterministic and complete TA, an inversion of final and non final states is sufficient. But in order to characterize the complement of a VRTA language, the disjunction of the negation of the two above conditions is necessary, and VRTA are not expressive enough in order to characterize a term not satisfying a rigidity condition.

Theorem 7. The class of VRTA languages is not closed under complement.

Proof. Let us consider the language L g of Example 3: the set of terms t ∈ T (Σ), with Σ = {a : 0, g : 1, f : 2}, such that s 1 = s 2 for every two subterms g(s 1 ), g(s 2 ) of t. L g is recognized by the VRTA A given in Example 3 but its complement is not a language of VRTA.

Assume that the complement T (Σ) \ L g of L g is recognized by a VRTA A ′ and let ν ′ be the function associated to A ′ like in Definition 4. Since L g is not regular, L(A ′ ) is neither regular, and hence A ′ has to contain at least one rigid state q r such that L(A ′ , q r ) = ∅. Hence, there exists a function symbol h ∈ Σ such that ν(h) = q r . It cannot be g, otherwise A ′ would not be able to recognize any term of the form f (g(t 1 ), g(t 2 )) with t 1 = t 2 (such a term is in the complement of L g ). It cannot be f either, otherwise A ′ would not be able to recognize terms of the form f (g(t 1 ), g(t 2 )) with t 1 = f (t 3 , t 4 ) and t 1 = t 2 (those terms are also all is in the complement of L g ). Hence h has to be a, but with rigid states bound to constant symbols, VRTA do not have more expressive power than standard TA. It follows that there does not exist any VRTA A ′ recognizing T (Σ) \ L g . 2

It is not known whether or not, in general, the complement of a VRTA language is an RTA language.

Decision problems

We study in this section several decision problems for RTA: emptiness, membership, intersection non-emptiness, universality, inclusion, equivalence, and finiteness. Table 1 provides a summary of closure and decision results and a comparison with other classes of extended TA mentioned in Section 3.

Emptiness

Emptiness is the problem of deciding, given an RTA A whether L(A) = ∅. We show below that deciding emptiness for an RTA amounts to decide emptiness for the underlying TA.

Theorem 8. The emptiness problem is decidable in linear time for RTA.

Proof. Let A = Σ, Q, R, F, ∆ and let rigid (A) = Σ, Q, Q, F, ∆ be a copy of A where every state is rigid. We show that the emptiness of L(A) and L rigid (A) and L ta(A) are equivalent. The latter problem (emptiness for standard TA) is known to be decidable in linear-time (see e.g. [START_REF] Comon | Tree Automata Techniques and Applications[END_REF]) with an algorithm marking the inhabited states of ta(A) and using an appropriate data structure for the transitions rules. The idea of the proof is that if L(ta(A)) is not empty, then the classical "state marking" algorithm builds a witness which respects the rigidity condition for all states, and is therefore a witness for L(A) non-emptiness.

In order to establish the above equivalence, we use a similar algorithm for A except that every inhabited state q is marked by a witness (minimal) term t q ∈ L(rigid (A), q) and a run r q of rigid (A) on t q . At the beginning, each t q and r q are undefined. Then we iterate the following transformation until it is applicable: if q ∈ Q, t q is undefined, and there exists f (q 1 , . . . , q n ) → q ∈ ∆ such that t q1 , . . . , t qn are all defined, then let t q := f (t q1 , . . . , t qn ) and r q := q(r q1 , . . . , r qn ).

The above step will be repeated at most |Q| times, and using suitable data structures (see [START_REF] Comon | Tree Automata Techniques and Applications[END_REF]) for the representation of transition rules ensures that it runs in linear time (note that the update of t q and r q can be performed in constant times at each step). For all q ∈ Q, the following facts are equivalent: i. t q is defined, ii. L(rigid (A), q) = ∅, iii. L(A, q) = ∅. iv. L(ta(A), q) = ∅.

i ⇒ ii follows from the construction: if t q is defined then r q is a run of L(rigid (A)) on t q . This can be shown e.g. by induction on the number of iteration steps before t q is defined.

ii ⇒ iii and iii ⇒ iv are immediate, because by definition we have L(rigid (A), q) ⊆ L(A, q) ⊆ L(ta(A), q). iv ⇒ i can be shown by induction on the number of transition rules of A. This procedure terminates and at the end, t q is defined iff L(rigid (A), q) = ∅ iff L(A, q) = ∅ iff L(ta(A), q) = ∅. 2

Membership

Membership is the problem of deciding, given an RTA A and a term t ∈ T (Σ), whether t ∈ L(A). A similar proof of the following result (in the case of TAGED) already appeared in [START_REF] Filiot | Tree automata with global constraints[END_REF].

Theorem 9. Membership is NP-complete for RTA ( PTIME for DRTA).

Proof. A non-deterministic algorithm for this problem consists in, given an RTA A and a term t, guessing a labelling of the nodes of t with states of A and checking that this labelling is a successful run of A on t. The checking operation can be performed in polynomial time. In the deterministic case, there is at most one labelling of the term t compatible with the transition rules. It can be computed in PTIME and it can be checked in PTIME that this labelling is a successful run. Hence the membership problem is decidable in PTIME for DRTA.

In order to show NP-hardness for general RTA, we propose a reduction of 3-SAT for a formula φ into the membership for an RTA A and a term t representing φ.

Let us consider an instance φ of 3-SAT with variables from a set V . It is represented as a term t over the signature Σ = {0, 1 : 0, ¬ : 1

∧ :2, ∨ : 3} ∪ {x : 2 | x ∈ V }. Every variable x is represented by a subterm x(0, 1), a 3 literal clause ℓ 1 ∨ ℓ 2 ∨ ℓ 3 is encoded into ∨(t 1 , t 2 , t 3 ) where t 1 , t 2 , t 3 encode respectively ℓ 1 , ℓ 2 , ℓ 3 . Finally we encode a conjunction of disjunctions D 1 ∧ • • • ∧ D n into ∧(t 1 , . . . , ∧(t n-1 , t n )) where each t i , i ≤ n, is the encoding of D i .
For instance, the tree encoding of the 3-SAT instance (x ∨ y ∨ z) ∧ (¬x ∨ y ∨ t) ∧ (¬y, ¬t, z) is depicted in Figure 3.

∧ ∨ x 0 1 y 0 1 z 0 1 ∧ ∨ ¬ x 0 1 y 0 1 t 0 1 ∨ ¬ x 0 1 ¬ t 0 1 z 0 1

We define an RTA

A = Q, R, F, ∆ on Σ by R = {q x , q ¬x | x ∈ V }, Q = {q 1 , q 0 } ∪ R, F = {q 1 }, and ∆ = {0 → q x |q ¬x , 1 → q x |q ¬x | x ∈ V }
∪ {x(q x , q ¬x ) → q 0 , x(q ¬x , q x ) → q 1 | x ∈ V } ∪ {∨(q 0 , q 0 , q 0 ) → q 0 } ∪ {∨(q, q ′ , q ′′ ) → q 1 | at least one of q, q ′ , q ′′ is q 1 , and the others are q 0 } ∪ {¬(q 0 ) → q 1 , ¬(q 1 ) → q 0 } ∪ {∧(q 1 , q 1 ) → q 1 , ∧(q 0 , q 1 ) → q 0 , ∧(q 1 , q 0 ) → q 0 , ∧(q 0 , q 0 ) → q 0 }.

Both the automata A and the tree t are linear in size relatively to the size of the 3-SAT instance φ. The most important transitions of A are those of the two above lines involving the rigid states q x and q ¬x . The states q 0 and q 1 represent the value associated to x (they are propagated bottom-up along t) and the rigidity condition ensures that the same value is associated to all occurrences of the variable x in φ.

Let us show now in detail that A recognizes t iff the corresponding 3-SAT instance φ has a solution.

Assume that the given 3-SAT instance has a solution σ : V → {0, 1} (mapping of propositional variables into truth values). We define a successful run r of A in t as follows. For each variable x ∈ V and for each position p ∈ Pos(t) such that t| p = x, we have by construction of t that t| p.1 = 0 and t| p.2 = 1. If σ(x) = 0, we define r(p.1) = q x and r(p.2) = q ¬x , and if σ(x) = 1, we define r(p.1) = q ¬x and r(p.2) = q x . Both options are possible thanks to the rules 0 → q (¬)x and 1 → q (¬)x , and since we do the same thing for all occurrence of x in t, the rigid condition on q x and q ¬x are satisfied for r. Only one rule can be applied at position p: x(q x , q ¬x ) → q 0 if σ(x) = 0 and x(q ¬x , q x ) → q 1 if σ(x) = 1. Therefore, for all x ∈ V and p ∈ Pos(t) such that t| p = x, r(p) = q σ(x) . It is obvious, considering the other rules of A that there is only one state possible for each other position in r, and that r(ε) = q 1 because σ is a solution. Hence t ∈ L(A).

Conversely, let r be a successful run of A on t. The transition rules of A ensure that t is a representation of the given 3-SAT instance. We show that the rigidity condition on r ensures that this instance is satisfiable. Let x ∈ V and p 1 , p 2 ∈ Pos(t) such that t| p1 = t| p2 = x. By construction of t, t| p1.1 = t| p2.1 = 0 and t| p1.2 = t| p2.2 = 1. Only the two transition rules x(q x , q ¬x ) → q 0 and x(q ¬x , q x ) → q 1 can be applied on p 1 and p 2 . Assume that r(p 1 ) = q 0 , then r(p 1 .1) = q x . If r(p 2 ) = q 1 , then r(p 2 .2) = q x and since t| p1.1 = t| p2.2 it does not respect the rigid condition. So the only possible values are r(p 2 .1) = q x , r(p 2 .2) = q ¬x and r(p 2 ) = q 0 , which respect the rigid condition of both q x and q ¬x . Following the same reasoning, if r(p 1 ) = q 1 then r(p 2 ) = q 1 . So, for all x ∈ V , there exists i x ∈ {0, 1} such that for all p ∈ Pos(t) such that t| p = x, r(p) = q ix . Hence, by the construction of t and A, it is obvious that the mapping σ(x) = i x is a solution for the 3-SAT instance. 2

Intersection non-Emptiness

Intersection non-emptiness is the problem of deciding, given a finite sequence of RTA whether there exists a term recognized by each RTA of the sequence.

Theorem 10. Intersection non-emptiness is EXPTIME-complete for RTA.

Proof. The upper-bound is a consequence of Lemma 2, Theorem 1 and Theorem 8. The lower-bound follows from the EXPTIME-hardness of the problem for TA [START_REF] Seidl | Haskell overloading is dexptime-complete[END_REF]. 2

Universality

Universality is the problem of deciding, given an RTA A on Σ whether

L(A) = T (Σ).
Theorem 11. Universality is undecidable for RTA.

Proof. We reduce the non-existence of a solution of an instance P of the Post Correspondence Problem to the universality of an RTA. This RTA recognizes the set of terms which do not represent a solution of P . It is defined as a disjoint union of RTA, one for each case. Some cases involve the construction of an RTA testing disequalities between unary subterms like in Example 5.

Let Γ be a finite alphabet and P = (u i , v i ) 1≤i≤n be an instance of PCP, with

u i , v i ∈ Γ * . A solution of P is a finite sequence i 1 , . . . , i k (1 ≤ i j ≤ n for all j ≤ k) such that u i1 . . . u i k = v i1 . . . v i k . Let Σ = {⊥ : 0, } ∪ {a : 1 | a ∈ Γ} ∪ {f i : 3 | 1 ≤ i ≤ n}.
For the sake of clarity, a term of the form a 1 (a 2 (. . . a n (t))), with a 1 , . . . , a n ∈ Γ will be denoted a 1 a 2 . . . a n t below.

Every solution of P will be represented by a term of T (Σ). For the definition of this representative, we use two sets U and V of terms of T (Σ) defined recursively as the smallest sets containing ⊥, V contains all f i (u i ⊥, ⊥, v i ⊥) for 1 ≤ i ≤ n, and such that

• if u ∈ U then f i (u i w 1 , u, v i w 3 ) ∈ U for all w 1 , w 3 ∈ T Γ ∪ {⊥} , • if v ∈ V \ {⊥} then f i (u i v| 1 , v, v i v| 3 ) ∈ V .
Note that U is regular and V ⊂ U (but V is not regular). Every solution of P is represented by a term v ∈ V \ {⊥} such that v| 1 = v| 3 .

Given the PCP instance P on Γ, we construct an RTA A on Σ recognizing the set of terms of T (Σ) which are not a representation of solution of P as above. Therefore, L(A) = T (Σ) iff P has no solution. The RTA A is defined as the union of several RTA, each one corresponding to a possible case for a term for not representing a solution of P :

• a TA recognizing the complement of U in T (Σ),

• an RTA recognizing exactly the terms u ∈ U \ {⊥} such that u| 1 = u| 3 .

This RTA can be constructed as the intersection of a TA recognizing U and an RTA similar to the one of Example 5.

• an RTA recognizing exactly U \ V , i.e. the terms of U with a subterm at a position 2 k (for some k ≥ 0) of the form

f i (u i w 1 , f j (w ′ 1 , u ′ , w ′ 3 ), v i w 3 ) with w ′ 1 = w 1 or w ′ 3 = w 3 .
Again, it is the intersection with a TA for U and the union of two RTA testing disequalities, like in Example 5.

2

Together, Theorem 8 and Theorem 11 induce another proof that the class of RTA languages is not closed under complement (the result of Theorem 2).

Inclusion, Equivalence

Inclusion (resp. equivalence) is the problem of deciding, given two RTA A 1 and A 2 on Σ whether

L(A 1 ) ⊆ L(A 2 ) (resp. L(A 1 ) = L(A 2 )).
Theorem 12. Inclusion and equivalence are undecidable for RTA.

Proof. The equivalence problem is reducible to inclusion. Hence both are undecidable as universality is a particular case of equivalence. 2

Finiteness

Finiteness is the problem of deciding, given an RTA A on Σ whether L(A) is finite or not. For an RTA A, the finiteness of L(ta(A)) implies the finiteness of L(A), but the converse is not true: the language of the RTA of Example 9 is {a, g(g(a))} whereas the language of its underlying TA is {a, g 2 (a), g 4 (a), . . .}.

Theorem 13. Finiteness is decidable in PTIME for RTA.

Proof. Like for TA [START_REF] Comon | Tree Automata Techniques and Applications[END_REF], checking finiteness amounts to detecting (in PTIME) some loops and paths in the accessibility graph of an RTA. The accessibility graph of a given RTA A = Q, R, F, ∆ is an oriented graph G A = Q, E A whose set of vertexes is Q and set of edges is E A := { q, q ′ | ∃f (. . . q . . .) → q ′ ∈ ∆}. A path in G A is a finite sequence of states q 1 , . . . , q n such that q i , q i+1 ∈ E A for all 1 ≤ i < n. We have that L(A) is infinite iff there exists a state q ∈ Q \ R such that L(A, q) = ∅, a loop on q in G A (path starting and ending with q) whose states are all in Q \ R, and a path in G A starting with q and ending with a final state of F .

The if direction is easy. The other direction can be shown with arguments similar as those in the proof of Lemma 1. If L(A) is infinite then it contains a term t of depth larger than (|Q| + 1)|R|. The idea is that the loop on q is the path from the variable position up to the root of the context D in a successful run r of A on t, and the path from q to a final state is the path from the root of D up to the root of t in r.

Checking that L(A, q) = ∅ can be done in linear time according to Theorem 8, and deciding the existence of the loop and the path can both be done in polynomial time in the size of A. Altogether, the finiteness of L(A) can be checked in polynomial time. 2

Rewrite Closure

Following the motivations presented in the introduction, we study here the closure under term rewriting of RTA languages. We observe first that in general, the rewrite closure of an RTA language is not an RTA language (Section 7.1) and it is even not recursive (Section 7.2) for linear and collapsing TRS. This is in contrast with TA languages, which are closed under rewriting with such TRS [START_REF] Salomaa | Deterministic tree pushdown automata and monadic tree rewriting systems[END_REF].

We show next that, under a syntactical restriction, namely for a linear and so called inverse visibly pushdown TRS R, it is decidable whether a given tree belongs to the rewrite closure of a given RTA language (Section 7.3).

Linear and Collapsing Rewrite Systems

We show first that the closure of an RTA language under rewriting is not an RTA language, even for a very restricted class of TRS. Proposition 6. In general R * (L) is not an RTA language when L is an RTA language and R a linear and collapsing TRS.

Proof. Let Σ = {h : 2, f : 1, g : 1, 0 : 0}, let R = {f (g(x)) → x}, and let A = Q, R, F, ∆ be the RTA on Σ with Q = {q 0 , q 1 , q 2 , q r , q f }, R = {q r }, F = {q f }, and ∆ = 0 → q 0 , g(q 0 ) → q 0 |q r , f (q r ) → q 1 , f (q 1 ) → q 1 , h(q r , q 1,2 ) → q f , h(q 1,2 , q 1,2 ) → q 2 , h(q f , q 1,2 ) → q f , where q 1,2 is either q 1 or q 2 . Every term of L(A) has the form H g m (0), f * (g m (0)), . . . , f * (g m (0)) where H is an k-context made of the symbol h only (with k ≥ 2), g m represents a nesting of m symbols g and f * represents a nesting of an arbitrary number of f 's. In other word, the leftmost argument of the context H contains m symbols g, and the other arguments of the context consist in an arbitrary number of f 's followed by m g's and finished by a 0. Indeed, the rigid state q r enforces that each argument has the same number of g's.

The terms of the closure R * L(A) of L(A) by R have a similar form except that the number of g's in the different arguments might not be equal. They only have to be all less than or equal to the number of g's in the leftmost argument. The intersection of this set R * L(A) with the regular tree language containing the terms of the form H g * (0), . . . , g * (0) is the language of Example 6, which is not recognized by RTA. It follows that R * L(A) is not an RTA language. 2 Note that the terms H g m (0), g n1 (0), . . . , g n k (0) in the language of Example 6 are R-normal forms in the above counterexample in the proof of Proposition 6 (since they do not contain the symbol f ). Hence, restricting to the terms of the rewrite closure in normal form does not help: the intersection of R * L(A) with R-normal-forms is not an RTA language in general, when A is an RTA and R a linear and collapsing TRS.

Undecidability of Membership Modulo

We show in this section that the rewrite closure of an RTA under a linear collapsing TRS is even not recursive. Let us call membership modulo the problem of deciding whether t ∈ R * (L(A)) given an RTA A, a TRS R and a ground term t ∈ T (Σ). Theorem 14. Membership modulo is undecidable for RTA and linear and collapsing TRS.

Proof. Let Γ be a finite alphabet and let P = (u i , v i ) 1≤i≤n be an instance of PCP, with u i , v i ∈ Γ * . A solution of P is a sequence i 1 , . . . , i m of integers smaller or equal to n such that u i1 . . .

u im = v i1 . . . v im .
Let us consider the signature Σ = {g i : 1,

f i : 1 | i ≤ n} ∪ {a : 1 | a ∈ Γ} ∪ {0 : 0, k : 1, h : 2},
and the language (for all w = a 1 , . . . , a p ∈ Γ * , the term a 1 (. . . a p (t)) is written w(t))

L = {h(s, k(s)) | s = f im (g im (. . . f i1 (g i1 (w(0)), 1 ≤ i 1 , . . . , i m ≤ n, m > 0, w ∈ Γ * }
Let R be a TRS on Σ containing the rules

f i (g i (u i (x))) → x (i ≤ n), g i (x) → x (i ≤ n), g j (f i (v i (x))) → x (i, j ≤ n), k(f i (v i (x))) → x (i ≤ n).
The tree language L is recognizable by an RTA on Σ. Hence the following property permits us to conclude the proof of Theorem 14.

Lemma 3. h(0, 0) ∈ R * (L) iff P has a solution.
The if direction is easy. Let i 1 , . . . , i m be a solution of P and let h(s, k(s)) be the term of L corresponding to this solution (i.e. s = f im (g im (. . . f i1 (g i1 (w(0))))) and w = u i1 . . . u im (0) = v i1 . . . v im (0)). This term is depicted in Figure 4. The s in the left branch can be reduced to 0 using the first rule of R, and the s in the second branch can be reduced to k(f im (v im (0))) using the two next rules of R. This latter term is in turn reduced to 0 using the last rule of R. For the only if direction, assume that L ∋ h(s, k(s)) --→ * R h(0, 0). In order to show that in this case, s corresponds to a solution, it is sufficient to make the following observations. First, only the first rule of R (with u i ) can be applied in order to reduce the s in the left branch to 0. Indeed, the only other rule of R applicable to s is g i (x) → x and after using this rule, only g j (f i (v i (x))) → x can be applied, and s cannot be reduced to 0. Moreover, assuming s minimal, and having the k at the top of the right branch imposes us to use only the last three rules of R in order to reduce k(s) to 0 (it is possible to start the reduction of the right branch with a sequence of applications of f i (g i (u i (x))) → x but this would contradict the minimality of s). Altogether, it follows that s corresponds to a solution of P . 2

h f im g im f i1 g i1 u i1 u im 0 k f im g im f i1 g i1 v i1 v im 0

Linear and Invisibly Pushdown Rewrite Systems

We show in this section that the problem of membership modulo becomes decidable with some further syntactic restrictions on R, based on the definition of visibly pushdown automata [START_REF] Alur | Visibly pushdown languages[END_REF].

The VPA (see also Section 5.2) recognize languages of words. They were generalized into tree recognizers in [START_REF] Chabin | Visibly pushdown languages and term rewriting[END_REF][START_REF] Comon-Lundh | Visibly tree automata with memory and constraints[END_REF]. In [START_REF] Chabin | Visibly pushdown languages and term rewriting[END_REF], Chabin and Rety show that the class of visibly pushdown tree automata (VPTA) languages is closed under rewriting with so called linear visibly context-free TRS. We use a similar definition in order to characterize a class of TRS modulo which membership is decidable for RTA. In the following definition, we assume a partition of the signature Σ into Σ c ⊎ Σ r ⊎ Σ ℓ . Definition 5. A collapsing TRS R is called inverse-visibly pushdown (invisibly pushdown) if for every rule ℓ → x ∈ R, d (ℓ) ≥ 1, x occurs once in ℓ, and if x occurs at depth 1 in ℓ then ℓ ∈ T (Σ ℓ , X ), otherwise, ℓ(ε) ∈ Σ c , the symbol immediately above x is in Σ r and all the other symbols of ℓ are in Σ ℓ .

Example 11. The TRS R = {fst(pair(x 1 , x 2 )) → x 1 , snd(pair(x 1 , x 2 )) → x 2 , dec(inc(x)) → x, decrypt(crypt(x, pk(A)), sk(A)) → x} is linear and invisibly pushdown with Σ c = {fst, snd, dec, decrypt} and Σ r = {pair, inc, crypt}, Σ ℓ = {pk, sk, A}.

3

The TRS in the proof of Proposition 6, {f (g(x)) → x}, is invisibly pushdown, but not the one in the proof of Theorem 14. Indeed, there exists no partition of Σ making this latter TRS invisibly pushdown. According to Definition 5, having a rule g i (x) → x implies that g i ∈ Σ ℓ but also having a rule

g j (f i (v i (x))) → x implies that g i ∈ Σ c .
Theorem 15. Membership modulo is decidable for RTA and linear and invisibly pushdown TRS.

Proof. The decision algorithm involves the construction of a visibly pushdown automata recognizing the language of ancestors of t wrt R that belong to L(A). We do this in three steps:

1. we compute a (big) context-free tree grammar that generates all terms that can rewrite to a single variable by R rules, such that there exists a run of A on them where the positions of the rigid states are not contradictory. 2. we add initial rules to the grammar in order to make it generate terms that rewrite to t instead of those rewriting to a variable. 3. finally, we transform the tree grammar obtained into a visibly pushdown tree automaton, and take the subterms under rigid states as independent languages. We replace each language under an occurrence of a rigid state by the intersection of all languages under all occurrences of the same rigid state.

After these constructions have been completed, we only need to check whether the given visibly pushdown language is empty or not in order to solve the problem.

Let A = Q, R, F, ∆ be an RTA, R an inverse-visibly pushdown TRS and t ∈ T (Σ) a term in normal form. We want to construct a CF tree grammar which simulates the application of the rules of R backwards, by expanding subterms into left-hand side of rules, in a way that the application of rules of A is possible. For this purpose, we shall use some tuples of the following form q1 q2 , ℓ, lbl, occ, occ x , < where

• q 1 , q 2 ∈ Q,

• ℓ is either the lhs of some rule ℓ → x ∈ R, or the single variable x,

• lbl is a labeling of ℓ by pairs of states denoted q q ′ , • occ is a set of pairs q r , p where q r ∈ R and p ∈ Pos(ℓ),

• occ x is a subset of occ where each rigid state occurs in at most one pair,

• < is a strict partial order on the set of rigid states R.

For each tuple ψ of this form, we will denote lq(ψ) for q 1 , rq(ψ) for q 2 and pair(ψ) for q1 q2 . When the use of lbl , occ, occ x or < is ambiguous we will index them with the tuple they are referencing (ex. occ ψ ). W.l.o.g. we will assume that the rule of R in which ℓ occurs rewrites to the variable x, and we will denote p x the position of this variable in ℓ. For the rest of the proof, we will need the following definition of a valid labelling of a term by those tuples. Definition 6. A labelling ξ of a term t by tuples of the form q1 q2 , ℓ, lbl, occ, occ x , < is said to be valid if 1. ∀p ∈ Pos(t), t(p)(lq(ξ(p.1)), . . . , lq(ξ(p.n))) → rq(ξ(p)) ∈ ∆, 2. there do not exist two rigid states q r1 , q r2 and two positions p, p ′ such that q r1 < ξ(p) q r2 and q r2 < ξ(p ′ ) q r1 , 3. there do not exist two positions p and p.w such that a rigid state q r appears in occ

ξ(p) x
and in occ ξ(p.w) , 4. there do not exist three positions p, p.w and p ′ such that a rigid state q r1 appears in occ

ξ(p)
x , a distinct rigid state q r2 appears in occ ξ(p.w) , and q r1 < ξ(p ′ ) q r2 . We will build a set T of tuples by induction. We start with

T 0 = { q q , x, q q , ∅, ∅, ∅ | q ∈ Q \ R} ∪ { q r q r , x, q r q r , {(q r , ε)}, {(q r , ε)}, ∅ | q r ∈ R}.
The set T i+1 is built from T i as follows

• for every ψ ∈ T i , we add ψ to T i+1 ,

• for every lhs ℓ of R and every valid labelling ξ of ℓ by tuples of T i , we add the tuple q1 q2 , ℓ, lbl, occ, occ x , < to T i+1 , where:

-q 1 = lq(ξ(ε)), q 2 = rq(ξ(p x )),

-∀p ∈ Pos(ℓ), lbl(p) = lp(ξ(l)) rp(ξ(l)) , -occ = { q r , p | q r appears in occ ξ(p) }, -occ x = { q r , p | p ≤ p x and q r appears in occ ξ(p)

x }, -q r1 < q r2 iff ∃p, q r1 < ξ(p) q r2 or ∃p, p.w ∈ Pos(ℓ), q r1 appears in occ

ξ(p) x
and q r2 appears in occ ξ(p.w) .

By induction, each tuple q1 q2 , ℓ, lbl, occ, occ x , < added in T verifies 1. q 1 is the top state of lbl(ε), 2. q 2 is the bottom state of lbl(p x ), 3. < is a partial strict order on R, 4. occ x ⊆ occ, 5. each position in occ x is a prefix of p x .

Since the number of lhs of R, the size of each lhs, the number of (rigid) states of A are all finite, each step takes a finite (in fact polynomial) amount of time. Also, the number of distinct tuples that can be added in some T i is also finite, so we will eventually reach a set T i where no new tuple can be added. We define T as the first T i where no new tuple can be added.

The terminal symbols of our CF tree grammar are the function symbols of Σ. Its non-terminals symbols are elements of N = Σ ∪ {⊤} × T , and f, ψ has arity n if f ∈ Σ n and every ⊤, ψ has arity zero.

Let us first define the main production rules of the grammar: for every f ∈ Σ ∪ ⊤ and every tuple φ = q1 q2 , ℓ, lbl, occ, occ x , < , -if ℓ = x, then we have in the grammar all the production rules:

f, ψ (x 1 , . . . , x n ) := u
where, f ∈ Σ n and u is a term of T Σ ∪ N , {x 1 , . . . , x n } such that Pos(u) = Pos(ℓ) and defined by, for every position p, u(p) = f ′ , ψ p with

• ψ p ∈ T • pair(ψ p ) = lbl(p)
• if q r , p ∈ occ, then q r occurs in occ ψp

• if q r , p ∈ occ x , then q r occurs in occ ψp x

• < ψp ⊆< By construction of T there exists a tuple ψ satisfying these conditions. Moreover,

• f ′ = ℓ(p) if ℓ(p) ∈ Σ (i.e. if p is not a variable position in ℓ),

• f ′ = f (x 1 , . . . , x n ) if p = p x (the position of x in ℓ),

• f ′ = ⊤ elsewhere.

-if ℓ = x, then q 1 = q 2 = q, and we add to our grammar the production rule f, ψ (x 1 , . . . , x n ) := f (x 1 , . . . , x n ) if f = ⊤. We also add to the tree grammar some non-terminal of arity zero and production rules that generates the terms of L(A, q), which is a regular language.

With this construction, the rules of our CF tree grammar generate the terms that rewrite to a single variable x with R, and that have a run r of A on them and where positions of rigid states are not contradictory with the rigid conditions. But we still need to ensure that we generate terms that rewrite to t instead of x and that subterms under rigid states are equal.

In order to generate terms rewriting to t instead of x, we just need to add initial rules to the grammar. Let S be the initial non-terminal symbol (of arity zero). For each valid labelling ξ of t such that lq(ξ(ε)) is a finite state of A, we add to our grammar the production rule: S := u where u(p) = (t(p), ξ(p)) for all p ∈ Pos(t).

The CF tree grammar constructed generates all the terms rewriting to t with R and with a run of A that have non-contradictory positions of rigid states. Only the rigidity condition is missing.

For the rigidity condition, we need to compare the languages generated by the grammar's production rules, starting from the non-terminal symbols of the form f, ψ with ψ = qr qr , x, qr qr , { q r , ε }, { q r , ε }, < for some rigid state q r ∈ R. Let us call such languages the language of the grammar associated to q r . For this purpose, we use the fact that R is a linear and invisibly pushdown rewrite system. Indeed, it ensures that the above languages of the grammar associated to rigid states are languages of visibly pushdown tree automata (VPTA). Such languages are closed under intersection, and the emptiness is decidable.

We consider the languages of the grammar associated to rigid states, beginning by the maximal rigid states according to the partial order. We compute the intersection of every language that can be generated at different occurrences of a same rigid state. We do that for each rigid state. Then, the intersection language of the minimal rigid states (according to the partial order) is used in the languages of greater rigid sates and in the general language of ancestors of t instead of the different languages of the different occurrences. We repeat this procedure, following the partial order, until having replaced each language of an occurrence of a rigid state by the corresponding intersection. Finally, we just have to decide the emptiness of the general language to know whether a term recognized by A (with a run respecting the rigidity condition for all rigid states) does rewrite to t. 2

Application to the Verification of Security Protocols

In this final section, we would like to present an application of RTA to the verification of security protocols; this application was actually our original motivation for studying rigid tree automata. Our purpose is not to propose new results in this domain, but rather to illustrate the potential of RTA for the automatic verification of some infinite state systems, in particular communicating processes.

Using automata for protocol analysis is a quite popular approach, see e.g. [START_REF] Comon | Tree automata with one memory, set constraints and cryptographic protocols[END_REF][START_REF] Genet | Rewriting for Cryptographic Protocol Verification[END_REF][START_REF] Goubault-Larrecq | Deciding H 1 by Resolution[END_REF]. In particular it is possible to analyze protocols with infinitely many sessions. But this kind of analyses has limitations due to approximations with regular sets. Such approximations may conduct to false alarms, as discussed e.g. in [START_REF] Amadio | On name generation and set-based analysis in the dolev-yao model[END_REF] or [START_REF] Affeldt | Verification of security protocols with a bounded number of sessions based on resolution for rigid variables[END_REF]. The approach with RTA overcomes several sources of imprecisions such as incorrect chaining of messages sent by agents, or ignoring the multiple occurrences of variables in the body of messages sent. Moreover, rigid state also permit to model a local finite memory in which both honest and dishonest agents can store read messages. This feature is generally not supported in other models.

Protocol Model

We consider a model of security protocols where a finite number of agents exchange messages, following a protocol, asynchronously over an insecure network. The messages are ground terms of T (Σ) build over cryptographic operators and are interpreted modulo an invisibly TRS R with rules like the above one for decrypt. For instance, we assume that Σ contains the binary operator crypt for encryption of data (in the first argument) with a public or secret key (in the second argument), and decrypt for the decryption with the associated secret key. We also use two unary operators pk and sk, associating to the name of an agent its public, respectively secret, key. For the name of agents, we use a finite set of constant function symbols of Σ 0 , A, B... Amongst the set of function symbols Σ, we distinguish a subset Σ pub of public function symbols, which represent the function publicly known. Below we assume that Σ pub contains crypt and decrypt, all the agent's names, the function pk (hence we assume that knowing somebody's name is sufficient to know his public key), a function inc for incrementation, but Σ pub does not contain the function sk.

We have the following rewrite rules in R (for each agent's name A) decrypt(crypt(x, pk(A)), sk(A)) → x (a message x encrypted using the function crypt with the public key of A, pk(A), can be recovered using decrypt and the secret key of A, sk(A)).

We also have the symmetric rules decrypt(crypt(x, sk(A)), pk(A)) → x

We also consider a binary constructor pair and two unary operators fst and snd for pairing and projection, and the associated rewrite rules

fst(pair(x 1 , x 2 )) → x 1 , snd(pair(x 1 , x 2 )) → x 2
As noticed in Section 7.3, the TRS containing the above rules is linear invisibly (see Example 11).

Example 12. We consider as a running example a simplified version of the mutual authentication protocol SPLICE/AS [START_REF] Yamaguchi | The design and implementation of an authentication system for the wide area distributed environment[END_REF], which consists of the following two messages exchanged between a client C and a server S. The purpose of this protocol is to establish a handshake between C and S: C sends to S some integer value N , encrypted with crypt and the public key of S, pk(S). Then, S sends to C in reply the successor of N , inc(N ), encrypted with crypt and the public key of C, pk(C), in order to prove that he was the real receiver of the first message -since only S has the secret key sk(S) which is necessary in order to recover N from crypt(N, pk(S)).

Moreover, in the first message, C further encrypts crypt(N, pk(S)) using the function crypt and its secret key of C, sk(C). The purpose of this second step of encryption is to act as a signature: only C is supposed to know his secret key, and the receiver of the message S, who knows C's public key pk(C) can check whether this part of the message was really encrypted with sk(C).

Finally, some more information is wrapped in the messages: C recalls his name in the signed part of the first message, for the purpose of the double check of the signature described above; moreover both messages start with a "header", i.e. a pair containing the name of the sender and the intended receiver.

The original SPLICE/AS protocol [START_REF] Yamaguchi | The design and implementation of an authentication system for the wide area distributed environment[END_REF] contains additional messages for the distribution of public keys pk(S) and pk(S) by a trusted authority AS, and timestamps. Here, we make the simplifying assumption that every public key is known by everyone (since everyone can obtain it from AS), and we skip the timestamps.

3

We consider a simple formal representation of programs executing cryptographic protocols which should fit with most of the formalisms in use.

A program is a finite set of agents, and each agent is a finite sequence of pairs of instructions of the form recv(x).send(s).i where i is a program point (in an arbitrary domain), x ∈ X and s ∈ T (Σ, X ). We assume that moreover every agent starts with an initial program point and that all the program points in a program are pairwise distinct. Note that every message is received as a variable (the argument of recv is always a variable). Hence recv acts as a variable binder, like in [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF]. Every agent is supposed to be closed, i.e. every variable x occurring in a send(s) is in the scope of a binder recv(x). For convenience, we assume that the variables in different instructions recv(x) of a program are distinct. C : c 0 .recv(x).send pair pair(C, S), crypt(pair(C, crypt(N, pk(S))), sk(C)) .c 1 S : s 0 .recv(y).send pair pair(t s , t c ), crypt(pair(t s , inc(t n )), pk(t c )) .s 1 where t s = snd(fst(y)), t c = fst(fst(y)), t n = decrypt snd decrypt(snd(y), pk(t c )) , sk(S)

The terms t s , t c and t n describe the recipes used by S to recover respectively the values S, C and N from the message received y. The variable x is useless. It is only for technical purpose that we assume that C receives an arbitrary value before sending the initial message of the protocol.

In order to define a semantics for the execution of these programs, we describe in the next section a model of the network used for the communications.

Example 14. The following sequence of configurations represents a valid execution of the program in Example 13, where the agent's messages are smoothly transferred without tampering.

({c 0 , s 0 }, ∅, N 0 ), ({c 1 , s 0 }, {x → t 0 }, N 1 ), ({c 1 , s 1 }, {x → t 0 , y → s 0 }, N 2 )

The set N 0 in the first configuration contains the initial knowledge of the attacker. For instance, N 0 contains A, pk(A), sk(A) (A is the official identity of the attacker), the identity of other agents and their public keys C, S, pk(C), pk(S)... and the terms build with these terms by application of the public function symbols pair, fst, snd, inc, crypt, decrypt, e.g. pair(A, S), pair(A, pair(A, S))... In other word, N 0 = cl {A, pk(A), sk(A), S, pk(C), pk(S)} .

Note that this set N 0 is infinite but regular. The term t 0 is an arbitrary element of N 0 , and

N 1 = cl (N 0 ∪ {s 0 }), s 0 = pair pair(C, S), crypt(pair(C, crypt(N, pk(S))), sk(C)) , N 2 = cl (N 1 ∪ {s 1 }), s 1 = pair pair(t s , t c ), crypt(pair(t s , inc(t n )), pk(t c )) , t s = snd(fst(s 0 )), t c = fst(fst(s 0 )), t n = decrypt snd decrypt(snd(s 0 ), pk(t c )) , sk(S) .
Note that in the sequence, the two agents exchange the messages of the protocol, as described in Example 12, because s 1 --→ * R pair pair(S, C), crypt(pair(S, inc(N )), pk(C)) .

With the above semantics, every message is build on the top of former messages (either by an agent or the attacker). The monotonicity of the definition of the messages sets N i makes bottom-up RTA suitable for their representation.

RTA construction

We show below that it is possible to build an RTA A recognizing exactly the sets of messages N (representing the state of the attacker's knowledge) in reachable configurations of a given program P . By reachable, we mean reachable from an initial configuration, which is specified precisely below and is assumed to be part of the problem. The RTA A models both the behaviour of the honest agents and of the attacker. It uses uses one rigid state to memorize every message received by the honest agents (the codomain of the substitution σ in configuration). The first component of configurations (program points of all agent) is encoded directly into the states (as the amount of information needed is finite).

Assume that the program P contains n agents P 1 , . . . , P n . We detail below the construction of the states and transitions of A. We have in A one state q i1...in for each tuple of values (i 1 , . . . , i n ) of program points of respectively P 1 , . . . , P n . transitions (additionally to the one presented in Example 18 above) pk(q c0s1 ) → q c0s1 |q x c0s1 |q y c0s1 , pk(q c1s0 ) → q c1s0 |q x c1s0 |q y c1s0 , pk(q c1s1 ) → q c1s1 |q x c1s1 |q y c1s1 (and idem for fst, snd, inc), crypt(q c0s1 , q c0s1 ) → q c0s1 |q x c0s1 |q y c0s1 , crypt(q c0s1 , q c1s0 ) → q c1s1 |q x c1s1 |q y c1s1 , . . . (and idem for decrypt, pair).

3

Verification of Security Properties

We will see that in our setting, it is possible to express and verify confidentiality and authentication properties for a protocol by a reduction to decision problems for the RTA A constructed above.

Example 20. The protocol of Example 12 is supposed to ensure the authenticity of the message of S and also the confidentiality of inc(N ) (for instance the value inc(N ) can be supposed to be reused later as a key for symmetric encryption of a communication tunnel). However, both these properties can be attacked with a replay attack described in the following counter example. This counter example involves two parallel sessions of the protocol. In the first session (messages 1 and 2), the client C contacts the server S, following the protocol. But the first message is diverted by the attacker, (i.e. the message 1 stays in the network without being delivered to S) as indicated by the receiver denoted by A(S). Then the attacker opens a new session (messages 1 ′ and 2 ′ ), between himself, A, (acting as a client) and the same server S. It is important to note that in message 1 ′ , the attacker reuses the same number N as in 1.

Actually, the attacker is not able to decrypt crypt(N, pk(S)), because he does not know the secret key sk(S). However, he is able to decrypt crypt(pair(C, crypt(N, pk(S))), sk(C)), using the public key of C. Hence he reuses this ciphertext crypt(N, pk(S)) in 1 ′ , as a ciphertex protecting a fresh value of N . The server, who is not aware that this is a replay, replies with crypt(pair(S, inc(N )), pk(A)), a message that the attacker is able to decrypt, with his own secret key sk(A). Hence the attacker learns the value inc(N ) which is supposed to be shared only by S and C. It means that N is also compromised if we assume that inc is invertible, i.e. that there exists a public unary function dec ∈ Σ pub and a rewrite rule dec(inc(x)) = x ∈ R (we did not consider these additional symbols and rules in our example above because they are not necessary for our purpose).

Moreover, the attacker can send the last message 2, impersonating S (this is denoted by the sender A(S)). Hence this is also an attack on the authenticity of this message (the server S was actually not involved in the session of the protocol made of messages 1 and 2).

3

The existence of a confidentiality flaw like the one described in Example 20 is reducible to the problem of membership modulo R (t ∈ R * L(A) , see Section 7.2), for the RTA A constructed above.

Example 21. The confidentiality attack described in Example 20 occurs with two parallel sessions, involving 3 agents: 1 agent C playing the role of the client in the first session, and 2 agents playing the role of the server, respectively in the first and second session. The server agent in the first session is inactive. The role of the client in the second session is played by the attacker.

We can recognize this attack by analysing a program made of the 2 agents C and S defined in Example 13 plus the following second instance of a server S : s ′ 0 .recv(y ′ ).send pair pair(t ′ s , t ′ c ), crypt(pair(t ′ s , inc(t ′ n )), pk(t ′ c )) .s ′ 1 where t ′ s = snd(fst(y ′ )), t ′ c = fst(fst(y ′ )), t ′ n = decrypt snd decrypt(snd(y ′ ), pk(t ′ c )) , sk(S) This agent has the same identity S as the first one in Example 13. Despite the renaming of the variable y into y ′ and of the program points (for technical convenience), this agent is the same as the one of Example 13. Let us construct the RTA A for this 3 agents as above. The states of A have the form q cisj s ′ k or q z cisj s ′ k for i, j, k ∈ {0, 1} and z ∈ {x, y, y ′ }.

We have that inc(N ) ∈ R * L(A, q c1s0s ′ 1 ) . Since the closure under R of the language in state q c1s0s ′ 1 represents the knowledge of the attacker, it means that the value inc(N ) has been compromised. Indeed, following the construction of A, we have t 1 = pair pair(C, S), crypt(pair(C, crypt(N, pk(S))), sk(C)) ∈ L(A, q c1s0s ′ 0 ). This term t 1 corresponds to the message 1 (of C) in Example 20. Using the transitions of the attacker, we obtain that t 1 ′ = pair pair(A, S), crypt(pair(A, snd(decrypt(snd(t 1 ), pk(C)))), sk(A)) ∈ L(A, q y ′ c1s0s ′ 0 ).

Note that snd(decrypt(snd(t 1 ), pk(C))) --→ * R crypt(N, pk(S)). With the transitions for the pattern matching of the message of the second agent playing the role of S, we have t 2 ′ = pair pair(t ′ s , t ′ c ), crypt(pair(t ′ s , inc(t ′ n )), pk(t ′ c )) ∈ L(A, q c1s0s ′ 1 ) with t ′ s = snd(fst(t 1 ′ )), t ′ c = fst(fst(t 1 ′ )), t ′ n = decrypt snd decrypt(snd(t 1 ′ ), pk(t ′ c )) , sk(S) . Next, using again the transitions of the attacker, we obtain t ′ = snd(decrypt(snd(t 2 ′ ), sk(A))) ∈ L(A, q c1s0s ′ 1 ), and we have t ′ --→ * R inc(N ). Hence there is a positive answer to the problem of membership modulo for A, R and inc(N ), meaning that there exists a confidentiality attack.

3

40
Let us make a few remarks on the above analysis. The construction of two generic agents like in Example 13 is the specification of the protocol, written by the user. These agents represent the 2 roles (client and server in the protocol). Adding several instances of each agent in a program (to be verified) can be done automatically, just by variable and program point renaming as described above. The second part of the user specification is the construction of a TA recognizing the initial attacker's knowledge N 0 , like in Example 18. The construction of the rest of the RTA, on the top of the agents and the TA for N 0 is automatic and the definition of the signature Σ and the TRS R are generic and independent of the protocol.

To summarize, RTA techniques permit an automatic analysis of the confidentiality property for security protocols, by reduction to the problem of membership modulo for RTA, given

• a definition of the set of public symbols Σ pub ,

• a user specification (as programs) of the roles of the protocol,

• the number and identities of the agents playing the different roles of the protocol (generic results like [START_REF] Comon-Lundh | Security properties: Two agents are sufficient[END_REF] can help),

• a finite representation of the initial knowledge of the attacker N 0 , and

• a ground term whose confidentiality must be ensured.

Note that the verification technique described above is exact: it requires no approximation on the protocol and attacker model (as long as the protocol is a program in the syntax of Section 8.1). Hence, every attack reported is a real attack, all the confidentiality attacks are reported and a negative answer is reported to the problem of membership modulo only if there exists no confidentiality attack, under the above hypotheses.

Authentication flaws like the one described in Example 20 can be reduced to the problem of emptiness of the intersection between the RTA A and a TA E (does L(A) ∩ L(E) = ∅). The idea is to add some tags in the agent's messages, for instance marking the end of every agent. The tags are built with function symbols which are not public (hence they can only be added by the agents, with special instructions), but we can also consider other public functions that the attacker can apply to remove the tags (modulo some rules in R for that purpose). Then the TA E characterizes some traces corresponding to authentication errors. For instance, the authentication flaw described in Example 20 can be characterized by the fact that C has received a message 2 (in the first session) and entered program point c 1 (this is characterised by the presence of a tag T c in the term) while S did not send it, and is still at program point s 0 (this is characterised by the absence of a tag above T c in the term). The emptiness of the intersection of L(E) and L(A) (note that this language is not considered modulo R in this case) means that there is no authentication flaw.

However, with the above model this approach is quite limited, since the agents can accept any message in the input. Hence, many false authentication attacks will be reported. This verification technique, related to regular tree model checking, would make more sense with a model with some conditionals in the agents, between instructions recv(x) and send(s).

Conclusion and Further Work

We have presented the class of Rigid Tree Automata and its properties. We have also studied the closure of RTA languages under term rewriting, and proposed an algorithm to decide that a given term belong to the closure for linear and invisibly pushdown TRS.

This class of tree automata is thought to be well suited for the automatic verification of some infinite state systems, and in particular for the verification of traces or equivalence properties of security protocols, using regular tree model checking like techniques. In this context, it would be interesting to extend the result of Theorem 15 to invisibly pushdown (non-linear) TRS, in order to handle axioms like decrypt(encrypt(x, y), y) = x. We are also interested about the symmetric form of the TRS of [START_REF] Chabin | Visibly pushdown languages and term rewriting[END_REF], whose rhs's are not single variables but have the form f (x 1 , . . . , x n ).

In Section 3.5, we have also mentioned the possibility to define RTA as sets of Horn clauses and the use of general purpose first order theorem proving tools in order to decide properties like the ones related to the rewrite closure. Such an approach could be interesting for instance for the extension of RTA with equational tests like in [START_REF] Jacquemard | Tree automata with equality constraints modulo equational theories[END_REF], in order to be able to capture conditionals in the model of security protocols presented in Section 8.

A comparison with restricted TA with registers was also mentioned in Section 3.5. Another potential application is indeed concerned with the processing of trees containing data from an infinite domain (this was for instance the motivation for the definition of TAGED in [START_REF] Filiot | Satisfiability of a spatial logic with tree variables[END_REF]). With a modeling of such data into subterms in T (Σ ′ ) (where Σ ′ is an auxiliary alphabet), some comparisons between data values can be expressed with rigid states. In this context, it could be interesting to find a decidable extension of VRTA with some other constraints complementary to the rigidity condition, in order to obtain a class closed under complement. This closure could permit to ensure a correspondence with a logic in which some queries on data trees can be expressed.

Figure 1 :

 1 Figure 1: Pumping lemma

Proposition 4 .

 4 The classes of languages of DA and RTA are orthogonal.

4. 1 .

 1 Union and Intersection Theorem 1. Given two RTA A 1 and A 2 , there exist two RTA of respective sizes O(|A 1 | + |A 2 |) and O(2 |A1||A2| ), constructed respectively in polynomial and exponential time, and recognizing respectively L(A 1 )∪L(A 2 ) and L(A 1 )∩L(A 2 ).

Theorem 4 .

 4 DRTA RTA. Proof. Let Σ = {a:0, f :2}. The language L = {f (t, t) | t ∈ T (Σ)} is recognized by the RTA of Example 1, without the transitions rules for symbol b.

Figure 3 :

 3 Figure 3: Membership NP-hardness: tree encoding of a 3 SAT instance.

Figure 4 :

 4 Figure 4: Undecidability of membership modulo: encoding of a solution of PCP.

1 .

 1 C → S : pair pair(C, S), crypt(pair(C, crypt(N, pk(S))), sk(C)) 2. S → C : pair pair(S, C), crypt(pair(S, inc(N )), pk(C))

Example 13 .

 13 An example of program executing the simplified version of the SPLICE/AS protocol of Example 12 is made of the two following agents called C and S.

1 .

 1 C → A(S) : pair pair(C, S), crypt(pair(C, crypt(N, pk(S))), sk(C)) 1 ′ . A → S : pair pair(A, S), crypt(pair(A, crypt(N, pk(S))), sk(A)) 2 ′ . S → A : pair pair(S, A), crypt(pair(S, inc(N )), pk(A)) 2. A(S) → C : pair pair(S, C), crypt(pair(S, inc(N )), pk(C))

  x 1 , . . . , x k are distinct variables). Since r(p 1 ) = r(p 2 ) and there are no rigid states between p 1 and p 2 , we can construct a run on every C ′ [D n [u]]. Moreover, t| πi = t| πj for all i, j ∈ {1..k}, hence we may assume wlog that the subruns r| πi are equal for all i ∈ {1..k}. It follows that we can perform the same operation as in C ′ [D n [u]] under each r| πi , and that

Table 1 :

 1 Summary of closure and decision results

		TA	RTA	TAGED+	DA
	∪	PTIME	PTIME	PTIME	PTIME
	∩	PTIME	EXPTIME	EXPTIME	not [24]
	¬	EXPTIME	not	not	not
	emptiness	linear-time	linear-time	EXPTIME-complete	NP-complete
	membership	PTIME	NP-complete	NP-complete	NP-complete
	∩-emptiness EXPTIME-complete EXPTIME-complete EXPTIME-complete
	universality EXPTIME-complete	undecidable	undecidable	undecidable
	inclusion	EXPTIME-complete	undecidable	undecidable	undecidable
	finiteness	PTIME	PTIME	EXPTIME

 [START_REF] Filiot | Tree automata with global constraints[END_REF]This work has been partly supported by the FET-Open grant agreement FOX no. FP7-ICT-23359, the INRIA ARC 2010 project ACCESS, and the ANR Sesur 07 project AVOT É.

Protocol Semantics

The network is assumed to be under the control of an active attacker who is able to read and divert messages and to sent newly forged messages under fake identities. The attacker is able to use terms and function symbols that he knows (like terms sent by honest processes and public functions such as crypt or decrypt), in order to forge new messages.

To summarize, in this network model, the communication of one message m between two agents C and S can be decomposed into three phases:

• C sends the message m to the attacker (send instruction),

• the attacker analyze the message as much as he can (applying public functions like decrypt, known public keys like pk(S) and the rewrite rules of R) and possibly changes m into m ′ (but m ′ may be equal to m),

• the attacker transfers m ′ to S, pretending that the sender is C, and S reads m ′ (recv instruction).

Later, S may reuse m ′ in order to prepare an answer to C, following the rules of the protocol. A configuration of a program P is a triple (S, σ, N ) where S is a set of programs points (one for each agent), σ is a substitution whose domain is the variables of P and codomain is a subset of T (Σ) and N ⊂ T (Σ). Intuitively, S contains the current program point of each agent of P , σ is the list of messages read by the agents so far with instructions recv(x), and N represents the set of terms known by the attacker. Hence, according to the above hypotheses, N corresponds to the content of the network (at a step of execution defined by S and σ) i.e. it is the set of all terms which can be read (with recv(x)) by the agents.

We define now small step semantics for the execution of programs. Each step changes the running configuration S, σ, N of P into S ′ , σ ′ , N ′ if S = {i} ∪ U , the program point i appears in one agent of P (this agent is unique by assumption that the program points are pairwise distinct) and in this agent, i is followed by the instructions recv(x).send(s).i ′ , x is not in the domain of σ and

• N ′ is the closure of cl(N ∪ {σ(s)}) under application of public function symbols and R, as defined below.

The closure cl(M ) of a set M ⊆ T (Σ) is defined recursively as the smallest set containing all the terms of M and such that for all f ∈ Σ pub of arity n, for all

Intuitively, cl(M ) represents the set of terms than the attacker can deduce from the terms of M .

Example 15. For the program of Example 13 (for the simplified version of the SPLICE/AS protocol presented in Example 12), with two agents called C and S, we have the states q c0s0 , q c1s0 , q c0s1 , q c1s1 . 3

Intuitively, A will be such that L(A, q i1...in ) is the set of messages N such that a configuration ({i 1 . . . i n }, σ, N ) is reachable, for some σ. Hence this language contains the set of terms readable (at this point) by the agents and the attacker.

For each state q i1...in and each (bound) variable x occurring in P , we consider one copy denoted q x i1...in , which is a rigid state.

Example 16. For the program of Example 13, we have the rigid states q x c0s0 , q y c0s0 , q x c1s0 , q y c1s0 . . . Intuitively, A will be such that L(A, q y c1s0 ) is exactly the set of terms t such that there exists a reachable configuration ({c 1 , s 0 }, {x → t 0 , y → t}, N ), for some t 0 and N .

3

Now, we will describe the transitions of A modeling the operations recv and send of the agents. The idea is that when an agent P i has an instruction send(s), then A will perform pattern matching of s, using transitions similar to the ones described in the construction of Proposition 1. Like in Proposition 1, we consider for this purpose some auxiliary states of the form q u i1...in for every strict subterm u of s and tuple (i 1 , . . . , i n ) of program points values. Note that for every variable x ∈ vars(s), one rigid states q x i1...in has already been added above.

Let (i 1 , . . . , i n ) be a tuple of program point values, such that i j occurs in the agent P j and is followed by the instructions recv(x).send(s).i ′ j . Then the following transitions are added to A for the recognition of s (like in Proposition 1, we assume that s is not a variable): g(q u1 i1...in , . . . , q um i1...in ) → q g(u1,...,um) i1...in s.t. g ∈ Σ m , g(u 1 , . . . , u m ) strict subterm of s, g(q u1 i1...in , . . . , q um i1...in ) → q i ′ s.t. g(u 1 , . . . u m ) = s, i ′ = i 1 . . . i j-1 i ′ j i j+1 . . . i n .

Note that since the states q x i1...in are rigid (when x is a variable), the non linearities in s are respected.

Example 17. Let us consider for instance the instructions of the agent S in the program of Example 13 s 0 .recv(y).send pair pair(t s , t c ), crypt(pair(t s , inc(t n )), pk(t c )) .s 1 with t s = snd(fst(y)), t c = fst(fst(y)), and t n = decrypt snd decrypt(snd(y), pk(t c )) , sk(S) . We have the following transitions in A fst q y c1s0 → q fst(y) c1s0

snd q fst(y) c1s0

→ q ts c1s0 . . . pair q pair(ts,tc) c1s0

, q crypt(...) c1s0

We need next some transitions in A modeling the behaviour of the attacker. As said above, the purpose of a state q i1...in is to characterize the set of messages N in a reachable configuration ({i 1 . . . i n }, σ, N ). In other words, this state characterizes the knowledge of the attacker when the n agents reached the respective steps i 1 , . . . , i n .

Let us consider first the tuple (i 0 1 , . . . , i 0 n ) of the initial program points of the agents P 1 , . . . , P n of P . The corresponding set of terms N 0 is characterized explicitly by a set of transitions of A using the states q i 0 1 ...i 0 n and q x i 0 1 ...i 0 n (and possibly some auxiliary states used only for that purpose, see the Example 18 below). This set N 0 defines a unique initial configuration ({i 0 1 , . . . , i 0 n }, ∅, N 0 ), which was mentioned when we discussed the reachable configurations, and N 0 is assumed to be part of the verification problem. Note that with this approach, it is possible to consider an infinite initial knowledge for the attacker. Moreover, the regular language N 0 is defined in a way that cl(N 0 ) = N 0 , in order to conform to the above semantics.

Example 18. The initial set of the attacker's knowledge N 0 which was mentioned in Example 14 is defined by the following transitions of A (for the sake of readability, we denote below the state q c0s0 by q 0 and the states q c0s0 |q x c0s0 |q y c0s0 by q xy 0 )

A → q xy 0 , A → q A , C → q xy 0 , S → q xy 0 , pk(q 0 ) → q xy 0 , sk(q A ) → q xy 0 , fst(q 0 ) → q xy 0 , snd(q 0 ) → q xy 0 , inc(q 0 ) → q xy 0 , crypt(q 0 , q 0 ) → q xy 0 , decrypt(q 0 , q 0 ) → q xy 0 , pair(q 0 , q 0 ) → q xy 0 .

where q A is an auxiliary state that occurs only in the above 2 transitions of A, in order to have sk(A) ∈ N 0 .

Next, we define some transitions modeling the evolution of the attacker's knowledge during the execution of the protocol. With the transitions defined above, we know that the states q i1...in characterise the messages that can be sent to the network by the agents. Moreover, we want to enrich the languages of these states with the information that the attacker is able to learn form the messages sent. According to the semantics presented above, the technique used by the attacker to learn information from messages consists in applying public function symbols of Σ pub at the top of the terms of its knowledge, i.e. the terms recognized in states q i1...in . It is expressed by transitions of the form: f (q i1 , . . . , q im ) → q i |q x i f ∈ Σ pub , i = max 1≤j≤m i j , x variable of P where the operator max is applied componentwise to the vectors i j and refers to an order defined on the program points of each agents by their order of appearance in the P j 's.