Florent Jacquemard
email: florent.jacquemard@inria.fr

Yoshiharu Kojima
email: kojima@trs.cm.

Masahiko Sakai
email: sakai@is.nagoya-u.ac.jp

Controlled Term Rewriting ⋆

Motivated by the problem of verification of imperative tree transformation programs, we study the combination, called controlled term rewriting systems (CntTRS), of term rewriting rules with constraints selecting the possible rewrite positions. These constraints are specified, for each rewrite rule, by a selection automaton which defines a set of positions in a term based on tree automata computations. We show that reachability is PSPACE-complete for so-called monotonic CntTRS, such that the size of every left-hand-side of every rewrite rule is larger or equal to the size of the corresponding right-hand-side, and also for the class of context-free non-collapsing CntTRS, which transform Context-Free (CF) tree language into CF tree languages. When allowing size-reducing rules, reachability becomes undecidable, even for flat CntTRS (both sides of rewrite rules are of depth at most one) when restricting to words (i.e. function symbols have arity at most one), and for ground CntTRS (rewrite rules have no variables). We also consider a restricted version of the control such that a position is selected if the sequence of symbols on the path from that position to the root of the tree belongs to a given regular language. This restriction enables decision results in the above cases.

Introduction

Term rewriting is a rule-based formalism for describing computations in ranked terms. In the context of formal verification, term rewriting systems (TRS) can be used to provide a finite abstraction of the dynamics of a system whose configurations are represented by ranked terms. In this case, the rewrite relation represents the transitions between configurations. For instance, functional programs manipulating (tree) structured data values with pattern matching can be described by rewrite rules [START_REF] Jones | Flow analysis of lazy higher-order functional programs[END_REF] such that the rewriting relation represents the program evaluation. This approach can also be applied to systems [START_REF] Abdulla | Regular tree model checking[END_REF] or imperative programs [START_REF] Bouajjani | Abstract regular tree model checking of complex dynamic data structures[END_REF][START_REF] Jacquemard | Rewrite-based verification of xml updates[END_REF] modifying some parts of tree shaped data structures in place, while leaving the rest unchanged. These update operations can be modeled by rewrite rules or similarly, tree transducers. A crucial problem for the automatic reachability and flow analysis of programs is to find finite and decidable representations of the closure the above TRS representations of sets of terms representing configurations. This approach is related to static type checking of XML transformations (see e.g. [START_REF] Milo | Typechecking for xml transformers[END_REF]), which is the problem to verify that a program always converts valid source trees (documents) into valid output trees (where types are defined by TA). It has also been shown useful for the analysis of consistency of XML read and write access control policies [START_REF] Jacquemard | Rewrite-based verification of xml updates[END_REF].

A rewrite rule is an oriented equation, whose left-hand-side (lhs) describe a pattern to be replaced in a term, and whose right-hand-side (rhs) is the new term for replacement. It can be applied at any position in a term, providing that the lhs matches the subterm at this position. For instance, a rule with lhs a(x 1 , x 2 ) can be applied at any position labelled by a. This simple approach is in general relevant in domains like theorem proving or algebraic computation. For some applications however, like the analysis of programs for XML document transformations or of access-control policies, it is important to be able to express explicitly some context conditions to be checked before applying a rewrite rule. For instance, one may want to rename the label at some position with a rewrite rule a(x) → b(x) providing that there is no occurrence of b above the position to be rewritten (position labeled with a). Some standard XML transformation languages like XSLT or XQuery update [START_REF] Chamberlin | Xquery update facility 1.0. W3C Candidate Recommendation[END_REF], use the path specification language XPath or a XQuery expressions in order to define the position where the transformation can be applied.

In this paper, we study the so called controlled term rewriting systems (Cnt-TRS) in the context of regular tree model checking. They are defined by the combination of term rewriting rules with some constraints (called control) specifying the possible rewrite positions. In order to define the constraints, we have chosen a model similar to the selection tree automata (SA) of [START_REF] Frick | Query evaluation on compressed trees (extended abstract)[END_REF], which, intuitively, select positions in a term based on the computations of a tree automaton. This gives a powerful selection mechanism, with the same expressiveness as the monadic second order logic of the tree, or monadic Datalog [START_REF] Gottlob | Monadic datalog and the expressive power of languages for web information extraction[END_REF]. We consider also a restriction of the SA where a position p in a term t is selected if the sequence of symbols on the path from p to the root of t belongs to a given regular language. The corresponding restricted rewriting model is called prefix CntTRS, or pCntTRS. It turns out quickly (Examples at the end of Section 1) that even the restricted pCntTRS are actually too powerful for preserving regularity, even for very simple rewrite rules. Therefore, we consider in Section 2 the classes of context-free (CF) and context-sensitive (CS) tree languages, which are both strictly larger than the class of TA languages (also called regular tree languages). We also define the so called CF and monotonic classes of rewrite systems (without control). A rewrite rule is CF if its lhs is of the form f (x 1 , . . . , x n ) where x 1 , . . . , x n are distinct variables, and monotonic if the size of its lhs is larger or equal to the size of its rhs. We show that CF and monotonic TRS respectively preserve CF tree languages and CS tree languages.

The monotonic uncontrolled rewrite rules already have the full power of CS tree grammars. Adding control with SA does not improve their expressiveness, and it follows that reachability is PSPACE-complete and model checking undecidable for monotonic CntTRS (Section 3.1). Similar results also hold for CF Cnt-TRS without collapsing rules (projection rules of the form f (x 1 , . . . , x n ) → x i ), even when restricting to prefix control (Section 3.2).

When allowing depth-reducing rules (Section 3.3), reachability becomes undecidable, even for flat CntTRS (lhs and rhs of rewrite rules are of depth at most one) and in the case of words (i.e. function symbols of arity at most one). Similarly, reachability is undecidable for ground CntTRS (rewrite rules have no variables). When restricting to words, prefix control and flat rewrite rules, reachability is decidable in PSPACE.

Finally, we consider in Section 4 a relaxed form of the prefix control of rewrite rules, where the selection is done by considering the term in input modulo the rewrite relation. We obtain a regularity preservation result for this recursive form of prefix controlled rewriting, using alternating tree automata with ε-transitions.

Related Work. Controlled rewrite systems have been introduced in the case of word rewriting, see [START_REF] Sénizergues | Formal languages and word-rewriting[END_REF] for a survey, and also [START_REF] Dassow | Handbook of Formal Languages, volume 2, chapter Grammars with Controlled Derivations[END_REF] for the case of conditional context-free (word) grammars, which are mentioned in Section 3.

Regarding term rewriting, there have been many studies for finding syntactical restriction on term rewrite rules ensuring the preservation of regularity, see e.g. [START_REF] Feuillade | Reachability analysis over term rewriting systems[END_REF]. This is the case for instance of linear and flat as well as ground TRS without control, in contrast to the results of Section 3.3 for their controlled counterpart.

Many strategies have been proposed for term rewriting, most often for efficiency purposes (our goal here is rather to study the expressiveness and decidability results for controlled rewriting). We cannot mention all of them, and will just give some elements of comparison with controlled rewriting. The innermost strategy, which is the analogous of call-by-value for functional languages (a subterm can be rewritten only when all its proper subterms are no more rewritable) can be expressed in controlled rewriting for left-linear TRS, because the set of non-rewritable terms (the normal forms) for such TRS are recognizable by tree automata (see e.g. [START_REF] Comon | Tree Automata Techniques and Applications[END_REF]). Some results of preservation of regularity for the innermost and the outermost and leftmost rewrite strategies can be found in [START_REF] Réty | Tree automata for rewrite strategies[END_REF] In the context sensitive strategy [START_REF] Lucas | Context-sensitive rewriting strategies[END_REF] (which is not related to the context-sensitive term languages presented in this paper), the rewriting positions are selected according to a mapping µ associating to every symbol of the signature the subset of the indexes of its argument that can be rewritten. More precisely, the positions selected for rewriting in a term f (t 1 , . . . , t n ) are the root position and all the positions selected in every t i such that i ∈ µ(f ). This set of positions can be defined by SA, i.e. context-sensitive rewriting is a particular case of controlled rewriting. It is a strict subcase because with the context-sensitive strategy, the root position is always rewritable whereas this is not the case for controlled rewriting.

A result of preservation of regularity for this rewrite strategy was established in [START_REF] Kojima | Innermost reachability and context sensitive reachability properties are decidable for linear right-shallow term rewriting systems[END_REF]. Another related topic is the optimal call-by-need rewrite strategies for TRS. In [START_REF] Comon | Sequentiality, second order monadic logic and tree automata[END_REF] and [START_REF] Durand | Decidable call-by-need computations in term rewriting[END_REF], it is shown how to select the needed redexes (positions at which rewriting must be performed in order to transform a term to its normal form) using monadic second order logic formulae, which is equivalent as using SA.

Top-down tree transducers with regular look-ahead [START_REF] Engelfriet | Top-down tree transducers with regular look-ahead[END_REF] are an extension of top-down tree transducers, where a transition can be fired provided that the current subtree belongs to some given regular tree language. This is similar to our notion of control for rewrite systems. A notable difference however is that the transducers transform terms in one (top-down) pass, whereas we consider here the terms computed by an arbitrary iteration of controlled rewrite rules.

Preliminaries

Terms. We use the standard notations for terms and positions, see [START_REF] Baader | Term Rewriting and All That[END_REF]. A signature Σ is a finite set of function symbols with arity. We denote the subset of function symbols of Σ of arity n as Σ n . 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 signature is called unary if it contains only symbols of arity 1 and one symbol ⊥ of arity 0. We make no distinction below between ground terms over a unary signature Σ and words of Σ * 1 . More precisely, a term a 1 (a 2 (. . . a n (⊥))) will be represented by the string a 1 a 2 . . . a n (the constant symbol ⊥ is forgotten in this representation).

A term t ∈ T (Σ, X ) can be seen as a function from its set of positions Pos(t) into Σ ∪ X . Positions in terms are denoted by sequences of natural numbers, ε is the empty sequence (root position), and p.p ′ denotes the concatenation of positions p and p ′ . The set Pos(t) of positions of the term t is defined recursively as Pos f (t 1 , . . . , t m ) = {ε} ∪ {i.p | i ∈ {1, . . . , m} ∧ p ∈ Pos(t i )}. The height of a term t, denoted h(t), is the maximal length of a position of Pos(t). The size t of a term t is the cardinality of Pos(t).

The subterm of t at position p is denoted t| p defined by t| ε = t and f (t 1 , . . . , t m )| i.p = t i | p . The term obtained from t by replacing subterm of t at position p by s, is denoted t[s] p . The notation t = t[s] p may also be used to emphasize that t| p is s.

A substitution is a mapping X → T (Σ, X ). Substitutions can also be applied to arbitrary terms by homomorphically extending its application to variables. The application of a substitution σ to a term t, denoted as tσ, is defined as follows for non-variable terms: f (t 1 , . . . , t n )σ = f (t 1 σ, . . . , t n σ). A variable renaming is a substitution from variables to variables.

