Pierre-Cyrille Héam
email: pierre-cyrille.heam@inria.fr

Vincent Hugot ⋆⋆

Olga Kouchnarenko
email: olga.kouchnarenko@inria.fr

From Linear Temporal Logic Properties to Rewrite Propositions

In the regular model-checking framework, reachability analysis can be guided by temporal logic properties, for instance to achieve the counter example guided abstraction refinement (CEGAR) objectives. A way to perform this analysis is to translate a temporal logic formula expressed on maximal rewriting words into a "rewrite proposition" -a propositional formula whose atoms are language comparisons, and then to generate semidecision procedures based on (approximations of) the rewrite proposition. This approach has recently been studied using a non-automatic translation method. The extent to which such a translation can be systematised needs to be investigated, as well as the applicability of approximated methods wherever no exact translation can be effected. This paper presents contributions to that effect: (1) we investigate suitable semantics for LTL on maximal rewriting words and their influence on the feasibility of a translation, and (2) we propose a general scheme providing exact results on a fragment of LTL corresponding mainly to safety formulae, and approximations on a larger fragment.

Introduction & Context

Term rewriting and rewriting logic have been intensively and successfully used for solving equational problems in automated deduction, for programming language definitions, for model transformations and generation of efficient interpreters as well as for specification and verification in software engineering. In this last context, system states are modelled by languages, while rewrite rules stand for actions of the system; for instance procedure or method calls. This technique has been successfully used to prove the security of cryptographic protocols [START_REF] Genet | Rewriting for cryptographic protocol verification[END_REF] and Java Bytecode programs [START_REF] Boichut | Rewriting approximations for fast prototyping of static analyzers[END_REF]. When proving security, reachability analysis over sets of terms can be guided by temporal logic properties, like e.g., in [START_REF] Courbis | TAGED Approximations for Temporal Properties Model-Checking[END_REF][START_REF] Boyer | Verifying Temporal Regular Properties of Abstractions of Term Rewriting Systems[END_REF].

In [START_REF] Courbis | TAGED Approximations for Temporal Properties Model-Checking[END_REF], three specific Linear Temporal Logic (LTL) formulae -chosen for their relevance to model-checking [START_REF] Manna | Temporal Verification of Reactive Systems -Safety[END_REF], in particular with respect to Java MIDLets, in the framework of the French ANR RAVAJ project -have been translated into what we will call rewrite propositions, with respect to straightforward semantics for LTL on finite words. For instance, given a rewrite system R, of which X, Y ⊆ R are subsets, and an initial language Π, the LTL property (X ⇒ •Y) signifies that whenever an accessible term is rewritten by some rewrite rule in X, then the resulting term can be rewritten by some rule in Y, and not by any other rule. As shown in [START_REF] Courbis | TAGED Approximations for Temporal Properties Model-Checking[END_REF], that property is satisfied if and only if the following rewrite proposition holds: [R \ Y] X (R * (Π)) = ∅ ∧ X (R * (Π)) ⊆ Y -1 (T(A)), where R * (Π) is the transitive-reflexive forward closure of Π by R, and T(A) is the set of all trees. The point of translating satisfaction in terms of rewrite propositions is that they present a more tractable intermediary form which can itself be translated into automata-based (semi-)decision procedures. Indeed, if the initial language Π is regular, then the literature is rife with constructive results concerning questions such as preservation of regularity under a rewriting step, or under forward closure; that is to say, "under which conditions on the rewrite system R is R(Π) (resp. R * (Π)) still regular?". And when preserving regularity is not an option, one may fall back on more expressive classes of tree automata (TA) such as TAGED [START_REF] Filiot | Tree automata with global constraints[END_REF]. As an example of both aspects, [START_REF] Courbis | TAGED Approximations for Temporal Properties Model-Checking[END_REF]Prop. 5] states that a language given by R -1 (T(A)) can in all generality be represented by a positive TAGED; furthermore, if R is left-linear, then regularity is preserved. Such results can be combined with regular approximation techniques; for instance, if A is a tree automaton, a procedure Approx(A, R) in [START_REF] Boichut | Approximation-based tree regular model-checking[END_REF] yields another TA B such that Lang(B) ⊇ R * (Lang(A)), where Lang(A) is the language accepted by A. Put together, those tools provide a framework for building decision and semi-decision procedures from rewrite propositions. For instance, the proposition given above is semi-decided by the conjunction of the procedures IsEmpty(OneStep(R \ Y, Approx(A, R)), X) and Subset(OneStep(X, Approx(A, R)), Backward(Y)), where Lang(A) = Π and under the additional constraint that Y must be left-linear. Note that this is almost a straightforward reformulation of the original rewrite proposition.

To summarise the above, our approach to model-checking temporal properties of sequences of rewrite rules consists of two phases outlined in [START_REF] Courbis | TAGED Approximations for Temporal Properties Model-Checking[END_REF]: (1) translation of a temporal logic formula expressed on maximal rewriting words into a "rewrite proposition" -a propositional formula whose atoms are language comparisons, and (2) translation of the rewrite proposition into a semi-decision procedure. To make this approach useful for program verification, both steps must be automated; neither is at present. The general question investigated in the present paper is whether -and more specifically how and to what extent -such a translation can be automated for arbitrary temporal properties. More specifically, we focus solely on the first step, i.e. translation from temporal logic to rewrite propositions. The second step is an entirely different problem, and is out of the scope of this paper.

Related work.

In recent years, new results in rewriting logic have deeply extended the spectrum of its applications [START_REF] Escobar | Symbolic model checking of infinite-state systems using narrowing[END_REF][START_REF] Serbanuta | A rewriting logic approach to operational semantics[END_REF][START_REF] Boronat | Rewriting logic semantics and verification of model transformations[END_REF][START_REF]Rewriting Logic and Its Applications[END_REF], especially in relation with temporal logic for rewriting [START_REF] Meseguer | The temporal logic of rewriting: A gentle introduction[END_REF][START_REF] Bae | The linear temporal logic of rewriting Maude model checker[END_REF]. Unlike [START_REF] Bae | The linear temporal logic of rewriting Maude model checker[END_REF], where LTL model checking is performed over finite structures, our approach handles temporal formulae over infinite state systems. In this sense, it is close to [START_REF] Escobar | Symbolic model checking of infinite-state systems using narrowing[END_REF]. However, in spite of its simplicity for practical applications, it does not permit -in its current state, at least -to consider equational theories. Our viewpoint differs slightly from other regular model-checking approaches such as Regular LTL [START_REF] Boyer | Verifying Temporal Regular Properties of Abstractions of Term Rewriting Systems[END_REF] in that the temporal property relates to sequences of actions as opposed to sequences of states. It is however very similar to the method presented in [START_REF] Meseguer | Conditioned Rewriting Logic as a United Model of Concurrency[END_REF], when reducing the equational theory to the identity.

Organisation of the paper. Section 2 presents the notions and notations in use throughout this paper, including the choice of temporal semantics and a precise statement of the problem at hand. Section 3 [p6] deals with the main contributions of the paper: the translation rules and the technical tools (signatures, weak/strong intertwined semantics, etc) on which they depend.

Preliminaries & Problem Statement

The extended naturals are denoted by N ⊳ = N ∪ {+∞} and n, m denotes the integer interval [n, m] ∩ Z, with the convention that 0, +∞ = N. For any k ∈ N,

N k ⊳ = k, +∞ and N k ⊳ = N k ∪ {+∞}.
The powerset of S is written ℘(S). Substitution is written f[v/X], meaning "v replaces X in the expression f".

Rewrite Words & Maximal Rewrite Words

A comprehensive survey on term rewriting can be found in [START_REF] Dershowitz | Rewrite Systems[END_REF]. Let T(A) be the set of all terms on a ranked alphabet A, let R be a finite rewrite system, and Π ⊆ T(A) any set of terms. A finite or infinite word on R is an element of

W ⊳ = n∈N 1, n → R .
The length #w ∈ N of a word w is defined as Card (dom w). Note that the empty function -of graph ∅ × R = ∅ -is a word, which we call the empty word, denoted by λ. Let w ∈ W be a word of domain 1, n , for n ∈ N, and let m ∈ N 1 ; then the m-suffix of w is the word denoted by w m , such that

w m ⊳ = 1, n -m + 1 -→ R k -→ w(k + m -1) .
Note that w 1 = w, for any word w. The intuitive meaning that we attach to a word w is a sequence of rewrite rules of R, called in succession -in other words, it represents a "run" of the TRS R. Of course, there is nothing in the above definition of words that guarantees that such a sequence is in any way feasible, and such a notion only makes sense with respect to initial terms to be rewritten.

Thus we now define the maximal rewrite words of R, originating in Π:

R Π ⊳ = w ∈ W ∃u 0 ∈ Π : ∃u 1 , . . . , u #w ∈ T(A) : ∀k ∈ dom w, u k-1 w(k) ---→ u k ∧ #w ∈ N ⇒ R({u #w }) = ∅ .
Note the potential presence of the empty word in that set. Informally, a word w is in R Π if and only if the rewrite rules w(1), . . . , w(n), . . . can be activated in succession, starting from a term u 0 ∈ Π, and the word w is "maximal" in the sense that it cannot be extended. That is to say, w ends only when no further rewrite rule can be activated. Thus R Π captures the behaviours (or runs) of R, starting from Π; this notion corresponds to the full paths of the rewrite graph described in [START_REF] Courbis | TAGED Approximations for Temporal Properties Model-Checking[END_REF].

Defining Temporal Semantics on Rewrite Words

Choice of LTL & Syntax. Before starting to think about translating temporal logic formulae on rewrite words, we need to define precisely the kind of temporal formulae under consideration, and their semantics. Given that prior work in [START_REF] Courbis | TAGED Approximations for Temporal Properties Model-Checking[END_REF] was done on LTL, and that our aim is to generalise this work, LTL -with subsets of R as atomic proposition -seems a reasonable choice. In practice we shall use a slight variant with generalised weak and strong next operators; the reasons for this choice will be discussed when the semantics are examined. A formula ϕ ∈ LTL is generated by the following grammar:

