Y Boichut

B Boyer

T Genet

A Legay

Equational Abstraction Refinement for Certified Tree Regular Model Checking

Tree Regular Model Checking (TRMC) is the name of a family of techniques for analyzing infinite-state systems in which states are represented by trees and sets of states by tree automata. The central problem is to decide whether a set of bad states belongs to the set of reachable states. An obstacle is that this set is in general neither regular nor computable in finite time. This paper proposes a new CounterExample Guided Abstraction Refinement (CEGAR) algorithm for TRMC. Our approach relies on a new equational-abstraction based completion algorithm to compute a regular overapproximation of the set of reachable states in finite time. This set is represented by R /E -automata, a new extended tree automaton formalism whose structure can be exploited to detect and remove false positives in an efficient manner. Our approach has been implemented in TimbukCEGAR, a new toolset that is capable of analyzing Java programs by exploiting an elegant translation from the Java byte code to term rewriting systems. Experiments show that TimbukCEGAR outperforms existing CEGAR-based completion algorithms. Contrary to existing TRMC toolsets, the answers provided by TimbukCEGAR are certified by Coq, which means that they are formally proved correct.

Introduction

Infinite-state models are often used to avoid potentially artificial assumptions on data structures and architectures, e.g. an artificial bound on the size of a stack or on the value of an integer variable. At the heart of most of the techniques that have been proposed for exploring infinite state spaces, is a symbolic representation that can finitely represent infinite sets of states. In this paper, we rely on Tree Regular Model Checking (TRMC) [START_REF] Bouajjani | Extrapolating tree transformations[END_REF][START_REF] Kesten | Symbolic model checking with rich assertional languages[END_REF], and assume that states of the system are represented by trees and sets of states by tree automata. The transition relation of the system is represented by a set of rewriting rules. Contrary to specific approaches that are dedicated to specific applications, TRMC is generic and expressive enough to describe a broad class of communication protocols [START_REF] Abdulla | Simulation-based iteration of tree transducers[END_REF], various C programs [START_REF] Bouajjani | Abstract rmc of complex dynamic data structures[END_REF] with complex data structures, multi-threaded programs [START_REF] Patin | Spade: Verification of multithreaded dynamic and recursive programs[END_REF], cryptographic protocols [START_REF] Genet | Rewriting for Cryptographic Protocol Verification[END_REF][START_REF] Genet | Verification of Copy Protection Cryptographic Protocol using Approximations of Term Rewriting Systems[END_REF][START_REF]Avispa -a tool for Automated Validation of Internet Security Protocols[END_REF], and Java [START_REF] Boichut | Rewriting Approximations for Fast Prototyping of Static Analyzers[END_REF].

In TRMC, the central objective is to decide whether a set of states representing some state-property belongs to the set of reachable states. An obstacle is that this set is in general neither regular nor computable in a finite time. Most existing solutions rely on computing the transitive closure of the transition relation of the systems through heuristic-based semi-algorithms [START_REF] Kesten | Symbolic model checking with rich assertional languages[END_REF][START_REF] Abdulla | Simulation-based iteration of tree transducers[END_REF], or on the computation of some regular abstraction of the set of reachable states [START_REF] Bouajjani | Extrapolating tree transformations[END_REF][START_REF] Bouajjani | Abstract rmc of complex dynamic data structures[END_REF]. While the first approach is precise, it is acknowledged to be ineffective on complex systems. This paper focuses on the second approach.

The first abstraction-based technique for TRMC, Abstract Tree Regular Model Checking (ATRMC), was proposed by Bouajjani et al [START_REF] Bouajjani | Abstract regular model checking[END_REF][START_REF] Bouajjani | Abstract regular tree model checking[END_REF][START_REF] Bouajjani | Abstract rmc of complex dynamic data structures[END_REF]. ATRMC computes sequences of automata by successive applications of the rewriting relation to the automaton representing the initial set of states. After each computation step, techniques coming from predicate abstraction are used to over-approximate the set of reachable states. If the property holds on the abstraction, then it also holds on the concrete system. Otherwise, a counter-example is detected and the algorithm has to decide if it is a false positive or not. In case of a spurious counter-example, the algorithm refines the abstraction by backward propagation of the set of rewriting rules. The approach, which may not terminate, proceeds in a CounterExample Guided Abstraction Refinement fashion by successive abstraction/refinement until a decision can be taken. The approach has been implemented in a toolset capable, in part, to analyse C programs. Independently, Genet et al. [START_REF] Genet | Decidable approximations of sets of descendants and sets of normal forms[END_REF] proposed Completion that is another technique to compute an over-approximation of the set of reachable states. Completion exploits the structure of the term rewriting system to add new transitions in the automaton and obtain a possibly overapproximation of the set of one-step successor states. Completion leads to a direct application of rewriting rules to the automaton, while other approaches rely on possibly heavy applications of sequences of transducers to represent this step. Completion alone may not be sufficient to finitely computes the set of reachable states. A first solution to this problem is to plug one of the abstraction techniques implemented in ATRMC. However, in this paper, we prefer another solution that is to apply equational abstraction [START_REF] Meseguer | Equational abstractions[END_REF]. There, the merging of states is induced by a set of equations that largely exploit the structure of the system under verification and its corresponding TRS, hence leading to accurate approximations. We shall see that, initially, such equations can easily be derived from the structure of the system. Latter, they are refined automatically with our procedure without manual intervention. Completion with equational abstraction has been applied to very complex case studies such as the verification of (industrial) cryptography protocols [START_REF] Genet | Rewriting for Cryptographic Protocol Verification[END_REF][START_REF] Genet | Verification of Copy Protection Cryptographic Protocol using Approximations of Term Rewriting Systems[END_REF] and Java bytecode applications [START_REF] Boichut | Rewriting Approximations for Fast Prototyping of Static Analyzers[END_REF]. CEGAR algorithms based on equational-abstraction completion exist [START_REF] Boichut | Finer is better: Abstraction refinement for rewriting approximations[END_REF][START_REF] Boichut | Characterizing conclusive approximations by logical formulae[END_REF], but are known to be inefficient.

In this paper, we design the first efficient and certified CEGAR framework for equational-abstraction based completion algorithm. Our approach relies on R /E -automaton, that is a new tree automaton formalism for representing sets of reachable states. In R /E -automata, equational abstraction does not merge states, but rather link them with rewriting rules labeled with equations. Such technique is made easy by exploiting the nature of the completion step. During completion steps, such equations are propagated, and the information can used to efficiently decide whether a set of terms is reachable from the set of initial states. If the procedure concludes positively, then the term is indeed reachable. Else, one has to refine the R /E -automaton and restart the process again.

Our approach has been implemented in TimbukCEGAR. (T)RMC toolsets result from the combination of several libraries, each of them being implemented with thousands of lines of code. It is thus impossible to manually prove that those tool deliver correct answers. A particularity of TimbukCEGAR is that it is certified. In order to ensure that the whole set of reachable states has been explored, any TRMC technique needs to check whether a candidate overapproximation B is indeed a fixed point, that is if L(B ) ⊇ R * (L(A)). Such check has been implemented in various TRMC toolsets, but there is no guarantee that it behaves correct. In [START_REF] Boyer | Certifying a Tree Automata Completion Checker[END_REF], a checker for tree automata completion was designed and proved correct using the Coq [START_REF] Bertot | Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions[END_REF] proof assistant. Any automaton B that passes the checker can be claimed to formally satisfy the fixed point. TimbukCEGAR implements an extension of [START_REF] Boyer | Certifying a Tree Automata Completion Checker[END_REF] for R /E -automata, which means that the tool delivers correct answers. Our TimbukCEGAR is capable, in part, of analyzing Java programs by exploiting a elegant translation from the javabyte code to term rewriting systems. Experiments show that TimbukCEGAR outperforms existing CEGAR-based completion algorithms by orders of magnitude.

Related work. Regular Model Checking (RMC) was first applied to compute the set of reachable states of systems whose configurations are represented by words [START_REF] Bouajjani | Regular model checking[END_REF][START_REF] Boigelot | Iterating transducers in the large (extended abstract)[END_REF][START_REF] Dams | Iterating transducers[END_REF]. The approach was then extended to trees and applied to very simple case studies [START_REF] Abdulla | Simulation-based iteration of tree transducers[END_REF][START_REF] Bouajjani | Extrapolating tree transformations[END_REF]. Other regular model checking works can be found in [START_REF] Abdulla | Parameterized verification of infinitestate processes with global conditions[END_REF][START_REF] Abdulla | Parameterized tree systems[END_REF], where an abstraction of the transition relation allows to exploit well-quasi ordering for finite termination. Such techniques may introduce false positives; a CEGAR approach exists for the case of finite word [START_REF] Abdulla | Constrained monotonic abstraction: A cegar for parameterized verification[END_REF], but not for the one of trees. Learning techniques apply to RMC [START_REF] Vardhan | Using language inference to verify omega-regular properties[END_REF][START_REF] Vardhan | Lever: A tool for learning based verification[END_REF] but trees have not yet been considered. We mention that our work extends equational abstractions [START_REF] Meseguer | Equational abstractions[END_REF][START_REF] Takai | A Verification Technique Using Term Rewriting Systems and Abstract Interpretation[END_REF] with counter-example detection and refinement. We mention the existence of other automata-based works that can handle a specific class of system [START_REF] Patin | Spade: Verification of multithreaded dynamic and recursive programs[END_REF]. CEGAR principles have been implemented in various tools such as Arme [START_REF] Podelski | Armc: The logical choice for software model checking with abstraction refinement[END_REF] or SLAM [START_REF] Ball | Slam and static driver verifier: Technology transfer of formal methods inside microsoft[END_REF]. Those specific tools are more efficient than our approach. On the other hand, RMC and rewriting rules offers a more general framework in where the abstraction and the refinements can be computed in a systematic manner.

Structure of the paper. Section 2 introduces the basic definitions and concepts used in the paper. TRMC and Completion are introduced in Section 3. R /E -automata are introduced in Section 4. A new completion procedure is then defined in Section 5. Section 6 proposes a CEGAR approach for TRMC and Completion. Section 7 presents TimbukCEGAR. Section 8 concludes the paper and discusses future research. Due to space constraints proofs are reported to appendix.

Background

In this section, we introduce some definitions and concepts that will be used throughout the rest of the paper (see also [START_REF] Baader | Term Rewriting and All That[END_REF][START_REF] Comon | Tree automata techniques and applications[END_REF][START_REF] Gilleron | Regular tree languages and rewrite systems[END_REF]). Let F be a finite set of symbols, each associated with an arity function, and let X be a countable set of variables. T (F, X ) denotes the set of terms and T (F) denotes the set of ground terms (terms without variables). The set of variables of a term t is denoted by Var(t). A substitution is a function σ from X into T (F, X ), which can be uniquely extended to an endomorphism of T (F, X ). A position p for a term t is a word over N. The empty sequence λ denotes the top-most position. The set Pos(t) of positions of a term t is inductively defined by

Pos(t) = {λ} if t ∈ X and Pos(f (t 1 , . . . , t n )) = {λ} ∪ {i.p | 1 ≤ i ≤ n and p ∈ Pos(t i )} otherwise. If p ∈ Pos(t)
, then t| p denotes the subterm of t at position p and t[s] p denotes the term obtained by replacement of the subterm t| p at position p by the term s.

