Stéphane Demri

Ranko Lazić

David Nowak

On the freeze quantifier in Constraint LTL: decidability and complexity

Keywords: linear temporal logic, constraints, freeze quantifier, decidability, computational complexity

Constraint LTL, a generalisation of LTL over Presburger constraints, is often used as a formal language to specify the behavior of operational models with constraints. The freeze quantifier can be part of the language, as in some real-time logics, but this variable-binding mechanism is quite general and ubiquitous in many logical languages (first-order temporal logics, hybrid logics, logics for sequence diagrams, navigation logics, logics with λ-abstraction etc.). We show that Constraint LTL over the simple domain N, = augmented with the freeze quantifier is undecidable which is a surprising result in view of the poor language for constraints (only equality tests). Many versions of freeze-free Constraint LTL are decidable over domains with qualitative predicates and our undecidability result actually establishes Σ 1 1completeness. On the positive side, we provide complexity results when the domain is finite (ExpSpace-completeness) or when the formulae are flat in a sense introduced in the paper. Our undecidability results are sharp (i.e. with restrictions on the number of variables) and all our complexity characterisations ensure completeness with respect to some complexity class (mainly PSpace and ExpSpace).

Introduction

Model-checking for infinite-state systems. Temporal logics are wellstudied formalisms to specify the behavior of finite-state systems and the computational complexity of the model-checking problems is nowadays wellknown, see e.g. a survey in [START_REF] Schnoebelen | The complexity of temporal logic model checking[END_REF]. However, many systems such as communication protocols have infinitely many configurations and usually the techniques for the finite case cannot be applied directly. For numerous infinite-state systems, the model-checking problem for the linear-time temporal logic LTL can be easily shown to be undecidable (counter automata, hybrid automata and more general constraint automata [START_REF] Revesz | Introduction to Constraint Databases[END_REF]Chapter 6]). Actually, simpler problems such as reachability are already undecidable. However, remarkable classes of infinite-state systems admit decidable model-checking problems, such as timed automata [START_REF] Alur | A theory of timed automata[END_REF] and subclasses of counter automata [START_REF] Ibarra | Reversal-bounded multicounter machines and their decision problems[END_REF][START_REF] Boigelot | Symbolic methods for exploring infinite state spaces[END_REF][START_REF] Boigelot | Representing arithmetic constraints with finite automata: an overview[END_REF][START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF][START_REF] Leroux | Flat counter systems are everywhere![END_REF]. For instance, fragments of LTL with Presburger constraints have been shown decidable over appropriate counter automata [START_REF] Comon | Flatness is not a weakness[END_REF][START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF]. In order to push further the decidability border, one way consists in considering larger classes of operational models, see e.g. [START_REF] Ibarra | Reversal-bounded multicounter machines and their decision problems[END_REF]. Alternatively, enriching the specification language is another possibility. In the paper, we are interested in studying systematically the extensions of versions of LTL over concrete domains by the so-called freeze quantifier, and in analysing the consequences in terms of decidability and computational complexity.

A variable-binding mechanism. The freeze quantifier in real-time logics has been introduced by Alur and Henzinger in the logic TPTL, see e.g. [START_REF] Alur | A really temporal logic[END_REF]. The formula x • φ(x) binds the variable x to the time t of the current state: x • φ(x) is semantically equivalent to φ(t). Alternatively, in the explicit clock approach [START_REF] Harel | Explicit clock temporal logic[END_REF], there is an explicit clock variable t and even though in this approach the freeze variable-binding mechanism is possible, the logical formalisms from [START_REF] Alur | A really temporal logic[END_REF] and [START_REF] Harel | Explicit clock temporal logic[END_REF] are incomparable. In this paper, we want to extend some of the decidable logics from [START_REF] Comon | Flatness is not a weakness[END_REF][START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF][START_REF] Demri | LTL over integer periodicity constraints[END_REF] to admit the freeze quantifier: ↓ y=x φ(y) holds true at a state iff φ(y) holds true at the same state with y taking the value of x. Here, y can be in the scope of temporal operators. A crucial difference with the logics in [START_REF] Alur | A really temporal logic[END_REF][START_REF] Harel | Explicit clock temporal logic[END_REF] rests on the fact that the variable x may not be monotonic. We focus on decidability and complexity issues when the language of constraints (at the atomic level of the logics) is very simple in order to isolate the effects of the freeze quantifier. We know for instance that LTL over integer periodicity constraints augmented with the freeze quantifier is ExpSpace-complete [START_REF] Demri | LTL over integer periodicity constraints[END_REF].

The above-mentioned variable-binding mechanism that allows the binding of logical variables to objects is very general and it has been used in the literature for various purposes. Details will be provided along the paper (see e.g. Sections 2.2 and 5). In particular, one can see flexible variables as processes, values of the domain as resources, and the freeze quantifier and rigid variables as ways to extract and store the current resource used by a process. This view is nicely illustrated in [START_REF] Lisitsa | Temporal logic with predicate λ-abstraction[END_REF] by the specification of a communication protocol. In Section 2.2, we consider the case of a process requesting memory blocks.

Our contribution. In the paper, we analyse decidability and complexity issues of Constraint LTL augmented with the freeze quantifier. The temporal operators we consider are restricted to the standard future-time operators 'until' and 'next' (no past-time operators). CLTL ↓ (D) denotes such a logic over the concrete domain D. A concrete domain is composed of a non-empty set equipped with a family of relations. The atomic formulae of CLTL ↓ (D) are based on constraints over D with the ability to compare values of variables at states of bounded distance (see details in the body of the paper) as done in [START_REF] Wolter | Spatio-temporal representation and reasoning based on RCC-8[END_REF][START_REF] Balbiani | Computational complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning[END_REF][START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF][START_REF] Gabelaia | On the computational complexity of spatio-temporal logics[END_REF].

First, we show that when the underlying domain D is finite, CLTL ↓ (D) satisfiability is in ExpSpace. If moreover D has at least two elements with the equality predicate, then CLTL ↓ (D) is ExpSpace-hard. As a corollary, CLTL ↓ (D, =) satisfiability is ExpSpace-complete when |D| ≥ 2 and D is finite (Section 3.2). This witnesses an exponential blow-up since satisfiability for the freeze-free fragment CLTL(D) when D is finite can be easily shown in PSpace as plain LTL [START_REF] Sistla | The complexity of propositional linear temporal logic[END_REF].

When the domain D is infinite, we show that CLTL ↓ (D, =) is undecidable which is the main result of the paper (Section 4). This is quite surprising since the language of constraints is poor (only equality tests) and only futuretime operators are used unlike what is shown in [14, Section 7] with past-time operators. Our proof, based on a reduction from the Recurrence Problem for 2-counter machines, refines this result: CLTL ↓ (D, =) is Σ 1 1 -complete even if only one flexible variable and two rigid variables (used to record the values of flexible variables) are involved. Hence, in spite of the very basic Presburger constraints in CLTL ↓ (N, =), satisfiability is Σ 1 1 -complete. Decidability of CLTL ↓ (D) can be obtained either at the cost of syntactic restrictions or by assuming semantical constraints (as in the logic TPTL [START_REF] Alur | A really temporal logic[END_REF] where the freeze quantifier can only record the value of a monotonic variable, namely time).

In order to regain decidability, we introduce the flat fragment of CLTL ↓ (D) which contains the freeze-free fragment CLTL(D) and we show that there is a logarithmic-space reduction from the flat fragment of CLTL ↓ (D) into CLTL(D) assuming that the equality predicate belongs to D. As a corollary, we obtain that the flat fragments of CLTL ↓ (Z, <, =) and CLTL ↓ (R, <, =) are PSpace-complete (Section 3.2). Flat fragments of plain LTL versions have been studied in [START_REF] Dams | Flat fragments of CTL and CTL*: separating the expressive and distinguishing powers[END_REF][START_REF] Comon | Flatness is not a weakness[END_REF] (see also in [START_REF] Ibarra | On removing the stack from reachability constructions[END_REF]Section 5] the design of a flat logical temporal language for model-checking pushdown machines) and our definition of flatness takes advantage in a non-trivial way of the polarity of 'until' subformulae occurring in a formula. This is a standard way to restrict the interplay between modalities and quantifiers, see e.g. [START_REF] Bouajjani | Constrained properties, semilinear sets, and Petri nets[END_REF][START_REF] Comon | Flatness is not a weakness[END_REF][START_REF] Cate | On the complexity of hybrid logics with binders[END_REF]. Although we do not claim that flat formulae are especially interesting in practice, they cover nontrivial uses of the freeze quantifier. However, they cannot express the property that a variable at distinct points takes distinct values.