ϕ := X | ¬ϕ | ϕ ∧ ϕ | • m ϕ | • m ϕ | ϕ U ϕ X ∈ ℘(R) ⊤ | ⊥ | ϕ ∨ ϕ | ϕ ⇒ ϕ | ϕ | ϕ m ∈ N .
Note that the operators which appear on the first line are functionally complete; the remaining operators are defined syntactically as:

⊤ ⊳ = R ∨ ¬R, ⊥ ⊳ = ¬⊤, ϕ ∨ ψ ⊳ = ¬(¬ϕ ∧ ¬ψ), ϕ ⇒ ψ ⊳ = ¬ϕ ∨ ψ, ϕ ⊳ = ⊤ U ϕ and ϕ ⊳ = ¬ ¬ϕ.

Choice of Semantics.

In the literature, the semantics of LTL are defined and well-understood for ω-words; however the words of R Π may be infinite or finite, or even empty, which corresponds to the fact that, depending on its input, a rewrite system may either not terminate, terminate after some rewrite operations, or terminate immediately. Therefore we need semantics capable of accommodating both ω-words and finite words, as well as the edge-case of the empty word. In contrast to the classical case of ω-words, there are several ways to define (two-valued) semantics for LTL on finite, maximal words. One such way found in the literature is Finite-LTL (F-LTL) [START_REF] Manna | Temporal Verification of Reactive Systems -Safety[END_REF], which complements the long-standing use of a "strong" next operator introduced in [START_REF] Kamp | Tense Logic and the Theory of Linear Order[END_REF] by coining a "weak" next variant. Figure 1 [p5] presents our choice of semantics for this paper,

(w, i) | = X iff i ∈ dom w and w(i) ∈ X (w, i) | = ¬ϕ iff (w, i) | = / ϕ (w, i) | = (ϕ ∧ ψ) iff (w, i) | = ϕ and (w, i) | = ψ (w, i) | = • m ϕ iff i + m ∈ dom w and (w, i + m) | = ϕ (w, i) | = • m ϕ iff i + m dom w or (w, i + m) | = ϕ (w, i) | = ϕ U ψ iff ∃j ∈ dom w : j i ∧ (w, j) | = ψ ∧ ∀k ∈ i, j -1 , (w, k) | = ϕ For any w ∈ W, i ∈ N 1 , m ∈ N and X ∈ ℘(R).

Fig. 1: LTL Semantics on Maximal Rewrite Words

which is essentially F-LTL with generalised next operators and the added twist that words may be infinite or empty. Note that • 1 and • 1 correspond exactly to the classical strong and weak next operators, and that for m 1, • m (resp. • m ) can trivially be obtained by repeating • 1 (resp. • 1 ) m times. So the only non-trivial difference here is the existence of • 0 and • 0 ; this will prove quite convenient when we deal with the translation of , using the following lemma.

Lemma 1 (Weak-Next & Always). Let ϕ ∈ LTL, w ∈ W, k ∈ N and i ∈ N 1 ; it holds that (1) (w, i) | = ϕ iff (w, i) | = ∞ m=0 • m ϕ and (2) (w, i) | = ϕ iff (w, i) | = k-1 m=0 (• m ϕ) ∧ • k ϕ.
Before moving on, let us stress that the choice of semantics, or even the choice of LTL for that matter, should by no means be considered as etched in stone; it is very much a variable of the general problem. However it will henceforth be considered as data for the purposes of this paper.

TRS & LTL.

Let ϕ be an LTL formula. We say that a word w satisfies/is a model of ϕ (denoted by w | = ϕ) iff (w, 1) | = ϕ. Alternatively, we have (w, i) | = ϕ iff w i | = ϕ. We say that the rewrite system R, with initial language Π, satisfies/is a model of ϕ (denoted by R,

Π | = ϕ) iff ∀w ∈ R Π , w | = ϕ.

Rewrite Propositions & Problem Statement

A rewrite proposition on R, from Π is a formula of propositional logic whose atoms are language or rewrite systems comparisons. More specifically, a rewrite proposition π is generated by the following grammar:

π := γ | γ ∧ γ | γ ∨ γ γ := ℓ = ∅ | X ⊆ X | ℓ ⊆ ℓ X ∈ ℘(R) . ℓ := Π | T(A) | X(ℓ) | X -1 (ℓ) | X * (ℓ)
Since the comparisons γ have obvious truth values, the interpretation of rewrite propositions is trivial; thus we will not introduce any notation for it, and automatically confuse π with its truth value in the remainder of this paper. Note that while other operators for propositional logic could be added, conjunction and disjunction will be enough for our purposes.

Problem Statement. We have now done enough groundwork to state our problem more formally. Given a rewrite system R, a temporal formula ϕ in LTL (or some fragment of LTL), and an initial language Π ⊆ T(A), we search for an algorithmic method of building a rewrite proposition π such that R, Π | = ϕ if and only if π holds. We call such a method, as well as its result, an exact translation of ϕ, and say that π translates ϕ. If π is only a sufficient (resp. necessary) condition, then it is an under-approximated (resp. over-approximated) translation.

Building Translation Rules

Overview & Intuitions of the Translation

The Base Cases. Counterintuitively, ϕ = ¬X is actually a simpler case than ϕ = X as far as the translation is concerned, so we will consider it first. Case 1: Negative Literal. Suppose R, Π | = ¬X. Recalling the semantics in Fig. 1 [p5] , this means that no term of Π can be rewritten by a rule in X. They may or may not be rewritable by rules not in X, though. Consider now π 1 ≡ X(Π) = ∅; it is easy to become convinced that this is an exact translation. Case 2: Positive Literal. Let ϕ = X. A first intuition would be that this is roughly the same case as before, but with the complement of X wrt. R. So we write π 2 ≡ [R \ X](Π) = ∅. This, however, is not strong enough. It translates the fact that only rules of X can rewrite Π.

But again, while X may in fact rewrite Π, there is nothing in π 2 to enforce that. Looking at the semantics, all possible words of R Π must have at least one move (i.e. 1 ∈ dom w); this condition must be translated. It is equivalent to saying that all terms of Π are rewritable, which is expressed by Π ⊆ R -1 (T(A)). More specifically, since we already impose that they are not rewritable by R \ X, we can even write directly that they are rewritable by X, i.e. Π ⊆ X -1 (T(A)). Putting those two conditions together, we obtain

π ′ 2 ≡ [R \ X](Π) = ∅ ∧ Π ⊆ X -1 (T(A))
, and this is an exact translation.

Of Strength & Weakness. Let us reflect on the previous cases for a minute; the immediate intuition is that X is stronger than ¬X, in the sense that whenever we see X, we must write an additional clause -enforcing rewritability -compared to ¬X. This actually depends on the context, as the next example will show. Case 3: Always Negative. Let ϕ = ¬X. This means that neither the terms of Π nor their successors can be rewritten by X; in other words

π 3 ≡ X R * (Π) = ∅.
The translation is almost the same as for ¬X, the only difference being the use of R * (Π) (Π and successors) instead of just Π as in π 1 . More formally,

π 3 ≡ π 1 [R * (Π)/Π]. Case 4: Always Positive.
Seeing this, one is tempted to infer that the same relationship that exists between the translations of ¬X and ¬X exists as well between those of X and X. In the case ϕ = X, this would yield

π 4 ≡ π ′ 2 [R * (Π)/Π] ≡ [R \ X] R * (Π) = ∅ ∧ R * (Π) ⊆ X -1 (T(A)).
But clearly this translation is much too strong as its second part implies that every term of Π can be rewritten by X, and so can all of the successors; consequently, R Π must form an ω-language. Yet we have for instance λ | = X -note incidentally that λ | = ψ holds vacuously for any ψ. In general, under the semantics for , words of any length, infinite, finite or nought, may satisfy X. Thus the correct translation was simply π

′ 4 ≡ [R \ X] R * (Π) = ∅.
So, unlike Cases 1 and 2, X is not in any sense stronger than ¬X when behind a . This is an important point which we shall need to keep track of during the translation; that necessary bookkeeping is the reason for the introduction of the weak and strong intertwined semantics described in Section 3.

(R, Π | = ϕ ∧ ψ) ⇐⇒ (R, Π | = ϕ)∧(R, Π | = ψ).
Contrariwise, the same does not hold for the disjunction, and we have no general solution (a) to handle it. Given that one of the implications still holds, namely (R,

Π | = ϕ ∨ ψ) ⇐= (R, Π | = ϕ) ∨ (R, Π | = ψ), a crude under-approximation can still be given if all else fails: π 5 ∨ π ′ 5 =⇒ R, Π | = ϕ ∨ ψ. Case 6:
Negation. Although we have seen in Case 1 that a negative literal can easily be translated, negation cannot be handled in all generality by our method. Note that, because of the universal quantification, R, Π | = / ϕ R, Π | = ¬ϕ; thus the fact that π 6 translates ϕ does not a priori imply that ¬π 6 translates ¬ϕ. This is why we will assume in practice that input formulae are provided in Negative Normal Form, which is licit as the presence of both weak and strong next operators enables any formula to be put in NNF.

Handling Material Implication. Case 7. We have just seen in Cases 5 and 6 that we can provide exact translations for neither negation nor disjunction. Inasmuch as ϕ ⇒ ψ is defined as ¬ϕ ∨ ψ, must material implication be forgone as well? An example involving an implication has been given in the introduction (page 1), so it would seem that a translation can be provided in at least some cases. Let us take the simple example X ⇒ •Y. Assuming that any term u ∈ Π is rewritten into some u ′ by a rule in X, then u ′ must be rewritable by Y, and only by Y. The set of X-successors of Π being X(Π), those conditions yield the translation

π 7 ≡ X(Π) ⊆ Y -1 T(A) ∧ [R \ Y] X(Π) = ∅.
Note that the way in which implication has been handled here is very different from the approach taken for the other binary operators, which essentially consists in splitting the formula around the operator and translating the two subparts separately. In contrast, the antecedent of the implication was "assumed", whilst the consequent was translated as usual. In fact, recalling that π ′ 2 translates X, and thus