A term is linear if no variable occurs more than once in it. A term is shallow if each occurrence of variables is at most depth one, and flat if its height is at most one.

A context of dimension n is a linear term C ∈ T (Σ, {x 1 , . . . , x n }). When C = x 1 , it is called the empty context. Given a context C of dimension n and n terms t 1 , . . . , t n ∈ T (Σ, X ), we write C[t 1 , . . . , t n ] to denote Cσ where σ is the substitution {x 1 → t 1 , . . . , x n → t n }.

Tree Automata. A tree automaton (TA) A over a signature Σ is a tuple Q, F, ∆ where Q is a finite set of nullary state symbols, disjoint from Σ, F is a set of states of Q called final states, ∆ is a set of transition rules of the form: f (q 1 , . . . , q n ) → q, where f ∈ Σ n , and q 1 , . . . , q n , q ∈ Q. Sometimes, we shall refer to A as a subscript of its components, like in Q A to indicate that Q is the state set of A. The size of A is A = f (q1,...,qn)→q∈∆ (n + 2). Transition from s to t in one step by a TA A is denoted by s -→ A t, and its reflexive and transitive closure is denoted by s

* -→ A t. A run of A on a term t ∈ T (Σ) is a mapping ρ from Pos(t) into Q A such that for all p ∈ Pos(t), t(p) ρ(p.1), . . . , ρ(p.n) → ρ(p) is in ∆ A , where n is the arity of the symbol t(p) in Σ. The run ρ is called successful (or accepting) if ρ(ε) is in F A .
The set of successful runs of A on t is denoted sruns(A, t). For the sake of conciseness, we shall sometimes apply term-like notations (subterm, replacement...) to runs. The language L(A) of A is the set of terms t for which sruns(A, t) is not empty.

Selection Automata. Besides being able to recognize terms, tree automata can also be used to select positions in a term [START_REF] Frick | Query evaluation on compressed trees (extended abstract)[END_REF][START_REF] Neven | Query automata over finite trees[END_REF]. We propose here a definition of position selection by TA very close to [START_REF] Frick | Query evaluation on compressed trees (extended abstract)[END_REF].

A selection automaton (SA) A over a signature Σ is a tuple Q, F, S, ∆ where Q, F, ∆ is a tree automaton denoted ta(A) and S is a set of states of Q called selection states. Given a SA A and a term t ∈ T (Σ), the set of positions of t selected by A is defined as sel(A, t) = {p ∈ Pos(t) | ∃ρ ∈ sruns(ta(A), t), ρ(p) ∈ S}.

Note that it is required that t is recognized by A in order to select positions.

We shall consider below a restricted kind of selection by TA, where a position p in a term t is selected only according to its strict prefix (i.e. the sequence of symbols labeling the path from the root of t down to the immediate ancestor of p), which is tested for membership to a regular (word) language. More precisely, a selection automaton A = Q, F, S, ∆ is called prefix if Q contains two special states: q 0 (universal state) and q s (selection state), F ⊆ Q\{q 0 }, S = {q s }, and ∆ contains f (q 0 , . . . , q 0 ) → q 0 and f (q 0 , . . . , q 0 ) → q s for all f ∈ Σ, and ∆ contains some other transition rules of the form f (q 1 , . . . , q n ) → q where q ∈ Q \ {q 0 , q s } and there exists exactly one i ≤ n such that q i = q 0 . Intuitively, assume that we are given a finite automaton B defining the strict prefixes of selected positions. Then q s is the initial state of B, F is the set of final states of B, and for all a ∈ Σ n , ∆ contains n rules a(q 0 , . . . , q 0 , q ′ , q 0 , . . . , q 0 ) → q for each transition q ′ -→ a q of B. Note that with this definition, the root position is always selected by a by a prefix selection automaton.

Controlled Term Rewriting Systems. We propose a formalism that strictly extends standard term rewriting systems [START_REF] Baader | Term Rewriting and All That[END_REF] by the restricting the possible rewrite positions to positions selected by a given SA. Formally, a controlled term rewriting system (CntTRS) R over Σ is a finite set of controlled rewrite rules of the form A : ℓ → r, made of a SA A over Σ and a rewrite rule ℓ → r such that ℓ ∈ T (Σ, X ) \ X (the left-hand side of the rule), and r ∈ T (Σ, vars(ℓ)) (the right-hand side). Ths size of R is the number of the rewrite rules inn R.

A term s rewrites to t in one step by an CntTRS R, denoted by s --→ R t, if there exists a controlled rewrite rule A : ℓ → r ∈ R, a position p ∈ sel (A, s), and a substitution σ such that s| p = ℓσ and t = s[rσ] p . In this case, s is said to be R-reducible, and otherwise s is called an R-normal form. The reflexive and transitive closure, and reflexive, symmetric and transitive closure of --→ R are denoted as * -→ R and ← --→ * R , and = -→ R denotes the union of -→ R and =. Example 1. Let us consider the CntTRS R = {(1) A 1 : a → c, (2) A 2 : b → c, (3) A 3 : f (x, y) → g(x, y)} where each SA is as follows (Q = {q 1 , q 2 , q f }):

A 1 = Q, {q f }, {q 1 }, {a → q 1 , b → q 2 , f (q 1 , q 2 ) → q f } A 2 = Q, {q f }, {q 2 }, {c → q 1 , b → q 2 , g(q 1 , q 2 ) → q f } A 3 = Q, {q f }, {q f }, {c → q 1 , b → q 2 , f (q 1 , q 2 ) → q f } Then, the following rewriting is possible with R f (a, b) --→ (1) f (c, b) since sel(A 1 , f (a, b)) = {1} and the subterm of f (a, b) at the position 1 is a. Similarly, we have f (c, b) --→ (3) g(c, b) --→ (2) g(c, c) where sel (A 3 , f (c, b)) = {ε}, and sel (A 2 , g(c, b)) = {2}.
We call prefix controlled term rewriting system (pCntTRS), resp. term rewriting systems (TRS), the special cases of CntTRS such that every SA in a controlled rewrite rule is a prefix SA, resp. is the universal SA A 0 = {q 0 }, {q 0 }, {q 0 }, {f (q 0 , . . . , q 0 ) → q 0 | f ∈ Σ} . In the latter case, A 0 may be dropped when defining the rewrite rules, i.e. we present a TRS as a finite set of uncontrolled rewrite rules, as usual.

A controlled rewrite rule A : ℓ → r is ground, flat, linear, shallow if ℓ and r are so. It is collapsing if r is a variable. A CntTRS is flat, linear, etc if all its rules are so.

Decision Problems. The closure of a ground term set L by a CntTRS R is {t | ∃s ∈ L, s --→ * R t} (it is sometimes denoted R * (L)).
Ground reachability is the problem to decide, given two ground terms s, t ∈ T (Σ) and a CntTRS R whether s --→ * R t. Regular Model checking (RMC) is the problem to decide, given two TA languages L in and L err and a CntTRS R whether R * (L in ) ∩ L err = ∅. The name of the problem is coined after state exploration techniques for checking safety properties. In this setting, L in and L err represent (possibly infinite) sets of initial, respectively error, states.

Example 2. Let us consider the following CntTRS R over the unary signature Σ with Σ 1 = {a, b, c, d} and Σ 0 = {⊥}. Let R be the CntTRS containing the following controlled rewrite rules. The SA of these rules select one position per term, and they are represented by a regular expression where the selected letter is underlined.

(1) c * a * d * d b * : d(x) → b ′ (x) (3) c * a ′ a * d * b ′ b * : b ′ (x) → b(x) (2) c * c a * d * b ′ b * : c(x) → a ′ (x) (4) c * a ′ a * d * b * : a ′ (x) → a(x)
More precisely, the SA for the above rules are respectively (Q is the state set {q a , q b , q c , q d , q})

A 1 = Q, {q c , q a , q d , q}, {q}, {⊥ → q b , b(q b ) → q b , d(q b ) → q, d(q|q d ) → q d , a(q|q d |q a ) → q a , c(q a |q c |q) → q c } A 2 = Q, {q c , q}, {q}, {⊥ → q b , b(q b ) → q b , b ′ (q b ) → q d , d(q d ) → q d , a(q d |q a ) → q a , c(q a ) → q, c(q|q c ) → q c } A 3 = Q, {q c }, {q}, {⊥ → q b , b(q b ) → q b , b ′ (q b ) → q, d(q|q d ) → q d , a(q|q d ) → q a , a ′ (q|q d |q a ) → q c , c(q c ) → q c } A 4 = Q, {q c , q}, {q}, {⊥ → q b , b(q b ) → q b , d(q b |q d ) → q d , a(q b |q d |q a ) → q a , a ′ (q b |q d |q a ) → q, c(q|q c ) → q c }
Note that these SA are all deterministic. The SA A 1 selects the last d (starting from the top), A 2 selects the last c when there is a b ′ , A 3 selects the b ′ when there is a a ′ , and A 4 selects the a ′ when there is no b ′ . The closure of the regular tree language L = c + (d

+ (⊥)) by the CntTRS is such that R * (L) ∩ a * (b * (⊥)) = {a n b n ≤ n ≥ 0}. Therefore, R * (L)
is a non regular tree language (it is a contextfree tree language).

Example 3. Using the same signature as in Example 2, we can obtain a contextfree set of descendants with a flat pCntTRS. Indeed, intersection of a * b * and the closure of c * d * by the following set of rewrite rules is {a n b m | n ≥ m} which is CF and not regular. In the rewrite rules, we use an informal description of the languages of the prefix allowed, instead of giving explicitly the prefix SA. no a ′ , no a : c(x) → a ′ (x), exactly one

a ′ : d(x) → b ′ (x), no a ′ , no a : a ′ (x) → a(x), no a ′ , no b ′ , no b : b ′ (x) → b(x).
It is not difficult to generalize the construction of Example 3 in order to obtain a context sensitive rewrite closure of the form {a n b m c p | n ≥ m ≥ p}, starting from a regular set of the form c * d * e * and using a flat pCntTRS.

CF and CS Tree Languages and TRS

In this section, we define the context-free and context-sensitive sets of terms, and give properties of their closure under term rewriting. A rewrite rule over Σ is called

context-free (CF) if it is of the form f (x 1 , . . . , x n ) → r where r ∈ T Σ, {x 1 , . . . ,
x n } , x 1 , . . . , x n are distinct variables and f ∈ Σ n . Recall that when r = x i for some i ≤ n, then the rule is called collapsing.

monotonic if it is of the form C[x 1 , . . . , x n ] → D[x 1 , . . . , x n ]
where C and D are two contexts over Σ and such that C ≤ D and x 1 , . . . x n are distinct variables (note that it implies that the rule is linear).