Along the paper, we consider the satisfiability problem, but as shown in Section 2.3, our results extend to the model-checking problem.

CLTL ↓ (D) extends naturally the freeze-free fragment CLTL(D), and we show that it increases strictly the expressive power (Proposition 1). However, we prove that significant fragments of CLTL ↓ (D) are as expressive as the full language, for instance by recording only values of flexible variables at the current state or by allowing only rigid variables in atomic formulae (see Section 2.4).

Apart from the technical contributions of the paper, we provide comparisons with several works which involve freeze-like operators, such as in first-order quantification, in timed LTL, in hybrid logics with reference pointers, to quote a few examples.

Structure of the paper. In Section 2, we present Constraint LTL with the freeze quantifier, satisfiability and model-checking problems of interest, and consider relative expressivity. Section 3 contains decidability and complexity results when the underlying concrete domain is finite or with restricting to the flat fragment. In Section 4, we show that CLTL ↓ (N, =) is Σ 1 1 -complete. Related work is discussed in Section 5. In Section 6, we conclude and enumerate a few open problems.

2 Constraint LTL with the freeze quantifier

Syntax and semantics

A constraint system is a set, called the domain, with a countable family of relations on this set. Let D = (D, (R i ) i∈I ) be a constraint system. We define the logic CLTL ↓ (D) by giving its syntax and semantics.

Syntax. Let FleVarSet and RigVarSet be countable sets of variables which are respectively called flexible variables and rigid variables. Terms are given by the grammar:

t ::= X • • • X n times x | y
where x is in FleVarSet and y is in RigVarSet. We use X n as an abbreviation for X • • • X n times . Formulae are given by the grammar:

φ ::= R(t 1 , . . . , t n ) | ¬φ | φ 1 ∧ φ 2 | Xφ | φ 1 Uφ 2 |↓ y=X n x φ
where R ranges over the predicate symbols associated to the relations in (R i ) i∈I , x over FleVarSet, and y over RigVarSet. Note that we use X for denoting either the n th next value X n x of the variable x or the formula Xφ. We define the Boolean constants, and the temporal operators 'sometimes' and 'always', as the following abbreviations:

def = R(t 1 , . . . , t n ) ∨ ¬R(t 1 , . . . , t n ), Fφ def = Uφ, ⊥ def = R(t 1 , . . . , t n ) ∧ ¬R(t 1 , . . . , t n ), and Gφ def = ¬F¬φ.
Let FleVars(φ) and RigVars(φ) denote the sets of all flexible and rigid (respectively) variables which occur in φ.

Freeze-free fragment. CLTL(D) is the fragment of CLTL ↓ (D) with no rigid variables and hence without freeze quantifier.

Flat fragment. We say that the occurrence of a subformula in a formula is positive if it occurs under an even number of negations, otherwise it is negative. The flat fragment of CLTL ↓ (D) is the restriction of CLTL ↓ (D) where, for any subformula φ 1 Uφ 2 , if it is positive then ↓ does not occur in φ 1 , and if it is negative then ↓ does not occur in φ 2 .

More precisely, the flat fragment consists of the following formulae ϕ. Subformulae ϕ are positive, whereas subformulae ϕ -are negative.

ϕ ::= R(t 1 , . . . , t n ) | ¬ϕ -| ϕ 1 ∧ ϕ 2 | Xϕ | ψUϕ |↓ y=X n x ϕ ϕ -::= R(t 1 , . . . , t n ) | ¬ϕ | ϕ - 1 ∧ ϕ - 2 | Xϕ -| ϕ -Uψ |↓ y=X n x ϕ - ψ ::= R(t 1 , . . . , t n ) | ¬ψ | ψ 1 ∧ ψ 2 | Xψ | ψ 1 Uψ 2 Semantics. A model σ : N → (FleVarSet → D
) is a sequence of mappings from FleVarSet to D. For any i ∈ N, we write σ i for the model defined by σ i (j) = σ(i+j) for every j ≥ 0. An environment ρ is a mapping from RigVarSet to D. We write ρ[x → v] for the environment mapping x to v ∈ D, and any other variable y to ρ(y). The semantics of terms is given by:

X n x σ,ρ = σ(n)(x) if x is in FleVarSet y σ,ρ = ρ(y) if y is in RigVarSet
The semantics of formulae is given by the following satisfaction relation. (Note that we use R for both a relation symbol and the relation it denotes.)

• σ |= ρ R(t 1 , . . . , t n ) iff ( t 1 σ,ρ , . . . , t 2 σ,ρ ) ∈ R, • σ |= ρ ¬φ iff σ |= ρ φ, • σ |= ρ φ 1 ∧ φ 2 iff σ |= ρ φ 1 and σ |= ρ φ 2 , • σ |= ρ Xφ iff σ 1 |= ρ φ, • σ |= ρ φ 1 Uφ 2 iff there exists i such that σ i |= ρ φ 2 and for all j < i, σ j |= ρ φ 1 , • σ |= ρ ↓ y=X n x φ iff σ |= ρ[y →σ(n)(x)] φ.

Examples

As a first example, consider the formula

φ x ∞ def = G ↓ y=x XG x = y
which states that the values of the variable x at different points in time are mutually distinct. This is interesting for the verification of cryptographic protocols, where nonces are variables which have to be fresh, i.e. they cannot take twice the same value.

As a second example, we consider a process requesting memory blocks. Let us assume two flexible variables o (for operator) and a (for argument) such that o takes its values in the finite domain {Malloc, Access, Free} and a takes its values in an infinite set of memory locations.

We use Malloc(x), Access(x) and Free(x) as respective abbreviations for o = Malloc ∧ a = x, o = Access ∧ a = x, and o = Free ∧ a = x (x is a rigid variable).

We can easily express the following properties in CLTL ↓ (D).

• As soon as a memory location is freed, either it is never accessed again, or it is not accessed until it is allocated again:

G(o = Free ⇒ ↓ x=a (G¬Access(x) ∨ ¬Access(x)UMalloc(x)))
• When a memory location is allocated, it will either be freed in the future or will always be eventually accessed (so that we do not waste memory):

G(o = Malloc ⇒ ↓ x=a (FFree(x) ∨ GFAccess(x)))

Satisfiability and model-checking problems

We recall below the problems we are interested in.

Satisfiability problem for CLTL ↓ (D): instance: a CLTL ↓ (D) formula φ; question: is there a model σ and an environment ρ such that σ |= ρ φ?

Without loss of generality we can assume that no rigid variable occurs free in φ, which means that ρ is not essential above.

The model-checking problem rests on D-automata which are constraints automata. A D-automaton is simply a Büchi automaton with alphabet a finite set of Boolean combinations of atomic CLTL ↓ (D) formulae with terms of the form x and Xx (x ∈ FleVarSet). In a D-automaton, letters on transitions induce constraints between the variables of the current state and the variables of the next state as done in [START_REF] Comon | Flatness is not a weakness[END_REF]. Alternatively, labelling the transitions by CLTL ↓ (D) formulae (as done in [START_REF] Wolper | Temporal logic can be more expressive[END_REF]) would not modify essentially the decidability status of model-checking problems considered in this paper.

Model-checking problem for CLTL ↓ (D): instance: a D-automaton A and a CLTL ↓ (D) formula φ; question: are there a symbolic ω-word v = φ 0 , φ 1 , . . . accepted by A, a model σ (a realisation of v) and an environment ρ such that σ |= ρ φ and for every i ≥ 0, σ i |= ρ φ i ?

It is not difficult to show that as soon as D is non-trivial the satisfiability problem and the model-checking problem are reducible to each other in logarithmic space following techniques from [START_REF] Sistla | The complexity of propositional linear temporal logic[END_REF]. In the sequel, we prove results for the satisfiability problems but one has to keep in mind that our results extend to the model-checking problem.