π ′′ 2 ≡ π ′ 2 [Y/X] translates Y, we have π 7 ≡ π ′′ 2 [X(Π)/Π].
So, "assuming" the antecedent consisted simply in changing our set of reachable terms -which we will from now on call the past, hence the notation Π. This is not an isolated observation; if π 0 denotes the translation of (X ⇒ •Y) given in the introduction, then

π 0 ≡ π 7 [R * (X(Π))/X(Π)].
Thus "updating" the past is enough of a tool to deal with some simple uses of and implication. . . but consider the following formula: •Y ⇒ X. In that case the antecedent lies in the future, relatively to the consequent. Therefore, in order to deal with all cases, we need some means of making assumptions about both past and future. This is the goal of the signatures presented in Section 3.3 [p10] .

(a) There are however special cases where disjunction can be translated exactly; see rules (∨ ⇒ ∧ ) [p15] and (∨ ¬ ⇒ ).

Weak and Strong Semantics for LTL

Restricting the Fragment. As mentioned in Cases 3 and 4 of the previous section, we will in practice be restricted to working with formulae provided in Negative Normal Form. Furthermore, there are operators, such as , for which we think that no translation can be provided, because rewrite propositions are not expressive enough -in particular, R * (Π) hides all information regarding finite or infinite traces. If this is the case, then none of the operators of the "Until" family { , U, W, R, . . . } can be dealt with. Consequently, we are restricted to the following fragment of LTL, which will be denoted by R-LTL:

ϕ := X | ¬X | ϕ ∧ ϕ | ϕ ∨ ϕ | ϕ ⇒ ϕ | X ∈ ℘(R) • m ϕ | • m ϕ | ϕ m ∈ N .
Bookkeeping. (cf. Sec. 3.1 [p6] , case 4) In order to address the question of whether the translation of an atom X should be "strong" -enforce rewritability -or "weak", information is needed from the context. Namely, does the atom appear in the direct scope of a ? We solve this by introducing intertwined weak semantics -written | = w -and strong semantics -written | = s , given in Fig. 2. For µ ∈ { w, s } , where the translation rules are given. The important point for now is that the strong semantics are equivalent to the normal semantics of LTL on the fragment R-LTL, which is shown by Lemma 3.

(w, i) | = µ ⊤ (w, i) | = / µ ⊥ (w, i) | = s X iff i ∈ dom w and w(i) ∈ X (w, i) | = w X iff i dom w or w(i) ∈ X (w, i) | = µ ¬X iff i dom w or w(i) X (w, i) | = µ (ϕ ∨ ψ) iff (w, i) | = µ ϕ or (w, i) | = µ ψ (w, i) | = µ (ϕ ∧ ψ) iff (w, i) | = µ ϕ and (w, i) | = µ ψ (w, i) | = µ (ϕ ⇒ ψ) iff (w, i) | = s ϕ =⇒ (w, i) | = s ψ (w, i) | = µ • m ϕ iff i + m ∈ dom w and (w, i + m) | = s ϕ (w, i) | = µ • m ϕ iff i + m dom w or (w, i + m) | = w ϕ (w, i) | = µ ϕ iff ∀j ∈ dom w, j i ⇒ (w, j) | = w ϕ For any m ∈ N, µ ∈ { w, s }
Lemma 2 (Strong-Weak Domain-Equivalence). For all w, ϕ, i, it holds that i ∈ dom w =⇒ (w, i) | = s ϕ ⇔ (w, i) | = w ϕ.

Lemma 3 (Strong Semantics). For all words w ∈ W and all formulae

ϕ ∈ R-LTL, we have ∀i ∈ N 1 , (w, i) | = s ϕ ⇐⇒ (w, i) | = ϕ.

Girdling the Future: Signatures

As discussed in Sec. 3.1 [p6] , Case 7, implication is handled by converting the antecedent ϕ of a formula ϕ ⇒ ψ into "assumptions". Concretely, this consists in building a model of ϕ -called a signature of ϕ, written ξ(ϕ) -which can be manipulated during the translation. The variety of signatures defined hereafter handles formulae ϕ within the fragment A-LTL (A for antecedent), which is R-LTL without ∨ or ⇒. This section covers the technical tools needed for building signatures (Fig. 3 [p13] ) and understanding the translation rules (Sec. 3.4 [p15] ).

Definitions.

Signatures. A signature σ is an element of the space

Σ = n∈N 1, n ∪ {ω} → ℘(R) × ℘(N) .
Core, Support, Domain, Cardinal. Let σ = (f, S); then the function f is called the core of σ, denoted by ∂σ, and S is called its support, written ∇σ. The domain of σ is defined as dom σ ⊳ = dom f \ {ω}, and its cardinal is #σ ⊳ = Card (dom σ). Special Notations, Empty Signature. A signature σ = (f, S) will be written either compactly as σ = f | S , or in extenso as f(1), f(2), . . . , f(#σ) f(ω) | S . We denote by ε

⊳ = R | N the empty signature. Let k ∈ N 1 ∪ {ω}, then we write σ[k] ⊳ = f(k) if k ∈ dom σ f(ω) if k dom σ .
Signature Product. Let σ and σ ′ two signatures; then their product is another signature defined as

σ σ ′ ⊳ = g | ∇σ ∩ ∇σ ′ , where g ⊳ = dom ∂σ ∪ dom ∂σ ′ -→ ℘(R) k -→ σ[k] ∩ σ ′ [k] . Note that as a consequence, ∀k ∈ N 1 , (σ σ ′ )[k] = σ[k] ∩ σ ′ [k]. (e.g. Let σ = X, Y Z | N 2 and ρ = X ′ Z ′ | N 3 ; then σ ρ = X ∩ X ′ , Y ∩ Z ′ Z ∩ Z ′ | N 3 .)
Remark 4 (Summation Notation). The set of signatures Σ, equipped with the signature-product , forms a commutative monoid whose neutral element is ε.

Convergence. Let ρ = (σ n ) n∈N be an infinite sequence of signatures. It is

convergent if (1) the sequence (∇σ n ) n∈N converges towards a limit ∇σ ∞ , and (2)
for all k ∈ N 1 , the sequence (σ n [k]) n∈N converges towards a limit σ ∞ [k], and (3) the sequence of limits (σ ∞ [k]) k∈N 1 itself converges towards a limit σ ∞ [∞]. We call this sequence the limit core. It is not directly in the form of a bona fide signature core. However, its co-domain being ℘(R), which is finite, there exists a rank N 0 such that for all k > N, σ

∞ [k] = σ ∞ [∞],
and thus, taking the smallest such N, we define σ

∞ [1] , . . . , σ ∞ [N] σ ∞ [∞]
| ∇σ ∞ to be the limit of ρ, which we denote by lim ρ or lim n→∞ σ n , or more simply by σ ∞ . Note that the core of the limit is equivalent to the limit core, in the intuitive sense that they define the same constrained words. Otherwise ρ is divergent, and its limit is left undefined. (e.g.

The sequence ( R 1 , . . . R n , X R | 1, n ) n∈N , with R i = R ∀i,
= { 1 → X, 2 → Y, ω → Z }, its domain is dom σ = 1, 2 , its support is ∇σ = N 2 , its cardinal is #σ = 2, and we have σ[1] = X, σ[2] = Y, σ[3] = σ[4] = • • • = σ[ω] = Z.
Its constrained words are the maximal words of length at least 2, whose first two letters are in X and Y, respectively, and whose other letters are all in Z.) Lemma 5 serves in the base cases of signature-building, and Lem. 6 in the constructions of ξ(ϕ ∧ ψ) and ξ( ϕ), and rule (⇒ Σ ) [p15] ;

Lemma 5 (No Constraints). We have R Π ε = R Π .
Lemma 6 (Breaking Products). For any signatures σ, σ ′ ∈ Σ, and any language Π, we have

(1) R Π σ σ ′ = R Π σ ∩ R Π σ ′ . Furthermore, this generalises to infinitary cases: (2) given a sequence (σ n ) n∈N such that the infinite product ∞ n=0 σ n converges, it holds that R Π ∞ n=0 σ n = ∞ n=0 R Π σ n .
Arithmetic Overloading. We overload the operators + andon the profile ℘(N) × N → ℘(N) such that, for any S ∈ ℘(N) and n ∈ N, we have S + n