A term rewriting system (TRS) R is a set of rewrite rules l → r, where l, r ∈ T (F, X ), l ∈ X , and Var(l) ⊇ Var(r). A rewrite rule l → r is left-linear (resp. right-linear) if each variable of l (resp. r) occurs only once in l. A TRS R is left-linear if every rewrite rule l → r of R is left-linear. The TRS R induces a rewriting relation → R on terms as follows. Let s, t ∈ T (F, X ) and l → r ∈ R, s → R t denotes that there exists a position p ∈ Pos(s) and a substitution σ such that s| p = lσ and t

= s[rσ] p . The reflexive transitive closure of → R is denoted by → * R and s → ! R t denotes that s → * R t and t is irreducible by R. The set of R- descendants of a set of ground terms I is R * (I) = {t ∈ T (F) | ∃s ∈ I s.t. s → * R
t}. An equation set E is a set of equations l = r, where l, r ∈ T (F, X ). For all equation l = r ∈ E and all substitution σ, we have lσ = E rσ. The relation = E is the smallest congruence such that for all substitution σ we have lσ = rσ. Given a TRS R and a set of equations E, a term s ∈ T (F) is rewritten modulo E into t ∈ T (F), denoted s → R/E t, if there exist s ∈ T (F) and t ∈ T (F) such that s = E s → R t = E t. Thus, the set of R-descendants modulo E of a set of ground terms

I is R /E * (I) = {t ∈ T (F) | ∃s ∈ I s.t. s → * R/E t}. Let Q be a finite set of symbols with arity 0, called states, such that Q ∩F = ∅. T (F ∪ Q) is called the set of configurations. A transition is a rewrite rule c → q,
where c is a configuration and q is state. A transition is normalized when c = f (q 1 , . . . , q n ), f ∈ F is of arity n, and q 1 , . . . , q n ∈ Q. A ε-transition is a transition of the form q → q where q and q are states. A bottom-up nondeterministic finite tree automaton (tree automaton for short) over the alphabet

F is a tuple A = F, Q, Q F , ∆ , where Q F ⊆ Q, ∆
L(A, q) = {t ∈ T (F) | t → * A q}. We define L(A) = q∈Q F L(A, q).

Tree Regular Model Checking with Completion

We first introduce Tree Regular Model Checking (TRMC), a tree automata based framework to represent possibly infinite-state systems. In TRMC, a program is represented by a tuple (F, A, R), where F is an alphabet on which a set of terms T (F) can be defined; A is the tree automaton representing a possibly infinite set of configurations I, and R is a set of term rewriting rules that represent a transition relation Rel. We consider the following problem.

Definition 1 (Reachability Problem (RP)). Consider a program (F, A, R) and a set of bad terms Bad. The Reachability Problem consists in checking whether there exists a term of R * (L(A)) that belongs to Bad.

For finite-state systems, computing the set of reachable terms (R * (L(A))) reduces to enumerating the terms that can be reached from the initial set of configurations. For infinite-state systems, acceleration-based methods are needed to perform this possibly infinite enumeration in a finite time. In general, such accelerations are not precise and the best one can obtain is an R-closed approximation

A * R,E . A tree automaton A * R,E is R-closed if for all terms s, t ∈ T (F) such that s → R t and s is recognized by A * R,E into state q then so is t. It is easy to see that if A * R,E is R-closed and L(A * R,E ) ⊇ L(A), then L(A * R,E ) ⊇ R * (L(A))
. A wide range of acceleration techniques have been developed, most of them have been discussed in Section 1. Here, we focus on Completion [START_REF] Genet | Decidable approximations of sets of descendants and sets of normal forms[END_REF], whose objective is to computes successive automata

A 0 R = A, A 1 R , A 2 R , .
. . that represent the effect of applying the set of rewriting rules to the initial automaton. To compute infinite sets in a finite time, each completion step is eventually followed by an widening operator. More precisely, each application of R, which is called a completion step, consists in searching for critical pairs t, q with s → R t, s → * A q and t → * A q. The idea being that the algorithm solves the critical pair by building from A i R , a new tree automaton A i+1 R with the additional transitions that represent the effect of applying R. As the language recognized by A may be infinite, it is not possible to find all the critical pairs by enumerating the terms that it recognizes. The solution that was promoted in [START_REF] Genet | Decidable approximations of sets of descendants and sets of normal forms[END_REF] consists in applying sets of substitutions σ : X → Q mapping variables of rewrite rules to states that represent infinite sets of (recognized) terms. Given a tree automaton A i R and a rewrite rule l → r ∈ R, to find all the critical pairs of l → r on A i R , completion uses a matching algorithm [START_REF] Feuillade | Reachability Analysis over Term Rewriting Systems[END_REF] that produces the set of substitutions σ : X → Q and states q ∈ Q such that lσ → *

A i R q and rσ → * A i R q.
Solving critical pairs thus consists in adding new transitions: rσ → q and q → q. Those new transitions may have to be normalized in order to satisfy the definition of transitions of tree automata (see [START_REF] Feuillade | Reachability Analysis over Term Rewriting Systems[END_REF] for details). As it was shown in [START_REF] Genet | Decidable approximations of sets of descendants and sets of normal forms[END_REF], this operation may add not only new transitions but also new states to the automaton. In the rest of the paper, the completion-step operation will be represented by C, i.e., the automaton obtained by applying the completion step to

A i R is denoted C(A i R ).
Observe that when considering right-linear rewriting rules, we have that C is precise, i.e. it does not introduce in A i+1 R terms that cannot be obtain from A i R by applying the set of rewriting rules. Observe also that if the system is non left-linear, then completion step may not produce all the reachable terms. Non left-linear rules will not be considered in the present paper.

The problem is that, except for specific classes of systems [START_REF] Feuillade | Reachability Analysis over Term Rewriting Systems[END_REF][START_REF] Genet | Reachability analysis of rewriting for software verification[END_REF], the automaton representing the set of reachable terms cannot be obtained by applying a finite number of completion steps. The computation process thus needs to be accelerated. For doing so, we apply a widening operator W that uses a set E of equations 5 to merge states and produce a R-closed automaton that is an overapproximation of the set of reachable terms, i.e., an automaton A * R,E such that

L(A * R,E ) ⊇ R * (L(A)
). An equation u = v is applied to a tree automaton A as follows: for all substitution σ : X → Q and distinct states q 1 and q 2 such that uσ → * A q 1 and vσ → * A q 2 , states q 1 and q 2 are merged. Completion and widening steps are applied, i.e.,

A i+1 R,E = W(C(A i R,E )), until a R-closed fixpoint A *
R,E is found. Our approximation framework and methodology are close to the equational abstractions of [START_REF] Meseguer | Equational abstractions[END_REF]. In [START_REF] Genet | Equational tree automata completion[END_REF], it has been shown that, under some assumptions, the widening operator may be exact, i.e., does not add terms that are not reachable.

Example 1. Let R = {f (x) → f (s(s(x)))} be a rewriting system, E = {s(s(x)) = s(x)} be an equation, and A = F, Q, Q F , ∆ be a tree automaton with Q F = {q 0 } and ∆ = {a → q 1 , f (q 1 ) → q 0 }, i.e. L(A) = {f (a)}. The first completion step finds the following critical pair: f (q 1 ) → * A q 0 and f (s(s(q 1 ))) → * A q 0 . Hence, the completion algorithm produces A 1 R = C(A) having all transitions of A plus {s(q 1 ) → q 2 , s(q 2 ) → q 3 , f (q 3 ) → q 4 , q 4 → q 0 } where s(s(q 1 ))

A 1 R * s(q 1 ) * A 1 R q 3 q 2
q 2 , q 3 , q 4 are new states produced by normalization of f (s(s(q 1 ))) → q 0 . Applying W with the equation s(s

(x)) = s(x) on A 1 R is equivalent to rename q 3 into q 2 . The set of transitions of A 1 R,E is thus ∆ ∪ {s(q 1 ) → q 2 , s(q 2 ) → q 2 , f (q 2 ) → q 4 , q 4 → q 0 }. Completion stops on A 1 R,E that is R-closed, and thus A * R,E = A 1 R,E .
Observe that if the intersection between A * R,E and Bad is not empty, then it does not necessarily mean that the system does not satisfy the property. Consider a set Bad = {f (s(a)), f (s(s(a)))}, the first term of this set is not reachable from A, but the second is. There is thus the need to successively refine the Rclosed automaton. The latter can be done by using a CounterExample Guided Abstraction Refinement algorithm (CEGAR). Developing such an algorithm for completion and equational abstraction is the objective of this paper.

R /E -Automata

Existing CEGAR approaches [START_REF] Bouajjani | Abstract regular model checking[END_REF][START_REF] Bouajjani | Abstract regular tree model checking[END_REF][START_REF] Bouajjani | Abstract rmc of complex dynamic data structures[END_REF][START_REF] Boichut | Finer is better: Abstraction refinement for rewriting approximations[END_REF] check for spurious counter examples by performing a sequence of applications of the rewriting rules to A * R,E . To avoid this potentially costly step, we suggest to replace the merging of states by the addition of new rewriting rules that carry out information on the merging through equations. Formally:

Definition 2 (R /E -automaton). Given a TRS R and a set E of equations, a R /E -automaton A is a tuple F, Q, Q F , ∆ ∪ ε R ∪ ε E . ∆ is a set of normalized transitions. ε E is a set of ε-transitions. ε R is a set of ε-transitions labeled by
or conjunctions over predicates of the form Eq(q, q ) where q, q ∈ Q, and q → q ∈ ε E .

Set ε R is used to distinguish a term from its successors that has been obtained by applying one or several rewriting rules. Instead of merging states according to the set of equations, A links them with epsilon transitions in ε E . During completion step, when exploiting critical pairs, the combination of transitions in ε E generates transition in ε R that are labeled with a conjunction of equations representing those transitions in ε E . In what follows, we use → * ∆ to denote the transitive and reflexive closure of ∆. Given a set ∆ of normalized transitions, the set of representatives of a state q is defined by

Rep(q) = {t ∈ T (F)|t → * ∆ q}.
Definition 3 (Run of a R /E -automaton A).

-t| p = f (q 1 , . . . , q n ) and f (q 1 , . . . , q n ) → q ∈ ∆ then t -→ A t[q] p -t| p = q and q → q ∈ ε E then t

Eq(q,q ) -----→ A t[q ] p -t| p = q and q α -→ q ∈ ε R then t α -→ A t[q ] p -u α -→ A v and v α -→ A w then u α∧α ---→ A w Theorem 1. ∀t ∈ T (F ∪ Q), q ∈ Q, t α -→ A q ⇐⇒ t → * A q
A run α -→ abstracts a rewriting path of → R/E . If t α -→ q, then there exists a term s ∈ Rep(q) such that s → * R/E t. The formula α denotes the subset of transitions of ε E needed to recognize t into q.

Example 2. Let I = f (a) be an initial set of terms, R = {f (c) → g(c), a → b} be a set of rewriting rules, and E = {b = c} be a set of equations. We build A an overapproximation automaton for R * (I), using E. Thanks to ε-transitions, the automaton A represented in Fig. 1 contains some information about the path used to reach terms using R and E. Each state has a representative term from which others are obtained. The equality b = c is represented by the two transitions q c → q b and q b → q c of ε E , taking into account that b and c are the representatives terms for states q b and q c , respectively. Consider now State q c , Transition q b → q c indicates that the term b is obtained from Term c by using the equality. Conversely, Transition q c → q b leads to the conclusion that Term c is obtained

q f q g f ( q a ) g( q c ) q a q b q c a b c
Eq(qc, q b ) = = Fig. 1: Automaton A q b → q a of ε R denote rewriting steps. The transition q b → q a denotes that the term b is a descendant of a by rewriting. Using Definition 3, the runs