Expressive power

The freeze quantifier strictly increases expressive power. In order to show formally that the freeze quantifier is powerful, we show that CLTL ↓ (N, =) is strictly more expressive than its freeze-free fragment CLTL(N, =). In fact,

φ x
∞ is an example of a formula φ in CLTL ↓ (N, =) with no free rigid variable for which there is no equivalent formula ψ in CLTL(N, =). The result will follow from the following property.

Lemma 1 Every satisfiable formula φ in CLTL(N, =) has a model which contains only finitely many distinct values. Moreover, the number of distinct values is polynomial in |φ|.

Proof. Let φ be a formula in CLTL(N, =) with variables in {x 1 , . . . , x n } and k be equal to 1 plus the maximal j such that X j x i occurs in φ for some flexible variable x i . Let C be the finite set of constraints of the form

X j 1 x i 1 = X j 2 x i 2 with 0 ≤ j 1 , j 2 ≤ k -1 and i 1 , i 2 ∈ {1, . . . , n}.
We define a total ordering on {1, . . . , n}×N as follows: i, j < i , j iff j < j or (j = j and i < i ). Given a model σ :

N → (FleVarSet → N), we build a model σ : N → (FleVarSet → {1, . . . , k × n}) such that σ |= φ iff σ |= φ.
If x is a flexible variable not occurring in φ, σ (i)(x) = 1 for every i ≥ 0. Otherwise σ (0)(x 1 ) = 1 ( 1, 0 is minimal wrt <). Now suppose that for every i , j < i, j , σ (j )(x i ) has been already defined. We shall define σ (j

)(x i ). If for some i , j in { i , j : 0 ≤ j -j ≤ k -1, 1 ≤ i ≤ n, i , j < i, j }, σ(j )(x i ) = σ(j)(x i ) then σ (j)(x i ) takes the value σ (j )(x i ). Otherwise, σ (j)(x i ) takes an arbitrary value from the set {1, . . . , k × n} \ {σ(j )(x i ) : 0 ≤ j -j ≤ k -1, 1 ≤ i ≤ n, i , j < i, j }
which is always possible since the second set has strictly less that k × n elements. One can show that for all c ∈ C and i ≥ 0,

σ i |= c iff σ i |= c. Hence, σ |= φ iff σ |= φ. 2 Proposition 1 No formula of CLTL(N, =) is equivalent to the formula φ x ∞ of CLTL ↓ (N, =).
The flatness concept is only related to occurrences of the freeze quantifier and for instance the formulae of the form φ x ∞ do not belong to the flat fragment. By contrast, ¬φ x ∞ belongs to the flat fragment of CLTL ↓ (N, =). By Proposition 1, the flat fragment of CLTL ↓ (N, =) is therefore strictly more expressive than CLTL(N, =) since CLTL(N, =) is closed under negation.

Equivalent syntactic restrictions. We now show that expressiveness of CLTL ↓ (D) does not change if we restrict the freeze quantifier to refer only to flexible variables in the current state, or if we restrict atomic formulae to contain only rigid variables, or with both restrictions. Therefore, those restrictions could have been incorporated into the definition of the logic. However, we chose to allow terms of the form X n x with flexible x in atomic formulae in order to have CLTL(D) as the freeze-free fragment, and to allow the freeze quantifier to refer to the future so that formulae would be closed under substitution of terms.

Proposition 2 For any formula φ of CLTL ↓ (D), there exists an equivalent formula φ such that:

(I) any occurence of ↓ in φ is of the form ↓ y=x ; (II) FleVars(φ ) = FleVars(φ); (III) RigVars(φ ) = RigVars(φ).
Proof. By structural induction on φ, it suffices to prove the statement for formulae of the form ↓ y=X n x φ where φ satisfies (I).

This can be done by induction on n. The base case n = 0 is trivial. For the inductive step, we use structural induction on φ . The most difficult case is φ = φ 1 Uφ 2 . We then have

↓ y=X n+1 x φ ≡ ↓ y=X n+1 x φ 2 ∨ (φ 1 ∧ Xφ ) ≡ (↓ y=X n+1 x φ 2 ) ∨ ((↓ y=X n+1 x φ 1 ) ∧ X ↓ y=X n x φ )
and the induction hypotheses apply to each of the three freeze subformulae. 2

It is worth observing that in the worst case, in the proof of Proposition 2, φ can be exponentially larger than φ.

Proposition 3 For any formula φ of CLTL ↓ (D), there exists an equivalent formula φ such that:

• atomic formulae in φ contain only rigid variables;

• if any occurence of ↓ in φ is of the form ↓ y=x , then the same is true of φ ; • FleVars(φ ) = FleVars(φ); • |RigVars(φ )| = max{|RigVars(φ)|, k},
where k is the maximum number of distinct terms in any atomic subformula of φ.

Proof. φ is constructed from φ by translating only atomic subformulae of φ. For example, R(X 2 x 1 , y 1 , X 3 x 2 , X 2 x 3 , x 4 , y 2 , x 4 ), where x i ∈ FleVarSet and

y i ∈ RigVarSet, is translated to ↓ y 3 =x 4 X 2 ↓ y 4 =x 1 ↓ y 5 =x 3 X 1 ↓ y 6 =x 2 R(y 4 ,
d i 1 , d i 0 , d i 0 , d i 0 , d i 1 , σ(i)(x 1 ), d i 2 , σ(i)(x 2 ), . . . , d i n , σ(i)(x n )
Using the equality predicate, the values d i j are constrained in φ so that three consecutive equal values occur in σ only at the beginnings of sequences which encode valuations in σ.

The formula φ is a conjunction φ enc ∧ T (φ) where φ enc enforces that models are sequences of sequences of length 2n + 4 of the above form (details are omitted here). Formula T (φ) is inductively defined as follows where start = X(x = Xx ∧ x = XXx ):

• T (R(t 1 , . . . , t m )) = R(T (t 1 ), . . . , T (t m )) where T (y) = y if y is rigid and T (X k x i ) = X k×(2n+4)+3+2i x , • T is homomorphic for Boolean connectives, • T (↓ y=X k x i φ 1 ) =↓ y=T (X k x i ) T (φ 1 ), • T (φ 1 Uφ 2 ) = (start ⇒ T (φ 1 ))U(start ∧ T (φ 2 )), • T (Xφ 1 ) = X 2n+4 T (φ 1 ). 2
The logics CLTL ↓ (D) as defined in Section 2.1 do not in general have propositional variables. If D has at least two elements and equality, then propositional flexible variables, or a flexible variable ranging over a finite alphabet, can be encoded using additional flexible variables over D and equality. A translation as above can then be employed to reduce the number of flexible variables.

For ease of expression, to avoid unnecessary constructs, and because equality on the domain is not necessarily present, arbitrarily many flexible variables and no special finitary variables are considered in the rest of the paper.

3 Decidability results

Finite domain case

In this section, we basically show that, when D is finite (with at least two elements) and contains the equality predicate, CLTL ↓ (D) is ExpSpace-complete. In Theorem 1 below, we establish that ExpSpace-hardness is very common when the freeze quantifier is present.

Theorem 1 Let D be a constraint system with equality such that the underlying domain D contains at least two elements. The satisfiability problem for CLTL ↓ (D) is ExpSpace-hard.

Proof. We prove this result by a reduction from an ExpSpace-complete tiling problem (see e.g. [START_REF] Van Emde | The convenience of tilings[END_REF]). A tile is a unit square of one of several types and the tiling problem we consider is specified by means of a finite set T of tile types (say T = {t 1 , . . . , t l }), two binary relations H (horizontal matching relation) and V (vertical matching relation) over T and two distinguished tile types t init , t f inal ∈ T . The problem consists in determining whether, for a given number n in unary, the region [0, . . . , 2 n -1] × [0, . . . , k -1] of the integer plane for some k can be tiled consistently with H and V , t init is the left bottom tile, and t f inal is the right upper tile.

Given an instance I = T, t init , t f inal , n of the tiling problem, we build a CLTL ↓ (D) formula φ I such that I = T, t init , t f inal , n has a solution iff φ I is CLTL ↓ (D) satisfiable.

We consider the following flexible variables:

• c 1 , . . . , c n are variables that allow to count until 2 n and x 0 , x 1 are variables that will play the role of 0 and 1, respectively; there are corresponding rigid variables c 1 , . . . , c n ; each element α, i of a row [0, . . . ,

2 n -1] × {i} such that the binary representation of α is b 1 . . . b n , satisfies c j = x 0 iff b j = 0 for every j ∈ {1, . . . , n}; • for t ∈ T , z 1 t , z 2 t are variables such that D t := z 1 t = z 2
t is the formula encoding the fact that at a certain position of the integer plane the tile t is present. There are also rigid variables z 1 t , z 2 t and D

t := z 1 t = z 2 t ; • end 1 , end 2 such that END := end 1 = end 2 ;
The formula φ I is the conjunction of the following formulae:

• The region of the integer plane for the solution is finite:

¬END ∧ (¬ENDU(c 1 = • • • = c n = x 0 ∧ G END))
• x 0 and x 1 behave as different constants:

¬(x 0 = x 1 ) ∧ G(x 0 = Xx 0 ∧ x 1 = Xx 1 )
• There is exactly one tile per element of the plane region:

G(¬END ⇒ t∈T (D t ∧ t =t ¬D t ))
• Constraint on the right upper tile:

F( 1≤i≤n (c i = x 1 ) ∧ ¬END ∧ D t f inal ∧ XEND)
• Constraint on the left bottom tile:

1≤i≤n (c i = x 0 ) ∧ D t init • Incrementation of the counters c 1 , . . . , c n : G( 2≤i≤n+1 (( i≤j≤n c j = x 1 ) ∧ c i-1 = x 0 ∧ ¬END) ⇒ ( 1≤j≤i-2 (c j = Xc j ) ∧ Xc i-1 = x 1 ∧ i≤j≤n (Xc j = x 0 ))))
• Limit condition for the incrementation of the counters c 1 , . . . , c n :