A tree grammar (TG, see e.g. [START_REF] Comon | Tree Automata Techniques and Applications[END_REF]) is a tuple G = N , S, Σ, P where N is a finite set of non-terminal symbols, each with an arity, S ∈ N has arity 0, it is called the axiom of G, Σ is a signature disjoint from N , (its elements are also called terminal symbols) and P is a set of (uncontrolled) rewrite rules, called production rules, of the form ℓ → r where ℓ, r are terms of T (Σ ∪ N , X ) such that ℓ contains at least one non-terminal. The tree grammar G is regular if all non-terminal symbols of N have arity 0 and all production rules of P have the form A → r, with A ∈ N and r ∈ T (Σ ∪ N ). It is context-free (CFTG), resp. context-sensitive (CSTG) if all production rules are CF, resp. monotonic. In the two later cases, we assume from now on wlog that every production rule either has the form A(x 1 , . . . , x n ) → a(x 1 , . . . , x n ) where A ∈ N and a ∈ Σ n , or it does not contain terminal symbols of Σ, by introducing the non-terminal symbol b , the production rule b → b, and replace all b in the other production rules by b .

The language generated by G, denoted by L(G), is the set of terms of T (Σ) which can be reached by successive applications of the production rules, starting from the axiom, i.e.

L(G) = {t ∈ T (Σ) | S --→ * P t}.
A tree language is called regular (resp. CF, CS) if it is the language of a regular (resp. CF, CS) grammar.

Note that the classical cases of word languages are particular cases of the above, if the symbols of N ∪ Σ are unary symbols of a unary signature.

The regular tree grammars are equivalent in expressiveness to TA. There exists a model of pushdown TA equivalent to the CF tree grammars [START_REF] Guessarian | Pushdown tree automata[END_REF]. The membership problem is, given a tree grammar G over Σ and a term t ∈ T (Σ), to decide whether t ∈ L(G). The emptiness problem is, given a tree grammar G, to decide whether L(G) = ∅. Proposition 1. Membership and emptiness are decidable in PTIME for CFTG.

The following result (perhaps a folklore knowledge) is almost immediate from the above definitions.

Proposition 2. Given a CFTG G and a CF TRS R, one can construct in PTIME a CFTG generating the closure of L(G) by R, and whose size is polynomial in the size of G and R.

Proof. Let G = N , S, Σ, P be a CFTG and R a CF TRS over Σ. For all a ∈ Σ, we create a new non-terminal N a with the same arity as a. Let N ′ = N ∪ {N a | a ∈ Σ}, and let P ′ be obtained from P by replacing every production rule Proof. For the RMC, we use the fact that the intersection of the languages of a CF tree grammar G and a TA A is the language of a CF tree grammar whose size is the product of the respective sizes of G and A. ⊓ ⊔ Note however that joinability, the problem to decide, given two ground terms s, t ∈ T (Σ) and a TRS R, whether there exists u ∈ T (Σ) such that s --→ * R u ← -- * R t, is undecidable for CF TRS [START_REF] Chabin | Visibly pushdown languages and term rewriting[END_REF], because the emptiness of intersection is undecidable for CF tree languages.

A(x 1 , . . . , x n ) → a(x 1 , . . . , x n ), with A ∈ N and a ∈ Σ, by A(x 1 , . . . , x n ) → N a (x 1 , . . . , x n ).
We can also observe that the CF TRS are left linear, but in general not right linear. They are the symmetric the so called right-linear, monadic and non-collapsing TRS, whose rules have the form f (x 1 , . . . , x n ) → r, where r ∈ T (Σ, {x 1 , . . . , x n })\X . It has been shown that these TRS preserve regularity [START_REF] Nagaya | Decidability for left-linear growing term rewriting systems[END_REF]: the closure of a regular tree language by such a TRS is a regular tree language. The decidability of reachability for CF TRS is already a consequence of this former result. It has been observed, see e.g. [START_REF] Hofbauer | Deleting string rewriting systems preserve regularity[END_REF], that in several cases, one class of word rewrite system preserves regularity and its symmetric class preserves CF languages. We have here an example of such a situation in the case of terms.

To our knowledge, the case of CSTG and monotonic TRS was not studied before but it is not very surprising.

Proposition 3. Membership is PSPACE-complete for CSTG.
Proof. The hardness is an immediate consequence of the same result for CS (word) grammars [START_REF] Kuroda | Classes of languages and linear-bounded automata[END_REF], which are a particular case of CSTG. For the decision algorithm, let G be a CSTG over Σ and let t ∈ T (Σ) be given. We can observe that if two terms s and s ′ over the non-terminal and terminal symbols of the CSTG G are successive in a derivation starting from the axiom S of G, then the size s ′ is larger or equal to s . Hence, if there is a derivation from S to t by G, then all the terms in this derivation have a size smaller or equal to t . Hence, it is possible to construct a linear bounded automata which, starting from t, will search backward (non deterministically) a derivation from S. The detailed construction is given in Appendix A.

⊓ ⊔ Proposition 4. Emptiness is undecidable for CSTG.

Proof. It is a consequence of the same result for CS (word) grammars. ⊓ ⊔ Proposition 5. Given a CSTG G and a monotonic TRS R, one can construct in PTIME a CSTG generating the closure of L(G) by R, and whose size is polynomial in the size of G and R.

Proof. The construction is similar as the one in the proof of Proposition 2. ⊓ ⊔ 3 Controlled Term Rewriting

Monotonic CntTRS

The result of Proposition 5 can be extended from uncontrolled to controlled monotonic TRS. Intuitively, monotonic TRS are powerful enough to be able to simulate a control with uncontrolled rewrite rules.

Theorem 1. Given a CSTG G and a monotonic CntTRS R, one can construct in PTIME a CSTG generating the closure of L(G) by R, and whose size is linear in the size of G and R.

Proof. (sketch) In order to prove this theorem, we show how to construct a CSTG G * that accepts the set of terms reachable by R from the terms in L(G).

The production rules P * of G * consists in two sets: the rules P of G and P 1 , that simulate rewriting by R. The basic idea for the construction of G * is the introduction of non-terminals of the form f, q where f is a symbol and q is a state of some SA. First, we produce the term t where t ∈ L(G) and t is the term obtained by replacing each symbol f by the non-terminal f . Next, we simulate the rewriting of R by P 1 . We simulate a transition f (q 1 , . . . , q n ) → q of a SA by some production rules in P 1 of the form f ( f 1 , q 1 (x 1 ), . . . , f n , q n (x n )) → f, q ( f 1 , q 1 (x 1 ), . . . , f n , q n (x n )). Finally, if a final state occurs at the root position of a term and a rewrite rule matches the subterm where a selection state appears, then we rewrite the term. A detailed proof of Theorem 1 can be found in Appendix B, as well as an illustration in the following example.

⊓ ⊔ Example 4. Consider the CntTRS R in Example 1 and the CSG G such that

L(G) = {f (a, b)}. We construct the CSG G * such that L(G * ) = {f (a, b), f (c, b), g(c, b), g(c, c)}. Let the set of production rules P of G be {S → f ( a , b ), a → a, b → b, f (x 1 , x 2 ) → f (x 1 , x 2 )
}, and mark i to each component of SA to distinguish each SA A i . Let the axiom of G * be S λ . We define the set of production rules P * of G * as P * = P ∪ P ′ ∪ P A ∪ P fin ∪ P R ∪ P re where

P ′ = {S λ → f λ ( a , b ), f λ (x 1 , x 2 ) → f (x 1 , x 2 )} P A = { c 1 → c 1 , q i | c 1 → q i ∈ ∆ i for some i}∪ f 1 λ ( c 1 , q i 1 , c 2 , q i 2 ) → f 1 , q i λ ( c 1 , q i 1 , c 2 , q i 2 ) c 1 , c 2 ∈ {a, b, c}, f 1 (q i 1 , q i 2 ) → q i ∈ ∆ i for some i P fin = { f 1 , q i λ (x 1 , x 2 ) → f 1 , q i λ fin (x 1 , x 2 ) | f 1 ∈ {f, g}, q i ∈ F i for some i}∪    f 1 , q i λ fin ( c 1 , q i 1 , c 2 , q i 2 ) → f 1 λ ( c 1 , q i 1 fin , c 2 , q i 2 fin ) f 1 ∈ {f, g}, c 1 ∈ {a, b, c}, f (q i 1 , q i 2 ) → q ∈ ∆ i for some i    P R = { a, q 1 1 fin → c } ∪ { b, q 2 2 fin → c } ∪ { f, q 3 f λ fin (x 1 , x 2 ) → g λ (x 1 , x 2 )} P re = { c 1 , q i → c 1 , c 1 , q i fin → c 1 | c 1 ∈ {a, b, c}, q i ∈ Q i for some i}∪ f 1 , q i λ (x 1 , x 2 ) → f 1 λ , f 1 , q i λ fin (x 1 , x 2 ) → f 1 λ (x 1 , x 2 ) f 1 ∈ {f, g}, q i ∈ Q i for some i The term f (c, b) is produced by G * with the production S λ -→ P ′ f λ ( a , b ) * --→ PA f, q f λ ( a, q 1 , b, q 2 ) * --→ P fin f λ ( a, q 1 fin , b, q 2 fin ) --→ PR f λ ( c , b, q 2 fin ) --→ Pre f λ ( c , b ) * ----→ P ∪P ′ f (c, b). Corollary 2.
Reachability is PSPACE-complete for monotonic CntTRS.

From Proposition 4, it immediately holds that regular model checking is undecidable for monotonic CntTRS. Moreover, the following lower bounds already hold in the very restricted case of controlled rewrite rules over words, and where each side of every rule has depth exactly one. Proposition 6. Reachability is NLINSPACE-complete and regular model checking is undecidable for monotonic and flat CntTRS over unary signatures.

Proof. We reduce the acceptance (for reachability) and emptiness (for regular model checking) problems for a linear bounded automaton (LBA) M [START_REF] Kuroda | Classes of languages and linear-bounded automata[END_REF]. The detailed reduction can be found in Appendix C, let us present here the general idea. Every configuration of M will be represented by a term of the form : a 1 . . . a j-1 a p j a j+1 . . . a n : , where :, : are the symbols for left and right endmarkers, a 1 . . . a n is the content of the tape of M, p is its current state and a p j marks the current position (j) of the head.

To every transition θ of M stating that in state p, reading a, M changes state to p ′ , write b and moves left, we associate the four following monotonic and flat controlled rules (Γ is the input alphabet of M, the selected position in the regular expression is obvious, it is the lhs of the rule)

: Γ * c a p Γ * : : a p (x) → a p , θ (x), : Γ * c a p , θ Γ * : : c(x) → c, θ (x), : Γ * c, θ a p , θ Γ * : : a p , θ (x) → b(x), : Γ * c, θ bΓ * : : c, θ (x) → c p ′ (x).
The rules for a transition moving to the right are similar. ⊓ ⊔ Some remarks about the above result. In the above construction, the selection of the rewrite position by the SA is not necessary. Only the selection of the rewritable terms by TA is needed (a weaker condition). Note also that linear and flat TRS preserve regularity, with a PTIME construction of the TA recognizing the closure (see e.g. [START_REF] Salomaa | Deterministic tree pushdown automata and monadic tree rewriting systems[END_REF]). Hence reachability is decidable in PTIME in the uncontrolled case.