f (c) Eq(qc,q b )
------→ q indicates that to obtain f (c) from f (a) -the representative term of q f -we used the equality b = c, which is obtained from q c → q b . We indeed observe f (a) → R f (b) = E f (c). If we now consider the transition q g → q f we labeled the transition with the formula Eq(q c , q b ). To reach g(c) from f (a), we rewrite f (c). We have seen this term is reachable thanks to the equivalence relation induced by b = c. By transitivity, this equivalence is also used to reach the term g(c). We thus label the transition of ε R to save this information. We obtain the run g(c)

Eq(qc,q b ) ------→ q f . We observe that the transition q b → q a is labeled by the formula since b is reachable from a without any equivalence. By congruence, so is f (b) from f (a). The run f (b) -→ q f denotes it.

We now introduce a property that will be used in the refinement procedure to distinguish between counter-examples and false positives.

Definition 4 (A well-defined R /E -automaton). A is a well-defined R /E - automaton, if :
-For all state q of A, and all term v such that v -→ A q, there exists u a term representative of q such that u

→ * R v -If q φ -→ q is a transition of ε R , then there exist terms s, t ∈ T (F) such that s φ → A q, t → A q and t → R s.
The first item in Definition 4 guarantees that every term recognized by using transitions labeled with the formula is indeed reachable from the initial set. The second item is used to refine the automaton. A rewriting step of → R/E denoted by q φ -→ q holds thanks to some transitions of ε E that occurs in φ. If we remove transitions in ε E in such a way that φ does not hold, then the transition q φ -→ q should also be removed.

According to the above construction, a term t that is recognized by using at least a transition labeled with a formula different from can be removed from the language of the R /E -automaton by removing some transitions in ε E . This "pruning" operation will be detailed in Section 6.

Solving the Reachability Problem with R /E -automaton

In this section, we extend the completion and widening principles introduced in Section 3 to take advantage of the structure of R /E -automata. We consider an initial set I that can be represented by a tree automaton A 0 R,E = F, Q 0 , Q F , ∆ 0 , and transition relation represented by a set of linear rewriting rules R. In the next section, we will see that the right-linearity condition may be relaxed using additionnal hypotheses. We compute successive approximations

A i R,E = F, Q i , Q f , ∆ i ∪ε i R ∪ε i E from A 0 R,E using A i+1 R,E = W(C(A i R,E )). Observe that A 0
R,E is well-defined as the sets ε 0 R and ε 0 E are empty.

The Completion step C

Extending completion to R /E -automaton requires to modify the concept of critical pair and so the algorithm to compute them. A critical pair for a R /Eautomaton is a triple rσ, α, q such that lσ → rσ, lσ

α -→ A i R,E q and there is no formula α such that rσ α -→ A i R,E q.
The resolution of such a critical pair consists of adding to

C(A i R,E ) the transitions to obtain rσ α -→ C(A i R,E
) q. This is followed by a normalization step Norm whose definition is similar to the one for classical tree automata (see appendix D).

Definition 5 (Resolution of a critical pair). Given a R /E -automaton A = F, Q, Q f , ∆ ∪ ε R ∪ ε E and a critical pair p = rσ, α, q , the resolution of p on A is the R /E -automaton A = F, Q , Q f , ∆ ∪ ε R ∪ ε E where -∆ = ∆ ∪ Norm(rσ, ∆ \ ∆ 0 ); -ε R = ε R ∪ {q α -→ q}
where q is the state such that rσ → ∆ \∆0 q ; -Q is the union of Q with the set of states added when creating ∆ .

Note that ∆ 0 , the set of transitions of A 0 R , is not used in the normalization process. This is to guarantee that A is well-defined. The R /E -automaton C(A i R,E ) is obtained by recursively applying the above resolution principle to all critical pairs p of the set of critical pairs between R and A i R,E . The set of all critical pairs is obtained by solving the matching problems l q for all rewrite rule l → r ∈ R and all state q ∈ A i R,E . Solving l q is in two steps. First, one computes S, that is the set of all couples (α, σ) such that α is a formula, σ is a substitution of X → Q i , and lσ α -→ q. The formula α is a conjunction of Predicate Eq that denotes the used transitions of ε E to rewrite lσ in q, in accordance with Definition 3. Due to space constraints the algorithm, which always terminates, can be found in Appendix C.

Second, after having computed S for l q, we identify elements of the set that correspond to critical pairs. By definition of S, we know that there exists a

transition lσ α -→ A i R,E q for (α, σ) ∈ S.
If there exists a transition rσ α -→ A i R,E q, then rσ has already been added to A i R,E . If there does not exist a transition of the form rσ α -→ A i R,E q, then rσ, α , q is a critical pair to solve on A i R,E . The following theorem shows that our methodology is complete.

Theorem 2. If A i R,E is well-defined then so is C(A i R,E ), and ∀q ∈ Q i , ∀t ∈ L(A i R,E , q), ∀t ∈ T (F), t → R t =⇒ t ∈ L(C(A i R,E ), q). Example 3. Let R = {f (x) → f (s(s(x)
))} be a set of rewriting rules and

A 0 R,E = F, Q, Q F , ∆ 0 be a tree automaton such that Q F = {q 0 } and ∆ 0 = {a → q 1 , f (q 1 ) → q 0 }. The solution of the matching problem f (x) q 0 is S = {(σ, φ)}, with σ = {x → q 1 } and φ = . Hence, since f (s(s(q 1 ))) -→ A 0
R,E q 0 , f (s(s(q 1 ))), , q 0 is the only critical pair to be solved. So, we have

C(A 0 R,E ) = F, Q 1 , Q F , ∆ 1 ∪ ε 1 R ∪ ε 0 E , with: ∆ 1 = Norm(f (s(s(q 1 ))), ∅) ∪ ∆ 0 = {s(q 1 ) → q 2 , s(q 2 ) → q 3 , f (q 3 ) → q 4 } ∪ ∆ 0 , ε 1 R = {q 4 -→ q 0 }, since f (s(s(q 1 ))) → ∆ 1 \∆ 0 q 4 , ε 0 E = ∅ and Q 1 = {q 0 , q 1 , q 2 , q 3 , q 4 }. Observe that if C(A i R,E ) = A i R,E
, then we have reached a fixpoint.

The Widening Step

W Consider a R /E -automaton A = F, Q, Q f , ∆ ∪ ε R ∪ ε E , the widening consists in computing a R /E -automaton W(A) that is obtained from A by using E.
For each equation l = r in E, we consider all pair (q, q ) of distinct states of Q i such that there exists a substitution σ to obtain the following diagram. Observe that = -→ A , the transitive and reflexive rewriting relation induced by ∆ ∪ ε E , defines particular runs which exclude transitions of ε R . This allow to build a more accurate approximation. The improvment in accurary is detailed in [START_REF] Genet | Equational tree automata completion[END_REF].

lσ E = A rσ = A q q
Intuitively, if we have u = -→ A q, then we know that there exists a term t of Rep(q) such that t = E u. The automaton W(A) is given by the tuple

F, Q, Q f , ∆ ∪ ε R ∪ ε E ,
where ε E is obtained by adding the transitions q → q and q → q to ε E (for each pair (q, q )).

Theorem 3. Assuming that A is well-defined, we have A syntactically included in W(A), and

W(A) is well-defined. Example 4. Consider the R /E -automaton C(A 0 R,E ) given in Example 3. Using Equation s(s(x)) = s(x), we compute A 1 R,E = W(C(A 0 R,E )).
We have σ = {x → q 1 } and the following diagram. We then obtain

A 1 R,E = F, Q 1 , Q f , ∆ 1 ∪ε 1 R ∪ ε 1 E , where ε 1 E = ε 0 E ∪ {q 3 → q 2 , q 2 → q 3 } and ε 0 E = ∅.
s(s(q 1 ))

E = C(A 0 R,E ) s(q 1 ) = C(A 0 R,E ) q 3 q 2 Observe that A 1 R,E is a fixpoint, i.e., C(A 1 R,E ) = A 1 R,E .
6 A CEGAR procedure for R /E -automata

Let R be a TRS, I be a set of initial terms characterized by the R /E -automaton A 0 R,E and Bad the set of forbidden terms represented by A Bad . We now complete our CEGAR approach by proposing a technique that checks whether a term is indeed reachable from the initial set of terms. If the term is a spurious counterexample i.e. an counter-example of the approximation, then it has to be removed from the approximation automatically, else one can deduce that the involved term is actually reachable.

Let

A k R,E = F, Q k , Q f , ∆ k ∪ ε k R ∪ ε k E be a R /E
-automaton obtained after k steps of completion and widening from A 0 R,E and assume that

L(A k R,E ) ∩ Bad = ∅. Let S A k
R,E ∩A Bad be a set of triples q, q , φ where q is a final state of A k R,E , q is a final state of A Bad and φ is a formula on transitions of ε k E and such that for each triple (q, q , φ), the formula φ holds if and only if there exists

t ∈ L(A k R,E , q) ∩ L(A Bad , q ) and t φ -→ A k R,E q. Note that S A k R,E
∩A Bad can be obtained using the algorithm in Definition 10 presented in Appendix H. We consider two cases. First, as A k R,E is well-defined, if φ = , we deduce that t is indeed a reachable term. Otherwise, φ is an formula whose atoms are of the form Eq(q j , q j ), and t is possibly a spurious counter-example, and the run

t φ -→ A k
R,E q must be removed. Refinement consists in computing a pruned version

P(A k R,E , S A k R,E ∩A Bad ) of A k R,E . Definition 6. Given a R /E -automaton A = F, Q, Q F , ∆ 0 ∪ ∆ ∪ ε R ∪ ε E and
a set of specified by the automaton A Bad , the prune process is defined by

P(A, S A∩A Bad ) =        P(A , S A ∩A Bad ) if S A ∩A Bad = ∅ and with A = Clean(A, S A∩A Bad ) A if S A∩A Bad = ∅ or there exists t ∈ Bad s.t. t -→ A q f and q f ∈ Q F .
where Clean(A, S A∩A Bad ), consists of removing transitions of ε E until for each q f , q f , φ ∈ S A∩A Bad , φ does not hold, i.e., φ =⊥ with q f , q f respectively two final states of A and A Bad .

To replace Predicate Eq(q, q ) by ⊥ in φ, we have to remove the transition q → q from ε E . In addition, we also have to remove all transitions q α -→ q ∈ ε R , where the conjunction α contains some atoms transitions removed from ε E . In general, removing Transition q → q may be too rude. Indeed, assuming that there also exists a transition q → q of ε E , removing the transition q → q also avoids the induced reduction q → q from the automaton and then, unconcerned terms of q are also removed. To save those terms, Transition q → q is added to ε E , but only if it has never been removed by a pruning step. This point is important to refine the automaton with accuracy. The prune step is called recursively as inferred transitions may keep the intersection non-empty. Theorem 4. Let t ∈ Bad be a spurious counter-example. The pruning process always terminates, and removes all the runs of the form t φ -→ q.

Example 5. We consider the R /E -automaton A of Example 2. It is easy to see that A recognizes the term g(c). Indeed, by Definition 3, we have g(c)

Eq(qc,q b ) ------→ q f . Consider now the rewriting path f (a) → R f (b) = E f (c) → R g(c). If we remove the step f (b) = E f (c) denoted by the transition q c → q b , then g(c)
becomes unreachable and should also be removed. The first step in pruning A consists thus in removing this transition. In a second step, we propagate the information by removing all transition of ε R labeled by a formula that contains Eq(q c , q b ). This is done to remove all terms obtained by rewriting with the equivalence b = E c. After having pruned all the transitions, we observe that the terms recognized by A are given by the set {f (a), f (b)}.

