Stéphane Demri

Morgan Deters

Temporal Logics on Strings with Prefix Relation

We show that linear-time temporal logic over concrete domains made of finite strings and the prefix relation admits a PSpace-complete satisfiability problem. Actually, we extend a known result with the concrete domain made of the set of natural numbers and the greater than relation (corresponding to the singleton alphabet case) and we solve an open problem mentioned in several publications. Since the prefix relation is not a total ordering, it is not possible to take advantage of existing techniques dedicated to temporal logics with concrete domains that are essentially linearly ordered structures. Instead, we introduce an adequate encoding of string constraints into length constraints that allows us to reduce the problem on strings to the problem on natural numbers. To do so, we also propose an extended version of the logic on strings that is able to compare lengths of longest common prefixes and for which the satisfiability problem is shown in PSpace. Finally, we show how to lift the result for the branching-time case in order to get decidability when the underlying temporal logic is CTL .

Introduction

String theories in a temporal setting. Reasoning about strings is increasingly required in program verification or in analysis of web applications and recently much effort has been dedicated toward designing solvers that handle string theories (possibly in combination with other theories), see e.g. [GKA + 11,ZZG13,LRT + 14,AAC + 14, [START_REF] Hutagalung | Model checking for string problems[END_REF][START_REF] Liang | Automated reasoning over string constraints[END_REF]. This also includes works related to first-order theory of strings with order, see e.g. [START_REF] Kuske | Theories of orders on the set of words[END_REF]. The decidability status of expressive string theories is not always known, see e.g. [LRT + 14, Section 2.1] or [AAC + 14], but fortunately, decidability of word equations is known to be decidable thanks to Makanin's result [START_REF] Makanin | The problem of solvability of equations in a free semigroup (english translation)[END_REF] and a PSpace algorithm has been designed by Plandowski in [START_REF] Plandowski | Satisfiability of word equations with constants is in PSPACE[END_REF] (see also [START_REF] Diekert | Finding all solutions of equations in free groups and monoids with involution[END_REF]). By contrast, first-order theory on strings is undecidable by Quine's undecidability result [START_REF] Quine | Concatenation as a basis for arithmetic[END_REF].

At the same time, many works have been dedicated to reasoning about temporal logics on concrete domains, see e.g. [BC02,Lut04,BG06,BGL12,DHV14], so that temporal reasoning is done about the evolution of typed variables (for instance interpreted by integers or by strings to cite a few examples). Hence, fibring a temporal logic with a concrete domain happens to be a very natural approach, see e.g. [START_REF] Gabbay | Fibring Logics[END_REF], but this may easily lead to undecidability, see e.g. [DD07, Section 10]. Even when decidability is preserved, computational complexity can be high. For instance, while ALC-LTL satisfiability with rigid names is 2ExpTime-complete [START_REF] Baader | LTL over description logic axioms[END_REF], LTL over the concrete domain (N, ≤) is only PSpacecomplete [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF][START_REF] Demri | Verification of qualitative Z constraints[END_REF]. In this paper, we are interested in temporal logics when the concrete domain contains finite strings.

Our motivation. Linear-time temporal logics on concrete domains have been shown decidable mainly when the underlying concrete domain has the completion property, see e.g. [Dec92,BC02,LM05,DD07,Gas09] or when it is a linearly ordered structure [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF][START_REF] Segoufin | Automata based verification over linearly ordered data domains[END_REF]. 1 Branching-time extensions have also been considered in [ Čer94,BG06,Gas07,Gas09,CKL13] and a remarkable breakthrough has been made recently in [START_REF] Carapelle | Satisfiability of CTL * with constraints[END_REF] by showing that CTL over the domain (N, ≤) is decidable by using the decidability of Boolean combinations of formulae from MSO and from WMSO+U [START_REF] Bojańczyk | Weak MSO+U over infinite trees[END_REF] where U is the unbounding second-order quantifier (see also the follow-up work [START_REF] Carapelle | Satisfiability of ECTL * with constraints[END_REF] involving ECTL ). Unfortunately, none of the known techniques has been able to handle LTL over concrete domain of the form (Σ * , ) where is not a total ordering on Σ * such as the prefix relation p or the subword relation . This is surprising since the prefix relation p seems quite harmless whereas the subword relation is a well-quasi-ordering and therefore one could expect decidability by Higman's Lemma. Actually, the fact that the decidability status of the satisfiability problem for LTL over ({0, 1} * , p ) is open first appeared in [START_REF] Demri | Verification of qualitative Z-constraints[END_REF] and it has been reformulated for the branching-time version based on CTL in [START_REF] Carapelle | Satisfiability of CTL * with constraints[END_REF], see also [START_REF] Segoufin | Automata based verification over linearly ordered data domains[END_REF]. Even worse, in [CKL14, Section 9], it is stated that a new strategy is needed to solve the satisfiability problem for LTL over ({0, 1} * , p ). In this work, we aim to better understand how to solve the satisfiability problem for temporal logics over concrete domains that are of the form (Σ * , ) when is not necessarily linearly ordered. More specifically, we focus our attention on the prefix relation.

Our contribution. In this paper, we write LTL(Σ * , p ) to denote LTL over the concrete domain (Σ * , p ) (see a formal definition in Section 2). Our main result is that for every (finite or infinite and countable) non-empty alphabet Σ, the satisfiability problem for LTL(Σ * , p ) is PSpace-complete. It is worth noting that the decidability status of these logics was open until now for card(Σ) ≥ 2 (the case k = 1 naturally corresponds to LTL over the concrete domain (N, ≤), written LTL(N, ≤)). We adopt an original approach since prefix constraints are first generalized and then translated into numerical constraints so that we are able to design a satisfiability-preserving reduction into LTL(N, ≤), and then use the PSpace upper bound from [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF][START_REF] Demri | Verification of qualitative Z constraints[END_REF] (see also [START_REF] Segoufin | Automata based verification over linearly ordered data domains[END_REF]). The PSpace upper bound also holds for many extensions of LTL as soon as they behave as LTL for the translation of formulae into Büchi automata (see Section 4.1). Solving string constraints by formulae in Presburger arithmetic is not a new idea (see e.g. [START_REF] Plandowski | An efficient algorithm for solving word equations[END_REF]) but in the paper we provide a straightforward method to deal with temporal logics on finite strings with the prefix relation. Moreover, in the technical developments, we have considered a substantial extension of LTL(Σ * , p ), namely LTL(Σ * , clen), for which our technique can be applied naturally.

As by-products of our method, we are also able to establish a small alphabet property when Σ = N (see Corollary 1) and more importantly, the satisfiability problem for CTL (Σ * , clen), the branching-time extension of LTL(Σ * , clen) based on CTL , is decidable by taking advantage of the decidability of CTL (N, ≤) recently shown in [START_REF] Carapelle | Satisfiability of CTL * with constraints[END_REF]. As for the linear-time case, we provide a reduction from CTL (Σ * , clen) to CTL (N, ≤) by encoding length constraints about longest common prefixes into counters. It is worth noting that the decidability results in [START_REF] Carapelle | Satisfiability of CTL * with constraints[END_REF] are based on the decidability of Boolean combinations of formulae from MSO and from WMSO+U [START_REF] Bojańczyk | Weak MSO+U over infinite trees[END_REF] where U is the unbounding second-order quantifier, see e.g. [START_REF] Bojańczyk | A bounding quantifier[END_REF][START_REF] Bojańczyk | Bounds in w-Regularity[END_REF] (note that full MSO+U has been shown recently undecidable in [START_REF] Bojańczyk | The MSO+U theory of (N, <) is undecidable[END_REF]). Nevertheless, to get advantage of this result on monadic second-order logics, a property for (Z, ≤) needs to be established, see e.g. [START_REF] Carapelle | Satisfiability of CTL * with constraints[END_REF]Lemma 15] or an earlier analogous formulation in [DD07, Lemma 6.1] or in [START_REF] Čerans | Deciding properties of integral relational automata[END_REF]Lemma 5.5] and therefore, our result for CTL (Σ * , clen) requires the decidability results from [START_REF] Bojańczyk | Weak MSO+U over infinite trees[END_REF][START_REF] Carapelle | Satisfiability of CTL * with constraints[END_REF]. We wonder whether the (complexity/decidability) results established in the present paper can be simply explained by an approach using the definability of existence of homomorphisms in a monadic second-order logic, as done in [START_REF] Carapelle | Satisfiability of CTL * with constraints[END_REF][START_REF] Carapelle | Satisfiability of ECTL * with constraints[END_REF] (this would require to provide a variant to this approach). Our translations have some flavor of the notion of interpretability from [START_REF] Carapelle | Satisfiability of CTL * with constraints[END_REF], but this does not fit completely, as far as we can judge.

At the time of completing this paper, we have been aware of the work [START_REF] Kartzow | Model checking constraint LTL over trees[END_REF] that has been done independently and that answers similar questions by using techniques for constraint automata.

Preliminaries

LTL on finite strings with the prefix relation

Let SVAR = {x 1 , x 2 , . . .} be a countably infinite set of string variables. Given a non-empty alphabet Σ, we write LTL(Σ * , p ) to denote the corresponding version of LTL over the concrete domain (Σ * , p ) where p is the prefix relation. Given two words w, w in Σ * , we write w p w whenever w is a prefix of w , i.e., there is w ∈ Σ * such that w • w = w .

Terms in the logic LTL(Σ * , p ) are defined as follows:

t ::= w | x | X i x
where w ∈ Σ * , x ∈ SVAR and X i x is the sequence of i ≥ 1 occurrences of the symbol X followed by the string variable x. We write ε to indicate the empty string. The term X i x is interpreted as the value of x, ith position ahead of the current position.

Formulae in the logic LTL(Σ * , p ) are defined as follows:

φ ::= t p t | ¬φ | φ ∧ φ | Xφ | φ U φ
Hence, LTL(Σ * , p ) contains the usual temporal connectives from LTL. The symbol X is overloaded since it is used in terms of the form X • • • Xx and in formulae of the form Xφ. This will not cause any confusion but we keep the current usage, since in both cases, the presence of 'X' refers to future positions of bounded distance. Standard abbreviations related to Boolean or temporal connectives are also used in the rest of this paper (for ∨, ⇒, ⇔, F, G, etc.). Here is an example of a formula in LTL({0, 1} * , p ):

GF((001 p x) ∨ (x p 1001)) ∧ G(¬(x p Xx)).
A string valuation s is a map of the form s : SVAR → Σ * (or a restriction to a subset of SVAR), and a model for LTL(Σ * , p ) is an ω-sequence σ of string valuations. For every model σ and i ∈ N, the satisfaction relation |= is defined as follows (standard Boolean clauses are omitted):

σ, i |= t p t def ⇔ t i p t i where

w i def = w for all w ∈ Σ * x i def = σ(i)(x) for all x ∈ SVAR X j x i def = σ(i + j)(x)
for all x ∈ SVAR and j ≥ 1

-σ, i |= Xφ def ⇔ σ, i + 1 |= φ, -σ, i |= φ U ψ def
⇔ there exists j ≥ i such that σ, j |= ψ and for all i ≤ k < j, we have σ, k |= φ.

Note that the temporal operators have their usual semantics and for a given formula φ built over the finite set of string variables {x 1 , . . . , x q }, we can restrict ourselves to {x 1 , . . . , x q } to evaluate the formula on a model. Similarly, in the sequel, we use the abbreviation t = t instead of (t p t ) ∧ (t p t) and the abbreviation t ≺ p t instead of ¬(t = t ) ∧ t p t . Unsurprisingly, we have that σ, i |= t = t iff t i = t i .