The conditional grammars of [START_REF] Dassow | Handbook of Formal Languages, volume 2, chapter Grammars with Controlled Derivations[END_REF] can be redefined in our settings as (word) grammars whose production rules are CF controlled rewrite rules (and derivations are defined using the controlled rewrite relation). It is shown in [START_REF] Dassow | Handbook of Formal Languages, volume 2, chapter Grammars with Controlled Derivations[END_REF] that the class of languages of conditional grammars without collapsing rules coincide with CS (word) languages. Hence, it also holds that reachability is PSPACE-complete and regular model checking is undecidable for CF non-collapsing CntTRS over unary signatures.

Prefix control

Some other former results in the case of words imply that the above lower bounds still hold when control is limited to prefix SA. It is shown in [START_REF] Penttonen | One-sided and two-sided context in formal grammars[END_REF] that every CS word language can be generated by a CS grammar with production rules of the form AB → AC, A → BC, A → a (where A, B, C are non-terminal and a is a terminal). It follows that every CS word language is the closure of a constant symbol under a CF non-collapsing pCntTRS (over a unary signature).

Proposition 7. For all CS tree language L over a unary signature Σ, there exists a CF non-collapsing pCntTRS R over

Σ ′ ⊃ Σ such that L = R * ({c}) ∩ T (Σ) for some constant c ∈ Σ ′ 0 \ Σ.
Proof. Since L is the language over unary symbols, L can be regarded as a word language. Moreover, we can easily construct a pCntTRS that has the rule c → S(⊥) where S is the start symbol of the grammar for L and inverse of every production rule. ⊓ ⊔ Corollary 3. Reachability is PSPACE-complete and regular model checking undecidable for CF non-collapsing pCntTRS over unary signatures.

Another consequence of Proposition 7 is that deterministic top-down SA (which are incomparable with prefix SA in general but more general than prefix SA in unary signatures) already capture CS languages, for unary signatures.

To add a final remark, we can observe that following Example 3, there is no hope of regularity preservation even for very simple CF CntTRS containing only flat and monotonic rules, and even restricting to prefix control.

Non-monotonic rewrite rules

It is also shown in [START_REF] Dassow | Handbook of Formal Languages, volume 2, chapter Grammars with Controlled Derivations[END_REF] that the class of languages of conditional grammars with collapsing rules coincide with recursively enumerable languages. As a consequence, reachability is undecidable for CF CntTRS (with collapsing rules) already in the case of unary signatures. Actually, the following propositions shows that flat (but not monotonic) controlled rewrite rules are sufficient for the simulation of Turing machines. Proposition 8. Reachability is undecidable for flat CntTRS over unary signatures.

Proof. Flat CntTRS is a super class of monotonic and flat CntTRS. We can extend the flat CntTRS R that simulates the moves of LBA in the proof for Proposition 6, by adding some flat rules of the form : → ♭: and ♭: →: to R (: denotes the right endmarker), in order to simulate all the moves of a TM. ⊓ ⊔ Note that when the signature is unary, all the rewrite rules are necessary linear. Again, this result is in contrast with the case of uncontrolled rewriting, because linear and flat TRS preserve regularity, and hence have a decidable reachability problem. Restricting the control to prefix permits to obtain a decidability result for non-monotonic rewrite rules, as long as they are not collapsing.

Theorem 2. Reachability is decidable in PSPACE for flat non-collapsing pC-ntTRS over unary signatures.

Proof. We show the following claim:

u rewrites to v iff u = u 0 -→ R u 1 -→ R • • • -→ R u k = v with u 0 , . . . , u k ≤ max ( u , v ).
The "if" direction is trivial. For the "only if" direction, assume given a reduction u = w 1 * -→ R w n = v, and let max ( u , v ) = M . We make an induction on the number of strings w i longer than M . Suppose that the reduction contains one w i such that ||w i || > M . Then there exists a sub-sequence w k

+ -→ R w m such that w k = w m = M , with k < m. It holds that w k = w k [⊥] M * -→ R w m [⊥] M =
w m because we consider only prefix control. This reduces the number of string w i longer than M .

⊓ ⊔

Non-monotonicity is also a source of undecidability of reachability for Cnt-TRS even in the case of ground controlled rewrite rules. Proposition 9. Reachability is undecidable for ground CntTRS.

Proof. By representing the words a 1 , . . . , a n as right combs f (a

1 , f (• • • f (a n , ⊥))),
we can construct a ground CntTRS that simulates the moves of Turing Machine. Like in the proof of Propositions 8 and 6, one move of the of the TM is simulated by several rewrite steps, controlling the context left or right of the current position of the TM's head. Here, the controlled rewrite rule will have the form A : a → a ′ were a and a ′ are constant symbols, and A controls c and d in a configuration f (. . . f (c, f (a, f (d(, . . .))))), where a is at the rewrite position. ⊓ ⊔ This result is in contrast to uncontrolled ground TRS, for which reachability is decidable in PTIME.

Recursive Prefix Control

We propose a relaxed form of control, where, in order to select the positions of application of a controlled rewrite rule, the term to be rewritten is tested for membership in the closure of a regular language L, instead of membership to L directly. The idea is somehow similar to conditional rewriting (see e.g. [START_REF] Baader | Term Rewriting and All That[END_REF]) where the conditions are equations that have to be solved by the rewrite system.

The definition is restricted to control with prefix SA, and a recursive pCnt-TRS R is defined as a pCntTRS. In order to define formally the rewrite relation, let us recall first that in the computations of a prefix SA A, the states below a selection state q s are universal (q 0 ), i.e. that we can have any subterm at a selected position (only the part of the term above the selected position matters). Following this observation, we say that the variable position p in a context C[x 1 ] over Σ is selected by the prefix SA A if p is selected in C[c] where c is an arbitrary symbol of Σ 0 . A term s rewrites to t in one step by a recursive pCntTRS R, denoted by s --→ R t, if there exists a controlled rewrite rule A : ℓ → r ∈ R, where A is a prefix SA, a substitution σ, a position p ∈ Pos(s), and a context

C[x 1 ] such that C[x 1 ] --→ * R s[x 1 ] p and the position of x 1 is selected in C[x 1 ]
by A, such that s| p = ℓσ and t = s[rσ] p . This definition is well-founded because of the restriction to prefix control (remember that the root position is always selected by prefix SA).

Example 5. Let Σ = {a, b, c, d, ⊥} be a unary signature, and let R be the flat recursive pCntTRS containing the rules C 1 : a(a(x)) → b(x), and C 2 : c(x) → d(x), where the SA C 1 selects the position after a prefix aa, and C 2 selects the position after a prefix aaaa. Then we have with R (we omit the parentheses and the tail ⊥, and underline the part of the term which is rewritten) aaaac --→ R aabc --→ R aabd Note that for the last step, we have use the fact that aaaa --→ R aab, i.e. there exists C[x 1 ] = aaaa(x 1 ) with C[x 1 ] --→ R aab(x 1 ) and the position of x 1 in C[x 1 ] is selected by C 2 . The last rewrite step would not be possible if R would not be recursive, because aab is not a prefix admitted by C 2 .

Theorem 3. Regular model-checking is decidable in EXPTIME for linear and right-shallow recursive pCntTRS.

Proof. (sketch) We show that, given a right-shallow and linear recursive pCnt-TRS R and given the language L ⊆ T (Σ) of a TA A L we can construct an alternating tree automaton with epsilon-transitions (ε-ATA) A ′ recognizing the rewrite closure R * (L). Intuitively, an alternating tree automata A is a top-down tree automaton that can spawn in several copies during computation on a term t. Formally, an ε-ATA over a signature Σ is a tuple A = Q, q 0 , δ where Q is a finite set of states, q 0 ∈ Q is the initial state and δ is a function which associates to every state q ∈ Q a disjunction of conjunctions of propositional variables of the following form a ∈ Σ, or q ′ , ε , for q ′ ∈ Q \ {q}, or q ′ , i , for q ′ ∈ Q and 1 ≤ i ≤ m where m is the maximal arity of a symbol in Σ. A run of A on t ∈ T (Σ) is a function ρ from Pos(t) into 2 Q such that for all position p ∈ Pos(t), with t(p) = a ∈ Σ n (n ≥ 0), and for all state q ∈ ρ(p), it holds that a, ρ(p.1), 1 , . . . , ρ(p.n), n , ρ(p), ε |= δ(q) where S, p is a notation for all the variables q, p with q ∈ S, and |= denotes propositional satisfaction, while assigning true to the propositional variables on the left of |=. The language L(A) of A is the set of terms t ∈ T (Σ) on which there exists a run ρ of A such that q 0 ∈ ρ(ε) (terms recognized by A).

Roughly, the principle of the construction of A ′ is to start with A L and the SA of R, casted into ATA and merged, and to complete the transition functions in order to reflect the effect of the possible rewrite steps. The detailed construction can be found in Appendix D. Let us present below the construction on an example, based on the recursive pCntTRS R of Example 5. The transitions of the prefix SA C 1 and C 2 , for control in R are explicitly the following

C 1 : ⊥ → q 1 s | q 1 0 , f (q 1 0 ) → q 1 s | q 1 0 , a(q 1 s ) → q 1 1 , a(q 1 1 ) → q 1 2 (f ∈ {a, b, c, d}) C 2 : ⊥ → q 2 s | q 1 0 , f (q 2 0 ) → q 2 s | q 2 0 , a(q 2 s ) → q 2 1 , a(q 1 1 ) → q 2 2 , a(q 2 2 ) → q 2 3 , a(q 2 3 ) → q 2 4
They are casted into the following transition functions

δ 1 : q 1 2 → a ∧ q 1 1 , 1 , q 1 1 → a ∧ q 1 s , 1 , δ 2 : q 2 4 → a ∧ q 2 3 , 1 , q 2 3 → a ∧ q 2 2 , 1 , q 2 2 → a ∧ q 2 1 , 1 , q 2 1 → a ∧ q 2 s , 1 with moreover δ i (q i s ) = ⊥ ∨ f =a,b,c,d (f ∧ q i 0 , 1 ) and δ i (q i 0 ) → ⊥ ∨ f =a,b,c,d (f ∧ q i 0 , 1 ) for i = 1, 2.
The initial language L = {aaaac} is recognized by a ε-ATA A ′ L with the transition function δ L : q 5 → a ∧ q 4 , 1 , q 4 → a ∧ q 3 , 1 , q 3 → a ∧ q 2 , 1 , q 2 → a ∧ q 1 , 1 , q 1 → c ∧ q 0 , 1 , q 0 → ⊥.