⊳ = { k + n | k ∈ S } and S -n ⊳ = { k -n | k ∈ S } ∩ N. Shifts Left & Right. Let m ∈ N;
⊳ = R 1 , . . . , R m , ∂σ(1), . . . , ∂σ(#σ) ∂σ(ω) | 0, m ∪ (∇σ + m) , with R 1 = R, . . . , R m = R. Note that for all m ∈ N and all k ∈ N 1 , (σ ⊳ m)[k] = σ[k + m], for all k m, (σ ◮ m)[k] = (σ ⊲ m)[k] = R and for all k > m, (σ ◮ m)[k] = (σ ⊲ m)[k] = σ[k -m]. (e.g. Let σ = X, Y Z | N 2 ; then σ ◭ 1 = σ ⊳ 1 = Y Z | N 1 , σ ◮ 1 = R, X, Y Z | N 3 , and σ ⊲ 1 = R, X, Y Z | N \ {2} . )
Lemma 7 justifies the fact that the computation of ξ( ϕ) always yields a useable signature; a closed form of the limit is given in the proof.

Lemma 7 (Automatic Convergences). Let (σ n ) n∈N be any sequence of signatures, and (ρ n ) n∈N its associated sequence of partial products ( n i=0 σ i ) n∈N . Then (ρ n ) n∈N satisfies convergence criteria (1) and (2). Furthermore, if σ is a given signature and σ i = σ ◮ i or σ i = σ ⊲ i, for any i ∈ N, then criterion (3) is satisfied as well, and the infinite product ∞ n=0 σ n converges.

Proof.

(1) For all n ∈ N, ∇ρ n = n i=0 ∇σ i , thus it is clear that ∇ρ n = n i=0 ∇σ i ⊇ n+1 i=0 ∇σ i = ∇ρ n+1 or, in other words, (∇ρ n ) n∈N is a (trivial) contracting sequence of finite sets. Therefore it converges towards ∞ i=0 ∇σ i . (2) Let k ∈ N 1 ; we have

ρ n [k] = n i=0 σ i [k] = n i=0 σ i [k] ,
and thus

ρ n [k] = n i=0 σ i [k] ⊇ n+1 i=0 σ i [k] = ρ n+1 [k] and again, (ρ n [k]
) n∈N is a trivial contracting sequence of finite sets; therefore it converges towards a limit which we denote by ρ ∞

[k] = ∞ i=0 σ i [k]. (3
) Suppose now that σ i = σ ⊲ i (resp. σ i = σ ◮ i, the computation will be unchanged), we have

ρ ∞ [k] = ∞ i=0 σ i [k] = ∞ i=0 (σ ⊲ i)[k] = k-1 i=0 (σ ⊲ i)[k] ∩ ∞ i=k (σ ⊲ i)[k] = k-1 i=0 σ[k -i] ∩ ∞ i=k R = k-1 i=0 σ[k -i] = k i=1 σ[i] . Given that for all i > #σ, σ[i] = σ[ω], it follows that for all k > #σ, ρ ∞ [k] = #σ+1 i=1 σ[i]. Thus (ρ ∞ [k]) k∈N 1 converges. This shows that the infinite product ∞ n=0 σ n is convergent.
Building Signatures. Figure 3 [p13] defines the function ξ(•) : A-LTL → Σ. As Theorem 8 shows, the signature ξ(ϕ) essentially captures a model of ϕ.

ξ(⊤) ⊳ = R | N = ε ξ(⊥) ⊳ = ∅ | ∅ ξ(X) ⊳ = X R | N 1 ξ(¬X) ⊳ = R \ X R | N ξ(• m ϕ) ⊳ = ξ(ϕ) ◮ m ξ(• m ϕ) ⊳ = ξ(ϕ) ⊲ m ξ(ϕ ∧ ψ) ⊳ = ξ(ϕ) ξ(ψ) ξ( ϕ) ⊳ = ∞ m=0 ξ(ϕ) ⊲ m
R Π ξ(ϕ) = w ∈ R Π w | = ϕ .

The Translation Rules

Now that the main technical tools are in place, there remains to define what is meant by "translation rule", and to state the rules themselves. For any µ ∈ { w, s }, ϕ ∈ LTL, Π ⊆ T(A), σ ∈ Σ, we define Π σ µ ϕ as shorthand for ∀w ∈ R Π σ , w | = µ ϕ. We call such a notation Π σ µ ϕ a translation block.

A translation rule is of the form

A P(σ, ϕ) E or ↑ A P(σ, ϕ) E or ? A ↑ P(σ, ϕ) Q(σ, ϕ) E ,
where A stands for some translation block Π σ µ ϕ , P, Q ∈ Σ × R-LTL → B are predicates on signatures and formulae, and E is a mixed translation/reachability proposition. More precisely, E is generated by the grammar given in Sec. 2.3 [p6] , with the added production γ := Υ, where Υ is a translation block. The -rules (exact translations) are defined to hold iff P(σ, ϕ) =⇒ (A ⇔ E), the ↑-rules (under-approximations) hold iff P(σ, ϕ) =⇒ (E ⇒ A), and the ?-rules hold iff P(σ, ϕ) =⇒ (E ⇒ A) and (P(σ, ϕ) ∧ Q(σ, ϕ)) =⇒ (A ⇔ E). When omitted, P is assumed to be ⊤. Theorem 9 entails that any derivation (i.e. tree of rule applications with no translation blocks left in the leaves) starting with Π ε s ϕ yields an exact translation of ϕ (if only exact rules are involved), or an under-approximation (if some ↑-rules are used).

Theorem 9 (Translation Satisfaction

). Π ε s ϕ ⇐⇒ R, Π | = ϕ.
A few additional definitions and results about signatures are needed in order to justify some translation rules: Remark 10 is needed by rule ( h ) [p15] ; Lem. 13 intervenes in rules (• m ) [p15] and (• m ); Lem. 11 and Cor. 12 in rule (• m ); Rmk. 14 and Lem. 15 in rule ( * ); Prp. 16 [p15] justifies that rule ( h ) eventually terminates. Signature Iteration. Let Π ⊆ T(A) a language, and σ ∈ Σ a signature; then for n ∈ N we let

Π n σ ⊳ = σ[n] σ[n -1] (• • • σ[1] (Π) • • •) be the n-iteration of the signature σ. More formally, it is defined recursively such that Π 0 σ ⊳ = Π and Π n+1 σ ⊳ =σ[n + 1] (Π n σ ).
Length Rejector. For n ∈ N, the rewrite proposition Ψ σ Π (n) is called the n-length rejector, and defined as

Ψ σ Π (n) ⊳ = Π n σ ⊆ σ[n + 1] -1 (T(A)). Strengthening. If σ is a signature, then ⋆σ ⊳ = ∂σ | ∇σ \ {0} is its strengthening. Note that (σ ◭ m) = ⋆(σ ⊳ m), for all m.
Remark 10 (Strengthening of Always). Let Π ⊆ T(A), σ ∈ Σ, and ϕ ∈ R-LTL. Then Π σ µ ϕ ⇐⇒ Π ⋆σ µ ϕ . Lemma 11. Let σ be a signature and Π ⊆ T(A) a language; then for any n ∈ N, the proposition Ψ σ Π (n) holds iff for all w ∈ R Π σ , #w n. Corollary 12 (Length Rejection). Let S ∈ ℘(N), σ a signature and Π a language; the rewrite proposition n∈S∩∇σ Ψ σ Π (n) holds iff for all w ∈ R Π σ , #w S. Lemma 13 (Shifting Words). Let σ be a signature and Π ⊆ T(A) a language; then

R Π m σ σ ⊳ m = w m+1 w ∈ R Π σ ∧ #w m .
Remark 14 (Constrained Union). Let σ ∈ Σ, I ⊆ N, and for each i ∈ I, Π i ⊆ T(A).

Then i∈I R Π i σ = R i∈I Π i σ . Stability. A signature σ ∈ Σ is called stable if σ ⊳ 1 = σ;
this is equivalent to the condition #σ = 0 and ∇σ ∈ { ∅, {+∞} , N, N }, and also to the condition ∀n ∈ N, σ ⊳ n = σ. High Point. The high point hσ of a signature σ is the smallest h ∈ N such that σ ⊳ h is stable. Note that σ is stable if and only if hσ = 0. Given the characterisation of stability given above, an alternative definition of hσ would be the smallest h #σ such that either N h ⊆ ∇σ or ∇σ ∩ N h = ∅. If no such h exists (b) , we take by convention hσ = +∞. Low Point. The low point ℓσ of a signature σ is the smallest length authorised by σ; more precisely, it is defined as ℓσ ⊳ = min ∇σ.

(b) Consider a signature σ such that ∇σ is the set of odd numbers, or the set of prime numbers, for instance.

Such a signature cannot be stabilised. Fortunately, Proposition 16 [p15] shows that such exotic cases are irrelevant to this paper.

Lemma 15 (All Suffixes). Let σ be a stable signature, and Π ⊆ T(A) a language. Then we have

w 1+n n ∈ N, w ∈ R Π σ , #w n = R σ[ω] * (Π) σ .
Proposition 16 (Stability of ξ(•)). The signature of any formula ϕ ∈ A-LTL is stabilisable; in other words, hξ(ϕ) ∈ N, ∀ϕ ∈ A-LTL.

Theorem 17 (Translation). All the following translation rules hold.

Π σ µ ⊤ ⊤ (⊤) Π σ µ ⊥ ⊥ (⊥) Π σ µ X ∧ Y Π σ µ X ∩ Y (∧ X ) Π σ µ X ∨ Y Π σ µ X ∪ Y (∨ X ) Π σ µ ϕ ∧ ψ Π σ µ ϕ ∧ Π σ µ ψ (∧) Π σ µ [ϕ ∨ ϕ ′ ] ⇒ ψ Π σ µ ϕ ⇒ ψ ∧ Π σ µ ϕ ′ ⇒ ψ (∨ ⇒ ∧ ) Π σ µ ϕ ∨ ψ ¬ϕ ∈ A-LTL Π σ µ ¬ϕ ⇒ ψ (∨ ¬ ⇒ ) ↑ Π σ µ ϕ ∨ ψ Π σ µ ϕ ∨ Π σ µ ψ (∨ ↑ ) Π σ µ ϕ ⇒ ψ Π σ ξ(ϕ) s ψ (⇒ Σ ) Π σ µ • m ϕ Π m σ σ ◭ m w ϕ (• m ) Π σ µ • m ϕ Π σ µ • m ϕ ∧ n∈ 0,m ∩∇σ Ψ σ Π (n) (• m ) Π σ µ ϕ σ is stable σ[ω] * (Π) ⋆σ w ϕ ( * ) Π σ µ ϕ hσ ∈ N 1 Π σ µ hσ-1 k=0 • k ϕ ∧ Π hσ σ σ ⊳ hσ µ ϕ ( h ) Π σ µ ¬X Π σ w R \ X (¬X)
Additionally, the following four rules are being explored as a possible coverage of the difficult case of the atom X. While the main bodies of those rules encompass all the necessary translations, adjusting their exact respective application predicates is still ongoing work, which sets them apart from the proven formulae of Thm. 17.

? Π σ w X ↑ ℓσ 1 σ ⊳ 1 = ε R \ (X ∩ σ[1]) (Π) = ∅ (X w ℓ 1 ) ? Π σ s X ↑ ℓσ = 0 σ ⊳ 1 = ε Π σ w X ∧ Π ⊆ X ∩ σ[1] -1 (T(A)) (X s ℓ0 ) ? Π σ s X ↑ ℓσ = 1 σ ⊳ 1 = ε Π σ w X (X s ℓ1 ) ? Π σ µ X ↑ ℓσ 2 σ ⊳ ℓσ = ε σ[ℓσ] • • • σ[2] R \ (X ∩ σ[1]) (Π) • • • = ∅ (X µ ℓ2 )
The general derivation algorithm consists in systematically applying the first rule that matches, starting with the block Π ε s ϕ . Let it be noted that not all of the given rules are strictly necessary. For instance (∨ ⇒ ∧ ) corresponds to a basic tautology of propositional logic, which rewrites the formula in a form more amenable to translation. Similarly, rule (∨ ¬ ⇒ ) relies on a transformation of the antecedent into A-LTL (which is not always possible, in which case the rule does not apply). While their presence is not fundamental to the system, they extend the number of translatable cases. There are doubtless many other such simplifications not listed here -an obvious one being the commutation of (∨ ¬ ⇒ ). This sensitivity of the translation to transformations of the input formula makes it difficult to give an exact characterisation of the supported fragment -it is not simply R-LTL, restricted to A-LTL for antecedents. For instance, even though cannot be translated in general, its presence in the NNF of the input ϕ is not enough in itself to assert that ϕ cannot be translated: if it appears in, say, X ∨ ψ, it can be handled using rule (∨ ¬ ⇒ ). We intend to expand the translatable fragment in future works; this will hopefully make it easier to characterise.

Example. Let us derive the translation of

ϕ = (X ⇒ • 1 Y). Π ε s (X ⇒ • 1 Y) ( * ) R * (Π) ⋆ε w X ⇒ • 1 Y (⇒ Σ ) R * (Π) X R | N 1 s • 1 Y (• m ) Ψ X R|N 1 R * (Π) (1) ∧ R * (Π) X R | N 1 s • 1 Y (• m ) X(R * (Π)) R | N 1 w Y (X w ℓ 1 ) [R \ Y] (X(R * (Π))) = ∅ . This yields the exact translation [R \ Y] (X(R * (Π))) = ∅ ∧ Ψ X R|N 1 R * (Π) (1) which, once expanded, yields [R \ Y] (X(R * (Π))) = ∅ ∧ X(R * (Π)) ⊆ R -1 (T(A)). This is equivalent to [R \ Y] (X(R * (Π))) = ∅ ∧ X(R * (Π)) ⊆ Y -1 (T(A))
, which is the expected exact translation.

Conclusions & Perspectives

In the term rewriting framework, to perform reachability analysis guided by properties of interest, the present paper addresses the question of a systematic translation of linear temporal logic properties into rewrite propositions. More precisely, we have investigated suitable semantics for LTL on maximal rewriting words and their influence on the feasibility of a translation, and proposed a framework providing exact translations on a fragment of LTL corresponding mainly to safety formulae, and approximations on a larger fragment.

As a future work, we intend to expand the fragment for which translations and approximations can be provided, and study the feasibility of handling equational theories in the same framework. The present work being a part of a rewrite approximation based analysis, the end goal is the integration of the paper's proposals into the verification chain dedicated to the automatic analysis of security-/safety-critical applications.

Appendix: Proofs

Lemma 1 [p5] Proof. (1) (w, i) | = ∞ m=0 • m ϕ ⇐⇒ ∞ m=0 (w, i) | = • m ϕ ⇐⇒ ∞ m=0 i + m dom w ∨ (w, i + m) | = ϕ ⇐⇒ ∞ m=i m dom w ∨ (w, m) | = ϕ ⇐⇒ #w m=i (⊥ ∨ (w, m) | = ϕ) ∧ ∞ m=1+#w (⊤ ∨ (w, m) | = ϕ) ⇐⇒ #w m=i (w, m) | = ϕ ⇐⇒ #w j=i (w, j) | = ϕ ⇐⇒ ∀j ∈ dom w, j i ⇒ (w, j) | = ϕ ⇐⇒ (w, i) | = ϕ (2) (w, i) | = ∞ m=0 • m ϕ ⇐⇒ (w, i) | = k-1 m=0 • m ϕ ∧ ∞ m=k • m ϕ ⇐⇒ (w, i) | = k-1 m=0 • m ϕ A ∧(w, i) | = ∞ m=k • m ϕ ⇐⇒ (w, i) | = A ∧ ∞ m=k (w, i) | = • m ϕ ⇐⇒ (w, i) | = A ∧ ∞ m=k i + m dom w ∨ (w, i + m) | = ϕ ⇐⇒ (w, i) | = A ∧ ∞ m=0 i + k + m dom w ∨ (w, i + k + m) | = ϕ ⇐⇒ (w, i) | = A ∧ ∞ m=0 (w, i + k) | = • m ϕ ⇐⇒ (w, i) | = A ∧ (w, i + k) | = ∞ m=0 • m ϕ ⇐⇒ (w, i) | = A ∧ (w, i + k) | = ϕ ⇐⇒ (w, i) | = A ∧ i + k dom w ∨ (w, i + k) | = ϕ ⇐⇒ (w, i) | = A ∧ (w, i) | = • k ϕ ⇐⇒ (w, i) | = A ∧ • k ϕ ⇐⇒ (w, i) | = k-1 m=0 • m ϕ ∧ • k ϕ Lemma 2 [p9]
Proof. Assume that i ∈ dom w; the proof is done by induction on ϕ ∈ R-LTL. Base Cases. Weak and strong semantics are identical by definition except for ϕ = X. In that case (w, i)

| = s X ⇐⇒ w(i) ∈ X ⇐⇒ (w, i) | = w X, because i ∈ dom w. Inductive Cases. Let ∈ { ∧, ∨ }. We have (w, i) | = s (ϕ ψ) ⇐⇒ (w, i) | = s ϕ (w, i) | = s ψ ⇐⇒ (w, i) | = w ϕ (w, i) | = w ψ ⇐⇒ (w, i) | = w (ϕ ψ) ,
(w, i) | = s ψ ⇐⇒ ∀j ∈ dom w, j i ⇒ (w, j) | = w ψ .
Since j ∈ dom w, by the previous lemma we have (w, j) | = s ψ ⇔ (w, j) | = w ψ and can effect this replacement in the formula:

(w, i) | = s ψ ⇐⇒ ∀j ∈ dom w, j i ⇒ (w, j) | = s ψ .
There remains to recall our hypothesis H, : ∀j, (w, j) | = s ψ ⇐⇒ (w, j) | = ψ:

(w, i) | = s ψ ⇐⇒ ∀j ∈ dom w, j i ⇒ (w, j) | = ψ ⇐⇒ (w, i) | = ψ ,
which concludes the proof for case [START_REF]Term Rewriting and Applications[END_REF]. Now we deal with (2) ϕ = • m ψ, using the same arguments.

(w, i) | = s • m ϕ ⇐⇒ i + m dom w ∨ (w, i + m) | = w ϕ ⇐⇒ i + m ∈ dom w =⇒ (w, i + m) | = w ϕ ⇐⇒ i + m ∈ dom w =⇒ (w, i + m) | = s ϕ ⇐⇒ i + m ∈ dom w =⇒ (w, i + m) | = ϕ ⇐⇒ (w, i) | = • m ϕ . Remark 4 [p10]
Proof. The associativity and commutativity of stem directly from those of ∪ and ∩. The neutrality of ε = R | N stems from that of N (= ∇ε) for ∩ within ℘(N), of R (= ε[k] , ∀k) for ∩ within ℘(R), and of ∅ (its domain) for ∪.

Lemma 7 [p12] Proof. (1) For all n ∈ N, ∇ρ n = n i=0 ∇σ i , thus it is clear that ∇ρ n = n i=0 ∇σ i ⊇ n+1 i=0 ∇σ i = ∇ρ n+1 or, in other words, (∇ρ n ) n∈N is a (trivial) contracting sequence of finite sets. Therefore it converges towards ∞ i=0 ∇σ i . (2) Let k ∈ N 1 ; we have ρ n [k] = n i=0 σ i [k] = n i=0 σ i [k] ,
and thus

ρ n [k] = n i=0 σ i [k] ⊇ n+1 i=0 σ i [k] = ρ n+1 [k] and again, (ρ n [k]
) n∈N is a trivial contracting sequence of finite sets; therefore it converges towards a limit which we denote by ρ ∞

[k] = ∞ i=0 σ i [k]. (3
) Suppose now that σ i = σ ⊲ i (resp. σ i = σ ◮ i, the computation will be unchanged), we have

ρ ∞ [k] = ∞ i=0 σ i [k] = ∞ i=0 (σ ⊲ i)[k] = k-1 i=0 (σ ⊲ i)[k] ∩ ∞ i=k (σ ⊲ i)[k] = k-1 i=0 σ[k -i] ∩ ∞ i=k R = k-1 i=0 σ[k -i] = k i=1 σ[i] .
Given that for all i > #σ,

σ[i] = σ[ω], it follows that for all k > #σ, ρ ∞ [k] = #σ+1 i=1 σ[i]. Thus (ρ ∞ [k]) k∈N 1 converges. This shows that the infinite product ∞ n=0 σ n is convergent. Lemma 5 [p11] Proof. R Π ε = w ∈ R Π #w ∈ ∇ε ∧ ∀k ∈ dom w, w(k) ∈ ε[k] = w ∈ R Π #w ∈ N ∧ ∀k ∈ dom w, w(k) ∈ R = w ∈ R Π ⊤ ∧ ⊤ = w ∈ R Π ⊤ = w ∈ R Π w | = ⊤ = w ∈ R Π = R Π . Lemma 6 [p11] Proof. (1) Let ρ = σ σ ′ . R Π ρ = w ∈ R Π #w ∈ ∇ρ ∧ ∀k ∈ dom w, w(k) ∈ ρ[k] .
Let us rewrite this condition using the definition of ρ:

#w ∈ ∇ρ ∧ ∀k ∈ dom w, w(k) ∈ ρ[k] ⇐⇒ #w ∈ ∇σ ∩ ∇σ ′ ∧ ∀k ∈ dom w, w(k) ∈ σ[k] ∩ σ ′ [k] ⇐⇒ #w ∈ ∇σ ∧ ∀k ∈ dom w, w(k) ∈ σ[k] ∧ #w ∈ ∇σ ′ ∧ ∀k ∈ dom w, w(k) ∈ σ ′ [k] ⇐⇒ w ∈ R Π σ ∧ w ∈ R Π σ ′ ⇐⇒ w ∈ R Π σ ∩ R Π σ ′ , therefore R Π ρ = w ∈ R Π w ∈ R Π σ ∩ R Π σ ′ = R Π ∩ R Π σ ∩ R Π σ ′ = R Π σ ∩ R Π σ ′ . (2) Let ρ ∞ = ∞ n=0 σ n . We have R Π ρ ∞ = w ∈ R Π #w ∈ ∇σ ∞ ∧ ∀k ∈ dom w, w(k) ∈ ρ ∞ [k] = w ∈ R Π #w ∈ ∞ n=0 ∇σ n ∧ ∀k ∈ dom w, w(k) ∈ ρ ∞ [k] = w ∈ R Π #w ∈ ∞ n=0 ∇σ n ∧ ∀k ∈ dom w, w(k) ∈ ∞ n=0 σ n [k] = w ∈ R Π ∞ n=0 #w ∈ ∇σ n ∧ ∀k ∈ dom w, ∞ n=0 w(k) ∈ σ n [k] = w ∈ R Π ∞ n=0 #w ∈ ∇σ n ∧ ∀k ∈ dom w, w(k) ∈ σ n [k] = w ∈ R Π ∞ n=0 w ∈ R Π σ n = w ∈ R Π w ∈ ∞ n=0 R Π σ n = ∞ n=0 R Π σ n . Lemma 13 [p14] Proof. (1 : ⊆) Let x ∈ R Π m σ σ ⊳ m . There exists u m ∈ Π m σ such that u m x(1) --→ u m+1 x(2) --→ u m+2 x(3) --→ • • •, and u m+#x R -1 (T(A)). By definition of Π m σ , there exist u 0 , . . . , u m-1 ∈ T(A) such that u 0 ∈ Π 0 σ = Π, . . . , u m-1 ∈ Π m-1 σ and ρ 1 , . . . , ρ m ∈ R such that ρ 1 ∈ σ[1] , . . . , ρ m ∈ σ[m] and u 0 ρ 1 -→ u 1 ρ 2 -→ • • • ρ m --→ u m . Let us consider the word w = ρ 1 . . . ρ m x; its length is #w = #x + m and #x ∈ ∇(σ ⊳ m) = ∇σ -m, thus #w ∈ (∇σ -m) + m = ∇σ \ 0, m -1 . Furthermore, for all k ∈ 1, m , we have by construction w(k) = ρ k ∈ σ[k], and for all k ∈ m + 1, #w , w(k) = x(k -m). By definition of x ∈ R Π m σ σ ⊳ m , for all i ∈ dom x, x(i) ∈ (σ ⊳ m)[i] = σ[i + m], thus for all k ∈ m + 1, #w , w(k) = x(k -m) ∈ σ[k -m + m] = σ[k -m + m] = σ[k].
∈ dom x, x(k) = w m+1 (k) = w(k + m) ∈ σ[k + m] = (σ ⊳ m)[k].
As above, we have #w ∈ ∇σ \ 0, m -1 , and since #x = #wm, it follows that #x ∈ (∇σ \ 0, m -1 )m = (∇σm)

∩ N = ∇(σ ⊳ m). Thus x ∈ R Π m σ σ ⊳ m . Lemma 11 [p14]
Proof. Let us start by noting that the statements (#w n) and (#w n ⇒ #w > n) are equivalent, and keeping in mind that if w ∈ R Π σ is of length n, we have u 0 w(1)

---→ u 1 w(2) ---→ • • • w(n) ---→ u n , with u 0 ∈ Π 0 σ = Π and u n ∈ Π n σ . This said, Ψ σ Π (n) holds by definition if and only if Π n σ ⊆ σ[n + 1] -1 (T(A))
, which is the formal way of saying "any term in Π n σ can be rewritten by a rule in σ[n + 1]". It is equivalent to saying that for any w ∈ R Π σ , if n ∈ dom w, then n + 1 ∈ dom w, because only the maximal rewrite words are in R Π σ . In other words, ∀w ∈ R Π σ , #w n ⇒ #w n + 1, or even more simply, ∀w ∈ R Π σ , #w n.

Corollary 12 [p14]

Proof. By Lemma 11 [p14] , we have immediately

n∈S∩∇σ Ψ σ Π (n) ⇐⇒ ∀w ∈ R Π σ , #w S ∩ ∇σ ⇐⇒ ∀w ∈ R Π σ , #w S ∨ #w ∇σ ⇐⇒ ∀w ∈ R Π σ , #w S ∨ ⊥ ⇐⇒ ∀w ∈ R Π σ , #w S . Remark 14 [p14]
Proof. It is immediate from the definition that we have i∈I R Π i = R i∈I Π i . Likewise, we have by definition R Π σ = w ∈ R Π P(w, σ) , where P(w, σ) is some predicate depending only on on w and σ, the details of which are irrelevant for this proof. We have i∈I

R Π i σ = i∈I w ∈ R Π i P(w, σ) = w ∈ n∈I R Π i P(w, σ) = w ∈ R n∈I Π i P(w, σ) = R n∈I Π i σ . Lemma 15 [p15]
Proof. Using Lemma 13 [p14] .

w 1+n n ∈ N, w ∈ R Π σ , #w n = ∞ n=0 w 1+n w ∈ R Π σ , #w n = ∞ n=0 R Π n σ σ ⊳ n = ∞ n=0 R Π n σ σ = R ∞ n=0 Π n σ σ = R ∞ n=0 σ[ω] n (Π) σ = R σ[ω] * (Π) σ . Theorem 8 [p13]
Proof. By induction on the structure of ϕ. Case σ = ξ(⊤):

R Π ξ(⊤) = R Π ε = R Π = w ∈ R Π w | = ⊤ . Case σ = ξ(⊥): R Π ξ(⊥) = R Π ∅ | ∅ = w ∈ R Π #w ∈ ∇σ ∧ ∀k ∈ dom w, w(k) ∈ σ[k] = w ∈ R Π #w ∈ ∅ ∧ ∀k ∈ dom w, w(k) ∈ ∅ = w ∈ R Π ⊥ ∧ ⊥ = w ∈ R Π ⊥ = w ∈ R Π w | = ⊥ Case σ = ξ(X): R Π ξ(X) = R Π X R | N 1 = w ∈ R Π #w ∈ ∇σ ∧ ∀k ∈ dom w, w(k) ∈ σ[k] = w ∈ R Π #w 1 ∧ w(1) ∈ X ∧ ∀k ∈ dom w, k > 1 ⇒ w(k) ∈ σ[k] = w ∈ R Π 1 ∈ dom w ∧ w(1) ∈ X ∧ ∀k ∈ dom w, k > 1 ⇒ w(k) ∈ R = w ∈ R Π 1 ∈ dom w ∧ w(1) ∈ X = w ∈ R Π (w, 1) | = X = w ∈ R Π w | = X Case σ = ξ(¬X): R Π ξ(¬X) = R Π R \ X R | N = w ∈ R Π #w ∈ ∇σ ∧ ∀k ∈ dom w, w(k) ∈ σ[k] = w ∈ R Π #w ∈ N ∧ ∀k ∈ dom w, w(k) ∈ σ[k] = w ∈ R Π ⊤ ∧ ∀k ∈ dom w, w(k) ∈ σ[k] = w ∈ R Π ∀k ∈ dom w, w(k) ∈ σ[k] = w ∈ R Π 1 ∈ dom w ⇒ w(1) ∈ R \ X ∧ ∀k ∈ dom w, k > 1 ⇒ w(k) ∈ σ[k] = w ∈ R Π 1 ∈ dom w ⇒ w(1) ∈ R \ X ∧ ∀k ∈ dom w, k > 1 ⇒ w(k) ∈ R = w ∈ R Π 1 ∈ dom w ⇒ w(1) ∈ R \ X = w ∈ R Π 1 dom w ∨ w(1) ∈ R \ X = w ∈ R Π 1 dom w ∨ w(1) X = w ∈ R Π w | = ¬X Case σ = ξ(X ∧ Y):
In the first steps, we successively use the definition of the signature, the signature-product lemma, and the induction hypothesis.

R Π ξ(ϕ ∧ ψ) = R Π ξ(ϕ) ξ(ψ) = R Π ξ(ϕ) ∩ R Π ξ(ψ) = w ∈ R Π w | = ϕ ∩ w ∈ R Π w | = ψ = w ∈ R Π w | = ψ ∧ w | = ϕ = w ∈ R Π w | = ψ ∧ ϕ Case ξ(• m ϕ) = ξ(ϕ) ◮ m: For simplicity of notation, let σ ⊳ = ξ(ϕ) and σ m = ξ(ϕ) ◮ m. By induction hypothesis we have R Π ξ(ϕ) = w ∈ R Π w | = ϕ . Let us note before beginning that #w ∈ ∇σ m implies that #w > m. We have: R Π ξ(• m ϕ) = R Π ξ(ϕ) ◮ m = R Π σ ◮ m = R Π σ m = w ∈ R Π #w ∈ ∇σ m ∧ ∀k ∈ dom w, w(k) ∈ σ m [k] = w ∈ R Π #w ∈ ∇σ m ∧ ∀1 k #w, w(k) ∈ σ m [k] = w ∈ R Π #w ∈ ∇σ m ∧ ∀1 k m, w(k) ∈ σ m [k] ∀m + 1 k #w, w(k) ∈ σ m [k] = w ∈ R Π #w ∈ ∇σ m ∧ ∀1 k m, w(k) ∈ R ∀m + 1 k #w, w(k) ∈ σ m [k] = w ∈ R Π #w ∈ ∇σ m ∧ ∀m + 1 k #w, w(k) ∈ σ m [k] = w ∈ R Π #w ∈ ∇σ m ∧ ∀m + 1 k #w, w(k) ∈ σ[k -m] = w ∈ R Π #w ∈ ∇σ m ∧ ∀1 k -m #w -m, w(k -m + m) ∈ σ[k -m] = w ∈ R Π #w ∈ ∇σ m ∧ ∀1 k #w -m, w(k + m) ∈ σ[k] = w ∈ R Π #w ∈ ∇σ m ∧ ∀1 k #w m+1 , w m+1 (k) ∈ σ[k] = w ∈ R Π #w ∈ ∇σ m ∧ ∀k ∈ dom w m+1 , w m+1 (k) ∈ σ[k] = w ∈ R Π #w ∈ (∇σ \ {0}) + m ∧ ∀k ∈ dom w m+1 , w m+1 (k) ∈ σ[k] = w ∈ R Π #w m+1 + m ∈ (∇σ \ {0}) + m ∧ ∀k ∈ dom w m+1 , w m+1 (k) ∈ σ[k] = w ∈ R Π #w m+1 ∈ (∇σ \ {0}) ∧ ∀k ∈ dom w m+1 , w m+1 (k) ∈ σ[k] = w ∈ R Π #w m+1 0 ∧ #w m+1 ∈ ∇σ ∧ ∀k ∈ dom w m+1 , w m+1 (k) ∈ σ[k] = w ∈ R Π m + 1 ∈ dom w ∧ #w m+1 ∈ ∇σ ∧ ∀k ∈ dom w m+1 , w m+1 (k) ∈ σ[k] = w ∈ R Π m + 1 ∈ dom w ∧ w m+1 ∈ R Π σ = w ∈ R Π m + 1 ∈ dom w ∧ w m+1 ∈ R Π ξ(ϕ) = w ∈ R Π m + 1 ∈ dom w ∧ w m+1 ∈ w ∈ R Π w | = ϕ = w ∈ R Π m + 1 ∈ dom w ∧ w m+1 | = ϕ = w ∈ R Π m + 1 ∈ dom w ∧ (w, m + 1) | = ϕ = w ∈ R Π (w, 1) | = • m ϕ = w ∈ R Π w | = • m ϕ . Case ξ(• m ϕ) = ξ(ϕ) ⊲ m: For simplicity of notation, let σ ⊳ = ξ(ϕ) and σ m = ξ(ϕ) ⊲ m. By induction hypothesis we have R Π ξ(ϕ) = w ∈ R Π w | = ϕ .
Note that we will reuse steps from the strong case, as the two proofs are very similar. Indeed they only differ where ∇σ m is concerned. We have:

R Π ξ(• m ϕ) = R Π ξ(ϕ) ⊲ m = R Π σ ⊲ m = R Π σ m = w ∈ R Π #w ∈ ∇σ m ∧ ∀k ∈ dom w, w(k) ∈ σ m [k] = w ∈ R Π #w ∈ ∇σ m ∧ ∀k ∈ dom w m+1 , w m+1 (k) ∈ σ[k] = w ∈ R Π #w ∈ 0, m ∪ (∇σ + m) ∧ ∀k ∈ dom w m+1 , w m+1 (k) ∈ σ[k] = w ∈ R Π (#w < m + 1 ∨ #w ∈ ∇σ + m) ∧ ∀k ∈ dom w m+1 , w m+1 (k) ∈ σ[k] = w ∈ R Π (#w < m + 1 ∨ #w m+1 + m ∈ ∇σ + m) ∧ ∀k ∈ dom w m+1 , w m+1 (k) ∈ σ[k] = w ∈ R Π (#w < m + 1 ∨ #w m+1 ∈ ∇σ) ∧ ∀k ∈ dom w m+1 , w m+1 (k) ∈ σ[k] = w ∈ R Π (#w < m + 1 ∧ ∀k ∈ dom w m+1 , w m+1 (k) ∈ σ[k]) ∨(#w m+1 ∈ ∇σ ∧ ∀k ∈ dom w m+1 , w m+1 (k) ∈ σ[k]) = w ∈ R Π (#w < m + 1 ∧ ∀k ∈ ∅, w m+1 (k) ∈ σ[k]) ∨(#w m+1 ∈ ∇σ ∧ ∀k ∈ dom w m+1 , w m+1 (k) ∈ σ[k]) = w ∈ R Π #w < m + 1 ∨(#w m+1 ∈ ∇σ ∧ ∀k ∈ dom w m+1 , w m+1 (k) ∈ σ[k]) = w ∈ R Π #w < m + 1 ∨ (w, m + 1) | = ϕ = w ∈ R Π m + 1 dom w ∨ (w, m + 1) | = ϕ = w ∈ R Π w | = • m ϕ . Case ξ( ϕ) = ∞ m=0 ξ(ϕ) ⊲ m .
Let us start by noting that, by application of the product-breaking lemma, we have

R Π ξ( ϕ) = R Π ∞ m=0 ξ(ϕ) ⊲ m = ∞ m=0 R Π ξ(ϕ) ⊲ m . Let w ∈ R Π ; we have w ∈ R Π ξ( ϕ) ⇐⇒ w ∈ ∞ m=0 R Π ξ(ϕ) ⊲ m ⇐⇒ ∞ m=0 w ∈ R Π ξ(ϕ) ⊲ m ⇐⇒ ∞ m=0 w ∈ R Π ξ(• m ϕ) ⇐⇒ ∞ m=0 w | = • m ϕ ⇐⇒ w | = ∞ m=0 • m ϕ ⇐⇒ w | = ϕ , the last step being by lemma 1 [p5] . So we have finally R Π ξ( ϕ) = w ∈ R Π w | = ϕ . Proposition 16 [p15]
Proof. By induction on ϕ.

Theorem 9 [p14]

Proof. Recall that the no-constraints lemma states that R Π ε = R Π . Keeping the Strong Semantics Lemma in mind as well, we have immediately

Π ε s ϕ ⇐⇒ ∀w ∈ R Π ε , w | = s ϕ ⇐⇒ ∀w ∈ R Π , w | = s ϕ ⇐⇒ ∀w ∈ R Π , w | = ϕ ⇐⇒ R, Π | = ϕ . Remark 10 [p14] Proof. Π σ µ ϕ ⇐⇒ ∀w ∈ R Π σ , w | = µ ϕ ⇐⇒ (λ ∈ R Π ⋆σ ⇒ λ | = µ ϕ) ∧ ∀w ∈ R Π ⋆σ , w | = µ ϕ ⇐⇒ (λ ∈ R Π ⋆σ ⇒ ⊤) ∧ ∀w ∈ R Π ⋆σ , w | = µ ϕ ⇐⇒ ⊤ ∧ ∀w ∈ R Π ⋆σ , w | = µ ϕ ⇐⇒ Π ⋆σ µ ϕ .

Proofs of translation rules.

Proof of rules (⊤) [p15] and (⊥). For all Π, σ, µ:

Π σ µ ⊤ ⇐⇒ ∀w ∈ R Π σ , w | = µ ⊤ ⇐⇒ ⊤ Π σ µ ⊥ ⇐⇒ ∀w ∈ R Π σ , w | = µ ⊥ ⇐⇒ ⊥ Proof of rule (∧ X ) [p15]
. Let us first assume that w is not the empty word, that is to say, 1 ∈ dom w; then w | = s X ⇐⇒ w | = w X ⇐⇒ w(1) ∈ X and we have, for all Π, σ, µ:

Π σ µ X ∧ Y ⇐⇒ ∀w ∈ R Π σ , w | = µ X ∧ Y ⇐⇒ ∀w ∈ R Π σ , w | = µ X ∧ Y ⇐⇒ ∀w ∈ R Π σ , (w | = µ X) ∧ (w | = µ Y) ⇐⇒ ∀w ∈ R Π σ , (w(1) ∈ X) ∧ (w(1) ∈ Y) ⇐⇒ ∀w ∈ R Π σ , w(1) ∈ X ∩ Y ⇐⇒ ∀w ∈ R Π σ , w | = µ X ∩ Y ⇐⇒ Π σ µ X ∩ Y
Now, if w is the empty word, we have

Π σ s X ∧ Y ⇐⇒ ∀w ∈ R Π σ , w | = s X ∧ Y ⇐⇒ ∀w ∈ R Π σ , w | = s X ∧ Y ⇐⇒ ∀w ∈ R Π σ , (w | = s X) ∧ (w | = s Y) ⇐⇒ ∀w ∈ R Π σ , ⊥ ∧ ⊥ ⇐⇒ ∀w ∈ R Π σ , ⊥ ⇐⇒ ∀w ∈ R Π σ , w | = s X ∩ Y ⇐⇒ Π σ s X ∩ Y Π σ w X ∧ Y ⇐⇒ ∀w ∈ R Π σ , w | = w X ∧ Y ⇐⇒ ∀w ∈ R Π σ , w | = w X ∧ Y ⇐⇒ ∀w ∈ R Π σ , (w | = w X) ∧ (w | = w Y) ⇐⇒ ∀w ∈ R Π σ , ⊤ ∧ ⊤ ⇐⇒ ∀w ∈ R Π σ , ⊤ ⇐⇒ ∀w ∈ R Π σ , w | = w X ∩ Y ⇐⇒ Π σ w X ∩ Y
The proof of (∨ X ) [p15] is the same, with the substitution ∨/∧, ∪/∩.

Proof of rule (∧)

[p15] . Π σ µ ϕ ∧ ψ ⇐⇒ ∀w ∈ R Π σ , w | = µ ϕ ∧ ψ ⇐⇒ ∀w ∈ R Π σ , w | = µ ϕ ∧ w | = µ ψ ⇐⇒ ∀w ∈ R Π σ , w | = µ ϕ ∧ ∀w ∈ R Π σ , w | = µ ψ ⇐⇒ Π σ µ ϕ ∧ Π σ µ ψ Proof of rule (∨ ↑ ) [p15] . Π σ µ ϕ ∨ Π σ µ ψ =⇒ ∀w ∈ R Π σ , w | = µ ϕ ∨ ∀w ∈ R Π σ , w | = µ ψ =⇒ ∀w ∈ R Π σ , w | = µ ϕ ∨ ψ ∨ ∀w ∈ R Π σ , w | = µ ϕ ∨ ψ =⇒ ∀w ∈ R Π σ , w | = µ ϕ ∨ ψ =⇒ Π σ µ ϕ ∨ ψ Proof of rule (∨ ¬ ⇒ ) [p15]
. Obvious by ϕ ∨ ψ ⇐⇒ ¬ϕ ⇒ ψ. The only snag is that ¬ϕ is not necessarily an A-LTL formula and thus its signature may not exist. In that case the rule cannot be invoked.

Proof of rule (∨

⇒ ∧ ) [p15] . Π σ µ [ϕ ∨ ϕ ′ ] ⇒ ψ ⇐⇒ ∀w ∈ R Π σ , w | = µ [ϕ ∨ ϕ ′ ] ⇒ ψ ⇐⇒ ∀w ∈ R Π σ , w | = µ (ϕ ⇒ ψ) ∧ (ϕ ′ ⇒ ψ) ⇐⇒ ∀w ∈ R Π σ , (w | = µ ϕ ⇒ ψ) ∧ (w | = µ ϕ ′ ⇒ ψ) ⇐⇒ ∀w ∈ R Π σ , w | = µ ϕ ⇒ ψ ∧ ∀w ∈ R Π σ , w | = µ ϕ ′ ⇒ ψ ⇐⇒ Π σ µ ϕ ⇒ ψ ∧ Π σ µ ϕ ′ ⇒ ψ

  2 [p9] . Conjunction, Disjunction & Negation. Case 5: And & Or. It is pretty clear that if π 5 translates ϕ and π ′ 5 translates ψ, then π 5 ∧ π ′ 5 translates ϕ ∧ ψ. This holds thanks to the implicit universal quantifier, as we have

Fig. 2 :

 2 Fig. 2: R-LTL Weak & Strong Semantics

  converges towards X | N . ) Infinite Products. Remark 4 legitimates the use of a Sigma-notation m k=l σ k for σ l σ l+1 • • • σ m , with the usual properties. We define a notion of infinite product of signatures as well, in the classical way: the infinite product ∞ k=l σ k converges if and only if the associated sequence of partial products ( n k=l σ k ) n∈N l converges, and in that case The words of R, originating in Π and constrained by σ are defined by R Π σ ⊳ = w ∈ R Π #w ∈ ∇σ ∧ ∀k ∈ dom w, w(k) ∈ σ[k] . (e.g. Let σ = X, Y Z | N 2 ; then its core is the function ∂σ

  then we define the strong m-left shift of σ as σ ◭ m ⊳ = ∂σ(m + 1), . . . , ∂σ(#σ) ∂σ(ω) | (∇σm) \ {0} and the weak m-left shift of σ as σ ⊳ m ⊳ = ∂σ(m + 1), . . . , ∂σ(#σ) ∂σ(ω) | ∇σm . Conversely, the strong m-right shift of σ is σ ◮ m ⊳ = R 1 , . . . , R m , ∂σ(1), . . . , ∂σ(#σ) ∂σ(ω) | (∇σ \ {0}) + m , while the weak m-right shift of σ is σ ⊲ m

Fig. 3 :

 3 Fig. 3: Building Signatures on A-LTL

  the second step being of course by induction hypothesis. Cases ϕ = ψ ⇒ ψ ′ , ϕ = • m ψ, ϕ = • m ψ and ϕ = ψ: weak and strong semantics are identical by definition. Lemma 3 [p10] Proof. By induction on the structure of ϕ. Let us start by noting that | = s is defined in the exact same way as | = in all cases but (1) ϕ = ψ and (2) ϕ = • m ψ. This automatically takes care of all those cases, which include the base cases, strong next, material implication, conjunction and disjunction. Now there only remains to deal with the two remaining cases. Let us start by (1) ϕ = ψ. We have the induction hypothesis H ≡ ∀i ∈ N 1 , (w, i) | = s ψ ⇐⇒ (w, i) | = ψ. With this in mind, recall that by definition

  So we have that for all k ∈ dom w, w(k) ∈ σ[k]. Thus we have built a word w ∈ R Π ∂σ | ∇σ \ 0, m -1 such that w m+1 = x. There only remains to remark that w ∈ R Π ∂σ | ∇σ \ 0, m -1 ⇐⇒ w ∈ R Π σ ∧ #w m, and we can conclude this part. (2 : ⊇) Let x ∈ w m+1 w ∈ R Π σ ∧ #w m , and let w ∈ R Π σ such that x = w m+1 ; by the same type of immediate arguments as for (1), x ∈ R Π m σ . For all k ∈ dom w, w(k) ∈ σ[k], so for all k

1 k=0• 1 k=0 • k ϕ A∧⇐⇒ Π σ µ hσ- 1 k=0•

 11ϕ1 Proof of rule (⇒Σ ) [p15] . Π σ µ ϕ ⇒ ψ ⇐⇒ ∀w ∈ R Π σ , w | = µ ϕ ⇒ ψ ⇐⇒ ∀w ∈ R Π σ , (w | = s ϕ) ⇒ (w | = s ψ) ⇐⇒ ∀w ∈ R Π σ , (w | = ϕ) ⇒ (w | = s ψ) ⇐⇒ ∀w ∈ R Π σ , (w ∈ R Π ξ(ϕ) ) ⇒ (w | = s ψ) ⇐⇒ ∀w ∈ R Π σ ∩ R Π ξ(ϕ) , w | = s ψ ⇐⇒ ∀w ∈ R Π σ ξ(ϕ) , w | = s ψ ⇐⇒ Π σ ξ(ϕ) s ψ Proof of rule (• m ) [p15] . We use Lemma 13 [p14] . Π σ µ • m ϕ ⇐⇒ ∀w ∈ R Π σ , w | = µ • m ϕ ⇐⇒ ∀w ∈ R Π σ , 1 + m dom w ∨ (w, 1 + m) | = w ϕ ⇐⇒ ∀w ∈ R Π σ , #w 1 + m =⇒ w 1+m | = w ϕ ⇐⇒ ∀x ∈ R Π m σ σ ⊳ m , #x + m 1 + m =⇒ x | = w ϕ ⇐⇒ ∀x ∈ R Π m σ σ ⊳ m , #x 1 =⇒ x | = w ϕ ⇐⇒ ∀x ∈ R Π m σ σ ◭ m , x | = w ϕ ⇐⇒ Π m σ σ ◭ m w ϕ . Proof of rule (• m ) [p15] . We use Corollary 12 [p14] , as well as Lemma 2 [p9] . Π σ µ • m ϕ ⇐⇒ ∀w ∈ R Π σ , w | = µ • m ϕ ⇐⇒ ∀w ∈ R Π σ , 1 + m ∈ dom w ∧ (w, 1 + m) | = s ϕ ⇐⇒ ∀w ∈ R Π σ , #w > m ∧ (w, 1 + m) | = s ϕ ⇐⇒ ∀w ∈ R Π σ , #w > m ∧ (1 + m ∈ dom w ⇒ (w, 1 + m) | = s ϕ) ⇐⇒ ∀w ∈ R Π σ , #w > m ∀w ∈ R Π σ , (1 + m ∈ dom w ⇒ (w, 1 + m) | = s ϕ) ⇐⇒ n∈ 0,m ∩∇σ Ψ σ Π (n) ∀w ∈ R Π σ , (1 + m ∈ dom w ⇒ (w, 1 + m) | = w ϕ) ⇐⇒ n∈ 0,m ∩∇σ Ψ σ Π (n) ∀w ∈ R Π σ , w | = µ • m ϕ ⇐⇒ Π σ µ • m ϕ ∧ n∈ 0,m ∩∇σ Ψ σ Π (n) . Proof of rule ( * ) [p15] .. Assume that σ is stable. Π σ µ ϕ ⇐⇒ ∀w ∈ R Π σ , w | = µ ϕ ⇐⇒ ∀w ∈ R Π σ , ∀i ∈ dom w, (w, i) | = w ϕ ⇐⇒ ∀w ∈ R Π σ , ∀i ∈ dom w, w i | = w ϕ ⇐⇒ ∀w ∈ R Π σ , ∀i ∈ N 1 , i ∈ dom w ⇒ w i | = w ϕ ⇐⇒ ∀w ∈ R Π σ , ∀i ∈ N 1 , #w i ⇒ w i | = w ϕ ⇐⇒ ∀x ∈ w i i ∈ N 1 , w ∈ R Π σ , #w i , x | = w ϕ ⇐⇒ ∀x ∈ w n+1 n ∈ N, w ∈ R Π σ , #w n + 1 , x | = w ϕ ⇐⇒ ∀x ∈ w n+1 n ∈ N, w ∈ R Π σ , #w n \ {λ} , x | = w ϕ ⇐⇒ ∀x ∈ R σ[ω] * (Π) σ \ {λ} , x | = w ϕ ⇐⇒ ∀x ∈ R σ[ω] * (Π) ⋆σ , x | = w ϕ ⇐⇒ σ[ω] * (Π) ⋆σ w ϕ . Proof of rule ( h ) [p15] . Using Lemma 1 [p5]andRemark 10 [p14] . Assume that σ is unstable but can be stabilised, with hσ ∈ N 1 .Π σ µ ϕ ⇐⇒ Π σ µ hσk ϕ ∧ • hσ ϕ ⇐⇒ Π σ µ hσ-Π σ µ • hσ ϕ ⇐⇒ A ∧ Π hσ σ σ ◭ hσ µ ϕ ⇐⇒ A ∧ Π hσ σ ⋆(σ ⊳ hσ) µ ϕ k ϕ ∧ Π hσ σ σ ⊳ hσ µ ϕ .Proof of rule (¬X) [p15] . Π σ µ ¬X ⇐⇒ ∀w ∈ R Π σ , w | = µ ¬X ⇐⇒ ∀w ∈ R Π σ , 1 dom w ∨ w(1) X ⇐⇒ ∀w ∈ R Π σ , 1 dom w ∨ w(1) ∈ R \ X ⇐⇒ ∀w ∈ R Π σ , w | = w R \ X ⇐⇒ Π σ w R \ X .

⋆ This author is supported by the project ANR 2010 BLAN 0202 02 FREC. ⋆⋆ This author is supported by the French DGA (Direction Générale de l'Armement).