An important feature of the semantics for LTL(Σ * , p ) is the ability to state properties for strings at the current state but also for strings at future positions, which may propagate constraints all over the model with the help of the temporal operator G.

As usual, an instance of the satisfiability problem for LTL(Σ * , p ) consists in checking whether a formula φ in LTL(Σ * , p ) admits a model σ such that σ, 0 |= φ. The validity problem is defined dually, as usual. By way of example, the formula below is valid in LTL({0, 1} * , p ):

G(x p 1001 ⇔ (x = ε ∨ x = 1 ∨ x = 10 ∨ x = 100 ∨ x = 1001)).
We write LTL(N, ≤) to denote LTL(Σ * , p ) when Σ is a singleton alphabet. Terms in the logic LTL(N, ≤) have one of the forms below: n ∈ N, x or X i x with i ≥ 1 and x ∈ SVAR. For example, GF(Xx < x) is satisfiable in LTL(N, ≤) whereas FG(Xx < x) is not satisfiable. By contrast, both GFp and FGp are satisfiable in standard LTL.

Unlike (R, ≤), the concrete domain (N, ≤) does not satisfy the completion property from [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF] (see also similar properties in [Dec92,BC02,LM05]), which does not help to decide LTL(N, ≤). Indeed, LTL augmented with a concrete domain satisfying the completion property can be decided with Büchi automata, since the sets of satisfiable symbolic models are ω-regular [DD07, Lemma 4.3]. However, the set of satisfiable symbolic models in LTL(N, ≤) is not ω-regular [DD07, Corollary 6.5] and therefore the automata-based approach to solve LTL(N, ≤) is certainly not a routine exercise. Still, it is possible to decide LTL(N, ≤) with the help of Büchi automata, see details in [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF] even though the proper extension of MSO that can express satisfiable symbolic models is presented in [START_REF] Carapelle | Satisfiability of CTL * with constraints[END_REF].

Proposition 1. [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF][START_REF] Demri | Verification of qualitative Z constraints[END_REF] The satisfiability problem for LTL(N, ≤) is PSpace-complete.

The way we define LTL(N, ≤) from LTL(Σ * , p ) implies a unary encoding of natural numbers in the formulae but the PSpace upper bound also holds with a binary encoding, as considered in [START_REF] Demri | Verification of qualitative Z constraints[END_REF].

So far, we have not assumed much about the alphabet Σ. When card(Σ) = k for some k ≥ 1, we can assume that Σ = [0, k -1]. In the sequel, we assume that card(Σ) ≥ 2 since the case k = 1 corresponds to the logic LTL(N, ≤). When Σ is a countably infinite alphabet, without any loss of generality, we can assume that N ⊆ Σ. However, it is sufficient to assume that Σ = N thanks to the simple property below.

Lemma 1. Let Σ be a countably infinite alphabet. There is a logarithmic-space reduction from the satisfiability problem for LTL(Σ * , p ) into the satisfiability problem for LTL(N * , p ).

Proof. Since Σ is countably infinite, there is a bijection f : Σ → N. Let φ be a formula in LTL(Σ * , p ) built over words in Σ * such that the letters a 1 , . . . , a k occur in φ. Let φ be the formula obtained from φ by replacing every occurrence of the letter a i by the natural number i. This provides a reduction that can be easily implemented in logarithmic space. It remains to show that φ is satisfiable in LTL(Σ * , p ) iff φ is satisfiable in LTL(N * , p ).

Let f be a bijection f : Σ → N. We write f(φ) to denote the formula obtained from φ by substituting every letter a by f(a). Similarly, we write f(σ) to denote the model in LTL(N * , p ) such that for all i, j ≥ 0, f(σ)(i)(x j ) is obtained from σ(i)(x j ) by substituting every letter a by f(a)

Given two bijections f : Σ → N and g : N → Σ, the following properties can be easily shown:

1. for all LTL(Σ * , p ) models σ, we have σ,

0 |= φ iff f(σ), 0 |= f(φ).
2. for all models LTL(N * , p ) models σ, we have σ, 0 |= φ iff g(σ), 0 |= g(φ).

(⇒) Let σ be an LTL(Σ * , p ) model σ such that σ, 0 |= φ. Let us build a bijection f : Σ → N such that for all i ∈ [1, k], we have f(a i ) = i and f(σ), 0 |= f(φ). Let b i 1 , . . . , b i k be all the letters in (Σ \ {a 1 , . . . , a k }) such that f (b i j ) ∈ {1, . . . , k}. So, there are k letters a j 1 , . . . , a j k whose image by

f is not in [1, k] since f is a bijection. f(a i ) def = i for all i ∈ [1, k] f(b iα ) def = f (a jα ) for all α ∈ [1, k ] f(a) def = f (a) otherwise
One can check that f is a bijection, φ = f(φ) and therefore f(σ), 0 |= φ .

(⇐) Let σ be a LTL(N * , p ) model σ such that σ, 0 |= φ . Similarly, one can build a bijection g : N → Σ such that for all i ∈ [1, k], we have g(i) = a i and g(σ),

0 |= φ. Let i 1 , . . . , i k be all the indices in N \ [1, k] such that (f ) -1 (i j ) ∈ {a 1 , . . . , a k }. So, there are k natural numbers j 1 , . . . , j k in [1, k] whose image by (f ) -1 is not in {a 1 , . . . , a k }. g(i) def = a i for all i ∈ [1, k] g(i α ) def = (f ) -1 (j α ) for all α ∈ [1, k ] g(n) def = (f ) -1 (n) otherwise
One can check that g is a bijection, φ = g(φ ) and therefore g(σ), 0 |= φ.

As a consequence, in the sequel, either we consider that Σ is finite and non-empty, or we consider that Σ = N. Similarly, we have the following property.

Lemma 2. Let Σ be a finite alphabet with cardinality k ≥ 2. There is a logarithmic-space satisfiability-preserving reduction from LTL(Σ * , p ) restricted to formulae without words in Σ * to LTL({0, 1} * , p ).

Note that Lemma 2 does not cover the case Σ = N but at the end of our investigation (see Corollary 1), we will be able to deal with the infinite case too, by reduction to the case with a finite alphabet.

Proof. Let Σ be a finite alphabet of cardinality k ≥ 2, say Σ = [0, k -1], and φ be a formula in LTL(Σ * , p ) without words in Σ * . For every n ∈ [0, k -1], we write enc(n) to denote the binary writing of n using log 2 (k) bits and we extend enc homomorphically to any finite word in Σ * . One can show that φ is satisfiable in LTL(Σ * , p ) iff φ is satisfiable in LTL({0, 1} * , p ). This is based on the property that for all w, w ∈ Σ * , we have w p w iff enc(w) p enc(w ). The other direction is by an easy verification since an LTL({0, 1} * , p ) model is an LTL(Σ * , p ) model too.

In the paper, we shall characterize the computational complexity of the satisfiability problem for any logic LTL(Σ * , p ). The problem is already PSpace-hard by the PSpacehardness of the LTL satisfiability problem. Branching-time extension shall be considered also.

LTL on finite strings with length constraints

In order to characterize the computational complexity for LTL(Σ * , p ), we make a slight detour by introducing an enriched version in which length constraints are allowed, instead of the prefix relation only.

Given w ∈ Σ * , we write len(w) to denote its length in N. When w is a word a 1 • • • a n of length n ≥ 1, for every i ∈ [0, n -1], we write w(i) to denote the letter a i+1 (so, as usual, the first index is zero). Similarly, given w, w ∈ Σ * , we write clen(w, w ) to denote the length of the longest common prefix between w and w . More precisely, there are w 0 , w 1 , and w 1 such that w = w 0 • w 1 , w = w 0 • w 1 and, w 1 and w 1 cannot start by the same first letter, if any. We set clen(w, w ) def = len(w 0 ). For instance clen(00100, 0011100) = 3. So, clen(w, w) = len(w), and w is a prefix of w iff clen(w, w) = clen(w, w ).

The logic LTL(Σ * , clen) is defined as LTL(Σ * , p ) except that atomic formulae of the form t p t are replaced by atomic formulae of the form clen(t 0 , t 0 ) ≤ clen(t 1 , t 1 ), where t 0 , t 0 , t 1 , t 1 are terms, defined exactly as in LTL(Σ * , p ). The argument of clen(•) should be viewed as a set and therefore the expressions clen(t, t ) and clen(t , t) are considered as identical. Expressions of the form clen(t 0 , t 0 ) are called counters since they are interpreted by natural numbers. Sometimes, we also write len(t) instead of clen(t, t). The satisfaction relation is then adapted as follows (only the clause for atomic formulae needs to be specified since the other clauses are identical):

σ, i |= clen(t 0 , t 0 ) ≤ clen(t 1 , t 1 ) def ⇔ clen( t 0 i , t 0 i ) ≤ clen( t 1 i , t 1 i ).
So, the logic LTL(Σ * , clen) allows us to express richer constraints than those from LTL(Σ * , p ). Roughly speaking, while atomic formulae in LTL(Σ * , p ) can only speak about the prefix relation, atomic formulae in LTL(Σ * , clen) are more precise and can state relationships between the lengths of longest common prefixes.

Lemma 3. Let Σ be either a finite non-empty alphabet or N. There is a logarithmic-space reduction from the satisfiability problem for LTL(Σ * , p ) to the satisfiability problem for LTL(Σ * , clen).