Let δ 0 be the union of δ 1 , δ 2 and δ L . It holds that, starting from q 3 , δ 0 permits to "reach" a(a(q 1 )), denoted a(a(q 1 )) |= 0 q 3 . Formally, the relation t |= i q holds in the following cases, for t = a(t 1 , . . . , t n ) ∈ T (Σ ∪ Q), with n ≥ 0 and the symbols of Q are assumed of arity 0 δ i (q) = φ 1 ∨ φ 2 and t |= i φ 1 or t |= i φ 2 δ i (q) = φ 1 ∧ φ 2 and t |= i φ 1 and t |= i φ 2 δ i (q) = q ′ , ε and t |= i q ′ δ i (q) = q ′ , j , with 1 ≤ j ≤ n and t j |= i q ′ δ i (q) = a.

In order to simulate the first rule of R, we let δ 1 (q 3 ) = δ 0 (q 3 )∨ b∧ q 1 , 1 ∧ q 1 s , ε . The term a(a(q 1 )) corresponds to the lhs of this rule, b(q 1 ) is matching the rhs and q 1 s , ε ensures that the control is satisfied (following the recursive definition). Similarly, a(a(q 2 s )) |= 1 q 2 2 , and we can let δ 2 (q 2 2 ) = δ 0 (q 2 2 ) ∨ b ∧ q 2 s , 1 ∧ q 1 s , ε . Moreover, c(q 0 ) |= 2 q 1 , and with the second rule of R, we can let

δ 3 (q 1 ) = δ 0 (q 1 ) ∨ d ∧ q 0 , 1 ∧ q 2 s , ε .
With these transitions, we have the following runs for 2 descendants of

L a a b c ⊥ q 5 q 1 2 q 4 q 1 1 q 3 q 1 s q 1 q 1 0 q 0 q 1 0 a a b d ⊥      q 5 q 2 4 q 1 2           q 4 q 2 3 q 1 1           q 3 q 2 2 q 1 s           q 1 q 2 s q 1 0           q 0 q 2 0 q 1 0     
The ε-ATA A ′ can be casted into a TA A whose size is exponential in the size of A ′ and such that L(A) = L(A ′ ) = R * (L), and hence we can decide the problem of regular model checking for R in exponential time.

⊓ ⊔

Conclusion

We have proposed a definition of controlled term rewrite systems based on selection automata for the specification of authorized rewrite position, and a restriction where the selection of a position depends only on the labels on its prefix path. We have shown that reachability is PSPACE-complete for controlled monotonic (non-size-reducing) rewrite rules, using context-sensitive tree languages, and for prefix-controlled context-free non-collapsing rewrite rules. When allowing size decreasing rules, reachability becomes undecidable, even for flat and linear or ground rules. Finally, we have presented a relaxed form of prefix control called recursive prefix control which permits to obtain preservation of regular tree languages, hence decidability of reachability and regular model checking (in EXP-TIME). The proof involves the construction of alternating tree automata with ε-transitions, and we believe that this technique could be useful for computing the rewrite closure of other classes of automata with local constraints.

The proof of undecidability for ground CntTRS (Proposition 9) does not work when restricting to prefix control. It could be interesting to know whether reachability is decidable for ground pCntTRS. Also, we are interested in knowing how the decidability result of Theorem 2 can be generalized to non-unary signatures.

In [START_REF] Dassow | Handbook of Formal Languages, volume 2, chapter Grammars with Controlled Derivations[END_REF], the conditional grammars (i.e. controlled (in the above sense) contextfree word grammars) are related to grammars with a restriction on the possible production sequences (the list of names of production rules used must belong to a regular language). It could be interesting to establish a similar comparison for term rewriting. In particular, results on the restriction defined by authorized sequences of rewrite rules could be useful for the analysis of languages for the extensional specification of the set of possible rewrite derivations like in [START_REF] Borovansky | Rewriting with strategies in elan: a functional semantics[END_REF].

Rewriting of unranked ordered labeled tree has been much less studied that its counterpart for ranked terms. We would like to study controlled rewriting in this case, in particular in the context of update rules for XML [START_REF] Chamberlin | Xquery update facility 1.0. W3C Candidate Recommendation[END_REF][START_REF] Jacquemard | Rewrite-based verification of xml updates[END_REF].

Simulation of one-step of inverse production. LBA M ℓ can simulate the string rewriting α

(ℓ) = ℓ 1 (x 1 σ)ℓ 2 (x 2 σ) • • • (x m σ)ℓ n σ → α(r) = r 1 (x m1 σ)r 2 (x m2 σ) • • • (x mm σ)r n ′ σ where ℓ → r ∈ R for inverse monotonic TRS R, i.e. ||ℓ|| ≥ ||r||, l i , r j ∈ (Σ ∪ {(, )}) * for 1 ≤ i ≤ n and 1 ≤ j ≤ n ′ , σ is substitution in X → (Σ ∪ {(, )}) * , x i ∈ X for 1 ≤ i ≤ m,
and x mj ∈ {x 1 , . . . x m } and no x i and x j for i = j are same.

M ℓ is constructed by connecting the following automata.

1. LBA M ℓ in such that Initial state q ℓ in Final state q ℓ1 in Behavier Head of the automaton moves right and can change state to q ℓ1 in in any time.

LBA M

li for 1 ≤ i ≤ n such that Initial state q ℓi in Final state q ℓi f Behavier u 1 q ℓi in • • • u k v * ---→ M ℓ i ♭ * v q ℓ i f if u 1 • • • u n = ℓ i .
Otherwise, the automaton terminate and input does not accepted. The final state appears at v i.e. the next symbol of rewritten ℓ i .

LBA M

i() for 1 ≤ i ≤ n -1 and n > 1 such that Initial state q ℓi f Final state q ℓi+1 in
Behavier If first symbol is "(", then move head to next symbol of corresponding ")" and change state to q ℓi+1 in . 4. LBA M ← such that Initial state q ℓn f Final state q mσ in Behavier Move left until reading ")". 5. LBA M iσ for 1 ≤ i ≤ msuch that Initial state q iσ in Final state q iσ f Behavier Move "(x i σ)" to right until the next symbol become other than ♭. Final state appears at the first position of "(" in "(x i σ)". 6. LBA M iσ← for 2 ≤ i ≤ m such that Initial state q iσ f Final state q (i-1)σ in Behavier Move left until reading ")". 7. LBA M sh such that

Initial state q 1σ f Final state q sh f Behavier Shuffle "(x 1 σ) • • • (x m σ)" to "(x m1 σ) • • • (x mm σ)".
Final state appears at first "(" in "(x m1 σ)". 8. LBA M ′← such that Initial state q sh f Final state q r1 in Behavier Move left until reading the symbol other than ♭. 9. LBA M ri for 1 ≤ i ≤ n ′ such that Initial state q ri in Final state q ri f Behavier Rewrite ♭ * to r i . The final state appears at the next symbol of r i . 10. LBA M ′i() for 1 ≤ i ≤ n ′ such that Initial state q ri f Final state q ri+1 in Behavier Move "(u)" that is most near and at right side of head to left until no symbol ♭ is there at left of "(u)". Final state appears at next symbol of ")" of "(u)". 11. LBA M ♭ such that Initial state q

r n ′ f Final state q ℓ f
Behavier Move all of ♭ to right-end and finally head move to left-end. Move ♭ to right-end.

In the following, we prove that

C[ℓσ] -→ R C[rσ] iff α(C)[α(ℓσ)] * -→ A α(C)[α(rσ)] for inverse monotonic TRSs. Lemma 3. If C[ℓσ] -→ R C[rσ] for inverse monotonic TRS R, then || : q l in α(C)[α(lσ)]: * -→ A ♭ l q l f α(C)[α(rσ)]♭ * : ||. Proof. From Lemma 1, we can take α(C) = u 1 • • • u k v 1 • • • , v h , α(ℓσ) = ℓ 1 (x 1 σ) • • • (x m σ)ℓ n , and α(rσ) = r 1 (x m1 σ) • • • (x mm σ)r n .
Thus, this lemma holds from the following transition sequence.

:q ℓ in uℓ 1 (x 1 σ) • • • (x m σ)ℓ n v: (1) * --→ M ℓ :uq ℓ1 in ℓ 1 (x 1 σ) • • • (x m σ)ℓ n v: (2) * ---→ M ℓ 1 :u♭ * q ℓ1 in (x 1 σ) • • • (x m σ)ℓ n v: (3) * ---→ A 1() :u♭ * (x 1 σ)q ℓ2 in • • • (x m σ)ℓ n v: (4) * ------→ A ℓ i ,A i () :u♭ * (x 1 σ) • • • (x m σ)♭ * q ℓn f v: (5) * --→ A ← :u♭ * (x 1 σ) • • • (x m σq mσ in )♭ * v: (6) * ---→ A mσ :u♭ * (x m1 σ)σ) • • • ♭ * q mσ f (x m σ)v: (7) * -------→ A iσ ,A iσ← :u♭ * q 1σ f (x 1 σ) • • • (x m σ)v: (8) * --→ A sh :u♭ * q sh f (x m1 σ) • • • (x mm σ)v: (9) * ---→ A ′← :uq r1 in ♭ * (x m1 σ) • • • (x mm σ)v: (10) * --→ A r 1 :ur 1 q r1 f ♭ * (x m1 σ) • • • (x mm σ)v: (11) * ---→ A ′i() :ur 1 (x m1 σ)q r2 in ♭ * • • • (x mm σ)v: (12) * ------→ A r i ,A ′i() :ur 1 (x m1 σ) • • • (x mm σ)r n ′ q r n ′ f ♭ * v: (13) * --→ A ♭ :q ℓ f ur 1 (x m1 σ) • • • (x mm σ)r n ′ v♭ * : (14)
Since ||ℓ|| ≥ ||r||, we can generate the all r i 's because Σ n i=1 ||ℓ i || < Σ n ′ i=1 ||r i || and there are sufficient ♭'s to be rewritten to each r i .

⊓ ⊔ Lemma 4.