G((¬XEND ∧ c 1 = • • • = c n = x 1 ) ⇒ X(c 1 = • • • = c n = x 0 ))
• Horizontal consistency:

G( not the last element of a row ¬(c 1 = • • • = c n = x 1 ) ∧¬END ⇒ t∈T (D t ⇒ t,t ∈H XD t ))
• Vertical consistency:

G(¬END ∧ not on the last row F(X¬END ∧ c 1 = . . . = c n = x 1 ) ⇒ ↓ c 1 =c 1 • • • ↓ c n =c n ↓ z 1 t 1 =z 1 t 1 ↓ z 2 t 1 =z 2 t 1 . . . ↓ z 1 t k =z 1 t k ↓ z 2 t k =z 2 t k X((¬ 1≤i≤n c i = c i )U( 1≤i≤n c i = c i ∧ t∈T (D t ⇒ t,t ∈V XD t ))) It is not difficult to show that the instance I = T, t init , t f inal , n has a solution iff φ I is CLTL ↓ (D) satisfiable. 2
This is reminiscent to the ExpSpace-hardness of Timed Propositional Temporal Logic (TPTL) [START_REF] Alur | A really temporal logic[END_REF]Theorem 2], PLTL+Now (NLTL) [START_REF] Laroussinie | Temporal logic with forgettable past[END_REF]Proposition 4.7] and a variant of the guarded fragment with transitivity [27, Theorem 2]. Our ExpSpace-hardness proof is in the same vein since basically in CLTL ↓ (D) we are able to count till 2 n using only a number of resources polynomial in n and we can compare the truth value of atomic formulae in states of "temporal distance" exactly 2 n .

Our proof is a slight variant of the proof of [14, Theorem 6]: instead of using integer periodicity constraints to count till 2 n , n binary counters are used. Observe also that the resulting formula is not flat because of the encoding of vertical consistency. Theorem 2 Let D be a finite constraint system. The satisfiability problem for CLTL ↓ (D) is in ExpSpace.

Proof. Assume that D = {d 1 , . . . , d l }. We introduce an auxiliary constraint system D = D, P 1 , . . . , P l such that P i = {d i }. For convenience, we write x = d i instead of P i (x). We shall show how to reduce the satisfiability problem for CLTL ↓ (D) into the satisfiability problem for CLTL(D ). PSpace-membership of CLTL(D ) is not very difficult to show and it is a direct consequence of [START_REF] Demri | LTL over integer periodicity constraints[END_REF]Theorem 4].

We introduce a translation T from CLTL ↓ (D) formulae into CLTL(D ) formulae defined as follows:

• T is homomorphic for the Boolean operators and the temporal operators,

• T(R(α 1 , . . . , α n )) def = ( R(d i 1 ,...,d i n ) (α 1 = d i 1 ∧ • • • ∧ α n = d i n )).
So far, the translation can be done in polynomial time and logarithmic space since |D| m is a constant of CLTL ↓ (D) where m is the maximal arity of relations in D. The last clause of T is related to the freeze quantifier:

T(↓ x =α ψ) def = d i ∈D (α = d i ) ⇒ T(ψ) x =d i ,
where T(ψ) x =d i is obtained from T(ψ) by replacing every occurrence of x = d j with j = i by ⊥ and every occurrence of x = d i by . This step requires an exponential blow up and therefore |T(φ)| is exponential in |φ|. It is easy to show that φ is CLTL ↓ (D) satisfiable iff T(φ) is CLTL(D ) satisfiable. Since T may cause at most an exponential blow up and CLTL(D ) is in PSpace, we obtain that CLTL ↓ (D) satisfiability is in ExpSpace. 2

Our proof can be easily adapted if the freeze quantifier is replaced by the full existential quantifier ∃.

Corollary 1 Let D be a finite constraint system with equality such that the underlying domain D contains at least two elements. The satisfiability problem for CLTL ↓ (D) is ExpSpace-complete.

A formula φ ∈ CLTL ↓ (D) is of ↓-height k, for some k ≥ 0, whenever every branch of the formula tree of φ has at most k freeze quantifiers. For example, the formula

↓ x =x (y = x )U ↓ x =z y = x is of ↓-height 2.
Corollary 2 Let D be a finite constraint system. For every k ≥ 0, the satisfiability problem for CLTL ↓ (D) restricted to formulae of ↓-height k is in PSpace.

Flat fragment between CLTL(D) and CLTL ↓ (D)

The main result of this section is to show that the freeze quantifier in the flat fragment of CLTL ↓ (D) can be encoded faithfully into CLTL(D) even though flat CLTL ↓ (D) can be more expressive than CLTL(D), see for instance the case with D = N, = in Section 2.4. However, as shown below, satisfiability for flat CLTL ↓ (N, =) can be reduced in logarithmic space to satisfiability for CLTL(N, =). By analogy, CTL * model-checking can be reduced to LTL modelchecking [START_REF] Emerson | Sometimes" and "Not Never" revisited: on branching versus linear time temporal logic[END_REF] even though CTL * is more expressive than LTL.

It is worth observing that our concept of flatness restricts the interplay between future-time operators and the freeze quantifier as done in [START_REF] Bouajjani | Constrained properties, semilinear sets, and Petri nets[END_REF][START_REF] Comon | Flatness is not a weakness[END_REF][START_REF] Cate | On the complexity of hybrid logics with binders[END_REF] to limit the interaction between modalities and freeze-like quantifiers. In order to understand why flat formulae are more manageable, in a formula like ↓ y=x Fφ that is flat, only the current value of x needs to be stored. By contrast, in a formula like G ↓ y=x φ that is not flat, one needs to store as many values of x as there are positions.

We assume that the flexible variables of CLTL ↓ (D) are {x 0 , x 1 , . . .} and the rigid variables of CLTL ↓ (D) are {y 0 , y 1 , . . .}. For ease of presentation, we assume that the flexible variables of CLTL(D) are composed of the following two disjoint sets: {x 0 , x 1 , . . .} and {y new 0 , y new 1 , . . .}. We define a map u from the flat fragment CLTL ↓ (D) into CLTL(D) as follows: u replaces each y j by y new j in atomic formulae, it is homomorphic for Boolean and temporal operators, and