It is clear that the reduction is homomorphic for any Boolean or temporal connective, whereas t p t is translated into clen(t, t) ≤ clen(t, t ). Not only is the reduction satisfiability-preserving (which is sufficient to conclude upper bounds for LTL(Σ * , p ) from upper bounds from LTL(Σ * , clen) but it preserves also the semantics, which is after all not so surprising at this point.

The definition of clen(•) can be easily generalized to any (finite) number of strings. Given w 1 , . . . , w n ∈ Σ * , we write clen(w 1 , . . . , w n ) to denote the length of the longest common prefix for all w i 's. The logic LTL (Σ * , clen) is defined as LTL(Σ * , p ) except that atomic formulae of the form t p t are replaced by atomic formulae of the form

clen(t 1 , . . . , t n ) ≤ clen(t 1 , . . . , t n ),
where the terms are defined exactly as in LTL(Σ * , p ) and n, n ≥ 1. The satisfaction relation is then adapted as follows:

σ, i |= clen(t 1 , . . . , t n ) ≤ clen(t 1 , . . . , t n ) def ⇔ clen( t 1 i , . . . , t n i ) ≤ clen( t 1 i , . . . , t n i ).
So, apparently, the logic LTL (Σ * , clen) allows us to express even richer constraints than those from LTL(Σ * , clen). Nevertheless, by noting that clen(w 1 , . . . , w n ) = min{clen(w i , w j ) : i = j ∈ [1, n]}, one can show that there is a logarithmic-space reduction from the satisfiability problem for LTL (Σ * , clen) and the satisfiability problem for LTL(Σ * , clen).

That is why, in the rest of the paper, we mainly focus our investigations on linear-time temporal logics of the form LTL(Σ * , clen) where Σ is either a finite alphabet or N. In the finite case, we cannot restrict ourselves to a binary alphabet since the proof for Lemma 2 cannot be used to show that LTL(Σ * , clen) with finite alphabet Σ can be reduced to LTL({0, 1} * ,clen) because the encoding used in the proof of Lemma 2 does not preserve the length of longest common prefixes.

Here are three simple properties about clen(•) that play a special role in the sequel, namely this is all that one needs to know about clen(•) (see Lemma 5 and Lemma 6 to justify that claim).

Proposition 2. Let Σ be a finite alphabet of cardinality k ≥ 2.

(I) For all w, w ∈ Σ * , len(w) ≥ clen(w, w ). (II) For all w 0 , w 1 , . . . , w k ∈ Σ * such that clen(w 0 , w 1 ) = • • • = clen(w 0 , w k ) and for all i ∈ [0, k], clen(w 0 , w 1 ) < len(w i ), we have that there are i = j ∈ [1, k] such that clen(w 0 , w 1 ) < clen(w i , w j ). (III) For all w 0 , w 1 , w 2 ∈ Σ * , if clen(w 0 , w 1 ) < clen(w 1 , w 2 ), then clen(w 0 , w 1 ) = clen(w 0 , w 2 ).

Similarly, if Σ = N, then the properties Proposition 2(I) and Proposition 2(III) hold true.

In Figure 1, we present the strings w 0 , . . . , w k so that assumptions of Proposition 2(II) are satisfied. In particular, clen(w 0 , w 1 ) = • • • = clen(w 0 , w k ) = 3 and for all i ∈ [1, k], w i (3) = w 0 (3) (here w 0 (3) = 1). Since for every i ∈ [1, k], the word w i has at least four letters, by the Pigeonhole Principle, there are i

= j ∈ [1, k] such that w i (3) = w j (3).
w 0 : 0 0 0 1 0 2 w 1 : 0 0 0 0 1 3 5 6 w 2 : 0 0 0 2 1 4 . . . w k : 0 0 0 3 1 3 Proof. (I) Since the longest common prefix between w and w is clearly a prefix of w, its length is necessarily bounded by the length of w, which is precisely the statement for (I). (II) The proof is essentially based on the famous Pigeonhole Principle. Let w 0 , w 1 , . . . , w k be words in Σ * satisfying the assumptions in statement (II). So, for every i ∈ [0, k], w i can be written in the form w • w i such that w is the longest common prefix between the words w 0 , w 1 , . . . , w k and w i ∈ Σ + . By the Pigeonhole Principle, since card(Σ \ w 0 (0)) = k -1, there are j = j ∈ [1, k] such that w j (0) = w j (0) ∈ (Σ \ w 0 (0)). Consequently, clen(w 0 , w 1 ) < clen(w j , w j ). (III) Let w 0 , w 1 and w 2 be words such that clen(w 0 , w 1 ) < clen(w 1 , w 2 ). So, the words w 0 , w 1 and w 2 can be decomposed in the following way

w 0 = w 1 0 • w 2 0 w 1 = w 1 0 • w 1 1 • w 2 1 w 2 = w 1 0 • w 1 1 • w 1 2
for some w 1 1 ∈ Σ + and, w 2 0 and w 1 1 do not start by the same letter if any. It is immediate that clen(w 0 , w 1 ) = clen(w 0 , w 2 ) = len(w 1 0 ). As a corollary, the formulae below are valid in LTL(Σ * , clen) with card(Σ) = k:

φ I def = len(x) ≥ clen(x, x ) φ k II def = (( i∈[0,k] (clen(x 0 , x 1 ) < len(x i ))) ∧ clen(x 0 , x 1 ) = • • • = clen(x 0 , x k )) ⇒ ( i =j∈[1,k] (clen(x 0 , x 1 ) < clen(x i , x j ))) φ III def = (clen(x, x ) < clen(x , x )) ⇒ (clen(x, x ) = clen(x, x )) Note that φ k II is valid in LTL(Σ * , clen) if card(Σ) ≤ k .
Below, we introduce another syntactic restriction that is useful in the sequel without sacrificing expressive power.

Lemma 4. Let Σ be a non-empty countable alphabet. There is a logarithmic-space reduction from the LTL(Σ * , clen) satisfiability problem into its restriction in which terms are restricted to w ∈ Σ * , x, and Xx, with x ∈ SVAR.

The proof is standard, and it is based on the renaming technique.

Proof. Given terms t and t , we write t = t to denote the formula below:

(t = t ) def = (clen(t, t) ≤ clen(t, t )) ∧ (clen(t , t ) ≤ clen(t, t )).
Obviously, (t = t ) holds true whenever t and t are interpreted by the same string. Now, let φ be a formula in LTL(Σ * , clen) with occurrences of the term X j x for some j ≥ 2. Let x new 1 , . . . , x new j be new variables. One can show that φ is satisfiable iff the formula below is satisfiable:

G(x new 1 = Xx) ∧ j α=2 G(x new α = Xx new α-1 ) ∧ φ[X j x ← x new j ],
where φ[X j x ← x new j ] is the formula obtained from φ by replacing every occurrence of X j x by x new j . Note that the first two conjuncts do not introduce terms of the form X j x with j > 1.

Therefore by applying such a transformation a number of times bounded by the size of φ, we obtain a logarithmic-space reduction from the LTL(Σ * , clen) satisfiability problem to its adequate restriction. We use the facts that logarithmic-space reductions are closed under composition and enumerating a polynomial amount of conjuncts, as done above, requires only logarithmic-space thanks to a binary encoding for indices (the size of the outcome formula is not part of the used space, as usual in complexity theory).

String-compatible counter valuations

This section contains the key result to transform string constraints with the prefix order into counter constraints (Lemma 6). Before presenting such a result, first we explain why solving word equations (see e.g. [START_REF] Makanin | The problem of solvability of equations in a free semigroup (english translation)[END_REF]) allows to solve Boolean combinations of prefix constraints in polynomial space thanks to the PSpace upper bound established in [START_REF] Plandowski | Satisfiability of word equations with constants is in PSPACE[END_REF]. Actually, at the end of the section, we show that the problem can be solved in NP by taking advantage of Lemma 6 and the NP upper bound for solving quantifier-free Presburger formulae.

A remark on word equations

Given a finite alphabet Σ, a word equation E is an expression of the form w = w where w, w ∈ (Σ SVAR) * . The equation E is satisfiable iff there is a valuation s : (Σ SVAR) → Σ * extended homomorphically to (Σ SVAR) * and equal to the identity on Σ * such that s(w) = s(w ). The satisfiability problem for word equations can be solved in PSpace [START_REF] Plandowski | Satisfiability of word equations with constants is in PSPACE[END_REF] (see also Makanin's contribution for decidability in [START_REF] Makanin | The problem of solvability of equations in a free semigroup (english translation)[END_REF]). Thanks to this result, deciding the Boolean combination of prefix constraints of the form t p t (the terms are either words in Σ * or string variables) can be decided in PSpace too, as briefly explained below. However, prefix constraints are simple enough so that it is possible to design an ad-hoc but much simpler decision procedure, as shown below. This happens to be very useful in Section 4.

Before introducing string-compatible counter valuations (thanks to constraints on the lengths of the longest common prefixes that lead to genuine string valuations), let us briefly explain first how to solve Boolean combinations of prefix constraints by solving word equations. This is indeed based on the following observations. 1. Simultaneous satisfiability for a finite set {w 1 = w 1 , . . . , w n = w n } of word equations can be done by checking the satisfiability of the single word equation below

w 1 1 w 2 2 • • • n-1 w n = w 1 1 w 2 2 • • • n-1 w n ,
where 1 , . . . , n-1 are new letters (separators) dedicated to synchronization. 2. t p t can be reduced to the word equation t • x new = t where x new is a new string variable. 3. ¬(t p t ) can be reduced to the positive Boolean combination of word equations below:

( a =b∈Σ (t = x 1 new a x 2 new ∧ t = x 1 new b x 3 new )) ∨ ( a∈Σ (t = t a x 4 new )).
So, given a Boolean combination φ of prefix constraints, the reduction works as follows.

Without any loss of generality, the formula φ is in negation normal form. First, replace every constraint t p t or ¬(t p t ) by its translation as a positive Boolean combination of word equations; call this result φ . Then, guess a finite set of word equations that makes φ true propositionally and, finally, apply the PSpace algorithm to the set of word equations using the reduction in (1) above. A finite set of word equations makes true a propositional formula in NNF that is built from word equations when replacing every word equation from the set by (truth constant) makes the formula true whatever the truth value of the other word equations. By way of example, {x = a, z = c} makes true the formula ((x = a) ∨ (y = b)) ∧ (x = a) ∧ (z = c). This leads to an NPSpace algorithm, which can be solved in PSpace thanks to Savitch's Theorem [START_REF] Savitch | Relationships between nondeterministic and deterministic tape complexities[END_REF]. At this point, it is worth noting that the above reduction does not work when Σ = N but adding suffix constraints to the prefix constraints can be dealt with similarly. As a by-product of the developments below, solving Boolean combinations of prefix constraints (whatever the cardinality of the fixed alphabet) can be done in NP.

The characterisation

Let Σ be either a finite alphabet of the form [0, k -1] for some k ≥ 2 or N. Let SVAR be a finite subset of SVAR. As usual, a string valuation s with respect to SVAR is a map s : SVAR → Σ * . A counter valuation c with respect to SVAR is defined as a map

c : {clen(x, x ) : x, x ∈ SVAR } → N.
When a counter valuation c satisfies the conjunction of the formulae below, we say that c is string-compatible (with respect to SVAR ):

-Formula ψ I related to condition (I) from Proposition 2:

x,x ∈SVAR (clen(x, x) ≥ clen(x, x )).
-Formula ψ II related to condition (II) from Proposition 2:

either if Σ = N or the formula below if Σ = [0, k -1] x 0 ,...,x k ∈SVAR (( i∈[0,k] (clen(x 0 , x 1 ) < clen(x i , x i ))) ∧ clen(x 0 , x 1 ) = • • • = clen(x 0 , x k )) ⇒ ( i =j∈[1,k] (clen(x 0 , x 1 ) < clen(x i , x j ))).
-Formula ψ III related to condition (III) from Proposition 2:

x,x ,x ∈SVAR (clen(x, x ) < clen(x , x )) ⇒ (clen(x, x ) = clen(x, x )).
The size of the above conjunction is in O(card(SVAR ) k+2 ), i.e. polynomial in card(SVAR ) when the alphabet is fixed and finite. If Σ = N, then the size of the above conjunction is in O(card(SVAR ) 3 ). When X ⊆ SVAR and c is string-compatible with respect to SVAR , the restriction of c to X is also string-compatible with respect to X.

Let X be a non-empty subset of SVAR , s be a string valuation and c be a counter valuation, both with respect to SVAR . We say that c agrees with s on X (written c ≈ X s)

def ⇔ c(clen(x, x )) = clen(s(x), s(x )) for all x, x ∈ X. So, if X ⊆ X and c ≈ X s, then c ≈ X s too.
Moreover, note that the interpretation of s on SVAR \X is useless for the binary relation ≈ X and therefore the restriction of s to SVAR \ X may be sometime omitted. Given a string valuation s, there is a counter valuation c such that c ≈ X s and c can be defined obviously by: c(clen(x, x )) def = clen(s(x), s(x )) for all x, x ∈ X.

Lemma 5. Let s be a string valuation and c be the counter valuation that agree on SVAR . Then, c is string-compatible with respect SVAR . This is an immediate consequence of Proposition 2. Whereas Lemma 5 corresponds to a correctness lemma (string valuations induce string-compatible counter valuations), Lemma 6 below states a completeness result: every string-compatible counter valuation can be indeed obtained from a string valuation. The statement in Lemma 6 is just a bit more complex than one might think at first because of the distinction between two sets of string variables, but this is due to its forthcoming use in relationship with the logics LTL(Σ * , clen) and CTL (Σ * , clen). Lemma 6. Let X = ∅ and Y be finite and disjoint sets of string variables, c be a stringcompatible counter valuation with respect to X Y and s : Y → Σ * be such that c ≈ Y s. Then, there is a string valuation s that is a conservative extension of s, such that c ≈ X Y s .

Assuming that Y = {y 1 , y 2 }, the string valuations s and s below are therefore equivalent as far as the existence of a conservative extension is concerned since the lengths of longest common prefixes are identical.

s(y 1 ) = 0101 s(y 2 ) = 01112 s (y 1 ) = 3456 s (y 2 ) = 34777
Proof. Below, we prove the result when card(X) = 1 (unary case) since this is sufficient to conclude the proof of the lemma when card(X) > 1 by applying the construction below exactly card(X) times. Indeed, let X = {x 1 , . . . , x r } with r ≥ 1. Here is how the general case can be solved from the unary case.

-Compute s 1 : Y {x 1 } → Σ * such that c ≈ Y {x 1 } s 1 by application of the lemma in the unary case. (c is also string-compatible with respect to Y {x 1 }) -Let Y := Y {x 1 }. Compute s 2 : Y {x 2 } → Σ * extending s 1 such that c ≈ Y {x 2 } s 2 by
application of the lemma in the unary case. (c is also string-compatible with respect to

Y {x 1 , x 2 }) . . . -Let Y := Y {x r-1 }. Compute s r : Y {x r } → Σ * extending s r-1 such that c ≈ Y {xr} s r
by application of the lemma in the unary case.

Let us therefore consider the unary case below with X = {x}. The construction of s (x) is done in at most four steps.

(Step 1) Let t 1 , . . . , t α be all the distinct variables in Y such that

c(clen(t 1 , x)) = • • • = c(clen(t α , x)) = max{c(clen(t, x)) : t ∈ Y } def = M.
In a sense, the first c(clen(t 1 , x)) values of the string s (x) are uniquely inherited from s. The only situation for which t 1 , . . . , t α is void is when Y is empty. In that case, we omit the steps (2), (3) and (4) below and for every j

∈ [0, c(clen(x, x)) -1], s (x)(j) def = 0. (Step 2) For every j ∈ [0, M -1], s (x)(j) def = s(t 1 )(j). If c(clen(x, x)) = M, then we are done, otherwise go to Step (3). (Step 3) Let β be min(N \ {s(t j )(M) : j ∈ [1, α], c(clen(t j , t j )) > M}). We pose s (x)(M) def = β. (Step 4) For every j ∈ [M + 1, c(clen(x, x)) -1], s (x)(j) def = 0.
Above, it is remarkable that s can be defined deterministically once c and s are provided. An alternative definition of s that allows nondeterminism consists of allowing in Step (4) any value in Σ to define s (x)(j). The same reasoning applies to the degenerate case in Step (1). Furthermore, nondeterminism in Step (3) would also be possible (and the construction would satisfy the same essential properties) by allowing any value in

(Σ \ {s(t j )(M) : j ∈ [1, α], c(clen(t j , t j )) > M})
for defining s (x)(M). By contrast, the situation would be quite different if we had constraints on suffixes or regularity constraints too. Note also that in (Step 2), β ≤ card(Y ) since there are at most card(Y ) values that are removed from N.

It remains to show that s satisfies the required properties, which amounts to checking the following three properties. (b) The proof is ad absurdum. Let J ∈ [0, c(clen(x, x)) -1], s (x)(J) ∈ Σ. When Σ = N this leads to an immediate contradiction, so let us assume that Σ = [0, k -1] for some k ≥ 2. Since s has the profile Y → Σ * , s (x)(J) cannot be defined in (Step 1). Similarly, s (x)(J) cannot be defined in (Step 4) since (always) 0 ∈ Σ. So, s (x)(J) can only be defined in (Step 3), M < c(clen(x, x)) and J = M. Since s (x)(J) ∈ Σ, this means that s (x)(J) ≥ k and therefore

[0, k -1] ⊆ s(t j )(M) : j ∈ [1, α], c(clen(t j , t j )) > M) .
So, there are terms t 0 , . . . , t k-1 in {t 1 , . . . , t α } such that for every j ∈ [0, k -1], s(t j )(M) = j. The strings s (x), s(t 0 ), . . . , s(t k-1 ) satisfy the assumption in Proposition 2(II). Since c is string-compatible, it satisfies the formula

z 0 ,...,z k ∈Y ∪{x} (( i∈[0,k] (clen(z 0 , z 1 ) < clen(z i , z i ))) ∧ clen(z 0 , z 1 ) = • • • = clen(z 0 , z k )) ⇒ ( j =j ∈[1,k] (clen(z 0 , z 1 ) < clen(z j , z j )))
So, there are j = j ∈ [1, k] such that s(t j )(M) = s(t j )(M), which leads to a contradiction (since j = j implies that s(t j )(M) is different from s(t j )(M)).

(c) The proof is ad absurdum. Let t in Y {x} with clen(s (x), s (t)) = c(clen(x, t)). Note that by assumptions in the lemma, such a mismatch cannot be due to two terms from Y . By Step (2), we have clen(s (x), s(t 1 )) ≥ M. Now suppose that clen(s (x), s(t j )) < M for some j ∈ [2, α]. By Proposition 2(III), we get that clen(s (x), s(t j )) = clen(s(t 1 ), s(t j )). Furthermore, we have clen(s(t 1 ), s(t j )) = c(clen(t 1 , t j )) since c ≈ Y s. So, c(clen(t 1 , t j )) < M and therefore c(clen(t 1 , t j )) < c(clen(x, t 1 )). Since c is string-compatible, this implies that c(clen(t 1 , t j )) = c(clen(x, t j )), which leads to a contradiction since c(clen(t 1 , t j )) < M and c(clen(x, t j )) = M. So, by definition of t 1 , . . . , t α and by Step (2), for every j ∈ [1, α], we have clen(s (x), s(t j )) ≥ M.

If c(clen(x, x)) = M, then we are done with the definition of s (x) and therefore we get clen(s (x), s(t )) = c(clen(x, t )) for all t ∈ {t 1 , . . . , t α }. Otherwise by definition of s (x)(M),

s (x)(M) ∈ s(t j )(M) : j ∈ [1, α], c(clen(t j , t j )) > M
and therefore not clen(s (x), s(t j )) > M, whence clen(s (x), s(t j )) = M.

Consequently, t does not belong to t 1 , . . . , t α and therefore c(clen(t, x)) < M. Indeed M = max{c(clen(t, x)) : t ∈ Y }. Remember that c is string-compatible and more specifically it satisfies the formula

z,z ,z ∈Y {x} (clen(z, z ) < clen(z , z )) ⇒ (clen(z, z ) = clen(z, z )),
from condition (III) in Proposition 2. So, c(clen(t, x)) = c(clen(t, t 1 )) and we obtain that clen(s(t), s(t 1 )) = c(clen(t, t 1 )). So, for every j ∈ [0, L -1] with L = clen(s(t), s(t 1 )), s(t)(j) = s(t 1 )(j) = s (x)(j).

If c(len(t)) = L, then obviously, clen(s(t), s (x)) = c(clen(t, x)), which leads to a contradiction. Otherwise, we know that s(t)(L) = s(t 1 )(L) and s (x)(L) = s(t 1 )(L) (by Step (2) and the fact that L = c(clen(t, x)) < c(clen(t 1 , x))); whence s(t)(L) = s (x)(L). So, we get clen(s(t), s (x)) = L and therefore clen(s(t), s (x)) = c(clen(t, x)), which leads to a contradiction.

Lemma 7 below states a simple property about testing the satisfiability status of a Boolean combination of atomic formulae expressing prefix relationships. The NP upper bound can be obtained by reduction to the satisfiability problem for quantifier-free Presburger formulae [START_REF] Borosh | Bounds on positive integral solutions of linear Diophantine equations[END_REF][START_REF] Chr | On the complexity of integer programming[END_REF][START_REF] Pottier | Minimal Solutions of Linear Diophantine Systems: Bounds and Algorithms[END_REF]. Its proof technique involving Lemma 6 is reused for the full logic LTL(Σ * , clen) and for the logic CTL (Σ * , clen).

Lemma 7. Let Σ be a non-empty alphabet equal to either [0, k -1] for some k ≥ 2 or N. The satisfiability problem for Boolean combinations of atomic formulae from LTL(Σ * , p ) [resp. from LTL(Σ * , clen)] is NP-complete.

Proof. NP-hardness is proved by an easy logarithmic-space reduction from SAT where each propositional variable p i is encoded by the atomic formula 0 p x new i and x new i is a string variable dedicated to p i . Below, we establish the NP complexity upper bound for LTL(Σ * , clen), the proof for LTL(Σ * , p ) being then a direct corollary. Let φ be a Boolean combination of atomic formulae from LTL(Σ * , clen). Without any loss of generality, we can assume that the terms are of the form x ∈ SVAR or w ∈ Σ * . Indeed, if a term X i x occurs in φ, we can substitute it by a new variable y new , leading to an equi-satisfiable formula in LTL(Σ * , clen). So, assume that φ contains the following terms only: the words w 1 , . . . , w q and the string variables x 1 , . . . , x r . Let φ be the formula obtained from φ by replacing every occurrence of w i by the new string variable y i . Let us show that φ is satisfiable iff the formula below is satisfiable in quantifier-free Presburger arithmetic

φ def = φ ∧ ψ I ∧ ψ II ∧ ψ III ∧ i,j∈[1,q] clen(y i , y j ) = clen(w i , w j ),
where the formulae ψ I , ψ II and ψ III are those obtained from the conditions in Proposition 2 with the two disjoint sets of variables Y = {y 1 , . . . , y q } and X = {x 1 , . . . , x r }. We have seen that

ψ I ∧ ψ II ∧ ψ III is of size O((q + r) k+2 ) if Σ = [0, k -1] or of size O((q + r) 3 ) if Σ = N.
Similarly, size(φ ) is linear in size(φ) and the last generalized conjunction is of quadratic size in size(φ). Hence, φ is of polynomial size in size(φ). Since the satisfiability problem for quantifier-free Presburger formulae is in NP, see e.g. [Pap81,BT76], we get the upper bound NP for solving our initial problem.

It remains to show that φ is satisfiable in LTL(Σ * , clen) iff φ is satisfiable in Presburger arithmetic.

First, let us suppose that there is a string valuation s such that s |= φ verifying for every j ∈ [1, q], the equality s(y j ) = w j (which is equivalent to state that φ is satisfiable). Let c be the counter valuation such that for all x, x ∈ X Y , we have c(clen(x, x )) def = clen(s(x), s(x )). Obviously, c |= φ ∧ ( i,j∈[1,q] clen(y i , y j ) = clen(w i , w j )) where |= is the satisfaction relation in Presburger arithmetic. Furthermore, by Lemma 5, we have that c |= ψ I ∧ ψ II ∧ ψ III . Consequently, φ is satisfiable in Presburger arithmetic. Now suppose that there is a counter valuation c such that c |= φ and let s be the string valuation such that for every j ∈ [1, q], we have s(y j ) = w j . In particular, c is stringcompatible, c ≈ Y s, and by application of Lemma 6, there is a string valuation s that is a conservative extension of s, such that clen(s (x), s (x )) = c(clen(x, x )) for all x, x ∈ X ∪ Y , i.e. c ≈ X∪Y s . Consequently, for all clen(t 0 , t 0 ) ≤ clen(t 1 , t 1 ) occurring in φ we have c |= clen(t 0 , t 0 ) ≤ clen(t 1 , t 1 ) (in the sense of Presburger arithmetic) iff s |= clen(t 0 , t 0 ) ≤ clen(t 1 , t 1 ) (in the sense of LTL(Σ * , clen)). Therefore, we get that s |= φ and φ is satisfiable since s (y j ) = w j for all j ∈ [1, q].

Temporal logics on strings with prefix constraints 4.1 Linear-time temporal logics

Let Σ be a fixed non-empty (either finite, or infinite and countable) alphabet and φ be a formula in LTL(Σ * , clen). Without any loss of generality, we can assume that the words in Σ * occurring in φ are w 1 , . . . , w q , the string variables occurring in φ are x 1 , . . . , x r and the other terms are among Xx 1 , . . . , Xx r (see Lemma 4).

We build a formula φ in LTL(N, ≤) such that φ is satisfiable in LTL(Σ * , clen) iff φ is satisfiable in LTL(N, ≤) and size(φ ) is polynomial in size(φ). Before defining φ , let us make preliminary remarks and constructions.

1. For all i, j ∈ [1, q], we write c i,j to denote the constant value clen(w i , w j ). 2. By convention, the counters in the formula φ from LTL(N, ≤) are of the form clen(t, t ) with t, t ∈ T and T def = {y 1 , . . . , y q } ∪ {x i , Xx i : i ∈ [1, r]}. So, the expression clen(t, t ) is overloaded: it may occur in the formula φ in LTL(Σ * , clen) or as a (symbolic) counter in φ , but no confusion will be possible. Moreover, note that we have introduced a new set of variables {y 1 , . . . , y q } but each variable y i shall be interpreted rigidly by taking the value w i . 3. Let φ subst be the formula in LTL(N, ≤) obtained from φ by replacing every occurrence of the word w i by y i . This formula can be also viewed as a formula in LTL(Σ * , clen). More generally, for every subformula ψ of φ, we write ψ subst to denote the formula obtained from ψ by performing similar substitutions. Obviously, ψ subst is a subformula of φ subst too. 4. Let φ rig be the formula in LTL(N, ≤) defined below:

G ( i,j∈[1,q]
(clen(y i , y j ) = c i,j )).

5. Let φ next be the formula in LTL(N, ≤) defined below:

G ( t,t ∈{y 1 ,...,yq}∪{Xx 1 ,...,Xxr} clen(t, t ) = X clen(t \ X, t \ X)),
where (Xx i )\X def = x i and y j \X def = y j . For example, an instance of a conjunct is clen(Xx 1 , Xx 2 ) = X clen(x 1 , x 2 ) where clen(Xx 1 , Xx 2 ) and clen(x 1 , x 2 ) are understood as counters in LTL(N, ≤). 6. The formula ψ I is defined as

ψ I def = G ψ I with ψ I def = t,t ∈T (clen(t, t) ≥ clen(t, t )). 7. The formula ψ II is defined as ψ II def = G ψ II with either ψ II def = if Σ = N or the formula below if Σ = [0, k -1] ψ II def = t 0 ,...,t k ∈T (( i∈[0,k] (clen(t 0 , t 1 ) < clen(t i , t i ))) ∧ clen(t 0 , t 1 ) = • • • = clen(t 0 , t k )) ⇒ ( i =j∈[1,k]
(clen(t 0 , t 1 ) < clen(t i , t j ))).

The formula ψ III is defined as ψ

III def = G ψ III with ψ III def = t,t ,t ∈T (clen(t, t ) < clen(t , t )) ⇒ (clen(t, t ) = clen(t, t )).
The formula φ is defined as the following conjunction:

φ def = φ subst ∧ φ rig ∧ φ next ∧ ψ I ∧ ψ II ∧ ψ III . When Σ = N, size(φ ) is in O(size(φ) 3 ) whereas size(φ ) is in O(size(φ) k+2 ) when Σ = [0, k -1] for some k ≥ 2.
Let us start by establishing the correctness of the reduction in one direction.

Lemma 8. If φ is satisfiable then φ is satisfiable.

Proof. Let σ : N → ({x 1 , . . . , x r } → Σ * ) be a model for LTL(Σ * , clen)-actually restricted to the relevant string variables in {x 1 , . . . , x r }-such that σ, 0 |= φ. Let σ : N → (({x 1 , . . . , x r } {y 1 , . . . , y q }) → Σ * ) be the conservative extension of σ such that each string variable y i is always interpreted by the string w i . So, the formula φ subst understood as a formula in LTL(Σ * , clen) verifies that σ , 0 |= φ subst . Let σ N be the model of LTL(N, ≤) such that for all i ∈ N, for all counters clen(t, t ) (built from terms in T), we have σ N (i)(clen(t, t )) def = clen( t i , t i ) where y j i = σ (i)(y j ) = w j , x j i = σ (i)(x j ) and Xx j i = σ (i + 1)(x j ). It is quite immediate that σ N , 0 |= φ subst ∧ φ rig . In order to show that σ N , 0 |= φ next , by way of example let us show that σ N , 0 |= G (clen(y j , Xx j ) = X clen(y j , x j )). Given i ∈ N, we have σ N (i)(clen(y j , Xx j )) = clen( y j i , Xx j i ) = clen(w j , σ (i + 1)(x j )) whereas σ N (i + 1)(clen(y j , x j )) = clen( y j i+1 , x j i+1 ) = clen(w j , σ (i + 1)(x j )). This means precisely that σ N , i |= clen(y j , Xx j ) = X clen(y j , x j ). A similar simple reasoning can be performed for the other cases, and we conclude that σ N , 0 |= φ next .

Let s i be the string valuation with respect to the set T such that:

s i (x j ) def = σ (i)(x j ) for all j ∈ [1, r] s i (Xx j ) def = σ (i + 1)(x j ) for all j ∈ [1, r] s i (y j ) def = w j for all j ∈ [1, q]
Note that s i and σ N (i) satisfy the hypotheses from Lemma 5 since σ N (i) ≈ T s i , and therefore σ N (i) is string-compatible. By definition of string-compatibility, this means that σ N , i |= ψ I ∧ ψ II ∧ ψ III . Since the position i above is arbitrary and G(ψ

I ∧ ψ II ∧ ψ III ) is logically equivalent to ψ I ∧ ψ II ∧ ψ III , we get that σ N , 0 |= ψ I ∧ ψ II ∧ ψ III .
As a conclusion, σ N , 0 |= φ and therefore φ is satisfiable.

Let us now establish the correctness of the reduction in the other direction.

Lemma 9. If φ is satisfiable then φ is satisfiable.

Proof. Let σ : N → ({clen(t, t ) : t, t ∈ T} → N) be a model for the formula φ , i.e. σ, 0 |= φ . For every i ∈ N, we can consider that σ(i) is a counter valuation with respect to the set T. Let us define a model σ Σ * for LTL(Σ * , clen) such that σ Σ * , 0 |= φ inductively on the position i.

Base case (i = 0): We have seen that σ(0) is a counter valuation with respect to T. Let s be a string valuation such that for every j ∈ [1, q], we have s(y j ) def = w j . Since σ, 0 |= φ , this implies that σ, 0 |= ψ I ∧ ψ II ∧ ψ III . So, by definition, σ(0) is string-compatible. Moreover, clen(s(y i ), s(y j )) = σ(0)(clen(y i , y j )) = c i,j (by satisfaction of the formula φ rig ) for all i, j ∈ [1, q], i.e. σ(0) ≈ Y 0 s with Y 0 = {y 1 , . . . , y q }. By application of Lemma 6, there is a string valuation s that is a conservative extension of s, such that clen(s (t), s (t )) = σ(0)(clen(t, t )) for all t, t ∈ T, i.e. σ(0) ≈ T s . Consequently, for all counters clen(t 0 , t 0 ), clen(t 1 , t 1 ), we have σ, 0 |= clen(t 0 , t 0 ) ≤ clen(t 1 , t 1 ) iff s |= clen(t 0 , t 0 ) ≤ clen(t 1 , t 1 ). We define σ Σ * (0) and σ Σ * (1) as follows:

σ Σ * (0)(y j ) def = σ Σ * (1)(y j ) def = w j for all j ∈ [1, q] σ Σ * (0)(x j ) def = s (x j ) for all j ∈ [1, r] σ Σ * (1)(x j ) def = s (Xx j ) for all j ∈ [1, r]
For all t, t in T, we have clen( t 0 , t 0 ) in σ Σ * is equal to σ(0)(clen(t, t )).

Induction step: Suppose that σ Σ * is defined until the position i ≥ 1, and let us define σ Σ * (i+1).

The induction hypothesis assumes that for all j ∈ [0, i -1], for all terms t and t in T we have that clen( t j , t j ) = σ(j)(clen(t, t )). So, for all j < i, for all counters clen(t 0 , t 0 ), clen(t 1 , t 1 ), we also have

σ, j |= clen(t 0 , t 0 ) ≤ clen(t 1 , t 1 ) iff σ Σ * , j |= clen(t 0 , t 0 ) ≤ clen(t 1 , t 1 ) (1)
Let s be a string valuation such that for every j ∈ [1, q], we have s(y j ) = w j and for every j ∈ [1, r], s(x j ) = σ Σ * (i)(x j ). Since σ, 0 |= φ , this implies that σ, i |= ψ I ∧ ψ II ∧ ψ III and therefore σ(i) is string-compatible with respect to X ∪ Y where Y = Y 0 ∪ {x 1 , . . . , x r } and X = {Xx 1 , . . . , Xx r }. Moreover, for all t, t ∈ Y , clen(s(t), s(t )) = σ(i)(clen(t, t )) by the induction hypothesis, i.e. σ(i) ≈ Y s. Indeed, by way of example, we have the following equalities:

clen(s(x j ), s(x j )) = clen(σ Σ * (i)(x j ), σ Σ * (i)(x j )) (by definition of s) = clen( x j i , x j i ) (by definition of • ) = clen( Xx j i-1 , Xx j i-1 ) (by definition of • ) = σ(i -1)(clen(Xx j , Xx j )) (by IH) = σ(i)(clen(x j , x j )) (since σ, 0 |= φ next )
By application of Lemma 6, there is a string valuation s that is a conservative extension of s, such that σ(i) ≈ X∪Y s . Let us define σ Σ * (i + 1) as follows:

σ Σ * (i + 1)(y j ) def = w j for all j ∈ [1, q] σ Σ * (i + 1)(x j ) def = s (Xx j ) for all j ∈ [1, r]
Observe that for all j ∈ [0, i], for all terms t, t , we have that clen( t j , t j ) = σ(j)(clen(t, t )), whence for all counters clen(t 0 , t 0 ), clen(t 1 , t 1 ), σ, i |= clen(t 0 , t 0 ) ≤ clen(t 1 , t 1 ) iff σ Σ * , i |= clen(t 0 , t 0 ) ≤ clen(t 1 , t 1 ), establishing (1). Now that the construction of σ Σ * is done, for all i ∈ N, we have σ, i |= clen(t 0 , t 0 ) ≤ clen(t 1 , t 1 ) iff σ Σ * , i |= clen(t 0 , t 0 ) ≤ clen(t 1 , t 1 ) for all expressions clen(t 0 , t 0 ), clen(t 1 , t 1 ) occurring in φ subst . By structural induction, one can show that for all i ∈ N, we get σ, i |= ψ subst iff σ Σ * , i |= ψ subst for all subformulae ψ of φ. The base case with atomic formulae of the form clen(t 0 , t 0 ) ≤ clen(t 1 , t 1 ) is obtained by construction of σ Σ * (see above) whereas the cases for the Boolean connectives in the induction step are by an easy verification. By way of example, below, we consider the case ψ = ϕ 1 Uϕ 2 .

σ, i |= (ϕ 1 Uϕ 2 ) subst iff σ, i |= (ϕ 1 ) subst U (ϕ 2 ) subst
(by definition of (•) subst ) iff there is j ≥ i such that σ, j |= (ϕ 2 ) subst and for all i ≤ k < j, we have σ, k |= (ϕ 1 ) subst (by definition of |=) iff there is j ≥ i such that σ Σ * , j |= (ϕ 2 ) subst and for all i ≤ k < j,

we have σ Σ * , k |= (ϕ 1 ) subst (by induction hypothesis) iff σ Σ * , i |= (ϕ 1 ) subst U (ϕ 2 ) subst (by definition of |= in LTL(Σ * , clen)) iff σ Σ * , i |= (ϕ 1 Uϕ 2 ) subst (by definition of (•) subst )
So, since σ, 0 |= φ subst , we conclude that σ Σ * , 0 |= φ subst (when φ subst is viewed as a formula in LTL(Σ * , clen)). Moreover, for all j ∈ [1, q] and for all i ∈ N, we have σ Σ * (i)(y j ) = w j , whence σ Σ * , 0 |= φ too.

Theorem 1. For every non-empty countable alphabet Σ, the respective satisfiability problems for LTL(Σ * , p ) and LTL(Σ * , clen) are PSpace-complete.

By Lemmas 8 and 9, there is a logarithmic-space reduction from the satisfiability problem for LTL(Σ * , clen) to the satisfiability problem for LTL(N, ≤) and we know that the satisfiability problem for LTL(N, ≤) is PSpace-complete.

As a nice corollary, we state below a small alphabet property for checking satisfiability of formulae in LTL(N * , p )-i.e., the alphabet is countably infinite. This is due to the fact that the construction of the value β in the proof of Lemma 6 is bounded by card(X ∪ Y ) which corresponds to a bound 3 × size(φ) in the context of the proof of Lemma 9, where it is invoked in an essential way. This assumes that no term of the form X i x with i > 1 occurs in φ (see Lemma 4).

Corollary 1. Let φ be a satisfiable formula in LTL(N * , p ) with maximal letter N and with no term of the form X i x with i > 1. Then, φ has a model in which all the strings are interpreted in the subalphabet [0, max(N, 3 × size(φ))].

As a consequence, there is no formula φ in LTL(N * , p ) that characterizes exactly the set of models with an infinite number of letters from N to occur in it. Note that if terms of the form X i x with i > 1 occur in φ, a renaming is performed first, as shown in the proof of Lemma 4 (which, in the worst case, may cause a quadratic blow-up to the size of the subalphabet). We also get the following consequence by noting that the satisfiability problem for LTL(N * , p ) is equivalent to the problem stated in the corollary below.

Corollary 2. The problem below is PSpace-complete: input: a formula φ built over a finite set X of letters, question: is there an alphabet Σ ⊇ X such that φ is satisfiable in LTL(Σ * , clen)? Indeed, given φ with maximal letter N , we first reduce it to an equi-satisfiable formula φ with maximal letter bounded by size(φ) (by renaming of the letters) and then we take advantage of the polynomial-space bound from Corollary 1.

The proof method from [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF][START_REF] Demri | Verification of qualitative Z constraints[END_REF] for establishing that the satisfiability problem for LTL(N, ≤) is in PSpace can be applied to any extension L of LTL that uses Büchi automata similarly to LTL. Nevertheless, the automata built in [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF] to solve LTL(N, ≤) satisfiability problem are obtained as the product of a standard automaton (roughly speaking, following the construction from [START_REF] Vardi | Reasoning about infinite computations[END_REF]) and an automaton to deal with satisfiable symbolic models. Any extension of LTL behaving as LTL for the first part of the product would provide a PSpace upper bound too. Let us be a bit more precise. Let L be an extension of LTL such that for every formula φ of L, we can construct a Büchi automaton B φ of size at most exponential in size(φ) such that:

1. B φ accepts exactly the models of φ, 2. the size of each state of B φ is polynomial in size(φ), 3. it can be checked if a state is initial [resp. accepting] in polynomial space in size(φ), 4. each transition of B φ can be checked in polynomial space in size(φ).

Past LTL [START_REF] Markey | Past is for free: On the complexity of verifying linear temporal properties with past[END_REF], linear µ-calculus µLTL [START_REF] Vardi | A temporal fixpoint calculus[END_REF] or Extended Temporal Logic ETL [START_REF] Wolper | Temporal logic can be more expressive[END_REF] are well-known examples of such logics. It is then easy to design the extensions of the form L(Σ * , p ). Corollary 3. Let L be an extension of LTL satisfying the above properties and Σ be a nonempty and countable alphabet. Then, the satisfiability problem for L(Σ * , p ) is PSpacecomplete.

Such results can be pushed a bit further either by noting that any extension of LTL(N, ≤) obtained by adding a finite amount of MSO-definable temporal operators remains in the complexity class PSpace [DG08, Section 5] (see also [START_REF] Gastin | Satisfiability and model checking for MSO-definable temporal logics are in PSPACE[END_REF]) or by considering a richer set of relations on natural numbers, as those considered in the constrained language IPC* [START_REF] Demri | Verification of qualitative Z constraints[END_REF] (see also the survey on LTL with Presburger constraints in [START_REF] Demri | Linear-time temporal logics with Presburger constraints: An overview[END_REF]). Typically, one could add the past-time temporal operators X -1 and S while preserving the PSpace upper bounds stated so far.

Branching-time temporal logics

Developments for LTL(Σ * , clen) using Lemma 6 can be lifted to the branching-time case, even though we can only establish decidability without providing an optimal complexity upper bound as we did for LTL(Σ * , clen).

First, let us define the branching-time temporal logic CTL (Σ * , clen) extending the lineartime logic LTL(Σ * , clen). Formulae in the logic CTL (Σ * , clen) are defined as follows:

φ ::= clen(t 0 , t 0 ) ≤ clen(t 1 , t 1 ) | ¬(clen(t 0 , t 0 ) ≤ clen(t 1 , t 1 )) | φ ∧ φ | φ ∨ φ | X φ | φ U φ | φ R φ | A φ | E φ
Negation appears only in front of atomic formulae, and each temporal operator occurs with its dual operator. Nevertheless, we still have the full power of CTL [START_REF] Emerson | Sometimes' and 'not never' revisited: on branching versus linear time temporal logic[END_REF] in terms of path quantifiers and linear-time temporal operators. This restriction on negation will simplify a few developments in proofs. Below, we use the standard abbreviation AG φ def = A(⊥ R φ). Formulae in CTL (Σ * , clen) contain the constraints on the longest common prefixes while the version with prefix constraints only, is easy to design and it can be translated to CTL (Σ * , clen) similarly to the linear-time case.

A model for CTL (Σ * , clen) is a structure of the form M = (S, R, L) such that S is a non-empty set of states, R ⊆ S × S is a total binary relation (totality means that every state has at least one successor state) and L is a labelling function L : S → (SVAR → Σ * ). For all models M, infinite paths π in M and positions i ∈ N, the satisfaction relation |= is defined as follows:

-π, i |= clen(t 0 , t 0 ) ≤ clen(t 1 , t 1 ) def ⇔ clen( t 0 π,i , t 0 π,i ) ≤ clen( t 1 π,i , t 1 π,i ) where w π,i def = w for all w ∈ Σ * x π,i def = L(π(i))(x) for every x ∈ SVAR X j x π,i def = L(π(i + j))(x)
for all x ∈ SVAR and j ≥ 1

-π, i |= ¬clen(t 0 , t 0 ) ≤ clen(t 1 , t 1 ) def ⇔ clen( t 0 π,i , t 0 π,i ) > clen( t 1 π,i , t 1 π,i ). π, i |= Xφ def ⇔ π, i + 1 |= φ π, i |= φ U ψ def ⇔ there is j ≥ i such that π, j |= ψ and for all i ≤ k < j, we have π, k |= φ. π, i |= φ R ψ def ⇔ either π, j |= ψ for all j ≥ i or, there is j ≥ i such that π, j |= φ and for all i ≤ k ≤ j, we have π, k |= ψ π, i |= Eφ def ⇔
there is a path π that agrees with π on the positions 0, . . . , i such that

π , i |= φ π, i |= Aφ def ⇔
for all paths π that agree with π on the positions 0, . . . , i, we have π , i |= φ

An instance of the satisfiability problem for CTL (Σ * , clen) consists in checking whether a formula φ in CTL (Σ * , clen) has a model M and a path π such that π, 0 |= φ.

We write CTL (N, ≤) to denote CTL (Σ * , clen) when Σ is a singleton alphabet and the atomic formulae are restricted to inequalities between terms. In the sequel, we take advantage of the recent result below, partly based on the decidability of Boolean combinations of formulae from MSO and WMSO+U [START_REF] Bojańczyk | Weak MSO+U over infinite trees[END_REF] where U is the unbounding second-order quantifier.

Proposition 3. [START_REF] Carapelle | Satisfiability of CTL * with constraints[END_REF] The satisfiability problem for CTL (N, ≤) is decidable.

As for LTL(Σ * , clen), we state below a few properties about CTL (Σ * , clen) that will simplify a bit the developments. The properties can either be proved as for LTL(Σ * , clen) or are easily inherited from CTL [START_REF] Emerson | Deciding full branching time logic[END_REF][START_REF] Emerson | Sometimes' and 'not never' revisited: on branching versus linear time temporal logic[END_REF].

(PROP1) There is a logarithmic-space reduction from CTL (Σ * , clen) satisfiability problem into its restriction in which terms are restricted to w ∈ Σ * , x or Xx with x ∈ SVAR. (PROP2) A formula φ is satisfiable in CTL (Σ * , clen) iff φ has a model that is a (k φ + 1)branching tree where k φ is the number of existential path quantifiers occurring in φ (see also [START_REF] Gascon | An automata-based approach for CTL* with constraints[END_REF][START_REF] Carapelle | Satisfiability of CTL * with constraints[END_REF] or [ES84, Theorem 3.2] for the classical argument on CTL ).

Let Σ be a fixed non-empty (either finite or infinite and countable) alphabet and φ be a formula in CTL (Σ * , clen). Without any loss of generality, we can assume that the words in Σ * occurring in φ are w 1 , . . . , w q , the string variables occurring in φ are x 1 , . . . , x r and the other terms are among Xx 1 , . . . , Xx r (see (PROP1) above). Let d = k φ + 1. By (PROP2), we can restrict ourselves to consider models of φ which are d-branching trees.

Below, we build a formula φ in CTL (N, ≤) such that φ is satisfiable in CTL (Σ * , clen) iff φ is satisfiable in CTL (N, ≤) and size(φ ) is polynomial in size(φ). Before defining φ , let us make preliminary remarks and constructions.

1. For all i, j ∈ [1, q], we write c i,j to denote the constant value clen(w i , w j ). 2. For every γ ∈ [1, d], we introduce a counter z γ and we write p γ (understood as a propositional variable) to denote the formula (z γ = 0). Let φ dtree be the formula stating that each reachable state satisfies a unique formula p j :

AG( γ∈[1,d] (p γ ∧ γ =γ∈[1,d] ¬p γ )).
So, along a path, to identify the direction γ ∈ [1, d] for the next position, it is sufficient to test Xp γ . 3. By convention, the counters in the formula φ from CTL (N, ≤) are of the form clen(t, t ) γ with γ ∈ [1, d], t, t ∈ T and T def = {y 1 , . . . , y q } ∪ {x i , Xx i : i ∈ [1, r]}. There are also the counters of the form z γ . This is the most substantial difference with the linear case since each direction γ comes with its set of counters. We do not claim here a new idea since this is just a relevant adaptation of arguments from [START_REF] Gascon | An automata-based approach for CTL* with constraints[END_REF][START_REF] Carapelle | Satisfiability of CTL * with constraints[END_REF] but at the logical level. For instance, similar arguments are used at the level of tree automata in [START_REF] Gascon | An automata-based approach for CTL* with constraints[END_REF], which can be done even more explicitly for automata accepting d-branching trees only.

4. Let φ subst be the formula in CTL (N, ≤) obtained from φ by replacing every occurrence of the word w i by y i and then, by replacing every (positive) occurrence of clen(t 0 , t 0 ) ≤ clen(t 1 , t 1 ) by the formula below:

γ∈[1,d] (Xp γ ) ⇒ clen(t 0 , t 0 ) γ ≤ clen(t 1 , t 1 ) γ .
by replacing every occurrence of ¬(clen(t 0 , t 0 ) ≤ clen(t 1 , t 1 )) by the formula below:

γ∈[1,d] (Xp γ ) ⇒ ¬(clen(t 0 , t 0 ) γ ≤ clen(t 1 , t 1 ) γ ) .
This is one of the places where it is convenient to have formulae in negation normal form (at the minor cost of introducing dual operators). Again, for every subformula ψ of φ, we write ψ subst to denote the formula obtained from ψ by performing similar substitutions. 5. Let φ rig be the formula in CTL (N, ≤) defined below:

AG ( γ∈[1,d],i,j∈[1,q]
(clen(y i , y j ) γ = c i,j )).

6. Let φ next be the formula in CTL (N, ≤) defined below:

AG ( γ∈[1,d] ((Xp γ ) ⇒ ( t,t ∈{y 1 ,...,yq}∪{Xx 1 ,...,Xxr} clen(t, t ) γ = X clen(t \ X, t \ X) γ ))).
7. φ agree be the formula in CTL (N, ≤) defined below: This a new formula by comparison to the linear case, that states constraints related to the lengths of the longest common prefixes for string variables interpreted at the current position. The values do not depend on the directions of child nodes. The linear case roughly corresponds to d = 1 and therefore the formula φ agree with d = 1 is valid but useless in the linear case. 8. The formula ψ I is defined as ψ

AG ( γ,γ ∈[1,d] t,
I def = AG ψ I with ψ I def = γ∈[1,d] ( t,t ∈T (clen(t, t) γ ≥ clen(t, t ) γ )). 9. The formula ψ II is defined as ψ II def = AG ψ II with either ψ II def = if Σ = N or the formula below if Σ = [0, k -1] ψ II def = γ∈[1,d] ( t 0 ,...,t k ∈T (( i∈[0,k] (clen(t 0 , t 1 ) γ < clen(t i , t i ) γ )) ∧ clen(t 0 , t 1 ) γ = • • • = clen(t 0 , t k ) γ ⇒ ( i =j∈[1,k] (clen(t 0 , t 1 ) γ < clen(t i , t j ) γ )))).
10. The formula ψ III is defined as

ψ III def = AG ψ III with ψ III def = γ∈[1,d] ( t,t ,t ∈T (clen(t, t ) γ < clen(t , t ) γ ) ⇒ (clen(t, t ) γ = clen(t, t ) γ )).
The formulae ψ I , ψ II and ψ III are defined as in the linear case except that d distinct directions have to be considered. The formula φ is equal to the following conjunction:

φ dtree ∧ φ subst ∧ φ rig ∧ φ next ∧ φ agree ∧ ψ I ∧ ψ II ∧ ψ III .
Observe that some of subformulae in the conjunction above are not defined in negation normal form but it is easy to get such a form (mainly by removing the occurrences of material implication).

Correctness of the reduction is stated below.

Lemma 10. φ is satisfiable iff φ is satisfiable.

The proof is quite similar to the proofs for Lemma 8 and for Lemma 9 except that for each direction γ in [1, d] for the next state in a path, we consider a distinct family of counters of the form clen(t, t ) γ . Actually, these two lemmas can be viewed as Lemma 10 when d = 1 (a few adjustments would be necessary to have a formal correspondence). But when the terms t and t only refer to values at the current position, clen(t, t ) γ and clen(t, t ) γ have to agree even if γ = γ . Moreover, whether we consider a model for φ or for φ , it is sufficient to consider models that are infinite branching trees. Given X ⊆ T and γ ∈ [1, d], we write c ≈ γ X s to denote the agreement between c and s with respect to X but restricted further to the counters of the form clen(•, •) γ .

Proof. (⇒) First, let us show that if φ is satisfiable, then φ is satisfiable. Let M = (S, R, L) be a model and π 0 be an infinite path in M such that π 0 , 0 |= φ. Without any loss of generality, we can assume that Let M = (S, R, L ) be the conservative extension of M such that each string variable y i is everywhere interpreted as the string w i . Let M N = (S, R, L N ) be the model in CTL (N, ≤) defined as follows:

-For all w ∈ S and γ, γ Note that for all infinite paths π of the form π 0 (w)(wγ)π 1 , the value t w,wγ defined above is equal to t π ,len(w) in M . So, for all γ ∈ [1, d], for all w ∈ [1, d] * , L N (w) ≈ γ T • w,wγ where • w,wγ is understood in the obvious way as a string valuation with respect to T.

∈ [1, d], L N (w • γ)(z γ ) def = 0 if γ = γ , otherwise L N (w • γ)(z γ ) def = 1. Moreover L N (ε)(z 1 ) def = 0 and L N (ε)(z γ ) def = 1 for all γ ∈ [2, d]
It is now quite easy to show that π 0 , 0 |= φ subst ∧ φ rig ∧ φ agree , in particular π 0 , 0 |= φ subst is proved by structural induction and by considering all paths in M N . Indeed, one can show that for all paths π starting at ε, for all positions i and for all subformulae ψ of φ, we have

π , i |= ψ in M implies π , i |= ψ subst in M N .
Let us start by showing the base case. Suppose that π , i |= (clen(t

0 , t 0 ) ≤ clen(t 1 , t 1 )) with π (i + 1) = γ ∈ [1, d] and w = π (0) • • • π(i) (π (0) = ε). For each j ∈ {0, 1}, we have L N (w)(clen(t j , t j ) γ ) = clen( t j
≥ i such that π , j |= (ψ 2 ) subst in M N and for all k ∈ [i, j -1], we have π , k |= (ψ 1 ) subst in M N (by IH) implies π , i |= (ψ 1 ) subst U (ψ 2 ) subst in M N (by definition of |=) implies π , i |= (ψ 1 Uψ 2 ) subst (by definition of (•) subst )
For the satisfaction of φ agree , it is sufficient to observe that the values y j w,wγ and x j w,wγ do not depend on the direction γ. Moreover, the satisfaction of the conjunctive formula φ next ∧ ψ I ∧ ψ II ∧ ψ III can be proved exactly as in the linear case (see the proof of Lemma 8); in particular the property L N (w) ≈ γ T • w,wγ for all w and γ, is crucial for the satisfaction of ψ I ∧ ψ II ∧ ψ III .

(⇐) Now, let us prove the other direction, namely, if φ is satisfiable, then φ is satisfiable. Let M = (S, R, L) be a model and π 0 be an infinite path in M such that π 0 , 0 |= φ . Without any loss of generality, we can assume that

-M is D-branching tree with D = k φ + 1, i.e. S = [1, D] * and wRw iff w = w • γ for some γ ∈ [1, D]. -L is of the form [1, D] * → ({clen(t, t ) γ : t, t ∈ T, γ ∈ [1, d]} ∪ {z 1 , . . . , z γ } → N). -π 0 is an infinite path starting at the root ε ∈ [1, D] * .
Observe that size(φ ) is clearly strictly greater than size(φ) but no new existential path quantifier is introduced in the reduction, so k φ = k φ . However, the proof below does not depend on the value D since what really matters is the existence of a D-branching tree model, for some D.

So, for all w ∈ S and for all γ ∈ [1, d], L(w) restricted to γ-counters (i.e., counters indexed by γ), written below L(w) |γ , can be viewed as a counter valuation with respect to T. Let us define a model M Σ * = (S, R, L Σ * ) in CTL (Σ * , clen) such that π 0 , 0 |= φ, where L Σ * is inductively defined on the nodes w as follows. Below we use the following abbreviations for the sake of clarity.

p ≤ def = clen(t 0 , t 0 ) ≤ clen(t 1 , t 1 ) p s ≤ def = (clen(t 0 , t 0 ) ≤ clen(t 1 , t 1 )) subst ¬p ≤ def = ¬(clen(t 0 , t 0 ) ≤ clen(t 1 , t 1 )) ¬p s ≤ def = (¬clen(t 0 , t 0 ) ≤ clen(t 1 , t 1 )) subst Base case (w = ε): Let γ ∈ [1, d].
We have seen that L(ε) |γ can be viewed as a counter valuation over the γ-counters defined from the terms in T. Let s γ be a string valuation such that for every j ∈ [1, q], we have s γ (y j ) def = w j . Since π 0 , 0 |= φ , this implies that π 0 , 0 |= ψ I ∧ ψ II ∧ ψ III . So, by definition, the restriction of L(ε) |γ is string-compatible. Moreover, clen(s γ (y i ), s γ (y j )) = L(ε)(clen(y i , y j ) γ ) = c i,j for all i, j ∈ [1, q] (by satisfaction of the formula φ rig ). Consequently, L(ε) ≈ γ Y 0 s γ with Y 0 = {y 1 , . . . , y q }. By application of Lemma 6, there is a string valuation s γ that is a conservative extension of s γ , such that clen(s γ (t), s γ (t )) = c(clen(t, t ) γ ) for all t, t ∈ T, i.e. L(ε) ≈ γ T s γ . Note that for all t ∈ {x 1 , . . . , x r } {y 1 , . . . , y q }, for all γ, γ ∈ [1, d], s γ (t) = s γ (t) since π 0 , 0 |= φ agree and the algorithm in the proof of Lemma 6 is deterministic (assuming that the first string variables for which we assign a string are ordered as x 1 , . . . , x r ).

We define L Σ * (ε) as the string valuation s 1 (equivalently, any s γ could be used here) restricted to variables in {x 1 , . . . , x r } {y 1 , . . . , y q }. Moreover, for every γ ∈

[1, D] such that L Σ * (γ)(z γ ) = 0 for some γ ∈ [1, d], L Σ * (γ)
is defined as the restriction of the string valuation s γ such that for all j ∈ [1, r], we have L Σ * (γ)(x j ) def = s γ (Xx j ). Of course, we also require that for all j ∈ [1, q], we have L Σ * (γ)(y j ) def = w j . So, for all counters clen(t 0 , t 0 ), clen(t 1 , t 1 ), π 0 , 0 |= p s ≤ implies π 0 , 0 |= p ≤ (in M Σ * ) and π 0 , 0 |= ¬p s ≤ implies π 0 , 0 |= ¬p ≤ . These last properties still hold for any path π starting from ε.

Induction step: Suppose that M Σ * is defined until the state w = ε, for all its strict prefixes and for all the extensions of the strict prefixes by adding exactly one more direction. Let us define L Σ * (wγ) for all γ ∈ [1, D]. The induction hypothesis also assumes that for all terms t, t in T, for all j ∈ [1, i], for all infinite paths π with prefix w(-1)

• • • w(j -2) (by convention w(-1) = ε), for all γ ∈ [1, d] with L(w(-1) • • • w(j -2)π(j))(z γ ) = 0, we have clen( t π,j-1 , t π,j-1 ) = L(w(-1) • • • w(j -2))(clen(t, t ) γ ).
So, for all paths π visiting w at the i = len(w)th position, for all j < i, for all counters clen(t 0 , t 0 ), clen(t 1 , t 1 ), π , j |= p s ≤ implies π , j |= p ≤ (in M Σ * ) and π , j |= ¬p s ≤ implies π , j |= ¬p ≤ . Observe that when len(w) = 1, we have indeed the satisfaction of the above condition in the induction hypothesis since this amounts to check that for all terms t, t in T, for all γ ∈ [1, d], for all infinite paths π with L(π(1))(z γ ) = 0, clen( t π,0 , t π,0 ) = L(ε)(clen(t, t ) γ ).

Let γ be the unique element of [1, d] such that L(wγ)(z γ ) = 0 (existence and unicity are guaranteed by satisfaction of φ dtree ). We have seen that L(w) |γ can be viewed as a counter valuation over the γ -counters with respect to T. Let s be a string valuation such that for every j ∈ [1, q], we have s(y j ) def = w j and for every j ∈ [1, r], we have s(x j ) def = L Σ * (w)(x j ). Since π 0 , 0 |= φ , this implies that π , len(w) |= ψ I ∧ ψ II ∧ ψ III for any path π starting at ε and visiting w. So, by definition, the restriction of L(w) |γ is string-compatible with respect to T = X ∪ Y where Y = Y 0 ∪ {x 1 , . . . , x r } and X = {Xx 1 , . . . , Xx r }. Moreover, clen(s(y i ), s(y j )) = L(w)(clen(y i , y j ) γ ) = c i,j (by satisfaction of the formula φ rig ) for all i, j ∈ [1, q]. Moreover, for all t, t ∈ Y , clen(s(t), s(t )) = L(w)(clen(t, t ) γ ) by the induction hypothesis, i.e. L(w) ≈ γ Y s. By application of Lemma 6, there is a string valuation s that is a conservative extension of s, such that clen(s (t), s (t )) = L(w)(clen(t, t ) γ ) for all t, t ∈ T, i.e. L(w) ≈ γ T s . We define L Σ * (wγ) such that for all j ∈ [1, r], we have L Σ * (wγ)(x j ) def = s (Xx j ). Of course, we also require that for all j ∈ [1, q], we have L Σ * (wγ)(y j ) def = w j . Hence, assuming w = wγ, for all terms t, t in T, for all j ∈ [1, i + 1], for all infinite paths π with prefix w (-1) • • • w (j -2) for all γ ∈ [1, d] with L(w (-1) • • • w (j -2)π(j))(z γ ) = 0, we have clen( t π,j-1 , t π,j-1 ) = L(w (-1) • • • w (j -2))(clen(t, t ) γ ). This guarantees the propagation of the induction hypothesis. Only the case j = i + 1 needs to be newly established (which amounts to check that clen(s (t), s (t )) = L(w)(clen(t, t ) γ ) but s is precisely defined to satisfy such a property). Now that the construction of M Σ * is done, we have that for all paths π starting at ε, for all i ∈ N, π , i |= p s ≤ implies π , i |= p ≤ for all expressions clen(t 0 , t 0 ), clen(t 1 , t 1 ) occurring in φ. Similarly, π , i |= ¬p s ≤ implies π , i |= ¬p ≤ . Actually, by structural induction, one can show that for all paths π starting at ε, for all i ∈ N, π , i |= (ψ) subst implies π , i |= ψ (in M Σ * ) where ψ is a subformula of φ. We have seen that the base case of the induction is already true and the cases in the induction step for Boolean connectives and for linear-time temporal operators can be done as in the proof of Lemma 6. By way of example, let us consider the case when ψ = A ϕ. Since π 0 , 0 |= φ subst , we conclude that π 0 , 0 |= φ (in M Σ * ).

Theorem 2. For every non-empty countable alphabet Σ, the satisfiability problem for the branching-time temporal logic CTL (Σ * , clen) is decidable.

By Lemma 10, there is a satisfiability-preserving reduction from CTL (Σ * , clen) to CTL (N, ≤) and we know that the satisfiability problem for CTL (N, ≤) is decidable [START_REF] Carapelle | Satisfiability of CTL * with constraints[END_REF]. Again, as for the linear-time case, we can state a small alphabet property for checking satisfiability of formulae in CTL (N * , p ).

Corollary 4. Let φ be a satisfiable formula in CTL (N * , p ) with maximal letter N and with no occurrence of X i x with i > 1. Then, φ has a model in which all the strings are interpreted in the subalphabet [0, max(N, 3 × size(φ))].

Conclusion

We have shown that the logic LTL(Σ * , p ) admits a PSpace-complete satisfiability problem (by using the PSpace upper bound from [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF][START_REF] Demri | Verification of qualitative Z constraints[END_REF] for the logic LTL(N, ≤)) and that CTL (Σ * , clen) is decidable by taking advantage of the decidability result on natural numbers from [START_REF] Carapelle | Satisfiability of CTL * with constraints[END_REF]. This solves open problems mentioned in [DG05,Dem07,Gas07,CKL13,CKL14] and our proof technique allows us to get a PSpace upper bound for other extensions of LTL such as linear µ-calculus or Past LTL. A similar result has been very recently shown independently in [START_REF] Kartzow | Model checking constraint LTL over trees[END_REF] with a different proof technique based on constraint automata. Our proof method is quite original, explicit and conceptually simple since prefix constraints are transformed into length constraints about longest common prefixes, so that only constraints on counters are ultimately considered. Since the prefix relation is not a total ordering (unlike a lexicographical ordering on Σ * for example), it is not possible to take advantage of techniques from [START_REF] Segoufin | Automata based verification over linearly ordered data domains[END_REF] dedicated to temporal logics on concrete domains that are linearly ordered structures. Moreover, our results imply an ExpSpace upper bound for the uniform satisfiability problem defined below but it is open whether this is an optimal upper bound (the alphabet is now part of the input):

input: alphabet Σ = [0, k -1] (k in unary) or Σ = N, and a formula φ in LTL(Σ * , clen) question: is φ satisfiable in LTL(Σ * , clen)?

The recent work [START_REF] Kartzow | Model checking constraint LTL over trees[END_REF] answers positively to this question. By using the obvious symmetry between the prefix relation p and the suffix relation s , we can also conclude that the satisfiability problem for LTL(Σ * , s ) is PSpace-complete and CTL (Σ * , s ) is decidable. Interestingly enough, when both the prefix relation and the suffix relation are in the concrete domain, the decidability status of LTL(Σ * , p , s ) remains open and it is unclear whether the counter abstraction presented herein for the prefix relation can be extended further with the additional presence of the suffix relation. This also applies if we consider regularity constraints with the prefix constraints. By contrast, adding word equations at the atomic level is a natural extension but this leads to undecidability since concatenation allows to simulate increments and decrements in Minsky machines. Considering the subword relation would be another direction to investigate as the decidability status of LTL({0, 1} * , ) is open too. It is obvious that the fact that is a well-quasi-ordering by Higman's Lemma can be used to design a decision procedure.

Fig. 1 .

 1 Fig. 1. Strings satisfying assumptions of Proposition 2(II).

  (a) len(s (x)) = c(clen(x, x)). (b) s (x) ∈ Σ * . (c) For all x , x ∈ Y ∪ {x}, clen(s (x ), s (x )) = c(clen(x , x )).(a) The only reason for assigning a letter to the string s (x) strictly after the index c(clen(x, x))-1 would be if M > c(clen(x, x)). This cannot occur since c is string-compatible and more specifically it satisfies the formulaz,z ∈Y ∪{x} (clen(z, z) ≥ clen(z, z ))from condition (I) in Proposition 2. Moreover, the abort condition in (Step 2) rules out the case M = c(clen(x, x)).

-

  M is a d-branching tree with d = k φ +1 where k φ is the number of occurrences of existential path quantifiers in φ, i.e. S = [1, d] * and wRw iff w = w • γ for some γ ∈ [1, d]. -L is of the form [1, d] * → ({x 1 , . . . , x r } → Σ * ), assuming that the string variables in φ are among {x 1 , . . . , x r }. π 0 is an infinite path starting at the root ε ∈ [1, d] * . Equivalently, π 0 can be represented by an ω-word in [1, d] ω .

  (this is a convention since ε has no parent). It is easy to show that π 0 , 0 |= φ dtree .-For all w ∈ S and for all γ ∈ [1, d], L N (w)(clen(t, t ) γ ) def = clen( t w,wγ , t w,wγ ) wherey j w,wγ def = w j x j w,wγ def = L (w)(x j ) Xx j w,wγ def = L (wγ)(x j )

  t ∈{y 1 ,...,yq}∪{x 1 ,...,xr} clen(t, t ) γ = clen(t, t ) γ ).

  |= (clen(t 0 , t 0 ) γ ≤ clen(t 1 , t 1 ) γ ). In M N , we have π , i |= Xp γ since L N (wγ)(z γ ) = 0 and by definition, p γ is equal to z γ = 0. So, in M N , we get π , i |= Xp γ ⇒ (clen(t 0 , t 0 ) γ ≤ clen(t 1 , t 1 )

		w,wγ , t j w,wγ )	(by definition of L N (w))
	=	clen( t j π ,i , t j π ,i )	(in M )
	So, we get that π , i

γ ). By contrast, for all γ = γ, we have L N (wγ)(z γ ) = 1 and therefore in M N , we obtain π , i |= Xp γ , which "vacuously" guarantees that π , i |= Xp γ ⇒ (clen(t 0 , t 0 ) γ ≤ clen(t 1 , t 1 ) γ ). So, π , i |= (clen(t 0 , t 0 ) ≤ clen(t 1 , t 1 )) subst . The proof for the base case with ¬(clen(t 0 , t 0 ) ≤ clen(t 1 , t 1 )) is very similar. By way of example, below we deal with the induction step for the cases ψ = E ψ and ψ = ψ 1 Uψ 2 . Case ψ = E ψ :

π , i |= E ψ

implies there is π such that π , i |= ψ and, π and π agree on the position 0, . . . , i (by definition of |=) implies there is π such that π , i |= (ψ ) subst in M N and, π and π agree on the position 0, . . . , i (by IH) implies π , i |= E (ψ ) subst in M N (by definition of |=) implies π , i |= (E ψ ) subst (by definition of (•) subst ) Case ψ = ψ 1 Uψ 2 : π , i |= ψ 1 Uψ 2 implies there is j ≥ i such that π , j |= ψ 2 and for all k ∈ [i, j -1], we have π , k |= ψ 1 (by definition of |=) implies there is j

  π , i |= (A ϕ) subst implies π , i |= A ϕ subst (by definition of (•) subst ) implies for all paths π that agree on π on the positions 0, . . . , i, we have π , i |= ϕ subst (by definition of |=) implies for all paths π that agree on π on the positions 0, . . . , i, we have π , i |= ϕ in M Σ * (by IH) implies π , i |= A ϕ in M Σ * (by definition of |=)

Acknowledgments: We would like to thank W. Plandowski (Warsaw University) for explanations about the encoding of Boolean combinations of prefix constraints as word equations. Furthermore, we thank Th. Colcombet (LIAFA, Paris) for several discussions we had that helped us to clarify some aspects of this work. We thank also Ph. Schnoebelen (LSV, Cachan) for directing our attention to the work [Kus06]. Furthermore we are deeply indebted to the two anonymous referees for their suggestions and remarks that help us to improve the manuscript; this has been highly appreciated especially for the proof of Lemma 6 and for simplifications in the formulae built in Section 4.

Funding: This work was supported by the EU Seventh Framework Programme [grant number PIOF-GA-2011-301166 (DATAVERIF) to S.D.]; the U.S. Air Force Office of Scientific Research [grant number FA9550-09-1-0596 to M.D.]; and the U.S. National Science Foundation [grant number 0644299 to M.D.]. This work was done, in part, while the first author visited the ACSys group at New York University.