Let us now characterize the soundness and completness of our approach.

Theorem 5 (Soundness on left-linear TRS). Consider a left-linear TRS R, a set of terms Bad, a set of equations E and a well-defined R /E -automaton

A 0 . Let A * R,E be a fixpoint R /E -automaton of P(A , S A ∩A Bad ) and A = W(C(A i )) for i ≥ 0. If L(A * R,E ) ∩ Bad = ∅, then Bad ∩ R * (L(A 0 )) = ∅.
Theorem 6 (Completeness on Linear TRS). Given a linear TRS R, a set of terms Bad defined by automata A Bad , a set of equations E and a well-defined R /E -automaton A 0 . For any i > 0, let us consider A i be the R /E -automaton obtained from A i-1 in such a way:

A i = P(A , S A ∩A Bad ) and A = W(C(A i-1 )).
If Bad ∩ R * (L(A 0 )) = ∅ then there exists t ∈ Bad and j > 0 such that t → Aj q f and q f is a final state of A j .

This result also extends to left-linear TRS with a finite set of initial terms. This is sufficient to capture a large class of systems such as various java programs.

Theorem 7 (Completeness on Left-Linear TRS). Theorem 6 extends to left-linear TRS if for any state q of A 0 , the cardinality of Rep(q) is 1.

Implementation and Certification

Our approach has been implemented in TimbukCEGAR that is an extension of the Timbuk 3.1 toolset [START_REF] Genet | Timbuk 2.0 -a Tree Automata Library[END_REF]. Timbuk is a well-acknowledged tree automata library that implements several variants of the completion approach. TimbukCEGAR is around 11000 lines of OCaml, 75% of them being common with Timbuk 3.1. Tim-bukCEGAR exploits a BDD based representation of equation formulas through the Buddy BDD library [START_REF] Lind-Nielsen | Buddy 2.4[END_REF].

A particularity of TimbukCEGAR is that it is certified. At the heart of any abstraction algorithm there is the need to check whether a candidate overapproximation B is indeed a fixed point, that is if L(B ) ⊇ R * (L(A)). Such check has been implemented in various TRMC toolsets, but there is no guarantee that it behaves correct, i.e., that the TRMC toolset gives a correct answer. In [START_REF] Boyer | Certifying a Tree Automata Completion Checker[END_REF], a checker for tree automata completion was designed and proved correct using the Coq [START_REF] Bertot | Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions[END_REF] proof assistant. As such, any TRMC toolset that produces an automaton B that passes the checker can be claimed to work properly. TimbukCEGAR implements an extension of [START_REF] Boyer | Certifying a Tree Automata Completion Checker[END_REF] for R /E -automata, which means that the tool delivers correct answers.

In what follows, we describe how Java programs can be analyzed using our approach. Both Timbuk and TimbukCEGAR are available at http://www.irisa. fr/celtique/genet/timbuk/.

In a national initiative called RAVAJ [START_REF]Ravaj: Rewriting and approximations for java applications verification[END_REF], we have defined a generic certified verification chain based on TRMC. This chain is composed of three main links. The two first links rely on an encoding of the operational semantics of the programming language as a term rewriting system and a set of rewrite rules. The third link is a TRMC toolset, here TimbukCEGAR. With regards to classical static analysis, the objective is to use TRMC and particularly tree automata completion as a foundation mechanism for ensuring, by construction, safety of static analyzers. For Java, using approximation rules instead of abstract domains makes the analysis easier to fine-tune. Moreover, our approach relies on a checker that certifies the answer to be correct.

We now give more details and report some experimental results. We used Copster [START_REF] Barré | Copster homepage[END_REF], to compile a Java .class file into a TRS. The obtained TRS models exactly a subset of the semantics6 of the Java Virtual Machine (JVM) by rewriting a term representing the state of the JVM [START_REF] Boichut | Rewriting Approximations for Fast Prototyping of Static Analyzers[END_REF]. States are of the form IO(st,in,out) where st is a program state, in is an input stream and out and output stream. A program state is a term of the form state(f,fs,h,k) where f is current frame, fs is the stack of calling frames, h a heap and k a static heap. A frame is a term of the form frame(m,pc,s,l) where m is a fully qualified method name, pc a program counter, s an operand stack and t an array of local variables. The frame stack is the call stack of the frame currently being executed: f. We consider the following program: Let us now check that the sum output by the program can never be equal to zero, for all non-empty input stream of integers.

The TRS generated by Copster has 879 rules encoding both the JVM semantics and the bytecode of the above Java program. Initial terms are of the form IO(s,lin,nilout) where s is the initial JVM state, lin is a non-empty unbounded list of integers and nilout is the empty list of outputs. Starting from this initial set of terms, completion is likely to diverge without approximations. Indeed, the program is going to allocate infinitely many objects of class List in the heap and, furthermore, compute an unbounded sum in the method printSum. In the heap, there is one separate heap for each class. Each heap consists of a list of objects. For instance, in the heap for class List, objects are stored using a list constructor stackHeapList(x,y). Thus, to enforce termination we can approximate the heap for objects of class List using the following equation stackHeapList(x,y)=y. The effect of this equation is to collapse all the possible lists built using stackHeapList, hence all the possible heaps for class List. The other equations are succ(x)=x and pred(x)=x for approximating infinitely growing or decreasing integers. By using those equations, TimbukCEGAR finds a counterexample. This is due to the fact that, amongst all considered input streams, an input stream consisting of a list of 0 results into a 0 sum. The solution is to restrict the initial language to non-empty non-zero integer streams. However, refinement of equations is needed since succ(x)=x and pred(x)=x put 0 and all the other integers in the same equivalence class. Refining those equations by hand is hard, e.g. using equations succ(succ(x))=succ(x) and pred(pred(x))=pred(x) is not enough to eliminate spurious counterexamples. After 334 completion steps and 4 refinement steps, TimbukCEGAR is able to complete the automaton and achieve the certified proof. The resulting automaton produce by the tool has 3688 transitions which are produced in 128s and certified in 17017s. The memory usage for the whole process does not exceed 531M b. One of the reason for which certifying automata produced by TimbukCEGAR takes more time than for Timbuk 3.1 is that the checker has to normalize epsilon transitions of R /E -automata. This is straightforward but may cause an explosion of the size of the tree automaton to be checked. It is worth mentioning that the term rewriting rules corresponding to the above example is not right-linear. However, here completion steps do not introduce spurious counter examples.

We give another example of application in Appendix J.

Conclusion

We have presented a new CounterExample Guided Abstraction Refinement procedure for TRMC based on equational abstraction. Our approach has been implemented in TimbukCEGAR that is the first TRMC toolset certified correct.

Our approach leads, in part, to a java program analyzer starting from code to verification, but without relying on (1) potentially heavy assumptions on datas and architectures, (2) abstraction techniques when translating the code to TRS. We are convinced that our work open news doors in application of RMC approaches to rigorous system design. One of the remaining challenge is definitively to consider non left-linear TRS. Completion can be extended to deal with such TRS [START_REF] Genet | Reachability analysis of rewriting for software verification[END_REF]. This is necessary to verify cryptographic protocols with completion [START_REF] Genet | Rewriting for Cryptographic Protocol Verification[END_REF][START_REF]Avispa -a tool for Automated Validation of Internet Security Protocols[END_REF]. The theoretical challenge is to extend the CEGAR completion to non left-linear TRS. The technical challenge is to extend the Coq checker to handle non left-linear TRS and tree automata with epsilon transitions. Tackling those two goals would allow us to propose the first certified automatic verification tool for security protocols, a major advance in the formal verification area.

A Running Example

Consider the R /E -automaton A 1 R,E given in Example 4 in Section 5.2. We define A Bad to be a tree automaton whose final state is q 0 and whose transitions are a → q 1 , s(q 1 ) → q 2 , s(q 2 ) → q 1 and f (q 2 ) → q 0 . The forbidden terms in L(A Bad ) are of the form f (s 2k+1 (a)). We that L(A 1 R,E ) ∩ L(A Bad ) = ∅. According to the intersection algorithm described in Appendix H, one can build a set S A 1 R,E ∩A B ad of triples (q0, q 0 , φ), where φ is the formula used to prune A 1 R,E , i.e., to remove those terms that belong to L(A 1 R,E ) ∩ L(A Bad ). Here, S A 1 R,E ∩A B ad = {(q0, q 0 , Eq(q2, q3) ∧ Eq(q3, q2)), (q0, q 0 , Eq(q2, q3)), (q0, q 0 , Eq(q3, q2))}. Thus, we perform the prune step

P(A 1 R,E , S A 1 R,E ∩A B ad ).
Removing the transition q2 → q3 from ε 1 E is sufficient to invalidate Eq(q2, q3) ∧ Eq(q3, q2). Moreover, this action invalidates (q0, q 0 , Eq(q2, q3)) too. It remains to prune with (q0, q 0 , Eq(q3, q2)). This is done by removing the transition q3 → q2 from ε 1 E . Thus, ε 1 E becomes empty. At this point, no transition of ε 1 R can be removed. Indeed, all these transitions are all labeled by . We thus define

A 2 R,E = P(A 1 R,E , S A 1 R,E ∩A B ad ), with ∆ 2 = ∆ 1 , ε 2 R = ε 1 R , and ε 2 E = ∅. We observe that A 2
R,E is not R-closed and should be completed. We thus define

A 3 R,E = W(C(A 2 R,E
)). We found a new critical pair for f (x) → f (s(s(x))) and we obtain

∆ 3 = ∆ 2 ∪ {s(q3) → q5, s(q5) → q6, f (q6) → q7, and ε 3 R = ε 2 R ∪ {q7 -→ q4}.
The interesting point is in the application of W. Observe that the transitions of ε 3 E directly results from the application of the equation s(x) = s(s(x)), i.e. transitions q2 → q3, q3 → q2, q3 → q5, q5 → q3, q5 → q6, and q6 → q5.

The two transitions q2 → q3 and q3 → q2 are ignored since they have been deleted earlier by a prune step, but two new transitions are added: q2 → q5 and q5 → q2. Indeed, it should have been possible to connect q2 and q5 together using transitions q2 → q3 and q3 → q5 if q2 → q3 had not been deleted. So, ε 3 E = {q2 → q5, q5 → q2, q5 → q6, q6 → q5, q3 → q5, q5 → q3}. We then check the emptiness of L(A 3 R,E ) ∩ L(A Bad ). This intersection is still not empty and we obtain the following set of triples:

S A 3 R,E ∩A Bad =       
(q0, q 0 , Eq(q3, q5)), (q0, q 0 , Eq(q5, q3)), (q0, q 0 , Eq(q5, q6)), (q0, q 0 , Eq(q6, q5)), (q0, q 0 , Eq(q2, q5) ∧ Eq(q5, q3)), (q0, q 0 , Eq(q2, q5) ∧ Eq(q5, q6)), (q0, q 0 , Eq(q5, q2) ∧ Eq(q3, q5)), (q0, q 0 , Eq(q5, q2) ∧ Eq(q6, q5))

       .
So, in order to perform P(A 3 R,E , S A 3 R,E ∩A Bad ), the first transitions to remove are q3 → q5, q5 → q3, q5 → q6 and q6 → q5. According to Figure 2, ε 3 E of 2a. becomes the one described in 2b. Note that four new transitions are generated: q3 → q6, q6 → q3, q2 → q6 and q6 → q2. We denote this new set of transitions by ε 3 E . According to Definition 6, one has to test if the removing of guilty transitions has broken the nonempty intersection. And here, it is not the case. Indeed, it is still possible to recognize an odd number of s between the symbols f and a using for instance the transition q2 → q6:

f (s(a)) → * ∆ 3 f (q2) and f (q2) → * ε 3 E f (q6) → ε 3 R q0. Let A 3 R,E be the R /E -automaton such that ∆ 3 = ∆ 3 , ε 3 E and ε 3 R = ε 3 R . Computing P(A 3 R,E , S A 3 R,E ∩A Bad ) remains to compute P(A 3 R,E , S A 3 R,E ∩A Bad ) where S A 3 R,E
∩A Bad is defined as follows:

S A 3 R,E ∩A Bad =
(q0, q 0 , Eq(q2, q6)), (q0, q 0 , Eq(q6, q2) ∧ Eq(q3, q6)), (q0, q 0 , Eq(q6, q2)), (q0, q 0 , Eq(q2, q6) ∧ Eq(q6, q3)) .

Removing the transitions q2 → q6 and q6 → q2 makes the whole set of formula involved in

S A 3 R,E ∩A Bad non valid. Let A 3 R,E be the R /E -automaton such that ε 3 R = ε 3 R , ε 3 E = ε 3 E \ {q2 → q6, q6 → q2} and ∆ 3 = ∆ 3 .
Note that as soon as these transitions are removed, the intersection between L(A 3 R,E ) and L(A Bad ) is empty. So,

P(A 3 R,E , S A 3 R,E ∩A Bad ) = A 3 R,E and consequently, P(A 3 R,E , S A 3 R,E ∩A Bad ) = A 3 R,E . q 5 q 6 q 2 q 3 q 5 q 6 q 2 q 3 q 5 q 6 q 2 q 3 a) ε 3 E before pruning b) ε 3 E c) ε 3
E after the pruning process q3 → q5, q5 → q3, q5 → q6 and q6 → q5 are removed Fig. 2: Evolution of ε 3 E during the pruning process