u(↓ y=X n x ψ) def = y new = X n x ∧ G(y new = Xy new ) ∧ u(ψ)
It is easy to show that u(φ) can be computed in logarithmic space in |φ|.

Proposition 5 Let D be a constraint system with equality. For any formula φ of the flat fragment of CLTL ↓ (D), φ is CLTL ↓ (D) satisfiable iff u(φ) is CLTL(D) satisfiable.

Proof. Given a model σ of CLTL ↓ (D), an environment ρ and a formula φ we say that the model σ of CLTL(D) agrees with σ, ρ and φ iff for all i, j ≥ 0, σ(i)(x j ) = σ (i)(x j ) and for all free rigid variable y j in φ and i ≥ 0, σ (i)(y new j ) = ρ(y j ).

We shall use the following basic properties:

• u(ψ) = ψ if ψ belongs to CLTL(D).
• If σ agrees with σ, ρ and ψ then (σ ) i agrees with σ i , ρ and ψ for every i ≥ 0.

Given the occurrence of a subformula ψ in φ with positive [resp. negative] polarity, we write the sign s ψ to denote the empty string [resp. ¬]. By abusing notation, we do not distinguish subformulae from occurrences.

We shall show by structural induction that for any occurrence of a subformula ψ in φ, for all models σ of CLTL ↓ (D) and environment ρ, σ |= ρ s ψ ψ iff there is σ that agrees with σ, ρ and ψ such that σ |= s ψ u(ψ). Statement of the lemma is then immediate.

The base case with atomic formulae and the cases in the induction step with ¬, ∧ and X are by an easy verification. By way of example, we treat the case with ψ = ¬ψ with negative polarity. So ψ occurs with positive polarity. Let σ be a model and ρ be an environment such that σ |= ρ ¬¬ψ . The statements below are equivalent:

• σ |= ρ ¬¬ψ , • σ |= ρ ψ ,
• there is σ that agrees with σ, ρ and ψ such that σ |= u(ψ ) (by (IH) and change of polarity), • there is σ that agrees with σ, ρ and ψ such that σ |= ¬u(¬ψ ) (by definition of u).

Let us treat the remaining cases.

Case 1 : ψ = ψ 1 Uψ 2 with positive polarity. Since φ belongs to the flat fragment, we have ψ 1 = u(ψ 1 ). Let σ be a model and ρ be an environment such that σ |= ρ ψ. The statements below are equivalent:

• σ |= ρ ψ,
• there is i ≥ 0 such that σ i |= ρ ψ 2 and for every j < i, σ j |= ρ ψ 1 ,

• there is σ that agrees with σ, ρ and ψ 2 such that (σ ) i |= u(ψ 2 ) and for every j < i, (σ ) j |= u(ψ 1 ) (by (IH), ψ 1 = u(ψ 1 ) and, σ and σ agree on flexible variables of ψ 1 ), • there is σ that agrees with σ, ρ and ψ such that σ |= u(ψ 1 )Uu(ψ 2 ) (ψ 1 has no free rigid variable).

Case 2 : ψ = ψ 1 Uψ 2 with negative polarity. Since φ belongs to the flat fragment, we have ψ 2 = u(ψ 2 ) and both ψ 1 and ψ 2 have negative polarity. Let σ be a model and ρ be an environment such that σ |= ρ ψ. The statements below are equivalent:

• σ |= ρ ¬ψ,
• either there is j ≥ 0 such that σ j |= ρ ¬ψ 1 and for every j ≤ i, σ i |= ρ ¬ψ 2 or for every i ≥ 0, σ i |= ρ ¬ψ 2 , • either there is σ that agrees with σ, ρ and ψ 1 such that there is j ≥ 0 such that (σ ) j |= ¬u(ψ 1 ) and for every j ≤ i, (σ ) i |= ¬u(ψ 2 ) (by (IH) and ψ 2 = u(ψ 2 )) or there is σ that agrees with σ, ρ and ψ 2 such that for every i ≥ 0, (σ ) i |= ¬u(ψ 2 ) (by (IH)), • there is σ that agrees with σ, ρ and ψ 1 Uψ 2 such that either there is j ≥ 0 such that (σ ) j |= ¬u(ψ 1 ) and for every j ≤ i, (σ ) i |= ¬u(ψ 2 ) or for every i ≥ 0, (σ ) i |= ¬u(ψ 2 ) (ψ 2 has no free rigid variables), • there is σ that agrees with σ, ρ and ψ 1 Uψ 2 such that σ |= ¬(u(ψ 1 )Uu(ψ 2 )).

Case 3 : ψ =↓ y=X n x ψ . Let σ be a model and ρ be an environment for s ψ and ψ. The statements below are equivalent:

• σ |= ρ s ψ ψ, • σ |= ρ[y →σ(n)(x)] s ψ ψ ,
• there is σ that agrees with σ, ρ[y → σ(n)(x)] and ψ such that σ |= s ψ u(ψ ) (by (IH)), • there is σ that agrees with σ, ρ[y → σ(n)(x)] and ψ such that σ |= s ψ u(ψ ) and σ |= G(y new = Xy new ) ∧ y new = X n x (y free in ψ ). • there is σ that agrees with σ, ρ and ψ such that σ |= s ψ u(ψ ) ∧ G(y new = Xy new ) ∧ y new = X n x (ψ has less free rigid variable than ψ ). 2

Corollary 3 For every constraint system D which contains equality, decidability of CLTL(D) implies decidability of the flat fragment of CLTL ↓ (D).

Since CLTL( Z, <, = ), CLTL( N, <, = ) and CLTL( R, <, = ) are PSpace-complete [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF], we can establish the following corollary.

Corollary 4 Flat fragments of each of CLTL ↓ ( Z, <, = ), CLTL ↓ ( N, <, = ), CLTL ↓ ( R, <, = ), and CLTL ↓ (D) with D finite are PSpace-complete.

Corollary 4 can be also adapted to the PSpace-complete constrained version of LTL introduced in [START_REF] Demri | Verification of qualitative Z-constraints[END_REF].

Undecidability results

In this section, we shall prove that, if the domain is infinite, and if we do not restrict to flat formulae, the satisfiability problem for CLTL ↓ (D) is undecidable even if we only have the equality predicate. More precisely, Theorem 3 below is a stronger result, stating that satisfiability is Σ 1 1 -hard, even restricted to formulae with 1 flexible variable and at most 2 rigid variables. (An exposition of the analytical hierarchy can be found in [START_REF] Rogers | Theory of Recursive Functions and Effective Computability[END_REF].) A corollary of Σ 1 1 -hardness is that the logic cannot be recursively axiomatised.

The following proposition complements the main result in this section, and states that, for countable and computable constraint systems D, satisfiability for CLTL ↓ (D) is in Σ 1 1 . Hence, for a countably infinite domain, the problem in Theorem 3 is Σ 1 1 -complete.

Proposition 6 If D is countable, and (R i ) i∈I is a countable family of computable relations on D, then the satisfiability problem for CLTL

↓ (D, (R i ) i∈I ) is in Σ 1 1 .
Proof. Let φ be a formula of CLTL ↓ (D, (R i ) i∈I ). We can assume FleVarSet = A first-order predicate on f 1 , . . . , f n and a 1 , . . . , a m which expresses that σ |= ρ φ is routine to construct by structural recursion on φ. We conclude that satisfiability of φ can be expressed by a Σ 1 1 -sentence. 2

We shall prove that the satisfiability problem for a fragment of CLTL ↓ (D, =) is Σ 1 1 -hard by reducing from the Recurrence Problem for nondeterministic 2-counter machines, which was shown to be Σ A nondeterministic 2-counter machine M consists of two counters C 1 and C 2 , and a sequence of n ≥ 1 instructions, each of which may increment or decrement one of the counters, or jump conditionally upon of the counters being zero. After the execution of a non-jump instruction, M proceeds nondeterministically to one of two specified instructions. Therefore, the l th instruction is written as one of the following:

l : C i := C i + 1; goto l or goto l l : C i := C i -1; goto l or goto l l : if C i = 0 then goto l else goto l
We represent the configurations of M by triples l, c 1 , c 2 , where 1 ≤ l ≤ n, c 1 ≥ 0, and c 2 ≥ 0 are the current values of the location counter and the two counters C 1 and C 2 , respectively. The consecution relation on configurations is defined in the obvious way, where decrementing 0 yields 0. A computation of M is an ω-sequence of related configurations, starting with the initial configuration 1, 0, 0 . The computation is recurring if it contains infinitely many configurations with the value of the location counter being 1.

Recurrence Problem is to decide, given a nondeterministic 2-counter machine M , whether M has a recurring computation. This problem is Σ 1 1 -hard.

Theorem 3 If D is infinite, then the satisfiability problem for CLTL ↓ (D, =)

with |FleVarSet| = 1 and |RigVarSet| = 2 is Σ 1 1 -hard. Proof. Suppose M is a nondeterministic 2-counter machine. We construct a formula φ M of CLTL ↓ (D, =) such that |FleVars(φ)| = 1, |RigVars(φ)| = 2,
and φ M is satisfiable iff M has a recurring computation. The basis of the construction is an encoding of computations of nondeterministic 2-counter machines by models of CLTL ↓ (D, =) with one flexible variable, i.e. by ωsequences of elements of D. As in the proofs of [12, Theorems 6 and 7], which show Σ 1 1 -hardness of satisfiability of formulae of TPTL extended with either multiplication by 2 or dense time, we shall encode the value of a counter by a sequence of that length. However, much further work is needed in this proof because the only operation we have on elements of D is equality.

Let n be the number of instructions in M . We encode a configuration l, c 1 , c 2 by a sequence of elements of of the form

ddd d . . . d . . . n f 1 1 . . . f 1 c 1 eee e f 2 1 . . . f 2 c 2
where:

(i) the only two pairs of equal consecutive elements are dd and ee, and also f 2 c 2 is distinct from the first element in the encoding of the next configuration, (ii) e = e , (iii) after the first 4 elements, there is a sequence of n elements, and only the l th equals d , (iv) f i 1 , . . . , f i c i are mutually distinct, for each i.

φ init n def = start d ∧ X 2 x = X 4 x ∧ X n+4 (start e ∧ X 4 (start d∨e )) φ glob n def = G(start d ⇒ ψ 1 n ∧ start e ⇒ ψ 2 n ) ψ 1 n def = in dd d...d ... any two consecutive values are distinct n+3 i=1 X i x = X i+1 x ∧ in ...d ... exactly one value equals d   n l=1 X 2 x = X l+3 x ∧   l-1 j=1 X 2 x = j+3 x ∧ n j=l+1 X 2 x = X j+3 x     ∧ f 1 1 ...f 1 c 1 mutually distinct X n+4 (ψ dist U start e ) ψ 2 n def = 3 i=1 X i x = X i+1 x ∧ f 2 1 ...f 2 c 2 mutually distinct X 4 (ψ dist U start d ) ψ dist def = ¬start d∨e ∧ ↓ y=x X((¬start d∨e ∧ x = y)U start d∨e )
We write start d∨e to denote the formula x = X 1 x stating that the current state is an occurrence of either dd or ee. We write start d [resp. start e ] to denote the formula start

d∨e ∧ x = X 3 x [resp. start d∨e ∧ x = X 3 x] stating the current state is a first occurrence of d [resp. e] in dd [ee].
The formula φ M is defined as a conjunction

φ init n ∧ φ glob n ∧ φ 1 M ∧ • • • ∧ φ n M ∧ φ rec
where the first two conjuncts state that the model is a concatenation of configuration encodings which satisfy (i)-(iv) above, and that it begins with an of the initial configuration 1, 0, 0 . Their definitions are given in Figure 1.

For any l ∈ {1, . . . , n}, φ l M states that, whenever the model contains an encoding of a configuration l, c 1 , c 2 , then the next encoding is of a configuration which is obtained by executing the l th instruction.

Consider the most complex case: l : C 2 := C 2 -1; goto l or goto l . The formula φ l M needs to state that, whenever the location counter is l, C 1 remains the same, C 2 either remains 0 or is decremented, and the next value of the location counter is either l or l :

χ 2 dec def = 0≤C 2 ≤1 and the next value of C 2 equals 0 ((x = X 1 x ∨ X 1 x = X 2 x) ∧ (¬start e U(start e ∧ X 4 (x = X 1 x))) ∨ ( C 2 >1 ¬(x = X 1 x ∨ X 1 x = X 2 x) ∧ (A) (↓ y=x ¬start e U(start e ∧ X 4 (¬start d ∧ x = y))) ∧ (B) ((¬X 2 start d∨e ∧ (↓ y=x X ↓ y =x (¬start e U(start e ∧ X 4 (x = yU(x = y ∧ X 1 x = y ))))))UX 2 start d∨e ) ∧ (C) ((X 2 ¬start d )U(X 2 start d ∧ ↓ y=x ¬start U(start e ∧ X 4 (x = yU (x = y ∧ ¬start d ∧ X 2 start d )))))
Fig. 2.

φ l M def = G((start d ∧ X 2 x = X l+3 x) ⇒ X n+4 (χ 1 eq ∧ (¬start d∨e U(start e ∧ X 4 (χ 2 dec ∧ (¬start d∨e U(start d ∧ (X 2 x = X l +3 x ∨ X 2 x = X l +3 x))))))))
The formula χ 2 dec given in Figure 2 specifies that, if the current value of C 2 is either 0 or 1, then the next value of C 2 is 0; and if neither, then the next encoding of the value of C 2 equals the current encoding with the last element removed.

The latter is specified as the following conjunction:

(A) the first element of the current encoding equals the first element of the next encoding, and (B) for any consecutive pair y and y of elements in the current encoding such that y is not the last element, the first occurence of y in the next encoding is followed by y , and (C) the element before the last in the current encoding is the last element in the next encoding.

The formula χ 1 eq , which specifies that the value of C 1 remains the same, is defined similarly.

Definitions of φ l

M for other forms of instruction use the same machinery. For incrementing a counter, it is not necessary to specify that the additional element in the next encoding is distinct from the rest, because that is ensured by φ glob n .

Finally, φ rec def = GF(start d ∧ X 2 x = X 4 x) states that the model encodes a recurring computation. 2 By Propositions 2 and 3, we have that Theorem 3 can be strengthened by restricting to the fragment of CLTL ↓ (D, =) with |FleVarSet| = 1, |RigVarSet| = 2 and such that the flexible variable occurs only in freeze quantifiers of the form ↓ y=x .

By adapting the proof of Theorem 3, the variant of CLTL ↓ (D, =) over models which are finite words is also undecidable, more precisely Σ 0 1 -hard through encoding the Halting Problem for 2-counter machines. This should be compared with the undecidability universality of 1-way nondeterministic register automata [START_REF] Neven | Finite state machines for strings over infinite alphabets[END_REF]Theorem 5.1].

The proof of Theorem 3 can also be modified to yield, for CLTL ↓ (D, =) augmented with the past-time operator U -1 ('since') but restricted to 1 rigid variable, Σ 1 1 -hardness over infinite models and Σ 0 1 -hardness over finite models. The sets of values from D which are used to encode counter values do not have to be enumerated in the same order for consecutive configurations, and simpler logical formulae suffice. These results are related to the undecidability of emptiness of 2-way deterministic register automata: see [START_REF] David | Mots et données infinies[END_REF]Section 7], [START_REF] Neven | Finite state machines for strings over infinite alphabets[END_REF]Theorem 5.3].

Related work

In this section, we compare the logic CLTL ↓ (N, =) and the results in this paper with a number of related works in the literature. We show that there is a surprising variety of formalisms which involve the freeze quantifier or related constructs, revealing links among several works which appear unconnected. This confirms that the binding mechanism of the freeze quantifier is fundamental.