If :q l in α(C)[α(ℓ ′ σ)]: * --→ A l :q l f α(C)[α(r ′ σ)]♭ * : , then C[ℓ ′ σ] -→ R C[r ′ σ] for monotonic TRS R. Proof. From Lemma 1, we can represent α(C[ℓ ′ σ]) and α(C[r ′ σ]) as uℓ ′ 1 (x 1 σ) • • • (x m σ)ℓ ′ n v and ur ′ 1 (x m1 σ) • • • (x mm σ)r ′ n ′ v where α(C) = u v, α(ℓ ′ σ) = ℓ ′ 1 (x 1 σ) • • • (x m σ)ℓ ′ n , and α(r ′ σ) = r ′ 1 (x m1 σ) • • • (x mm σ)r ′ n ′ . From the construction of A ℓ , the transition :q ℓ in uℓ ′ 1 (x 1 σ) • • • (x m σ)ℓ ′ n v: * --→ A ℓ :q ℓ f r ′ 1 (x m1 σ) • • • (x mm σ)r ′ n ′ ♭ * : is as of the form the transition in Lemma 3. Transition :uq ℓ1 in ℓ 1 (x 1 σ) • • • (x m σ)ℓ n v: * --→ A ℓ :u♭ * (x 1 σ) • • • (x m σ)♭ * q ℓn f v: and :uq r1 in ♭ * (x m1 σ) • • • (x mm σ)r n ′ v: * --→ A ℓ :ur 1 (x m1 σ) • • • (x mm σ)r n ′ q r n ′ f v: implies that ℓ 1 (x 1 σ) • • • (x m σ)ℓ n = α(lσ) and r 1 (x m1 σ) • • • (x mm σ)r n ′ = α(rσ) for some l → r ∈ R. Thus, we have C[ℓ ′ σ] -→ R C[r ′ σ]. ⊓ ⊔ We construct the LBA A = Q, Γ, q in , {q f }, Θ that simulates context-sensitive grammar G = N, T, P, S from A ℓ 's for ℓ → r ∈ P -1 . Q is disjoint union of all Q ℓ 's.
Γ are same for all A ℓ 's. Θ is consists of union of all Θ ℓ 's and the rules q in , x, q in , x, left for x = :, q in , :, q ℓ in , :, right , q ℓ f , :, q in , :, stay , q in , :, q S1 , :, right , q S1 , "(", q S2 , "(", right , q S2 , S, q S3 , S, right , q S3 , ")", q ♭ , ")", right , q ♭ , ♭, q ♭ , ♭, right , and q ♭ , : , q f , : , stay .

The following lemmas state completeness and soundness of LBA A.

Lemma 5. If t ∈ L(G), then α(t) ∈ A.
Proof. We prove that :q in α(t): * -→ A : (S)♭ * q f : for the start symbol S of G. If t = S, then this lemma holds trivially. Otherwise, let t -→ P t ′ * -→ P S. We have :q in α(t): * -→ A q ℓ in :α(t): * -→ A q ℓ f :α(t ′ ): -→ A q in :α(t ′ ): from Lemma 3. Thus, we have q in :α(t): * -→ A q f :(S)♭ * : by applying lemma 3 as the above transition. ⊓ ⊔ Lemma 6. If α(t) ∈ A, then t ∈ L(G).

Proof. α(t) ∈ A implies :q in α(t): * -→ A :(S)♭ * q f : . If t = S, then this lemma holds trivially. Otherwise, we have the transition :q in α(t): * -→ A q ℓ in :α(t): -→ A q ℓ f :α(t ′ ): * -→ A :(S)♭ * q f : for some ℓ and t ′ . From lemma 4, we have t -→ R t ′ . Thus, we have t -→ R S by applying lemma 4 repeatedly.

⊓ ⊔

The Proposition 3 follows from Lemmata 5 and 6.

B Proof of Theorem 1

We give below a detailed proof of Theorem 1, which states that given a CSTG G and a monotonic CntTRS R, one can construct in PTIME a CSTG generating the closure of L(G) by R, and whose size is linear in the size of G and R.

We denote the ith rewrite rule of CntTRS by A i : ℓ i → r i where ℓ i , r i ∈ T (F, X) and

A i = Q i , Q f i , S i , ∆ i is a selection automaton.
We assume that Q i 's are disjoint each other. In the sequel, we use large character A for non-terminal, and C, C ′ for contexts that has no terminal, t for the term obtained by replacing every signature a in t by the non-terminal a , t λ for the term obtained by replacing root symbol f of t by f λ , and let

Q := i Q i , F := i F i , and
∆ := i ∆ i .
We sometimes denote the sequence of terms t 1 , . . . , t n by t for readability.

Completion procedure.

Input CSTG G = N , S, Σ, P such that arbitrary terminal a is only produced from the non-terminal a by the rule a (x 1 , . . . , x n ) → a(x 1 , . . . , x n ), and monotonic CntTRS R Output Context-sensitive tree grammar G * = N * , S λ , Σ, P * that recognizes R * (L(G)).

Step1(initialize) Let N * be as follows:

-

N * := N ∪ {A λ , A, q , A, q λ , A, q f in , A, q λ f in | A ∈ N , q ∈ Q, 1 ≤ i ≤ n}
where n is the number of rewrite rules. Before constructing P * , we construct P ′ to mark λ at root symbol.

P ′ := P ∪ {A λ (C[x 1 , . . . , x n ]) → A ′λ (C ′ [x 1 , . . . , x n ]) | A(C[x 1 , . . . , x n ]) → A ′ (C ′ [x 1 , . . . , x n ]) ∈ P } ∪ { a λ (x 1 , . . . , x n ) → a(x 1 , . . . , x n ) | a (x 1 , . . . , x n ) → a(x 1 , . . . , x n ) ∈ P }
P * is composed by P ′ and the following sets of production rules. These are used to simulate a selection automaton.

P A :=        f ( f 1 , q 1 (x 1 ), . . . , f n , q n (x n )) → f, q ( f 1 , q 1 (x 1 ), . . . , f n , q n (x n )) f λ ( f 1 , q 1 (x 1 ), . . . , f n , q n (x n )) → f, q λ ( f 1 , q 1 (x 1 ), . . . , f n , q n (x n )) f, f 1 , . . . , f n ∈ Σ, f (q 1 , . . . , q n ) → q ∈ ∆        P f in :=            f, q f λ (x) → f, q f λ f in (x) f, q f in ( f 1 , q 1 (x 1 ), . . . , f n , q n (x n )) → f ( f 1 , q 1 f in (x 1 ), . . . , f n , q n f in (x n )) f, q λ f in ( f 1 , q 1 (x 1 ), . . . , f n , q n (x n )) → f λ ( f 1 , q 1 f in (x 1 ), . . . , f n , q n f in (x n )) f, f 1 , . . . , f n ∈ Σ, f (q 1 , . . . , q n ) → q ∈ ∆ q ∈ F            P R := f, q f in ( l 1 , . . . , l n ) → r i f, q λ f in ( l 1 , . . . , l n ) → r i λ q ∈ S i , A i : f (l 1 , . . . , l n ) = ℓ i → r i ∈ R . P re :=        f, q λ (x) → f λ (x) f, q (x) → f (x) f, q λ f in (x) → f λ (x) f, q f in (x) → f (x) f ∈ Σ, q ∈ Q        P A is
used to simulate transition of SA, P f in is used to propagate information that final state occur at the root position by marking f in, P R is used to simulate rewriting by CntTRS R, and P re is used to clear states in each non-terminal of the form f, q . Lemma 7. S * -→ P A(t 1 , . . . , t n ) iff S λ * --→ P ′ A λ (t 1 , . . . , t n ). Proof. We can prove this lemma by induction on the length of * -→ P for only if part and * -→

P ′ for if part. ⊓ ⊔ Lemma 8. For all i, f (t 1 , . . . , t n ) * --→ Ai q iff f ( t 1 , . . . , t n ) * --→ G * f, q ( t 1 , . . . , t n ) and f λ ( t 1 , . . . , t n ) * --→ G * f, q λ ( t 1 , . . . , t n ).
Proof. Since Q i 's are disjoint each other, we can easily prove only if part of this Lemma by the rules in P A and P re . In the following, we prove if part by induction on

||f (t 1 , . . . , t n )||. Let f (t 1 , . . . , t n ) be f (f 1 (t 1 ), . . . , f n (t n )) for n ≥ 0. Since f, q is produced by the rule f ( f 1 , q 1 (x 1 ), . . . , f n , q n (x n )) → f, q ( f 1 , q 1 (x 1 ), . . . , f n , q n (x n ))
where f (q 1 , . . . , q n ) → q ∈ ∆ i for some i, we have f i (t i ) * --→ ∆i q i from the induction hypothesis. Thus, f (f 1 (t 1 ), . . . , f n (t n )) → q follows.

In the case where the root position has mark λ, we can prove similarly. ⊓ ⊔

Lemma 9. 1. For q ∈ Q i , C[f (t 1 , . . . , t n )] * --→ Ai C[q] * --→ Ai q f for some q f ∈ F i iff C λ [ f ( t 1 , . . . , t n )] * --→ G * C λ [ f, q f in ( t 1 , . . . , t n )] for ||C|| > 0, and 2. f (t 1 , . . . , t n ) * --→ Ai q f ∈ F i iff f λ ( t 1 , . . . , t n ) * --→ G *
f, q λ f in ( t 1 , . . . , t n ). Proof. 2 of this lemma follows from Lemma 8 and rules in P f in .

We prove both direction of 1 of this lemma by induction on the length of the position p that f (t

(t ′ n ))] * --→ Ai C ′ [f ′ (q ′ 1 , , . . . , q, . . . , q ′ n )] --→ Ai C ′ [q ′ ] * --→ Ai q f ∈ F i . Then, from Lemma 8, we have f i ( t ′ i ) * --→ G * f i , q ′ i ( t ′ i ) and f ( t 1 , . . . , t n ) * --→ G *
f, q ( t 1 , . . . , t n ), and from the induction hypothesis or 1 of this lemma, we have the production:

C ′ [ f ′ ( f 1 ( t ′ 1 ), . . . , f ( t 1 , . . . , t n ), . . . , f n ( t ′ n ))] * --→ G * C ′ [ f ′ , q ′ f in ( f 1 ( t ′ 1 ), . . . , f ( t 1 , . . . , t n ), . . . , f n ( t ′ n ))
] Thus, we obtaine the production

C ′ [ f ′ ( f 1 ( t ′ 1 ), . . . , f ( t 1 , . . . , t n ), . . . , f n ( t ′ n ))] * --→ G * C ′ [ f ′ , q ′ f in ( f 1 , q ′ 1 ( t ′ 1 ), . . . , f, q ( t 1 , . . . , t n ), . . . , f n , q ′ n ( t ′ n ))] --→ G * C ′ [ f ′ ( f 1 , q ′ 1 f in ( t ′ 1 ), . . . , f, q f in ( t 1 , . . . , t n ), . . . , f n , q ′ n f in ( t ′ n ))] --→ G * C ′ [ f ′ ( f 1 ( t ′ 1 ), . . . , f, q f in ( t 1 , . . . , t n ), . . . , f n ( t ′ n ))]
from the rule in P f in and P re , and f (q ′ 1 , . . . , q, . . . , q ′ n ) → q ′ ∈ ∆ i .

(if part) Since the non-terminal f, q f in must be produced by the rule f ′ , q ′ f in ( f 1 , q ′ 1 (x 1 ), . . . , f, q (x), . . . , f n , q ′ n (x n )) → f ′ ( f 1 , q ′ 1 f in (x 1 ), . . . , f, q f in (x) , . . . , f n , q ′ n f in (x n )), we have the production

C ′ [ f ′ ( f 1 ( t ′ 1 ), . . . , f ( t 1 , . . . , t n ), . . . , f n ( t ′ n ))] * --→ G * C ′ [ f ′ , q ′ f in ( f 1 , q ′ 1 ( t ′ 1 ), . . . , f, q ( t 1 , . . . , t n ), . . . , f n , q ′ n ( t ′ n ))].
Hence, from the induction hypothesis, we have

C ′ [f ′ (f 1 (t 1 ), . . . , f (t 1 , . . . , t n ), . . . , f (t n ))] * --→ ∆i C ′ [q ′ ] * --→
∆i q f for some q f ∈ F i . Moreover, we have f (q 1 , . . . , q, . . . , q n ) → q ∈ ∆ i since states are disjoint for each A i , and from Lemma 8, f i (t i * --→ Ai q i for all i and f (t 1 , . . . , t n ) * --→ Ai q. Therefore, we have

C[f (t 1 , . . . , t n )] * --→ Ai C[q] * --→ Ai q f ∈ F i . ⊓ ⊔ Lemma 10. If C[ℓσ] -→ R C[rσ] and C[ℓσ] ∈ L(G * ), then C[rσ] ∈ L(G * ). Proof.
Consider the case where ||C|| > 0. We suppose that C[ℓσ] is rewritten to C[rσ] by the rule A i : f (l 1 , . . . , l n ) → r. Then, we have the transition

C[f (l 1 , . . . , l n )σ] * --→ Ai C[q] * --→ Ai q f where q ∈ S i and q f ∈ Q f i . Since S λ * --→ G * C [ f (l 1 , . . . , l n )σ ], we have S λ * --→ G * C λ [ f, q ( l 1 , . . . , l n ) σ ] * --→ G * C λ [ f, q f in ( l 1 , . . . , l n ) σ ] 1 of Lemma 9.
From the production rule P R , we have

C [ f, q f in ( l 1 , . . . , l n ) σ ] * --→ G * C [ r σ ]. Thus, we have S λ * --→ G * C[rσ].
In the case of ||C|| = 0, we can prove similary to the previous case.

⊓ ⊔

Lemma 11. If s ∈ L(G) and s * -→ R t, then t ∈ L(G * ).
Proof. From Lemma 7, we have S λ * --→ G * s λ , and since P * has the rules in P and the rule f λ (x 1 , . . . , x n ) → f (x 1 , . . . , x n ), we have S λ * --→ G * s. By applying Lemma 10 repeatedly, we also have t ∈ L(G * ).

⊓ ⊔ Lemma 12. If t ∈ L(G * ), then there exists s such that s * -→ R t and s ∈ L(G).

Proof. We show this lemma by induction on the number of the rules in P R that occur in the production S * --→ G * t. Consider the case that there is no rule in P R in the production S λ * --→ G * t. We have

S λ * --→ G * t * --→ G * t.
Here we aim at one symbol a in t . Suppose that a is produced by the rule in P * \(P ∪ P R ). In this case, we can produce a by the rule of the form a, q → a or a, q f in → a . Since the symbols a, q or a, q f in is produced from a by the rules in P A and P f in , the symbol a must be produced by P . Moreover, this claim also holds for the symbols of the form a λ . By applying this claim to all symbols in t , we have S λ * -→

P ′ t ,
S λ * --→ G * C λ [ C 2 [ t 1 , . . . , t n ]] --→ PR C λ [ C 1 [ t 1 , . . . , t n ]] * --→ G * t.
From the construction of P R , we have the rewrite rule

A i : C 1 [x 1 , . . . , x m ] → C 2 [x 1 , . . . , x m ] where C 1 [x 1 , . . . , x m ]σ = C 1 [t 1 , . . . , t n ] and C 2 [x 1 , . . . , x m ]σ = C 2 [t 1 , . . . , t n ] for some σ. Since root symbol in C 2 is of the form f, q f in , we have the transition C[C 2 [t 1 , . . . , t n ]] * --→ Ai C[q] * --→
Ai q f for some q ∈ S i and q f ∈ Q f i from Lemma 9.

Hence If ||C|| = 0, then root symbol in C 2 is of the form f, q λ f . In this case, we can prove similary to the previous case.

⊓ ⊔ Theorem 1 follows from Lemma 11 and Lemma 12.

C Proof of Proposition 6

We give a detailed proof of Proposition 6, which states that reachability is NLINSPACE-complete and regular model checking is undecidable for monotonic and flat CntTRS over unary signatures. It works by reducing the acceptance (for reachability) and emptiness (for regular model checking) problems for linear bounded automata (LBA) [START_REF] Kuroda | Classes of languages and linear-bounded automata[END_REF].

Let M = P, Γ, p 0 , G, Θ be a non-deterministic LBA where P is the set of states, Γ is an input alphabet containing in particular the left and right endmarkers : and : are p 0 ∈ is the initial state, G ⊆ P is the set of accepting states and Θ is the transition relation in P × Γ × P × Γ × {left, right}. The transition relation Θ is such that M cannot move left from :, cannot move right from : or print another symbols over : or : . Let Γ ′ = Γ ∪ {a p | a ∈ Γ, p ∈ P } and let us define the unary signature Σ = Γ ′ ∪ (Γ ′ × Θ) ∪ {⊥}, where ⊥ has arity 0 and every other symbol has arity 1. For the sake of simplicity, a term a 1 (a 2 (. . . a n (⊥))) will be denoted by the string a 1 a 2 . . . a n .

Every configuration of M will be represented by a term of T (Σ) of the form :x 1 . . . x j-1 x p j x j+1 . . . x n : , where, for each 1 ≤ i ≤ n, x i ∈ Γ \ { :, : } is the content of the i th cell of the tape of M, j is the current position of the head of M and p ∈ P is the current state. In particular, given an input word x 1 . . . x n ∈ Γ \ { :, : } * , the initial configuration of M is represented by : x p0 1 x 2 . . . x n : . We assume indeed wlog that the computation space of M is limited to the exact size of the input word. We moreover assume wlog that when M reaches an accepting state, it writes a special blank symbol ♭ ∈ Γ \ { :, : } in all the cells of the tape (except the left and right ends), then moves to the leftmost cell, and finally changes its state to a special state p 1 which does not occur in the left hand of any transition of Θ.

To every transition θ = p, a, p ′ , b, left in Θ, we associate the four following monotonic and flat controlled rules : Γ * c a p Γ * : :

a p (x) → a p , θ (x) : Γ * c a p , θ Γ * : : c(x) → c, θ (x) : Γ * c, θ a p , θ Γ * : : a p , θ (x) → b(x) : Γ * c, θ bΓ * : : c, θ (x) → c p ′ (x)
We use here for SA a simplified notation with regular expressions, assuming that the SA selects the position of the only rewritable letter in the expression. Similarly, to every transition θ = p, a, p ′ , b, right in Θ, we associate the following controlled rules : Γ * a p c Γ * : :

a p (x) → a p , θ (x) : Γ * a p , θ c Γ * : : c(x) → c, θ (x) : Γ * a p , θ c, θ Γ * : : a p , θ (x) → b(x) : Γ * b c, θ Γ * : : c, θ (x) → c p ′ (x)
Let R be the CntTRS containing all the controlled rewrite rules associated to the transitions Θ. It is easy to show that R simulates the moves of M, and that only the correct moves of M are simulated by R. Therefore, with the above hypotheses, M will accept the initial word x 1 . . . x n iff :

x p0 1 x 2 . . . x n : --→ * R : ♭ p1 ♭ . . . ♭ n-1
: and the language of M is empty iff

R * :((Γ \ { :, : }) × P ) (Γ \ { :, : }) * : ∩ : ♭ p1 ♭ * : = ∅.

D Proof of Theorem 3

We give below a detailed proof of Theorem 3, stating that regular model-checking is decidable in EXPTIME for linear and right-shallow recursive pCntTRS. Given a right-shallow and linear recursive pCntTRS R and the language L ⊆ T (Σ) of a TA A L = Q L , F L , ∆ L , the proof is the construction of an alternating tree automata with epsilon-transitions (ε-ATA) A ′ recognizing the rewrite closure R * (L).

Intuitively, an alternating tree automata A is a top-down tree automaton that can spawn in several copies during computation on a term t. At every computation step, there are several copies of A in different positions of t, each copy in its own state. Initially, there is one copy of A in its initial state at the root of t. Then, the copies can be propagated down to the leaves step by step.

Formally, an alternating TA with ε-transitions (ε-ATA) over a signature Σ is a tuple A = Q, q 0 , δ where Q is a finite set of states, q 0 ∈ Q is the initial state and δ is a function which associates to every state q ∈ Q a disjunction of conjunctions of propositional predicates of the following form a ∈ Σ, -q ′ , ε , for q ′ ∈ Q \ {q}, -q ′ , i , for q ′ ∈ Q and 1 ≤ i ≤ m where m is the maximal arity of a symbol in Σ.

We say that a set P of predicates as above satisfies a disjunction of conjunctions where S, p is a notation for all the predicates q, p with q ∈ S.

The language L(A) of A is the set of terms t ∈ T (Σ) on which there exists a run ρ of A such that q 0 ∈ ρ(ε) (terms recognized by A).

Given an ε-ATA A = Q, q 0 , δ , one can build a TA A ′ = 2 Q , {S ⊆ Q | q 0 ∈ S}, ∆ where ∆ contains all the TA transitions of the form a(S 1 , . . . , S n ) → S, for a ∈ Σ n , S 1 , . . . , S n , S ⊆ Q such that for all q ∈ S, a, S 1 , 1 , . . . , S n , n , S, ε |= δ(q). With these definitions, it is easy to see that every run of A on t is also a run of A ′ on t, and reciprocally, hence L(A ′ ) = L(A).

On the other hand, given a TA A = Q, F, ∆ , one can construct an ε-ATA A ′ = Q ∪ {q 0 }, q 0 , δ , with q 0 / ∈ Q, δ(q 0 ) = q∈F q, ε , and for all q ∈ Q, δ(q) = a(q1,...,qn)→q∈∆ (a ∧ q 1 , 1 ∧ . . . ∧ q n , n )

We will now construct an ε-ATA A ′ recognizing the rewrite closure R * (L). Let sr(R) be the set of ground direct subterms of the rhs of rules of R. For each r ∈ sr(R), we construct a TA

A r = Q r , F r , ∆ r such that L(A r ) = {r}. It is defined by Q r = Pos(r), F r = {ε} and ∆ = {a(p.1, . . . , p.n) → p | p ∈ Pos(r), r(p) = a ∈ Σ n }.
Let A ′ r be the ε-ATA associated to A r as above. Let A ′ L = Q L , q 0 , δ L be the ε-ATA associated to A L and for each controlled rule C : ℓ → r of R, let C ′ be the ε-ATA associated to C. We assume wlog that all the automata defined above have disjoint state sets. We will construct incrementally a finite sequence of ε-ATA A ′ 0 , . . . , A ′ k whose last element A ′ k recognizes R * (L). The first ε-ATA of the sequence, A ′ 0 = Q 0 , q 0 , δ 0 is defined as the disjoint union of the ε-ATAs A ′ L , all the A ′ r for r ∈ sr(R), and all C ′ , for C prefix SA controlling a rule of R. Every other A ′ i in this sequence will be Q 0 , q 0 , δ i , where the transition function δ i is defined as follows.

We introduce a notation that will be useful for the construction of the δ i . Let t = a(t 1 , . . . , t n ) be a ground term of T (Σ ∪ Q), where n ≥ 0 and the symbols of Q are assumed of arity 0. We write t |= i q if we are in one of the following cases δ i (q) = φ 1 ∨ φ 2 and t |= i φ 1 or t |= i φ 2 δ i (q) = φ 1 ∧ φ 2 and t |= i φ 1 and t |= i φ 2 δ i (q) = q ′ , ε and t |= i q ′ δ i (q) = q ′ , j , with 1 ≤ j ≤ n and t j |= i q ′ δ i (q) = a.

Assume that we have constructed all the functions up to δ i , and let us define δ i+1 . If there is a linear controlled rule C : ℓ → b(r 1 , . . . , r m ) in R, where every r i is either a variable or a ground term of T (Σ), and a substitution σ from X into Q grounding for ℓ, for all state q ∈ Q such that ℓσ |= i q, let δ i+1 (q) = δ i (q)∨ b∧ i∈N q ri , i ∧ j∈V r j σ, j ∧ q s , ε , δ i+1 (q ′ ) = δ i (q ′ ) for all q ′ = q where N = {i ≤ m | r i ∈ T (Σ)}, V = {j ≤ m | r j ∈ X }, and q s is the unique selection state of the ε-ATA C ′ associated to C.

If there is a linear controlled rule C : ℓ → x in R, where x ∈ X, and a substitution σ from X into Q grounding for ℓ and such that ℓσ |= i q then let δ i+1 (q) = δ i (q) ∨ q s , ε , δ i+1 (q ′ ) = δ i (q ′ ) for all q ′ = q where q s is the unique selection state of the ε-ATA C ′ associated to C. The number of conjunctions that can be added to a δ i (q) in the above construction is bounded. Assuming that we do not add twice the same conjunction, the process will terminate with a fixpoint A ′ k = A ′ . The size of A ′ is polynomial in the sizes of A L and R. It can be shown that L(A ′ ) ⊆ R * (L) by induction on the multiset of indexes i of the transition functions δ i used in a run of A ′ on a term, and that L(A ′ ) ⊇ R * (L) by induction on the length of a rewrite sequence.

It follows that there exists a TA A whose size is exponential in the size of A ′ and such that L(A) = L(A ′ ) = R * (L), and hence we can decide the problem of regular model checking for R in exponential time.

Example 6. Let us come back the recursive pCntTRS R of Example 5. The transitions of the prefix SA C 1 and C 2 for control in R are explicitly the following (their final states are respectively q 1 2 and q 2 4 )

C 1 : ⊥ → q 1 s | q 1 0 , f (q 1 0 ) → q 1 s | q 1 0 , a(q 1 s ) → q 1 1 , a(q 1 1 ) → q 1 2 (f ∈ {a, b, c, d}) C 2 : ⊥ → q 2 s | q 1 0 , f (q 2 0 ) → q 2 s | q 2 0 , a(q 2 s ) → q 2 1 , a(q 1 1 ) → q 2 2 , a(q 2 2 ) → q 2 3 , a(q 2 3 ) → q 2 4

The associated ε-ATA C ′ 1 and C ′ 2 have the following transition functions δ 1 : q 1 2 → a ∧ q 1 1 , 1 , q 1 1 → a ∧ q 1 s , 1 , q 1 s → ⊥ ∨ f =a,b,c,d (f ∧ q 1 0 , 1 ),

q 1 0 → ⊥ ∨ f =a,b,c,d
(f ∧ q 1 0 , 1 )

δ 2 : q 2 4 → a ∧ q 2 3 , 1 , q 2 3 → a ∧ q 2 2 , 1 , q 2 2 → a ∧ q 2 1 , 1 , q 2 1 → a ∧ q 2 s , 1 , q 2 s → ⊥ ∨ f =a,b,c,d (f ∧ q 2 0 , 1 ), q 2 0 → ⊥ ∨ f =a,b,c,d (f ∧ q 2 0 , 1 )
Let us consider the initial language L = {aaaac}, recognized by the ε-ATA A ′ L with the following transition function δ L : q 5 → a ∧ q 4 , 1 , q 4 → a ∧ q 3 , 1 , q 3 → a ∧ q 2 , 1 , q 2 → a ∧ q 1 , 1 , q 1 → c ∧ q 0 , 1 , q 0 → ⊥.

The transition function δ 0 in the above construction is the union of δ 1 , δ 2 and δ L . It holds that a(a(q 1 )) |= 0 q 3 . Hence, with the first rule of R, we can let δ 1 (q 3 ) = δ 0 (q 3 ) ∨ b ∧ q 1 , 1 ∧ q 1 s , ε

Similarly, a(a(q 2 s )) |= 1 q 2 2 , and we can let δ 2 (q 2 2 ) = δ 0 (q 2 2 ) ∨ b ∧ q 2 s , 1 ∧ q 1 s , ε . Moreover, c(q 0 ) |= 2 q 1 , and with the second rule of R, we can let δ 3 (q 1 ) = δ 0 (q 1 ) ∨ d ∧ q 0 , 1 ∧ q 2 s , ε

With these transitions functions, we have the following runs for 2 descendants of L a a b c ⊥ q 5 q 1 2 q 4 q 1 1 q 3 q 1 s q 1 q 1 0 q

0 q 1 0 a a b d ⊥      q 5 q 2 4 q 1 2           q 4 q 2 3 q 1 1           q 3 q 2 2 q 1 s           q 1 q 2 s q 1 0           q 0 q 2 0 q 1 0     
automaton for the initial term aaaac q 5 ← -a q 4 ← -a q 3 ← -a q 2 ← -a q 1 ← -c q 0 ← --

⊥ selection automaton A 1 u 2 ← - a u 1 ← - a u s ←--- ⊥,Σ u 0 ← -- Σ u 0
(last transition is a loop) the sequence of transitions q 3 ← -a q 2 ← -a q 1 matches the lhs of the first rewrite rule A 1 : aa → b, and we add the alternating transition: q 3 ∧ u s ← -b q 1 . (the conjunction with u s simulates the recursive control) selection automaton A 2

v 4 ← - a v 3 ← - a v 2 ← - a v 1 ← - a v s ←--- ⊥,Σ v 0 ← -- Σ u 0
the sequence of transitions v 2 ← -a v 1 ← -a v s matches the lhs of the first rewrite rule A 1 : aa → b, and we add the alternating transition: v 2 ∧ u s ← -b v s . the transition q 1 ← -c q 0 matches the lhs of the second rewrite rule A 2 : c → d, and we add the alternating transition: q 1 ∧ v s ← -d q 0 . with these transitions, we have the following runs for 2 descendants of aaaac a a b c ⊥ q 5 u 2 q 4 u 1

q 3 u s q 1 u 0 q 0 u 0 a a b d ⊥      q 5 v 4 u 2           q 4 v 3 u 1           q 3 v 2 u s           q 1 v s u 0           q 0 v 0 u 0     

Corollary 1 .

 1 Moreover, we add to P ′ the rules obtained from the rules of R by replacing every symbol a ∈ Σ by N a . The CFTG G ′ = N ′ , S, Σ, P ′ generates the closure of L(G) by R.⊓ ⊔ Reachability and RMC are decidable in PTIME for CF TRS.

  1 , . . . , t n ) occur in C[f (t 1 , . . . , t n )]. Let C[x] = C ′ [f ′ (t ′ 1 , . . . , x, . . . , t ′ n )] and hence C[f (t 1 , . . . , t n )] is represented as C ′ [f ′ (t ′1 , . . . , f (t 1 , . . . , t n ), . . . , t ′ n )]. (only if part) Assume that we have the transition C ′ [f ′ (f 1 (t ′ 1 ), . . . , f (t 1 , . . . , t n ), . . . , f n

  and hence S * -→ P t from Lemma 7. Otherwise, let t = C[C 1 [t 1 , . . . , t n ]] where ||C|| > 1, and t is produced as

  we have C[C 2 [t 1 , . . . , t n ]] -→ R C[C 1 [t 1 , . . . , t n ]]. Here, we can easily obtain the production C λ [ C 2 [ t 1 , . . . , t n ]] * --→ G * C[C 2 [t 1 , . . . , t n ]]. Thus, there exists s such that s * -→ R C[C 2 [t 1 , . . . , t n ]] from the induction hypothesis and we have s * -→ R t.

  D, denoted by P |= D, if either D is the empty disjunction or D = C 1 ∨ . . . ∨ C k , for k ≥ 1, and there exists one j, 1 ≤ j ≤ k, such that every propositional predicate in the conjunction C j belongs to P .A run of A on t ∈ T (Σ) is a function ρ from Pos(t) into 2 Q such that for all position p ∈ Pos(t), with t(p) = a ∈ Σ n , n ≥ 0, and for all state q ∈ ρ(p),

	it
	holds that
	a, ρ(p.1), 1 , . . . , ρ(p.n), n , ρ(p), ε |= δ(q)

Acknowledgements

The authors wish to thanks Olivier Ly for his suggestion for the proof of Proposition 9, and Sylvain Schmitz, Géraud Senizergues and Hubert Comon-Lundh for their useful remarks and recommendations.

⋆ This work has been partly supported by the ERC research project FoX under grant agreement FP7-ICT-233599 and by the INRIA ARC project ACCESS.

A Proof of Proposition 3

We give here a non-deterministic linear space decision algorithm for the membership problem for CSTG, using a simulation of CSTG by linear bounded automata.

Let α be the transformation of terms of T (Σ) into strings defined as follows: α(x) = "(x)" for x ∈ X and α(f

Proof. We show this lemma by induction on the size of C. If ||C|| = 0, then this lemma holds trivially. Otherwise, let p 1 , . . . , p n be the positions where t i 's occur in C[t 1 , . . . , t n ]. We take

. For j such that there exists p i where jp ′ = p i for some

from the induction hypothesis. By applying the above claim for all

the number of the occurrence of signature in Σ, and ||t|| X is the number of the occurence of variables in X .

Proof. We show this lemma by induction on the structure of term.

From the induction hypothesis, we have ||α(t 1 )

where α(σ) = α(xσ) for all domain x of σ. Hence, we can simulate the term rewriting

Since each production rules of CSTG is monotonic, we can simulate inverse of production rules by LBA.

In the following, we show the simulation of one-step of inverse production of CSTG by LBA. For the production rule ℓ → r, let α(ℓσ

In the following, we use different notation for LBA from the one in the proof for Proposition 6 for readability. We denote the configuration such that the head of LBA reads u in u 1 • • • u • • • u n and whose state is q as :u 1 • • • uq • • • u n : , while we denote :u 1 • • • u q • • • u n : in the proof for Proposition 6.