Considering A 4 R,E = P(A 3 R,E , S A 3 R,E ∩A Bad ),

we restart the completion process and we observe that

A 4 R,E = C(A 4 R,E
). We have thus reached a fix-point. There, we observe that L(A 4 R,E ) ∩ L(A Bad ) = ∅ and conclude that R * (I) ∩ Bad = ∅. Observe that our refinement is accurate in this case. Indeed L(A 4 R,E ) = f (s 2k (a)), that is the exact set of reachable states.

The above example cannot be handled with the approach of [START_REF] Boichut | Finer is better: Abstraction refinement for rewriting approximations[END_REF]. Indeed, this technique cannot handle set of bad terms whose cardinality is infinite.

B Proof of Theorem 1

We want to show that the following result holds:

∀t ∈ T (F ∪ Q), q ∈ Q, t α -→A q ⇐⇒ t → * A q
Proof. The proof is easily done by induction by arguing that it is enough to forget the formulas manipulated by the definition 3 to have the equivalent step with →A.

C Matching Algorithm for R /E -automata

We assume a left-linear TRS R and a R /E -automaton

A i R,E such that A i R,E = F, Q i , Q f , ∆ i ∪ ε i R ∪ ε i E Definition 7 (Matching Algorithm).
Assuming the matching problem l q for a R /E -automaton A i R,E . S is the solution of the matching problem, which is denoted l q A i R,E S, if there exists a derivation of the statement l q A i R,E S using the rules:

(Var) x q A {(α k , {x → q k }) | q k α k --→A q} (x ∈ X ) (Delta) t1 q1 A S1 . . . tn qn A Sn f (t1, . . . , tn) q A n 1 S k f (q1, . . . , qn) → q ∈ ∆ (Epsilon) t q A S0 t q 1 A S1 . . . t q n A Sn t q A S0 ∪ n k=1 {(φ ∧ α k , σ) | (φ, σ) ∈ S k } {(q k , α k ) | q k α k --→ q} n 1 t / ∈ X Using n 1 Sj = {( , id)⊕(φ1, σ1)⊕• • •⊕(φn, σn) | (φj, σj) ∈ Sj}, and (φ, σ)⊕(φ , σ ) = (φ ∧ φ , σ ∪ σ ).
Observe that, by definition, the matching problem considers possibly infinite runs of the form lσ α -→ q. Indeed, transitions in ε i R ∪ ε i E can introduce loops. In the matching algorithm, we exclude such runs. This is done to keep a finite set of rewriting path, which is computable in a finite amount of time. It is worth mentioning that removing loops does not influence the result. As an example, consider the automaton A of Example 2. We observe that f (b)

Eq(q b ,qc)∧Eq(qc,q b ) -------------→A q f uses the loop f (b) =E f (c) =E f (b).
This loop can be removed as f (a) → * R f (b) can be obtained by f (b) -→A q f , a run which does not contain any loops.

We show that the matching algorithm given in Definition 7 is complete.

Lemma 1. Let A be a R /E -automaton, q one of its states, l ∈ T (F, X ) the linear left member of a rewriting rule and σ a Q-substitution with a domain range-restricted to V(l). If the set S is solution of the matching problem lσ q, then we have ∀(α, σ), lσ α -→A q ⇐⇒ (α, σ) ∈ S Proof. Assuming F a set of symbols, X a set of variable and Q a set of states. We define A = F, Q, Q f , ∆ ∪ εR ∪ εE ; l ∈ T (F, X ) and q ∈ Q; σ : Var(l) → Q and α = n 1 Eq(q k , q k ) such that lσ α -→A q.

The proof is done by induction on the term l.

Base case: l is a variable. In this case, σ must be a Q-substitution of the form σ = {l → q }. Using this observation and the hypothesis, we have q α -→A q. The matching problem l q is solved using Rule (Var). This means that S = {(α k , {l → q k }) | q k α k --→A q}. By definition of S we see that S contains (α, σ).

Induction : Assume now l is a linear term of the form f (t1, . . . , tn).

We are going to decompose f (t1, . . . , tn)σ α -→A q into sequences of transitions. First observe that, by splitting σ into σ1 . . . σn, we have that f (t1, . . . , tn)σ is equal to f (t1σ1, . . . , tnσn). Assume σ = σ1 • • • σn with dom(σi) = V(ti) and ∀x ∈ dom(σi), σi(x) = σ(x). Since l is linear, each variable in X occurs at most one time in l. This means that the sets V(ti) are disjoints and so are the domains of the σi. This ensures that σ is well-defined.

We now study the decomposition of f (t1σ1, . . . , tnσn) α -→A q to show that transitions of A used to recognized the term f (t1σ1, . . . , tnσn) are considered by the corresponding steps of the matching algorithm.

We observe that the term f (t1σ1, . . . , tnσn) is recognized in State q. Indeed, we have f (q1, . . . , qn) → q ∈ ∆, and each subterm tiσi is recognized in state qi such that tiσi α i -→ qi. Composing recognizing of each subterm, we obtain the following sequence: f (t1, . . . , tn)

α 1 --→ f (q1, t2, . . . , tn) 2 1 α i ----→ f (q1, q2, t3, . . . , tn) 3 1 α i ----→ . . . . . . n 1 α i ----→ f (q1, . . . , qn) n 1 α i ∧ ------→ q
There are two cases that have to be considered : (1) q = q and (2) q = q . (1) If q = q , the decomposition is complete and f (t1σ1, . . . , tnσn) α -→A q with α = n 1 αi.

f (t1σ1, . . . , tnσn)

n i=1 α i -----→ f (q1, . . . , qn) n i=1 α i -----→ q
(2) q = q : f (t1σ1, . . . , tnσn) α -→A q holds only if we have a transition

q α -→ q such that α = n 1 αi ∧ α . f (t1σ1, . . . , tnσn) n i=1 α i -----→ f (q1, . . . , qn) -→ q α -→ q
By induction, we know that for each sequence tiσi α i -→ qi, the matching problem is solved i.e. ti qi Si with Si contains (αi, σi). Rule (Delta) is applied to all premises ti qi A Si for the transition f (q1, . . . , qn) → q ∈ ∆. From this, we obtain a set S = n 1 Si. By unfolding the definition of , we have

S = {( , id) ⊕ (a 1 , s 1 ) ⊕ . . . (a n , s n ) | (a i , s i ) ∈ Si}.
Since each Si contains (αi, σi), S contains ( , id)⊕(α1, σ1)⊕. . . (αn, σn) which is, by definition of ⊕ equal to ( n 1 αi, σ). Thus, we obtain a intermediate statement f (t1, . . . , tn) q A S such that f (t1, . . . , tn)σ n 1 α i ----→ q , where ( n 1 αi, σ) ∈ S . This statement must correspond to one of the premises of Rule (Epsilon) to produce the expected statement f (t1, . . . , tn) q A S. Two cases have to be considered :q = q and q = q .

If f (q1, . . . , qn) → q ∈ ∆ is the last transition used to have f (t1, . . . , tn)σ α -→A q then we have α = n 1 αi and we are in the case q = q : this case corresponds to the premiss 0 of Rule (Epsilon) and S = S0. By definition of Rule (Epsilon), S is included in S. This means that (α, σ) ∈ S.

If we have q = q , then it remains a sequence of transitions q α -→ q to have f (t1, . . . , tn)σ α -→A q. The couple (α , q ) is in the set {(q k , α k ) | q k α k --→ q}.This means that the statement f (t1, . . . , tn) q A S is one the remaining premisses. By definition of Rule (Epsilon), S contains all couple (a ∧ α , s) where (a, s) ∈ S . In particular, S contains ( n 1 αi ∧ α , σ) which concludes the proof.

D Normalization for R /E -automata

Definition 8 (Normalization). The normalization is done in two mutually inductive steps parametrized by the configuration c to recognize, and by the set of transitions ∆ to extend. Let Qnew be a set of new states,

       Norm(c, ∆) = Slice(d, ∆) c →∆ d, and c, d ∈ T (F ∪ Q) Slice(q, ∆) = ∆ q ∈ Q Slice(f (q1, . . . , qn), ∆) = ∆ ∪ {f (q1, . . . , qn) → q} qi ∈ Q and q ∈ Qnew Slice(f (t1, . . . , tn), ∆) = Norm(f (t1, . . . , tn), Slice(ti, ∆)) ti ∈ T (F ∪ Q) \ Q E Proofs of Theorem 2
In order to prove that C(A i R,E ) is well-defined, we need to show that, first C(A i R,E ) is determinist if we do not consider the transition set of A i R,E (Lemma 2) and second, solving one critical pair preserves well-definition (Lemma 3).

Lemma 2 (Existence of a representative). Assume that AR,E

= F, Q, Q f , ∆ ∪ εR ∪ εE is a R /E -automaton obtained after k steps of completion from A 0 R,E . Let c be a configuration. If ∆ = Norm(c, ∆ \ ∆ 0 )
, then there exists a state q such that c → ! ∆ q.

Proof. Let µ : T (F ∪ Q) → N be the measure that counts the number of occurences of symbols in F of a configuration. Example : µ(f (q1, g(q2), a)) = 3. We define it inductively by µ(q) = 0 if q ∈ Q, and µ(f (t1, . . . , tn)) = 1 + n 1 µ(ti). Assuming F a set of symbols, and Q a set of states. We define

AR,E = F, Q, Q f , ∆∪ εR ∪ εE ; c ∈ T (F ∪ Q). Assume that ∆ 1 = ∆ \ ∆ 0 is determinist.
The first step Norm(t, ∆ 1 ) consists in rewriting c by ∆ 1 in its normal form d The second step Slice(d, ∆ 1 ) returns ∆ 2 such that there exists a unique state q such that d → ! ∆ 2 q. The proof is one by induction on the decreasing of µ(d). We consider the 3 cases of Slice(d, ∆ 1 ) 1. Slice(q, ∆ 1 ) = ∆ 1 . It means that d is the state q. There exists a unique state ,which is q, such that d → ! ∆ 1 q. 2. Slice(f (q1, . . . , qn), ∆ 1 ) = ∆ 1 ∪ {f (q1, . . . , qn) → q | q ∈ Qnew}. Each qi is a state.