LTL over concrete domains. Complexity results for Constraint LTL over concrete domains can be found in [START_REF] Wolter | Spatio-temporal representation and reasoning based on RCC-8[END_REF][START_REF] Balbiani | Computational complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning[END_REF][START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF][START_REF] Gabelaia | On the computational complexity of spatio-temporal logics[END_REF][START_REF] Demri | LTL over integer periodicity constraints[END_REF] (see also related results for description logics over concrete domains in [START_REF] Lutz | NEXPTIME-complete description logics with concrete domains[END_REF]). Decidability and complexity issues for LTL over Presburger constraints have been studied for instance in [START_REF] Bouajjani | On the verification problem of nonregular properties for nonregular processes[END_REF][START_REF] Bouajjani | Constrained properties, semilinear sets, and Petri nets[END_REF][START_REF] Comon | Flatness is not a weakness[END_REF][START_REF] Demri | LTL over integer periodicity constraints[END_REF]. Most decision procedures in the above-mentioned works are automata-based whereas undecidability proofs often rely on an easy encoding of the Halting Problem for 2-counter machines.

LTL over integer periodicity constraints augmented with the freeze quantifier is shown ExpSpace-complete [START_REF] Demri | LTL over integer periodicity constraints[END_REF] but CLTL(N, <, =) with past-time operator F -1 and ↓ is undecidable [START_REF] Demri | LTL over integer periodicity constraints[END_REF].

Real-time logics. Similar issues for real-time and modal logics equipped with the freeze quantifier have been considered in [START_REF] Alur | A really temporal logic[END_REF][START_REF] Henzinger | Half-order modal logic: how to prove real-time properties[END_REF][START_REF] Harel | Explicit clock temporal logic[END_REF][START_REF] Brihaye | Model-checking for weighted timed automata[END_REF]. In spite of its rich language of constraints, TPTL model-checking is decidable [START_REF] Alur | A really temporal logic[END_REF] (discrete version). In this case, decidability is due to the subtle combination of the constraint system and the semantical restrictions (see also versions of metric temporal logics in [START_REF] Alur | A really temporal logic[END_REF][START_REF] Alur | The benefits of relaxing punctuality[END_REF]).

The class of logics CLTL ↓ (D) defined in this paper is quite general and it is not difficult to show that discrete-time TPTL [START_REF] Alur | A really temporal logic[END_REF] is exactly the fragment of CLTL ↓ (D) where In [START_REF] Alur | A really temporal logic[END_REF]Theorem 5], Σ 1 1 -hardness of satisfiability for TPTL without the monotonicity condition on time sequences is established. By Propositions 2 and 3, CLTL ↓ (N, =) restricted to one flexible variable can be seen as the fragment of TPTL where there are no atomic propositions, and where the only operation on time is equality. Moreover, it is straightforward to see that Theorem 3 in this paper still holds when satisfiability is restricted to models which contain infinitely many values, which is equivalent to the progress condition when the domain is N. Therefore, a corollary of Theorem 3 is the following strengthening of [START_REF] Alur | A really temporal logic[END_REF]Theorem 5]: satisfiability for TPTL without the monotonicity condition remains Σ 1 1 -complete even without atomic propositions and with only equality constraints. (The proof of [START_REF] Alur | A really temporal logic[END_REF]Theorem 5] uses arithmetic on time values.) Hybrid, navigation, spatio-temporal, and similar logics. Hybrid logics (see e.g. [START_REF] Goranko | Hierarchies of modal and temporal logics with references pointers[END_REF][START_REF] Areces | A road-map on complexity for hybrid logics[END_REF][START_REF] Franceschet | Hybrid logics on linear structures: Expressivity and complexity[END_REF]) contain a variable-binding mechanism similar to the freeze quantifier: ↓ x φ(x) holds true iff φ(x) holds true when the propositional variable x is interpreted as a singleton containing the current state. The downarrow binder in such hybrid logics records the value of the current state.

• D = N and
Similarly, in temporal logic with forgettable past [START_REF] Laroussinie | Temporal logic with forgettable past[END_REF], the effect of the Now operator is that the origin of time takes the value of the current state: the states before the current state are forgotten. Identical mechanisms are used in navigation logics for object structures, see e.g. [START_REF] De Boer | Decidable navigation logics for object structures[END_REF] and in half-order dynamic temporal logics interpreted over traces from sequence diagrams [START_REF] Cho | A semantics of sequence diagrams[END_REF].

In the context of spatio-temporal logics, Wolter and Zakharyaschev [START_REF] Wolter | Spatio-temporal representation and reasoning based on RCC-8[END_REF]Section 7] advocate the need to consider operators expressing constraints of the form i∈N R(x, X i y) and i∈N R(x, X i y). They are simple to express in CLTL ↓ (D), as ↓ x =x GR(x , y) and ↓ x =x FR(x , y). These formulae are in the flat fragment: see Section 3.2.

Quantified propositional temporal logic with repeating. The models of Quantified Propositional Temporal Logic with Repeating (also known as RQPTL) introduced in [START_REF] French | Quantified propositional temporal logic with repeating states[END_REF] can be encoded by CLTL ↓ (N, =) formulae, unlike the second-order quantification in the language. Such models are pairs of maps µ : N → S, π : S → 2 AP where S is an arbitrary set (of states). A possible encoding is by treating µ as the interpretation of a distinguished flexible variable, and using the freeze quantifier to specify that, whenever µ(i) = µ(j), any propositional variable has the same values at time points i and j. (See Section 2.4 regarding encodings of propositional variables.)

On the other hand, the variant logic RHLTL n [44, Section 4] can be shown equivalent to CLTL ↓ (N, =) with one flexible variable and n rigid variables, except that RHLTL n does not have the U operator but has F and the pasttime operators F -1 and X -1 . Theorem 3 in this paper and Σ 1 1 -hardness of RHLTL 2 [44, Corollary 1] are therefore complementary results.

Predicate λ-abstraction. A number of decidability and undecidability results for half-order modal logics (to be compared with [START_REF] Henzinger | Half-order modal logic: how to prove real-time properties[END_REF]) are presented in [START_REF] Fitting | Modal logic between propositional and first-order[END_REF]. The half-order aspect of such logics is due to a predicate λ-abstraction mechanism, which solves the famous problem of interpreting constants in modal logic. Even though this construct is essentially the same as the freeze quantifier, apparently there have been no cross-references between the literature dealing with predicate λ-abstraction (e.g. [START_REF] Fitting | Modal logic between propositional and first-order[END_REF][START_REF] Lisitsa | Temporal logic with predicate λ-abstraction[END_REF]) and that dealing with the freeze quantifier (e.g. [START_REF] Henzinger | Half-order modal logic: how to prove real-time properties[END_REF][START_REF] Alur | A really temporal logic[END_REF][START_REF] Demri | LTL over integer periodicity constraints[END_REF][START_REF] Demri | On the freeze quantifier in constraint LTL: decidability and complexity[END_REF]). However, several undecidability results for LTL-like logics with predicate λ-abstraction have recently been obtained in [START_REF] Lisitsa | Temporal logic with predicate λ-abstraction[END_REF], independently and concurrently with [START_REF] Demri | On the freeze quantifier in constraint LTL: decidability and complexity[END_REF]. The most related to Theorem 3 in this paper are Σ 1 1 -hardness results for the following logics:

(I) LTL λ= with temporal operators X and U, and with 3 rigid variables;

(II) LTL λ with temporal operators X and U, and with countably infinitely many unary predicate symbols (but no equality).

Remarkably, LTL λ= is essentially the same as CLTL ↓ (N, =). The proofs of (I) in [START_REF] Lisitsa | Temporal logic with predicate λ-abstraction[END_REF] and of Theorem 3 above reduce from the same Σ 1 1 -hard problem. However, the encodings are different, enabling Theorem 3 to be sharper by restricting to 1 flexible and 2 rigid variables.

An interesting discussion of applications to dynamic systems with resources, like communication protocols for mobile agents, can also be found in [START_REF] Lisitsa | Temporal logic with predicate λ-abstraction[END_REF].

Monodic first-order temporal logics. Since freeze quantification is firstorder quantification over a singleton set, the freeze quantifier can be expressed in first-order temporal logics [START_REF] Degtyarev | Equality and monodic first-order temporal logic[END_REF][START_REF] Wolter | Axiomatizing the monodic fragment of first-order temporal logic[END_REF][START_REF] Hodkinson | On the computational complexity of decidable fragments of first-order linear temporal logics[END_REF][START_REF] Gabbay | Many-dimensional modal logics: theory and practice[END_REF]. Indeed, CLTL ↓ (N, =) satisfiability can be reduced to first-order temporal logic T L satisfiability over the linear structure N, < (the latter logic was introduced in [49, Chapter 11]). To each flexible variable x one associates a monadic predicate symbol P x in such a way that P x is interpreted as the singleton set containing the value of x. A formula of the form ↓ x =Xx φ is then translated to ∃x XP x (x ) ∧ φ where φ is the translation of φ. The translation is homomorphic for Boolean and temporal operators, whereas for instance y = Xz with y, z ∈ FleVarSet is translated into ∃x P y (x) ∧ XP z (x). One needs also to be able to express that at every state P x is interpreted by a singleton, which can be encoded by the formula G(∃z P x (z) ∧ ∀z, z (P x (z) ∧ P x (z ) ⇒ z = z )).

Consider the fragment of CLTL ↓ (N, =) with |RigVarSet| = 1. It is easy to check that its translation is contained in the monodic fragment of T L with equality, and with only two individual variables and monadic predicate symbols. We recall that in the monodic fragment, any temporal subformula (i.e. whose outermost construct is a temporal operator) must have at most one free individual variable. Even though monodic T L over N, < is decidable [START_REF] Hodkinson | Decidable fragments of first-order temporal logics[END_REF], its extension with equality is not [START_REF] Wolter | Axiomatizing the monodic fragment of first-order temporal logic[END_REF], even with the above restrictions [START_REF] Degtyarev | Equality and monodic first-order temporal logic[END_REF].

Logics and automata for data languages. In [START_REF] Bouyer | An algebraic approach to data languages and timed languages[END_REF][START_REF] Bouyer | A logical characterization of data languages[END_REF], data languages are defined as sets of finite data words in (Σ × D) * where Σ is a finite alphabet and D is an infinite domain (generalising the concept of timed languages), and automata which recognise data languages are introduced. The latter are related to register and pebble automata for strings over infinite alphabets (e.g. [START_REF] Neven | Finite state machines for strings over infinite alphabets[END_REF]).

First-order logic over finite data word models is considered in [START_REF] Bojańczyk | Two-variable logic on words with data[END_REF], with motivations stemming from query languages for semistructured data. More precisely, the carrier of a model is the set of positions in a data word, there are no function symbols, the unary predicates correspond to elements of Σ, and there are binary predicates <, +1, as well as ∼ which is interpreted as equality of elements of D at given positions. FO k (∼, <, +1) denotes such a logic with k variables. The main result of [START_REF] Bojańczyk | Two-variable logic on words with data[END_REF] is that satisfiability of FO 2 (∼, <, +1) is decidable, by a doubly exponential-time reduction to emptiness of multicounter automata. (The latter problem is decidable, but there is no known elementary upper bound.)

The following variant of CLTL ↓ (D, =) has models which are words over Σ×D: there is one flexible variable x which takes values in D, plus one flexible variable l which takes values in Σ and on which freeze quantification cannot be used, but to which unary predicates P a for equality testing with a ∈ Σ can be applied. Interestingly, that logic with infinite D and 1 rigid variable is incomparable with FO 2 (∼, <, +1). In one direction, FO 2 (∼, <, +1) cannot express the U operator, and also not formulae of the form ↓ y=x φ where y occurs in φ under two or more temporal operators. In the other direction, FO 2 (∼, <, +1) can express past-time operators such as F -1 .

Conclusion

We have shown that adding the freeze quantifier to CLTL(D) leads to undecidability as soon as the underlying domain is infinite and the equality predicate is part of D. As illustrated in the paper, in most related work dealing with undecidable logics having a binding mechanism similar to freeze quantification, either past-time operators can be encoded or constraints richer than equality are available.

The logic CLTL ↓ (D) is ExpSpace-complete for most of finite domains D. In order to design a specification language over infinite domains with LTL temporal operators and the freeze quantifier that admits a decidable modelchecking problem, syntactic restrictions could be a reasonable solution. The existence of a logarithmic-space reduction from the flat fragment of CLTL ↓ (D) into CLTL(D) when the equality predicate is present leads us to believe that the flatness criterion is most relevant here.

As we have seen, the following fragments/variants of CLTL ↓ (D, =) with infinite D and |FleVarSet| = 1 are Σ 1 1 -hard:

• the temporal operators are X and U, and |RigVarSet| = 2;

• the temporal operators are X, U and U -1 , and |RigVarSet| = 1;

• the temporal operators are X, X -1 , F and F -1 , and |RigVarSet| = 2;

It is open whether the intersections of these fragments are decidable.

Other open problems include:

• decidability in the presence of semantic restrictions such as reversal bound-edness [START_REF] Ibarra | Reversal-bounded multicounter machines and their decision problems[END_REF] of a flexible variable; • decidability over infinite domains without equality (and where equality is not definable by other predicates), such as {0, 1} * , < with < being either the strict prefix relation or the strict subword relation.

  If we replace U by F, then NExpTime-hardness can be shown by reducing from the n × n tiling problem with n encoded in binary. Finiteness of D allows us to show the decidability of CLTL ↓ (D).

  complexity of CLTL ↓ (D) with finite D and restricted to the 'sometimes' operator F is still open. (NExpTime-hardness and ExpSpace upper bound are known.)

  FleVars(φ) and RigVarSet = RigVars(φ). Let n = |FleVarSet|, m = |RigVarSet|. Any model σ : N → (FleVarSet → D) can be encoded by functions f 1 , . . . , f n : N → N, and any environment ρ : RigVarSet → D as an m-tuple a 1 , . . . , a m : N.

1 1 -

 1 hard in [12, Section 4.1].

Fig. 1 .

 1 Fig. 1.

  the only flexible variable is t (time),• the predicates of D are(x ≤ c) c∈Z , (x ≤ y + c) c∈Z , (x ≡ d c) c,d∈N , (x ≡ d y + c) c,d∈Nwhere ≡ d is equality modulo d, and • the formulae are of the form G(t ≤ Xt) ∧ GF(t < Xt) ∧ φ with any use of the freeze quantifier being of the form ↓ x=t .

  y 1 , y 6 , y 5 , y 3 , y 2 , y 3 ) where y 3 , . . . , y 6 are drawn from RigVars(φ) \ {y 1 , y 2 }. If that set does not have enough elements, new rigid variable names are used. The latter can then be reused in translations of other atomic subformulae. 2Flexible and finitary variables. If the domain D has at least two elements, and if the equality predicate is present, then formulae and models of CLTL ↓ (D) with n ≥ 2 flexible variables can be translated to the fragment with only one flexible variable.Proposition 4 Let D be a constraint system with at least two elements and equality. For any formula φ of CLTL ↓ (D), one can compute in logarithmic space a formula φ of CLTL ↓ (D) with a unique flexible variable and the same set of rigid variables as φ, such that φ is satisfiable iff φ is satisfiable.Proof. Let φ be a formula of CLTL ↓ (D) with flexible variables x 1 , . . . , x n . We shall build in logspace a formula φ of CLTL ↓ (D) with only one flexible variable x and the same set of rigid variables as φ, such that σ |=

ρ φ iff there exists σ with σ |= ρ φ and σ is an encoding of σ in the following sense. A valuation σ(i) : {x 1 , . . . , x n } → D is encoded by 2n + 4 consecutive values of x in σ which form a sequence

Acknowledgements. We are grateful to Deepak D'Souza, Claire David, Anca Muscholl and Luc Segoufin for helpful discussions, and to Frank Wolter for having directed us to related work.

 [START_REF] Demri | On the freeze quantifier in constraint LTL: decidability and complexity[END_REF]Supported by the ACI "Sécurité et Informatique" Cortos. 2 Supported by an invited professorship from ENS Cachan, and by grants from the EPSRC (GR/S52759/01) and the Intel Corporation. Also affiliated to the Mathematical Institute, Serbian Academy of Sciences and Arts, Belgrade. 3 Supported by the ACI "Sécurité et Informatique" Persée and by the e-Society project of MEXT. A part of this work was done while affiliated to LSV, CNRS & ENS Cachan, and Department of Information Science, University of Tokyo.