The configuration f (q1, . . . , qn) can be used as the left-member of a normalised ground transition. We build the new transition f (q1, . . . , qn) → q using a new state q. Adding a such transition to ∆ 1 preserves determinism. We know that it is impossible to rewrite more d = f (q1, . . . , qn) using transitions of ∆ 1 : the new transition f (q1, . . . , qn) → q is the unique way to rewrite d. We deduce that

∆ 2 = ∆ 1 ∪ {f (q1, . . . , qn) → q | q ∈ Qnew} is deterministic, and d → ! ∆ 2 q. 3. Slice(f (t1, . . . , tn), ∆ 1 ) = Norm(f (t1, . . . , tn), Slice(ti, ∆ 1 ) ), ti ∈ T (F ∪ Q) \ Q.
Here, we have the direct subterm ti of d which is not a state. We deduce µ(ti) < µ(d) from the definition of µ. By induction, ∆ is extended by Slice(ti, ∆ 1 ) to obtain ∆ 2 for which there exists a state q such that ti → ! ∆ 2 q. Using this new set ∆ 2 , we unfold Norm(f (t1, . . . , tn), ∆ 2 ) which consists in rewriting f (t1, . . . , tn) using ∆ 2 . We obtain a new configuration f (t 1 , . . . , t n ) where we know at less t i is equal to q since the direct subterm ti can be rewritten in q using ∆ 2 . Note that if some subterms of ti are also subterms of some other tj, it will also be rewritten by ∆ 2 in t j until we reach the normal form. Each step of rewriting by ∆ 2 necessarly replaces a symbol of F by a state of Q by definition of a normalised transition. This remark allows to prove that µ(f (t1, . . . , tn) > µ(f (t 1 , . . . , t n ). For the direct subterm ti, we know µ(ti) > 0 (ti is not a state), and µ(t i ) = 0 (t i is the state q). For all other direct subterm tj with j <> i we deduce µ(tj) ≥ µ(t j ) from tj → ! ∆ 2 t j using ∆ 2 . We have µ(f (t1, . . . , tn) > µ(f (t 1 , . . . , t n ) by definition of µ, and f (t 1 , . . . , t n ) is rewritten as most as possible by the deterministic ∆ 2 . Then, we use again the induction hypothesis to deduce that ∆ = Slice(f (t 1 , . . . , t n ), ∆ 2 ) extends ∆ 2 in order to have a unique state q such that f (t 1 , . . . , t n ) → ! ∆ 3 q. By transivity, we have d → ! ∆ q using the deterministic set ∆ for d which is equal to f (t1, . . . , tn).

Finally, we proved that ∆ = Slice(d, ∆ 1 ) extends ∆ 1 preserving its determinism such that there exists a state q for which d → ! ∆ q. We also know that c → ! ∆ d. We can conclude that ∆ = Norm(c, ∆ 1 ) is determinist, and there exists a state q such that c → ! ∆ q.

Let us now show that solving one critical pair preserves well-definition. Let CP = { r1σ1, α1, q1 , . . . , rnσn, αn, qn } be the finite set of critical pairs computed from A i R,E that have to be solved by using Definition 5. By definition, considering A0 = A i R,E there exists a sequence of R /E -automata A1, . . . , An, where Aj is obtained from Aj-1 by solving the critical pair rjσj, αj, qj . Thus, C(A i R,E ) = An. For a question of readability and in order to prevent any confusion between notations, each R /E -automaton Aj is defined as follows:

Aj = F, Q n+1 , Q f , ∆ j ∪ ε j R ∪ ε j E .
Lemma 3. Let R be a linear TRS. Let A and A be two R /E -automaton such that A is obtained from A by solving a critical pair rσ, α, q of A. If A is well-defined then so is A .

Proof. Assume that A = F, Q, Q f , ∆ ∪ εR ∪ εE and A = F, Q , Q f , ∆ ∪ ε R ∪ ε E . According to Definition 5, ∆ = ∆ ∪ Norm(rσ, ∆ \ ∆ 0 ), ε R = {q α -→ q} ∪ εR and ε E = εE.
Following Definition 4, we first show in (1) that for all state q of A , and all term v such that v -→ A q , there exists u a term representative of q such that u → * R v. Then, in (2) we show that if q1 φ -→ q2 is a transition of ε R , then there exist terms s, t ∈ T (F) such that s φ → A q1, t → A q2 and t →R s.

1. We show the property by induction on the height of t. Let us assume that for all term t of height less than the height of t and for all q ∈ Q A , we have t -→ A q =⇒ ∃u ∈ Rep(q) : u → * R t . Now let us prove that the result holds for t. We consider several cases.

-If q ∈ QA and t -→A q, then since A is well defined, we get the representative u ∈ Rep(q) such that u → * R t from well-definition of A.

-Assume now that q ∈ QA, t -→A q and t -→ A q. We show the property by induction on the height of t. Since t is recognized in A and not in A, this means that the run t -→ A q needs the transitions added by the resolution of a critical pair. Hence there exists a rewrite rule l → r, a substitution σ : X → QA, a formula α and a state qc such that lσ α -→A qc and rσ, α, qc is the critical pair. Moreover, the resolution of this critical pair produces the following set of transitions:

∆ A = Norm(rσ, ∆A \ ∆0) and ε A R = ε A R ∪ {q c → qc} such that rσ → ! ∆ \∆ 0 q c .
Recall that t -→ A q needs transitions not occurring in A. However, all the new transitions produced by Norm(rσ, ∆A \∆0) necessarily range on new states, i.e. states not occurring in QA. As a result, those transitions cannot be used to get t -→ A q with q ∈ QA. This means that the run t -→ A q uses at least once q c → qc and α = . To sum up, we know that there exists a ground context

C[ ] such that t = C[t ] -→ A C[q c ] -→ A C[qc] -→A q.
Note that if q c → qc the same reasonning can be applied. We start to reason on the occurrence of q c → qc that is the closest to q. Now, our objective is to show that there exists u ∈ Rep(q c ) such that u → * R t . If t -→A q c , then since A is well defined the result is a direct consequence of Definition 4. Otherwise this means that q c is a new state of A (i.e. q c ∈ QA) that has been added by the resolution of the critical pair, i.e. rσ → ! ∆ q c . By Lemma 2, we get that there exists a substitution σ : X → T (F) such that t = rσ . Using the same Lemma, from t = rσ -→ A q c and rσ -→ A q c , we get that for all variable x of r: σ (x) -→ A σ(x). Note that σ(x) ∈ QA and that σ (x) are necessarily terms of height less to the height of t. Using the induction hypothesis, we get that for all state σ(x) there exists a representative ux such that ux → * R σ (x). Let σRep be the substitution mapping every variable x to ux. We have rσRep ∈ Rep(q c ). Moreover, rσRep → * R rσ = t . Now, we show that lσRep →R rσRep. This is not straightforward since Var(l) ⊇ Var(r). However, it is possible to extend σRep into σ Rep , where every variable y of Var(l) not occurring in σRep is mapped to a representative of σ(y). Hence, lσ Rep →R rσ Rep → * R t . From the critical pair we know that lσ α -→A qc and we found that α = . Hence lσ Rep -→A qc. Since A is well-defined, we get that there is a representative v ∈ Rep(qc) such that v → * R lσ Rep . By transitivity of →R, we get that v → * R t . Above, we found that t

= C[t ] -→ A C[q c ] -→ A C[qc] -→A q.
From this and v ∈ Rep(qc), we get that C[v] -→A q. Since A is well defined, we know that there exists a representative w ∈ Rep(q) such that

w → * R C[v].
To conclude, we found w ∈ Rep(q) and w

→ * R C[v] → C[t ] = t.
-If q ∈ QA (q ∈ Q A \ QA), t -→A q and t -→ A q. Since q ∈ Q A \ QA, we know that q has been added by the resolution of a critical pair. As above, we can deduce that there exists a rewrite rule l → r, a substitution σ : X → QA, a formula α and a state qc such that lσ α -→A qc and rσ, α, qc is the critical pair. Moreover, the resolution of this critical pair creates

∆ A = Norm(rσ, ∆A \ ∆0) and ε A R = ε A R ∪ {q c → qc} such that rσ → ! ∆ \∆ 0 q c .
Since q is a new state of A that has been used in the normalization of a subterm of rσ. More precisely, we know that there exists a term s ∈ T (F, X ) and a context C[ ] (possibly empty) such that rσ = C[s], C[s]σ → * ∆ q c and sσ → * ∆ q. Similarly, we know that there exists a substitution σ : X → T (F) such that sσ = t. We get that for every variable x of r: σ (x) -→ A σ(x). Note that σ(x) ∈ QA and that σ (x) are necessarily terms of height lesser to the height of t. By induction hypothesis, we obtain that for every state σ(x) there exists a representative ux such that ux → * R σ (x). Let σRep be the substitution mapping every variable x to ux. We have sσRep ∈ Rep(q) and sσRep → * R sσ = t. 2. It is easy to see that, for any transitions q1 φ → q2 ∈ εR, the property still holds. Let us now focus on the transition q α → q resulting from the resolution of Critical pair rσ, α, q . By definition, rσ, α, q results from the application of the matching algorithm of Definition 7 given in Appendix C. So there exists a rule l → r ∈ R such that (α, σ) ∈ S, with l q A S. Moreover, since the critical pair has to be solved: lσ α → q and there is no formula α such that rσ α -→A q. Since R is left-linear, for each variable x ∈ Var(l), one can define the substitution σ : X → T (F) as follows: Assuming qs being the state of A such that σ(x) = qs, let σ (x) = Rep(qs). By definition of Rep, Rep(qs) → qs. So, there exists a derivation such that lσ → lσ and lσ α → q. One can deduce that rσ → rσ. According to Lemma 2, one can deduce that there exists a unique q such that rσ → * Norm(rσ,∆\∆ 0 ) q . If Norm(rσ, ∆ \ ∆ 0 ) = ∅ then each transition composing it is of the form f (q 1 , . . . , q n ) → q n+1 . Consequently, rσ → q . Considering the transition q α → q, one has rσ → rσ → q α → q. Finally, assuming s = lσ and t = rσ , there exists s, t ∈ T (F) such that one has s α → q, t α → q and s →R t.

To conclude, A is also well-defined. Theorem 2 is in two parts. We first show that

C(A i R,E ) is well-defined if A i R,E is well-defined.
Proof. Let Pn be the following proposition: An is well-defined.

-P0: Trivial since A0 = A i R,E and A i R,E is well-defined by hypothesis. -Pn ⇒ Pn+1: By hypothesis, An+1 is obtained from An by solving the critical pair rn+1σn+1, αn+1, qn+1 . Applying Lemma 3, one obtains automatically that An+1 is well-defined.

So, one can deduce that C(A i

R,E ) is well-defined.

We now show that

L(A i R,E ) ⊆ L(C(A i R,E )).
Proof. Let q be a state of A i R,E and t be a term of L(A i R,E , q). Suppose that there exist a position p ∈ Pos(t), a rule l → r ∈ R and a substitution σ : X → T (F) such that t|p = lσ . Let t be the term such that t = t[rσ ]p. Since t ∈ L(A i R,E , q), there exists a state q of A i R,E such that t|p = lσ → *

A i R,E q and t[q ]p → * A i R,E
q. Following Property 1 given in Appendix C, there exists (α, σ) ∈ S with l q

A i R,E S such that lσ → * A i R,E lσ and lσ → * A i R,E q . If rσ, α, q is already solved then rσ → * A i R,E q .
Consequently, rσ can also be reduced to

q in A i R,E . Since t = t[rσ ]p → * A i R,E q, t ∈ L(C(A i R,E ), q). Suppose now that rσ → * A i R,E
q . So, there exists riσi, αi, qi ∈ CP such that riσi, αi, qi = rσ, α, q . By construction, rσ → * A i q . Consequently, rσ can also be reduced to q in Ai. Since Ai is syntactically included in

C(A i R,E ), one can deduce that t = t[rσ ]p → * C(A i R,E ) q. Concluding the proof.

F Proofs of Theorem 3

The theorem is in two parts. We first show that if a R /E -automaton A is well-defined, then so is W(A).

Proof. Assume that

A = F, Q, Q f , ∆ ∪ εR ∪ εE is well-defined. We have W(A) = F, Q, Q f , ∆ ∪ εR ∪ ε E .
We also have εR ⊇ ε R . Indeed, W only adds transitions to the εR. We have to prove that the two items of Definition 4 are satisfied.

-The transitions of ε E do not participate to runs of the form α -→, whith α = (due to the second item in Definition 3). This means that for any term t and any state q, t -→ W (A) q is equivalent to t -→A q. Since A is well-defined, we know that there exists u ∈ Rep(q) such that u → * R t. u is also a representative of W(A), and we deduce that first item of Definition 4 holds for W(A).

-By definition, W only adds transitions to ε E and do not remove transitions of A.

For all transitions q α -→ q ∈ ε R , we have q α -→ q ∈ Drw. Since A is well-defined, we know that there exist terms s, t ∈ T (F) such that s φ -→A q, t -→A q and t →R s.

We also have s φ -→ W(A) q, t -→ W(A) q and t →R s.

We now show the second part of the theorem. For all R /E -automaton A, L(W(A)) ⊇ L(A).

Proof. We observe that the widening operator can only adds transitions. As a consequence, this operator cannot restrict the language of A.

G Proofs of Theorem 4

The theorem is in two parts. We first show that the pruning process always terminates.

Proof. Let t ∈ T (F) be a term such that t φ -→ A k R,E
q and φ = . By hypothesis, t is thus a spurious counter-example. Moreover, φ is a formula whose atoms are of the form Eq(qi, qj), with qi → qj ∈ ε k E . Pruning A k R,E remains to remove transitions q i → q j from ε k E until φ does not hold anymore i.e. φ =⊥. Since ε k E is finite, the pruning process always terminates.

We now show that the pruning process removes any spurious counter-example using etablished results in Appendix C and Apendix D. Now, let us show that the pruning process removes a given spurious counterexample from L(A k R,E ).

Proof. According to Lemma 1, the matching algorithm is complete. So given a term

t ∈ T (F), if t ∈ L(A k R,E ) then there exists q ∈ Q f such that t → * A k R,E
q. According to Theorem 1, there exists α such that t

φ -→ A k R,E
q. More precisely, using Definition 7

given in Appendix C, one can deduce that (α, ∅) ∈ S with t q A k R,E S. Let φ be the following formula: φ = (α ,∅)∈S (α ). Consequently, φ is a formula characterizing all possible reductions of t into q. Since t is a spurious counter-example, for all (α , ∅) ∈ S, α = . Removing transitions of ε k E until φ does not hold remains to remove each possible reduction in A k R,E of t into q. As a conclusion, when the pruning process terminates, t is not recognized anymore.

H Computing the Intersection of a Tree Automaton and a R /E -Automaton

In Definition 10, we propose a specific algorithm building the set S of reachable states for the intersection between a R /E -automaton A and automaton B where each product state is labelled by a formula on states of A. As stated in Section 6, this is useful to characterize the possibly infinite set of terms that have to be refined in a single step. In addition, Lemma 4 proposes a methodology to decide whether the intersection is empty or not. We first define an order > on formulas.

Definition 9. Given φ1 and φ2 two formulas, φ1 > φ2 iff φ2 |= φ1 and φ1 |= φ2.

Definition 10 (Reachable states of the product of a R /E -automaton and a tree automaton).

Let A = F, Q A , Q A f , ∆ A , εR, εE be a R /E -automaton and B = F, Q B , Q B
f , ∆ B be an epsilon-free tree automaton. The set S of reachable states of A × B is the set of triples (q, q , φ) where q ∈ Q A , q ∈ Q B and φ is a formula. Starting from the set Q A × Q B × {⊥}, the value of S can be computed using the following two deduction rules : {(q1, q 1 , φ1), . . . , (qn, q n , φn)} ∪ {(q, q , φ)} ∪ P {(q1, q 1 , φ1), . . . , (qn, q n , φn)} ∪ {(q, q , φ ∨ n i=1 φi)} ∪ P if f (q1, . . . , qn) → q ∈ ∆ A and f (q 1 , . . . , q n ) → q ∈ ∆ B and (φ ∨ n i=1 φi) > φ {(q1, q, φ1), (q2, q, φ2)} ∪ P {(q1, q, φ1), (q2, q, (φ1

∧ φ) ∨ φ2)} ∪ P if q1 φ -→ q2 ∈ εR and ((φ1 ∧ φ) ∨ φ2) > φ2 or if q1 → q2 ∈ εE and φ = Eq(q1, q2) and ((φ1 ∧ φ) ∨ φ2) > φ2
With regards to the reachability problem, this definition, provides a way to distinguish between real counterexamples and terms which can be rejected using abstraction refinement. Indeed, for all triple (q, q , φ) ∈ S with q final in A and q final in B , if φ |= then some of the terms recognized by q in B are reachable. Otherwise, φ is the formula to invalidate, i.e. negate some of its atom so that it becomes ⊥.

Lemma 4 (Emptiness decision of the product of a R /E -automaton and a tree automaton). Let A be a R /E -automaton and B a tree automaton. Let S be the set of reachable states of A × B defined according to definition 10. For all final state q of A, all final state q of B , all formulas φS = ⊥, φ = ⊥ and all term t ∈ T (F), we have t φ -→ * A q and t → * B q (i.e. L(A) ∩ L(B ) = ∅) if and only if there exists a triple (q, q , φS) ∈ S such that φ |= φS.

Proof. Let A = F, Q A , Q A f , ∆ A , εR, εE be the R /E -automaton and B = F, Q B , Q B f , ∆ B be
the tree automaton. We prove a stronger property on all states q of A and q of B (and not only for final states). First, we prove the 'only if' part. Let us assume that there exists a term t ∈ T (F) such that t φ -→ * A q, t → * B q . By induction on the height of t we have:

-If t is a constant, since B is an epsilon-free tree automaton, the only way to have t → * B q is to have t → q ∈ B . With regards to A, by definition 3, t φ -→ * A q means that there exists states q0, q1, . . . , qn and formulas φ1, . . . , φn such that t →∆ A q0 -→ qi+1 are either transitions of εR or transitions of εE with φi = . Because of transitions t → q0 ∈ ∆A and t → q ∈ ∆B , using the first case of definition 10, we get that (q0, q , ) ∈ S. Similarly, using the second case of the definition, we obtain that there exists formulas φ i with i = 1 . . . n such that (q1, q , φ1 ∨ φ 1 ), (q2, q , (φ1 ∧ φ2) ∨ φ 2 ), . . . (qn, q , (φ1 ∧ . . . ∧ φn) ∨ φ n ) belong to S. Finally, since qn = q and φ = φ1 ∧ . . . ∧ φn, we that (q, q , φ ∨ φ n ) ∈ S. Furthermore, we trivially have that φS = φ ∨ φ n and φ |= φS.

-Assume that for all term of height lesser or equal to n ∈ N, the property is true. Let us prove that it is also true for a term f (t1, . . . , tn) with t1, . . . , tn of height lesser or equal to n. Since f (t1, . . . , tn) → * B q and B is an epsilon free tree automaton, we obtain that ∃q 1 , . . . , q n ∈ Q B such that ∀i = 1 . . . n : ti → * B q i and f (q 1 , . . . , q n ) → q ∈ ∆B . With regards to A, by definition 3, f (t1, . . . , tn) φ -→ * A q means that there exists states q0, q1, . . . , qm, q 1 , . . . , q n and formulas φ1, . . . , φm, φ 1 , . . . , φ n such that ∀i = 1 . . . n : ti

φ i -→ * A q i , f (q 1 , . . . , q n ) →∆ A q0 and q0 φ 1 -→ q1 φ 2 -→ . . . qn, q = qn.
Furthermore, we obtain that φ = n i=1 φ i ∧ m i=1 φi. Since terms ti are of height lesser or equal to n, ∀i = 1 . . . n : ti → * B qi and ∀i = 1 . . . n : ti φ i -→ * A q i , we can apply the induction hypothesis and obtain that ∀i = 1 . . . n : (qi, q i , φ i ) ∈ S with φ i |= φ i . Besides to this, using case 1 of definition 3 on f (q1, . . . , qn) → q ∈ ∆B , f (q 1 , . . . , q n ) → q0 ∈ ∆A, and ∀i = 1 . . . n : (qi, q i , φ i ) ∈ S, we obtain that there exists a formula φ such that (q0, q , ( n i=1 φ i ) ∨ φ ) ∈ S. Then, like in the base case, since q0

φ 1 -→ q1 φ 2
-→ . . . qn, q = qn, we can deduce that there exists a formula φ such that (q, q , ( n i=1 φ

i ∧ m i=1 φi) ∨ φ ) ∈ S. Let φS = ( n i=1 φ i ∧ m i=1 φi)∨φ . Since we know from above that φ = n i=1 φ i ∧ m i=1 φi and ∀i = 1 . . . n : φ i |= φ i , we obtain that φ |= φS.
Second, we prove the 'if' part: if (q, q , φS) ∈ S and φS = ⊥ then there exists a term t and a formula φ = ⊥ such that φ |= φS, t φ -→ * A q and t → * B q . We make a proof by induction on the number of applications of the two rules of definition 10, necessary to prove that (q, q , φS) in S.

-If the number of steps is 0 then, since the computation of S starts from the set Q A × Q B × ⊥, then all (q, q , φS) are such that φS = ⊥, which is a contradiction. -We assume that the property is true for any triple (q, q , φS) which can be deducted by n or less applications of the rules of definition 10. Now, we consider the case of a triple (q, q , φS) that is deduced at the n + 1-th step of application of the deduction rules.

• If the first rule is concerned, this means that there exists triples (q1, q 1 , φ1), . . . , (qn, q n , φn) and (q, q , φ) in S deduced before n+1-th step, as well as transitions f (q1, . . . , qn) → q ∈ ∆A and f (q 1 , . . . , q n ) → q ∈ ∆B . Furthermore, we know that φS = φ ∨ n i=1 φi. If φ = ⊥ then, since (q, q , φ) was shown to belong to S before n + 1-th step, we can apply the induction hypothesis and directly obtain that there exists a term t and a formula φ such that φ |= φ, t φ -→ * A q and t → * B q . Note that φ |= φ implies φ |= φS. Otherwise, if φ = ⊥, then we can apply the induction hypothesis on triples (qi, q i , φi), i = 1 . . . n and obtain that ∀i = 1 . . . n : ∃φ i : ∃ti ∈ T (F) :

φ i |= φi, ti φ i -→ * A qi and ti → * B q i .
Finally, because of the two transitions f (q1, . . . , qn) → q ∈ ∆A and f (q 1 , . . . , q n ) → q ∈ ∆B , we get that f (t1, . . . , tn) φ -→ * A f (q1, . . . , qn) → * A q with φ = n i=1 φ i on one side and f (t1, . . . , tn) →B f (q 1 , . . . , q n ) → * B q on the other side. Furthermore, since ∀i = 1 . . . n : φ i |= φi, we have n i=1 φ i |= n i=1 φi. Recall that φ = n i=1 φ i and φS = φ ∨ n i=1 φi. Hence, φ |= φS.

• If the second rule is concerned, this means that there exists triples (q1, q , φ1) and (q, q , φ2) in S deduced before the n + 1-th step. Furthermore, we know that φS = (φ1 ∧ φ) ∨ φ2. Like above, if φ2 = ⊥ then we can apply induction hypothesis on (q, q , φ2) and trivially get the result. Otherwise, if φ2 = ⊥ then we can use induction hypothesis on the triple (q1, q , φ1) and obtain that there exists a formula φ 1 and a term t1 such that t1 φ 1 -→ * A q1, t1 → * B q and φ 1 |= φ1. Then, by case on the epsilon transition used for the deduction on S, we prove that t1

φ 1 ∧φ ---→ * A q: * Assume that q1 φ -→ q ∈ εR.
Then, by definition 3, we obtain that t1 φ 1 ∧φ ---→ * A q. Furthermore, since φ 1 |= φ1, we have that φ 1 ∧ φ |= φ1 ∧ φ and, finally, that φ 1 ∧ φ |= φS. * Assume that q1 → q ∈ εE. By definition 3, we obtain that t φ 1 ∨Eq(q 1 ,q) --------→ * A q. Finally, like above, we can deduce that φ 1 ∧ Eq(q1, q) |= φ1 ∧ Eq(q1, q) and thus φ 1 ∧ Eq(q1, q) |= φS.

I Soundness and Completeness

Concerning the prune step P, it preserves also the well-definition of a R /E -automaton. Indeed, given an R /E -automaton A i R,E , one can see the prune step as a removing of transitions of ε i E and ε i R . So, it does not affect Definition 4.

I.1 Proof of Theorem 5

The completion stops when any critical pair is solved. We show that this automaton is R-closed for any state of A * R,E the fixpoint R /E -automaton. Since C(A * R,E ) = A * R,E , for any q of A * R,E , any rule l → r ∈ R and any substitution σ :

X → Q, one has lσ → * A * R,E q ⇒ rσ → * A * R,E
q. Applying Theorem 2, one has for any state q of A * R,E , any u ∈ L(A * R,E , q), any v ∈ T (F), u →R v =⇒ v ∈ L(A * R,E , q). Thanks to the fixpoint property, this result extends to the reflexive and transitive closure of →R for all state, and especially final states of A * R,E . We then deduce R * (L(A * R,E )) ⊆ L(A * R,E ). Finally, all the transitions of the initial automaton A 0 R,E are always preserved at each step of C and W, and never removed by P.

Similarly, the set of final states is never modified during the process. It means that we have a syntactical inclusion of all transitions of A 0 R,E in A * R,E , and thus L(A0) ⊆ L(A * R,E ). The conjunction of this last result with R

* (L(A * R,E )) ⊆ L(A * R,E ) is sufficient to conclude that if L(A * R,E ) ∩ L(A Bad ) = ∅ then R * (L(AO)) ∩ L(A Bad ) = ∅.

I.2 Proof of Theorem 6

Since P preserves the well-definition of a R /E -automaton, one can deduce that any R /E -automaton Ai is then well-defined for linear TRS. Let t ∈ Bad and t ∈ R * (L(A0)). Note that if Ai exists then necessarly, in order to get t -→ q f and q f a final state of Ai, Ai must contain a rewriting chain t0 →R t1 . . . →R tn such that t0 ∈ L(A0), tn = t and for any ti, ti -→ q f . Let t ∈ Bad and t ∈ R * (L(A0)). Thus, there exists a minimal rewriting chain t0 →R t1 . . . →R tn such that t0 ∈ L(A0) and tn = t. We are going to show that a such rewriting chain leads eventually to the wanted R /E -automaton Aj.

n = 0 By hypothesis, t0 ∈ L(A0) ∩ Bad. Since ε 0 E = ∅, one can deduce that there exists q f ∈ Q f such that t0 -→A 0 q f . So, A0 is the wanted R /E -automaton. n + 1 Suppose that the property is true for a rewriting chain of length n. Then, there exists a R /E -automaton A k such that for any ti with i = 0, . . . , n, ti -→A k q f and tn / ∈ L(A k-1 ). Consider now a rewriting chain of length n + 1. So, one has t0 →R t1 . . . →R tn →R tn+1. By construction, tn+1 can not be in L(A k ). Indeed, the rewriting chain is the minimal one to get tn+1. So, if tn+1 was in a previous R /E -automaton then it has been deleted because tn+1 would have been obtained by accelerating the computation and then considered as a spurious example. Thus, A k is not R-closed. So, applying Theorem 2 one gets that tn+1 ∈ L(C(A k )).

Moreoever, since there exists q f ∈ Q f such that tn -→ q f , one can deduce that there exists u, v ∈ T (F), p ∈ Pos(tn) and q ∈ Q k such that u -→A k q, tn|p = u, u →R v and tn+1 = tn[v]p. Consequently, there exists a rule l → r ∈ R and a substitution σ : X → Q k such that u -→A k lσ and v -→A k rσ. So, one can deduce that tn+1 -→ C(A k ) . Trivially, if tn+1 ∈ Bad then there exists j > 0 such that tn+1 -→A j .

I.3 Proof of Theorem 7

Since R is not linear, we can not applied directly Theorem 2.

We illustrate the problem of the non right-linearity of R. Let A be the R /E -automaton whose ∆ = {a → q , b → q f (q ) → q}, εR = ∅ and εE = ∅. Let R be the TRS composed of a single rule f (x) → g(x, x). To compute C(A), we have to add the new transitions g(q , q ) → q and q -→ q. We have the new runs g(a, a) -→ q, g(b, b) -→ q, g(a, b) -→ q and g(b, a) -→ q. but we note that terms g(a, b) and g(b, a) are not reachable from f (a) or f (b). R /E -automaton C(A) is not well-defined anymore. The reason is that several representative terms are in Rep(q ): it implies the term g(q , q ) denotes more than the expected terms. To avoid this approximation, it is sufficient to ensure that all q has a unique representative term the initial RE-automaton. The normalization defined in Appendix D maintains this property by producing a fresh state for each new transition created.

J Additional Experiments

J.1 Processes Counting Symbols

The example considered in [START_REF] Boichut | Finer is better: Abstraction refinement for rewriting approximations[END_REF] is linear. The example deals with a simple two processes counting system. The following TRS describes the behavior of two processes each one equipped with an input list and a FIFO. Each process receives a list of symbols '+' and '-' to count, as an input. One of the processes, say P+, is counting the '+' symbols and the other one, say P-is counting the '-' symbols. When P+ receives a '+', it counts it and when it receives a '-', it adds the symbol to P-'s FIFO. The behavior of P-is symmetric. When a process input list and FIFO is empty then it stops and gives the value of its counter.

Here is a possible rewrite specification of this system, given in the Timbuk language, where S( , , , ) represents a configuration with a process P+, a process P-, P+'s FIFO and P-'s FIFO. The term Proc( , ) represents a process with an input list and a counter, add( , ) implements adding of an element in a FIFO, and cons, nil, s, o are the usual constructors for lists and natural numbers (peano's representation). The symbols '+' and '-' are represented respectively by the terms plus and minus. When a process has terminated its task, the value returned by the process is represented by a term of the form stop(i) where i is a peano's integer.

A first TRS representing this system is given in Section J.2.

Our objective is to show that no deadlock state can be reached. A deadlock state is a state when the process has stopped but there are still symbols to count.

The set of bad terms is also defined by a tree automaton recognizing all terms of the form S(stop( ), ,cons(plus, ), ) and S( ,stop( ), ,cons(minus, )), i.e. any configuration where a stopped process has a non empty FIFO. What remains to be done is to provide the equations so as to have a finite model. Since each process reads symbols in an unbounded list and either counts it or adds it to the other's process FIFO, the terms which are likely to become infinite are counters and FIFOs. To have a finite completion, it is enough to add the following equations: s(X)=X whose effect is to place all natural numbers in the same equivalence class and add(X,add(Y,Z))=add(X,Z) whose effect is to place all terms built on FIFO additions in the same equivalence class. If we launch TimbukCEGAR on this example it stops in less than a second and states that there is a counterexample. This is due to the fact that after P+ termination, P-may add a "+" to P+'s FIFO. This can be solved by a more precise termination condition for each process: when a process exhausts its list it adds an end symbol to the FIFO of the other process. A process terminates if it exhausts its list and if it reads end on its FIFO. This patched specification is given in Section J.3.

Refining the termination condition in the TRS of the Timbuk's specification, we can restart completion. Then no counterexample is found but a refinement is necessary. This is due to the fact that the equation add(X,add(Y,Z))=add(X,Z) may break the order of symbols in the FIFO. Thus, using this equation, "+" or "-" symbols may be occur in the FIFO after the end symbol, resulting in a false counterexample. To achieve the proof using Timbuk 3.1, it was necessary to guess a good set of equations, which is hard in general. On this particular example, it is necessary to figure out that the equation add(X,add(Y,Z))=add(X,Z) is likely to mix additions of "+", "-" and end symbols. Hence, replacing this equation by the three equations add(plus,add(plus,Z))=add(plus,Z), add(minus,add(minus,Z))=add(minus,Z) and add(end,add(end,Z))=add(end,Z) avoid this problem and permits to have a terminating completion and no false counterexamples. Tuning of equations by hand is hard on large examples and can be avoided here using automatic refinement. TimbukCEGAR and the initial equation proves it in 8 steps of completion and 5 steps of refinement. All the results can be certified by the checker.

The table of Figure 3 gives the number of rules of the TRS, the number of transitions of initial tree automaton, the number of refinement steps, the size of the completed automaton, execution time and memory usage for completion, and checking time. Line 1 gives the results for the automatic refinement of the initial equation. The same example is run with the three good equations (no refinement necessary) on line 2 and with Timbuk 3.1 on line 3.

The completion time with refinement (255s) has to be compared with the execution time of [START_REF] Boichut | Finer is better: Abstraction refinement for rewriting approximations[END_REF] which is superior to one hour 7 .

  is a set of normalized transitions and ε-transitions. The transitive and reflexive rewriting relation on T (F ∪ Q) induced by all the transitions of A is denoted by → * A . The tree language recognized by A in a state q is

φ 2 -

 2 → . . . qn with q = qn and φ = φ1 ∧ . . . ∧ φn. Transitions qi φ i

Those equations have to be provided by the user. In many cases, they can be produced when formalizing the problem in the TRMC framework[START_REF] Takai | A Verification Technique Using Term Rewriting Systems and Abstract Interpretation[END_REF]. The situation is similar for the predicates used in[START_REF] Bouajjani | Abstract regular model checking[END_REF][START_REF] Bouajjani | Abstract regular tree model checking[END_REF][START_REF] Bouajjani | Abstract rmc of complex dynamic data structures[END_REF].

essentially basic types, arithmetic, object creation, field manipulation, virtual method invocation, as well as a subset of the String library.

Acknowledgements Thanks to F. Besson for his help in integrating Buddy.

Fig. 3: Time and memory usage for completion with and without refinement.

J.2 Timbuk Specification leading to a Counterexample

Ops S:4 proc:2 stop:1 cons:2 nil:0 plus:0 minus:0 s: