Stéphane Demri

Linear-time Temporal Logics with Presburger Constraints: an Overview 1

Keywords: logique temporelle, arithmétique de Presburger, automate de Büchi, complexité temporal logic, Presburger arithmetic, Büchi automaton, computational complexity

Ce papier présente un panorama de logiques temporelles du temps linéaire avec contraintes de Presburger dont les modèles sont des séquences de tuples d'entiers. De tels langages formels permettent de spécifier et vérifier certaines propriétés des systèmes à compteurs. Le papier rappelle le cadre général de LTL avec domaines concrets et présente les principaux résultats de décidabilité et complexité des fragments de LTL avec contraintes de Presburger. Une comparaison avec des formalismes alternatifs ou voisins est aussi ébauchée.

ABSTRACT. We present an overview of linear-time temporal logics with Presburger constraints whose models are sequences of tuples of integers. Such formal specification languages are welldesigned to specify and verify systems that can be modelled with counter systems. The paper recalls the general framework of LTL over concrete domains and presents the main decidability and complexity results related to fragments of Presburger LTL. Related formalisms are also briefly presented.

Introduction

Temporal logics. Temporal logics are standard formal specification languages to verify and specify complex systems/programs, see e.g. [START_REF] Pnueli | The temporal logic of programs[END_REF][START_REF] Bérard | Systems and Software Verification, Model-Checking Techniques and Tools[END_REF]. Such languages allow the user to specify by means of temporal formulae the properties which a program must satisfy and to verify that the specifications are met. Temporal logics are well-studied formalisms to specify the behavior of finite-state systems and the computational complexity of the model-checking problems is nowadays well-known, see e.g. a survey in [START_REF] Schnoebelen | The complexity of temporal logic model checking[END_REF]. However, it is known that many systems such as communication protocols have infinitely many configurations and usually the techniques for the finite case cannot be applied directly. Unfortunately, for numerous classes of 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 (Revesz, 2002, Chapter 6)). Actually, simpler problems such as reachability are already undecidable. Nevertheless, remarkable classes of infinite-state systems admit decidable model-checking problems, such as timed automata (Alur et al., 1994a) 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] Leroux | Flat counter systems are everywhere ![END_REF]. More specifically, fragments of LTL with Presburger constraints have been shown decidable over appropriate counter automata in [START_REF] Čerans | Deciding Properties of Integral Relational Automata[END_REF][START_REF] Comon | Flatness is not a weakness[END_REF][START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF]. We recall that Presburger arithmetic [START_REF] Presburger | Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt[END_REF] is the first-order theory of integers with addition (but without multiplication) and, it can be shown to be decidable by quantifiers elimination.

Content of the paper. The paper presents an overview of linear-time temporal logics over constraint systems and more precisely of fragments of Presburger arithmetic. Such logical formalisms allow to express effects of basic instructions in programs. For instance, a formula of the form F(x = Xy) states that eventually the value of the variable x is going to be equal to the next value of y. Decidability and complexity issues for satisfiability and model-checking about constrained automata (viewed as models for systems/programs) are discussed along the paper and we provide a generous amount of examples. Hence, we present the main framework for linear-time temporal logics over constraints systems, extending the standard logic LTL [START_REF] Sistla | The complexity of propositional linear temporal logic[END_REF]. We explain why symbolic representation of concrete models of the logics is needed and how symbolic models can be recognized by automata accepting ω-words languages. Most of our decidability results are based on the automata-based approach from [START_REF] Vardi | Reasoning about Infinite Computations[END_REF] but we cannot apply this method directly since the models of the logics are ω-sequences of valuations (providing an infinite alphabet incompatible with standard Büchi automata). Decidability and complexity results for fragments and for extensions of Presburger LTL are thoroughly presented whereas some undecidable logics are precisely placed in the arithmetical and analytical hierarchies. Finally, we illustrate the main concepts on simple examples and the results presented herein in details are compared to alternative formalisms.

Most of the results stated in the paper are presented in details in other papers. We have taken a special care to make uniform the notations and to provide a great amount of relevant bibliographical references.

Plan of the paper. The structure of the paper is the following. Section 2 introduces the framework of linear-time temporal logics over constraint systems and presents fragments of Presburger arithmetic useful in the rest of the paper. In Section 3, we present various fragments of LTL over constraint systems (some of them based on fragments of Presburger arithmetic) whose satisfiability problem is undecidable. In most cases, runs of Minsky machines can be simulated. The main proof technique to show decidability is presented in Section 4 where the relationships between satisfiability and symbolic models are clearly stated. This unifies known decidability proofs. As explained in Section 4, it still remains to check properties assumed in the main theorem. Decidability results are stated in Section 5 including those for which the constraint system has integer periodicity constraints or for which the class of symbolic models for a given formula is not necessarily ω-regular. A quite remarkable result is that model-checking one-counter automata with LTL over quantifier-free Presburger arithmetic is PSPACE-complete. Decidability and complexity results in presence of the freeze operator are presented in Section 6. In particular the presence of this powerful binding mechanism with the poor constraint system N, = already produces highly undecidable problems. On the decidability side, effective procedures can be designed with one rigid variable and finite models, or with integer periodicity constraints, to quote a few examples. Related formalisms are compared with the ones presented in the paper in Section 7. The main goal of this section is to provide the reader useful bibliographical references to other works related to (temporal) logics and Presburger constraints.

LTL over constraint systems

Linear-time temporal logic LTL equipped with "next-time" operator X, "until" operator U and their past-time counterparts is known to be equivalent to first-order theory of successors [START_REF] Kamp | Tense Logic and the theory of linear order[END_REF]). Satisfiability and model-checking problems for LTL (even with past-time operators) are also known to be PSPACE-complete [START_REF] Sistla | The complexity of propositional linear temporal logic[END_REF]. In spite of these nice features, it is worth recalling that a propositional variable p only represents a property of the current state of the system. For instance, p may hold true whenever the value of the variable x is greater than the value of the variable y after running the current instruction. A more satisfying solution is to include in the logical language the possibility to express directly constraints between variables of the program, whence giving up the standard abstraction made with propositional variables. When the variables are typed, they may be interpreted in some specific domain like integers, real numbers, strings and so on. Hence, a proposition like "x is greater than the next value of y" can be encoded in such extended temporal logics by x < Xy but this time the models are made of structured states. This means that each state comes with a valuation for variables. Hence, the basic idea behind the design of temporal logics over constraint systems is to refine the language of atomic formulae and to allow the possibility to compare values of variables at successive positions of the execution of programs, see e.g., in [START_REF] Comon | Flatness is not a weakness[END_REF] a representative example of such logics.

How to refine LTL with the help of constraint systems

Let VAR = {x 0 , x 1 , . . .} be a countably infinite set of variables. A constraint system is a pair D = D, (R α ) α∈I where D is a specific domain of interpretation for variables and (R α ) α∈I is a countable family of relations on the elements of D. So, a constraint system is simply a relational structure. An atomic D-constraint is a term of the form R(x 1 , . . . , x n ) where R is interpreted as a relation of the domain and n is the arity of this relation. A D-valuation is a function v : VAR → D that assigns to every variable a value in D. A constraint is satisfied by a D-valuation v, denoted by

v |= D R(x 1 , . . . , x n ), if (v(x 1 ), . . . , v(x n )) ∈ R, R being the relation in D associated to the symbol R.
The consistency problem consists in checking whether there is a valuation satisfying every atomic D-constraint from a finite set. Similarly, the maximal consistency problem checks for maximal consistency with respect to a finite set of variables and a finite set of relations. For instance, the maximal consistency problem for the constraint system R, <, = is NLOGSPACE-complete since it amounts to detect cycles in a finite graph. The implication problem consists in checking whether every valuation satisfying a finite set X of atomic D-constraints satisfies an atomic D-constraint A (written X |= D A). For instance, with D = R, < , we have {x < y, y < z} |= D {x < z}.

The logic CLTL(D) is defined as an extension of LTL where the propositional variables are refined by atomic D-constraints over terms (called atomic temporal Dconstraints). A term is defined as a variable x j prefixed by a certain number i of X "next" symbol X and is denoted by X i x j (its encoding requires O(i + log j) bits). The term X i x j is interpreted as the value of x j at the ith next state. The "next" symbol X is overloaded in this paper since X is also used below as a logical temporal operator. The CLTL(D) formulae are defined as follows :

φ ::= R(X l 1 x j 1 , . . . , X l n x j n ) | φ ∧ φ | ¬φ | Xφ | φUφ.
The symbols X and U are respectively the classical operators next-time and until from LTL. We use the notations Fφ and Gφ as the abbreviations for Uφ and ¬F¬φ. A one-step constraint is an atomic formula of the form R(X l 1 x j 1 , . . . , X l n x j n ) such that l 1 , . . . , l n ≤ 1. Given a CLTL(D) formula φ we define its X-length |φ| X as the maximal number i such that a term of the form X i x occurs in φ. Intuitively, the Xlength defines the size of a frame of consecutive states that can be compared. The models of CLTL(D) are sequences of D-valuations σ : N → (VAR → D) and the satisfaction relation is defined as for LTL except at the atomic level :

Xx = x + 1 Xx = x -1 Xx = 2 Figure 1. A 1-variable N, +1, = 2 -automaton A 0 -σ, i |= R(X l 1 x j 1 , . . . , X l n x j n ) iff σ(i + l 1 )(x j 1 ), . . . , σ(i + l n )(x j n )) ∈ R, -σ, i |= φ ∧ φ iff σ, i |= φ and σ, i |= φ , -σ, i |= ¬φ iff σ, i |= φ, -σ, i |= Xφ iff σ, i + 1 |= φ, -σ, i |= φUφ iff there is j ≥ i such that σ, j |= φ and for every i ≤ l < j, we have σ, l |= φ.
As usual, a formula φ ∈ CLTL(D) is satisfiable whenever there exists a model σ such that σ, 0 |= φ. We write CLTL l k (D) to denote the restriction of CLTL(D) to formulae with at most k variables and X-length less or equal to l. Standard LTL [START_REF] Sistla | The complexity of propositional linear temporal logic[END_REF] can be viewed as CLTL({ , ⊥}, T rue) where T rue = { }.

Lemma 2.1. Let D be a constraint system with equality predicate. There is a logarithmic space reduction from CLTL(D) satisfiability into CLTL 1 ω (D) satisfiability.

The proof of Lemma 2.1 is done by renaming terms and requires an unbounded amount of variables in CLTL 1 ω (D). We define the model-checking problem for the class of D-automata that are Büchi automata with transitions labeled with one-step constraints. A k-variable D-automaton A is a structure Q, δ, I, F such that Q is a finite set of states, I ⊆ Q is the set of initial states, F ⊆ Q is the set of final states and δ is a subset of Q × Σ × Q where Σ is a finite subset of 1SC k , the set of Boolean combinations of one-step constraints built over the set of variables {x 1 , . . . , x k }. We use the notation q c -→ q as an abbreviation for q, c, q ∈ δ. When the constraint system is a fragment of Presburger arithmetic, D-automata form a special class of counter automata. Figure 1 contains a graphical representation of a 1-variable N, +1, = 2 -automaton where "= 2" is the unary predicate interpreted by {2} which corresponds to a test-for-two.

The language accepted by a D-automaton is denoted by L(A). A CLTL(D) model σ is said to realize an ω-sequence of CLTL(D) formulae φ 0 φ 1 . . . iff for every i ≥ 0, we have σ, i |= φ i . We write L D (A) to denote the class of CLTL(D) models that realize some ω-word in L(A).

The model-checking problem1 for CLTL(D) is defined as follows :

input : a D-automaton A and a CLTL(D) formula φ, output :

1 iff there is a model σ in L D (A) such that σ, 0 |= φ (denoted by A |= ∃ φ).
As expected, this amounts to check that there is a computation of A that satisfies the property/formula φ. A universal version of the problem (more used in verification) can be also defined analogously (we then use A |= ∀ φ). For the restriction of the modelchecking to CLTL l k (D), φ belongs to CLTL l k (D) and A is a k-variable D-automaton. For all non-trivial constraint systems presented in the paper, satisfiability can be shown equivalent to the existential version of the model-checking problem and validity can be shown equivalent to its universal version. For instance, A 0 |= ∃ (x = 0) ∧ GF(x = 0) with A 0 defined in Figure 1. Indeed, ((Xx = x + 1) • (Xx = x -1)) ω ∈ L(A 0 ) and (0 • 1) ω realizes this ω-word.

Fragments of Presburger LTL

Presburger arithmetic

Presburger arithmetic (PA) is the first-order theory of Z, + of integers with addition [START_REF] Presburger | Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt[END_REF]. This theory is decidable in triple exponential-time [START_REF] Fischer | Super-exponential complexity of Presburger arithmetic[END_REF] and many fragments can be decided even with a lower complexity, see below. In [START_REF] Ginsburg | Semigroups, Presburger formulas and languages[END_REF], it is shown that PA defines precisely semilinear sets.

Given a Presburger formula A(x 1 , . . . , x n ) with free variables in x = x 1 , . . . , x n , and a = a 1 , . . . , a n ∈ Z n , the truth of A(x 1 , . . . , x n ) with respect to the interpretation a is denoted by a |= A( x). We write sol(A( x)) to denote the elements a ∈ Z n satisfying the formula A( x). In the sequel, any (possibly infinite) fragment FPA of PA (understood as a subset of PA) defines implicitely a constraint system D FPA = Z, (sol(A( x)) A( x)∈FPA .

Hence, the constraint system D FPA may contain an infinite set of relations. We shall write CLTL(FPA) instead of CLTL(D FPA ). For instance the constraints of the form x ≥ c with c ∈ Z induces the constraint system Z, ({n ∈ Z : n ≥ c}) c∈Z , with a countably infinite set of relations.

In the next subsection, we present fragments of Presburger arithmetic useful in the rest of the paper.

Integer periodicity constraints

We define below languages of the first-order theory of integer periodicity constraints. The constraint language IPC is defined by the grammar below :

A ::= x ≡ k y + c | x ≡ k c | A ∧ A | ¬A,
where k, c ∈ N, x, y ∈ VAR. Given X ⊆ {∃, [], <, Eq}, we define an extension of IPC, namely IPC X , by adding clauses to the definition of IPC :

-if ∃ ∈ X, then the clause ∃ x A is added (existential quantification), -if [] ∈ X, then the clause x ≡ k y + [c 1 , c 2 ] with c 1 , c 2 ∈ N is added, -if Eq ∈ X, then the clause x = y with x, y ∈ VAR is added, -if <∈ X, then the clauses x < d | x > d | x = d with x ∈ VAR and d ∈ Z are added.
Observe that the presence of " ¡ " in X allows to express equality constraints between two variables whereas the presence of "<" allows to express equality constraints between a variable and a constant. By way of example, we provide the semantics for the formula

x ≡ k y + [c 1 , c 2 ] : v |= x ≡ k y + [c 1 , c 2 ] def ⇔ there are c ∈ [c 1 , c 2 ] and l ∈ Z such that (v(x) -v(y)) = l × k + c.
Below, IPC + denotes IPC {∃,[],<} whereas IPC ++ denotes IPC {∃,[],<,Eq} . IPC ++ is the extension of the language of the first-order theory of integer periodicity constraints introduced in [START_REF] Toman | DATALOG with integer periodicity constraints[END_REF] but with the inclusion of negation as considered in [START_REF] Bertino | Supporting Periodic Authorizations and Temporal Reasoning in Database Access Control[END_REF]. Observe that what is called "IPC" in [START_REF] Toman | DATALOG with integer periodicity constraints[END_REF] is precisely defined by A ::

= x ≡ k y + c | x ≡ k c | A ∧ A | ∃x A.
As Presburger arithmetic, IPC ++ enjoys a quantifier elimination property but the complexity of the consistency problem is lower.

Theorem 2.2. [START_REF] Demri | LTL over integer periodicity constraints[END_REF] (I) IPC ++ consistency is PSPACE-complete.

(II) Given a constraint A in IPC ++ , one can compute an equivalent quantifier-free A in polynomial space in |A| and |A | is in O(2 |A| ).

Difference logic

Let DL be the following fragment of Presburger arithmetic made of difference constraints :

A

::= x ∼ y + d | x ∼ d |A ∧ A | ¬A
where x, y ∈ VAR, ∼∈ {<, =} and d ∈ Z. We use the notations x ≤ y, x ≥ y and x > y as the respective abbreviations of x < y ∨ x = y, ¬(x < y) and ¬(x ≤ y).

Given a valuation v : VAR → Z, the satisfaction relation v |= c is defined in the obvious way. DL is a proper fragment of quantifier-free Presburger arithmetic. Indeed, periodicity constraints of the form x ≡ k c or comparisons of the form x + y + z < 5 are not part of DL.

The satisfiability problem for CLTL(DL) can be placed in the analytical hierarchy in Σ 1 1 .

Quantifier free Presburger arithmetic

The last fragment of Presburger arithmetic we consider in this paper is quantifierfree Presburger arithmetic QFP that is mainly used in Section 5.6. It is defined as follows :

A ::= i∈I a i x i = d | i∈I a i x i < d | i∈I a i x i ≡ k c | ¬A | A ∧ A
where a i , d ∈ Z, k, c ∈ N and I is a finite subset of N. Observe that QFP is as expressive as Presburger arithmetic but it is less concise (consistency is in NP).

Quantitative constraints and undecidability

In this section, we present undecidable fragments of Presburger LTL even though some drastic syntactic restrictions are sometimes considered.

Minsky machines

Undecidability of LTL with Presburger constraints shall be mainly established by reducing the halting problem or the recurrence problem for nondeterministic Minsky machines. That is why, we recall below what are these problems. A nondeterministic Minsky 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. The l th instruction has one of the following forms : l : C i := C i + 1 ; goto l or goto l l : if C i = 0 then goto l else C i := C i -1 ; goto l or goto l

The configurations of M are 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. 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. The recurrence problem is to decide, given a nondeterministic Minsky machine M , whether M has a recurring computation. This problem is Σ 1 1 -hard (Alur et al., 1994b, Section 4.1). Similarly, the problem of checking whether from 1, 0, 0 a configuration with location counter 1 can be reached in at least one step is undecidable [START_REF] Minsky | Computation, Finite and Infinite Machines[END_REF]) -halting problem.

Constraint systems with counting mechanism

High undecidability of CLTL 1 ω (N, =, +1) satisfiability can be easily shown by reducing the recurrence problem for nondeterministic Minsky machines. More generally, we define below three abstract conditions for a constraint system to admit implicitly a counting mechanism which leads to undecidability. Definition 3.1. A constraint system D is said to admit an implicit counting mechanism if the following conditions are met :

1) D contains the equality predicate, 2) D contains a binary predicate R such that a) R = { a, b ∈ D 2 : f (a) = b} for some injective map f : D → D, b) D, R is a DAG. ∇ So, whenever D has an implicit counting mechanism, for any a ∈ D, a R -→ f 1 (a) R -→ . . . f i (a) R -→ . . . is isomorphic to N, < .
For instance, for every D ∈ {N, Z, Q, R} and for every i ∈ D \ {0}, the constraint system D, =, = +i has an implicit counting mechanism, where n = +i n iff n = n + i. Similarly, the constraint system D \ {0}, =, = ×i admits an implicit counting mechanism where n = ×i n iff n = n × i with i = -1.

Theorem 3.1. [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF] The satisfiability problem for CLTL 1 ω (D) is Σ 1 1hard for every constraint system D with an implicit counting mechanism.

The proof is by reducing the recurrence problem for nondeterministic Minsky machines (see Section 3.1) as done in the proof of (Comon et al., 2000, Theorem 3). Indeed, computations of such machines can be encoded as models of some CLTL 1 ω (D) formula. It is then easy to express that a location counter appears infinitely often. This is the way CLTL 1 3 (DL) satisfiability can be shown undecidable, see e.g. [START_REF] Comon | Flatness is not a weakness[END_REF]. For instance the instruction l : C 1 := C 1 + 1 ; goto l or goto l can be encoded by a temporal formula of the form

G(x l = y l ⇒ (Xz 1 = z 1 + 1 ∧ X(x l = y l ∨ x l = y l ))),
where z 1 is a variable dedicated to the counter C 1 .

Recall that Σ 1 1 -hardness implies that no recursively enumerable axiomatization exists. As corollaries we obtain :

Corollary 3.2. For every D ∈ {N, Z, Q, Q + R, R + }, (I) for every i ∈ D \ {0}, satisfiability for CLTL 1 ω (D, =, = +i ) is Σ 1 1 -hard. (II) for every i ∈ D \ {0, 1, -1}, satisfiability CLTL 1 ω (D, =, = ×i ) is Σ 1 1 -hard.

Restricting syntactic resources

In Section 3.2, we have seen that CLTL 1 ω (N, =, +1) and variants are highly undecidable. The obvious way to encode Minsky machines requires an unbounded amount of variables in order to encode their control states. In this section, we provide evidence that restricting further the syntactic ressources preserves undecidability. For instance, Lemma 3.3 states how to reduce the X-length of formulae and Lemma 3.4 how to reduce the number of variables.

Lemma 3.3. (Demri et al., 2006b) For all k, l, k , l ∈ N \ {0} and constraint systems D, there is an exponential time reduction from

CLTL l k (D) into CLTL l k (D) whenever k × l = k × l and k = k × m for some m ≥ 2. The idea of the proof is to encode m states from a CLTL l k (D) model into a single state in a CLTL l k (D) model. For instance, if k = 2k, then the CLTL l k (D) model below     1 2 . . . k         k + 1 k + 2 . . . 2k         2k + 1 2k + 2 . . . 3k     . . . is encoded as the CLTL l k (D) model below     1 2 . . . 2k         2k + 1 2k + 2 . . . 4k     . . .
Lemma 3.4 below states how to reduce the number of variables in formulae.

Lemma 3.4. (Demri et al., 2006b) For all k, l, k , l ∈ N \ {0} and constraint systems D with equality and at least three elements, there is a logspace reduction from

CLTL l k (D) into CLTL l k (D) whenever 3k × l ≤ k × l and k = k × m for some m ≥ 2.
The idea of the proof is to encode one state from a CLTL l k (D) model into 3m states in a CLTL l k (D) model. Only one state over three encodes values. Intermediate states are used to know when a sequence of 3m states in

CLTL l k (D) corresponds to a state in a CLTL l k (D) model. For instance, if k = 1 and k = 2, then the CLTL l k (D) model below 1 2 3 4 . . . is encoded as the CLTL l k (D) model position 0 1 = b = b = 2 = b = b = position 1 3 = b = b = 4 = b = b . . .
where b denotes arbitrary values satisfying the mentioned relations with its neighbors (each occurrence of b corresponds to a possibly distinct value). In order to ensure that such values exist, we assume that the domain has at least three distinct elements. The beginning of the encoding of some state from the CLTL l k (D) model is such that two consecutive values of the variable are identical.

The flat fragment of CLTL 1 ω (DL) is shown decidable in [START_REF] Comon | Flatness is not a weakness[END_REF] with a decision procedure of complexity at least the one of Presburger arithmetic. The flat fragment is defined by restricting the use of the until operator : the left arguments do not contain temporal operators. Undecidability of CLTL 1 3 (DL) is shown in [START_REF] Comon | Flatness is not a weakness[END_REF] by reducing the halting problem for Minsky machines. Similarly, undecidability of CLTL ω 2 (DL) is shown in [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF] with constraints of the form x = y and x = y + 1. It is possible to refine these results.

Theorem 3.5. (Demri et al., 2006b)

Satisfiability for CLTL 2 1 (DL) is Σ 1 1 -complete.
As a consequence of Theorem 3.5 and Lemma 3.3, we can improve the Σ 1 1hardness of CLTL 1 3 (DL) established in [START_REF] Comon | Flatness is not a weakness[END_REF].

Corollary 3.6. The satisfiability problem for

CLTL 1 2 (DL) is Σ 1 1 -complete.
Consequently, the logic L p from [START_REF] Comon | Flatness is not a weakness[END_REF] restricted to two variables is also highly undecidable. Moreover, the satisfiability problem can easily be reduced to the model-checking problem since φ ∈ CLTL(DL) is satisfiable iff A |= φ where A is the one-state D-automaton {q}, δ, {q}, {q} with unique transition q -→ q (i.e. every model is accepted by A ). So we get the following corollary.

Corollary 3.7. (Demri et al., 2006b) The model-checking problems for CLTL 1 2 (DL) and CLTL 2 1 (DL) are Σ 1 1 -complete.

By close inspection of the proofs of Theorem 3.5 and Corollary 3.6, one can show that satisfiability and model-checking for CLTL 1 2 (DL) and CLTL 2 1 (DL) but restricted to the sometime operator F (instead of until) are also Σ 1 1 -hard.

CLTL 1 1 (QFP) satisfiability

Extending CLTL(DL) with constraints of the form ax + by = 0 where a, b ∈ Z results to an undecidable logic even restricted to one variable and X-length one.

Theorem 3.8. (Demri et al., 2006b) CLTL 1 1 (QFP) satisfiability is undecidable.

Indeed, the values of two counters c 1 , c 2 in the configuration of a Minsky machine can be encoded by the value 2 c 1 3 c 2 for the variable. Zero tests, increments and decrements can be encoded with constraints of the form x ≡ 2 0, x ≡ 3 0, Xx = 2x (incrementation of the first counter) etc. The value of the instruction counter is encoded for instance by repeating the same configuration. As a consequence, the modelchecking problem is undecidable even for the fragment restricted to one variable and X-length one.

General schema with symbolic models

In this section, we explain the main approach to establish decidability of modelchecking and satisfiability problems for CLTL(D). Unless otherwise stated, D is a constraint system D = D, (R α ) α∈I with I possibly infinite.

ω-regularity via abstraction

Given an LTL formula φ built over the propositional variables in {p 1 , . . . , p s }, the LTL models of φ can be viewed as ω-sequences σ : N → Σ with Σ = P({p 1 , . . . , p s }). The automata-based approach advocated in [START_REF] Vardi | Reasoning about Infinite Computations[END_REF] establishes that one can effectively and efficiently build a Büchi automaton A φ such that the language accepted by A φ contains precisely the models of φ, whence providing a method to solve the satisfiability and model-checking problems for LTL. Indeed, the non-emptiness problem for Büchi automata is NLOGSPACE-complete. We recall that a Büchi automaton is a structure A = Σ, S, S 0 , ρ, F such that Σ is a finite set of symbols (the alphabet), S is a finite set of states, S 0 ⊆ S is the set of initial states, ρ : S × Σ → P(S) is the transition function and, F ⊆ S is a set of final (or accepting) states. A run is an infinite sequence s 0 -→ s 2 . . . whenever σ = a 0 a 1 a 2 . . .. The word σ is also said to be accepted by the automaton A and we write L(A) to denote the language of infinite words accepted by the Büchi automaton A.

a 0 -→ s 1 a 1 -→ s 2 . . . such that for every i ≥ 0, s i+1 ∈ ρ(s i , a i )
Given an CLTL(D) formula φ built over the variables x 1 , . . . , x k , the CLTL(D) models of φ are sequences N → D k . The product D k is not necessarily finite and therefore CLTL(D) models cannot be viewed as ω-sequences over a finite alphabet. In order to reuse results for Büchi automata, one strategy consists in abstracting CLTL(D) models of φ as sequences N → {0, 1} m for some m ≥ 1 depending on φ and on the constraint system D. Each element of {0, 1} m can be viewed as a finite set of local properties (for instance "the next value of y is equal to the current value of x"). Given a formula φ and a model σ : N → D k , we can define an abstract/symbolic model abs(φ, σ) : N → {0, 1} m . In order to solve CLTL(D) as it is done for LTL, the best situation we can hope for, is that the set of abstract models derived from a given CLTL(D) formula is ω-regular and the corresponding Büchi automaton can be built effectively and efficiently.

The rest of this section is dedicated to the presentation of the main steps to switch from the concrete models to the symbolic ones.

Syntactic measure

In order to check the satisfiability status of a given CLTL(D) formula φ, we only need to take into account relevant syntactic resources in φ. For instance, for LTL formulae, the number of propositional variables occurring in the formula is the appropriate criterion. Since we are dealing with constraint systems, we need to extend this notion.

Definition 4.1. A (syntactic) measure µ is a triple k, l, X such that k ∈ N \ {0} (the number of variables from VAR), l ∈ N (the X-length) and X is a finite subset of relation symbols related to D. ∇

For instance, given an CLTL(N, <, =) formula φ, a measure k, l, X for φ can be defined such that k is the number of distinct variables occurring in φ (assumed to be x 1 , . . . , x k ), l = |φ| X , and X = {<, =}. More generally, when I is finite, we can assume without any loss of generality that the relations in a measure are exactly those appearing in D.

Symbolic state

The set of atomic temporal D-constraints defined from a measure µ = k, l, X is denoted by CONS µ and is defined as the set

{R(t 1 , . . . , t n ) : R ∈ X} where each term t i is of the form X l x k with 0 ≤ l ≤ l and 1 ≤ k ≤ k. Cardinality of CONS µ is at most exponential in k + l + |X|.
In the case the arity of constraint relations in D is bounded (as for instance in R, <, = ), the cardinality of CONS µ is polynomial in k + l + |X|. We write FOR µ to denote the subset of CLTL(D) formulae restricted to atomic formulae in CONS µ . We define below a symbolic state as a finite set of (local) properties satisfied at a given position of a model. It abstracts a D-valuation whose range can have values arbitrarily large. Definition 4.2. A symbolic state with respect to the measure µ is a subset of CONS µ . ∇ Observe that not every symbolic state is [resp. maximally] consistent. The set of symbolic states is denoted by SYMB µ . A symbolic model ρ for CLTL(D) with respect to µ is a sequence ρ : N → SYMB µ (it is of the form N → {0, 1} m for some m ≥ 1, see Section 4.1). We are now in position to define the symbolic satisfaction relation |= µ with respect to the measure µ. Formulae are in FOR µ and symbolic models are ω-words over the alphabet SYMB µ . Boolean and temporal operators are defined homomorphically as for |=. Only the atomic case requires a special treatment that is indeed similar to what happens for LTL : for any φ ∈ CONS µ , we have

ρ, i |= φ def ⇔ φ ∈ ρ(i).

Abstraction

Given a concrete model σ of CLTL(D) and a measure µ, we write ρ µ σ (it corresponds to abs(φ, σ) in Section 4.1) to denote the symbolic model wrt µ such that for every i ≥ 0,

ρ µ σ (i) def = {φ ∈ CONS µ : σ, i |= φ}.
Lemma 4.1. Let µ be a measure, σ be a model, φ be a formula in FOR µ and i ∈ N.

If σ, i |= φ, then ρ µ σ , i |= µ φ.
Definition 4.3. An abstraction for CLTL(D) is a computable function f from the set of formulae to the set of measures. ∇

An abstraction is complete whenever for every formula φ, for all models σ and i

∈ N, σ, i |= φ iff ρ f (φ) σ , i |= f (φ) φ. Theorem 4.2. Let f be a complete abstraction. Then φ is CLTL(D) satisfiable iff there is a symbolic model ρ such that (I) ρ, 0 |= f (φ) φ, (II) there is a concrete model σ such that ρ = ρ f (φ) σ . In the proof, if σ, 0 |= φ, then by Lemma 4.1, ρ f (φ) σ , 0 |= f (φ) φ. Obviously, ρ f (φ) σ
has a concrete model. Conversely, if ρ satisfies (I) and (II), then by completeness of the abstraction, σ, 0 |= φ.

In order to establish that CLTL(D) satisfiability is in PSPACE, we often show that -CLTL(D) admits a complete abstraction f where consistent elements of SYMB f (φ) can be encoded in polynomial space and checking whether X ⊆ CONS f (φ) is consistent can be done in polynomial space, -the symbolic models satisfying Condition (I) in Theorem 4.2 can be defined with a Büchi automaton computable in polynomial space (as for LTL, see Section 4.5),

-the symbolic models satisfying Condition (II) in Theorem 4.2 can be defined with a Büchi automaton computable in polynomial space.

In order to preserve the PSPACE upper bound, Büchi automata can be replaced by any class of operational models whose non-emptiness problem can be check in NLOG-SPACE, see e.g. (Demri et al., 2006b). Examples of PSPACE upper bounds established with such an approach can be found in [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF]Demri et al., 2005a;[START_REF] Gascon | Verifying qualitative and quantitative properties with LTL over concrete domains[END_REF][START_REF] Demri | LTL over integer periodicity constraints[END_REF]Demri et al., 2006b). However, the class of symbolic models satisfying Condition (I) is usually ω-regular, unlike the class of symbolic models satisfying Condition (II), see e.g. [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF].

Büchi automaton for symbolic satisfaction

We define below a Büchi automaton accepting the symbolic models wrt f (φ) symbolically satisfying φ (Condition (I) in Theorem 4.2). This slightly extends the standard translation from LTL formulae into Büchi automata [START_REF] Vardi | Reasoning about Infinite Computations[END_REF].

We define cl (φ) the closure of φ with a slight modification to consider atomic constraints and an atom of φ is a maximally consistent subset of cl (φ). As usual

ψ 1 Uψ 2 ∈ cl (φ) implies X(ψ 1 Uψ 2 ) ∈ cl (φ) and ψ 1 Uψ 2 belongs to an atom X iff either φ 2 ∈ X or φ 1 , X(ψ 1 Uψ 2 ) ∈ X. Let A f (φ) φ
be the generalized Büchi automaton defined by the tuple Q, δ, I, F over the alphabet SYMB f (φ) such that :

-Q is the set of atoms of φ and

I = {X ∈ Q : φ ∈ X}, -X Z -→ Y iff -for every atomic temporal formula A in X, Z |= D A (instance of the impli- cation problem), -for every Xψ ∈ cl(φ), Xψ ∈ X iff ψ ∈ Y , -Let {ψ 1 Uφ 1 , . . . , ψ n Uφ n } be the set of until formulae in cl (φ). We pose F = {F 1 , . . . , F n } where F i = {X ∈ Q : ψ i Uφ i ∈ X or φ i ∈ X} for every i ∈ {1, . . . , n}.
It is then easy to show the following result.

Lemma 4.3. L(A f (φ) φ ) = {ρ : N → SYMB f (φ) | ρ, 0 |= f (φ) φ}.

Decidability results

In this section, we provide various examples of decidable fragments of Presburger LTL and more generally of decidable LTL over constraint systems.

Completion property

A general problem about the class of logics CLTL(D) is to identify sufficient conditions on the constraint system D for which model-checking and satisfiability for CLTL(D) admit effective decision procedures, ideally in polynomial space as for plain LTL. Very often this amount to check whether D has a complete abstraction and whether for every measure µ, the set {ρ µ σ : σ CLTL(D)-model} of symbolic models wrt µ is ω-regular or not. In this section, we present a class of constraint systems such that the above set is indeed ω-regular and there is an easy way to characterize it with a Büchi automaton.

A symbolic model ρ wrt µ is one-step consistent iff for every i ≥ 0, -ρ(i) is maximally consistent wrt µ, -for every atomic formula R(X l 1 x j 1 , . . . ,

X l n x j n ) ∈ CONS µ with l 1 , . . . , l n ≥ 1, R(X l 1 x j 1 , . . . , X l n x j n ) ∈ ρ(i) iff R(X l 1 -1 x j 1 , . . . , X l n -1 x j n ) ∈ ρ(i + 1).
For the constraint system R, <, = and the measure 1, 2, {<, =} , the symbolic model wrt µ below is one-step consistent :

ρ 0 = {x > Xx, Xx > XXx, x > XXx, x = x, Xx = Xx, XXx = XXx} ω .
One-step consistency is a necessary condition for a symbolic model to belong to {ρ µ σ : σ CLTL(D)-model}. We define below a class of constraint systems for which this condition is also sufficient.

A constraint system D has the completion property [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF] iff for every measure µ = k, 0, X , for every maximally consistent set Y ⊆ CONS µ (made of atomic D-constraints) and

1 ≤ k < k, if -Y = {φ ∈ Y : φ ∈ CONS k ,0,X } (restriction of Y to atomic D-constraints with {x 1 , . . . , x k }) and, -v : {x 1 , . . . , x k } → D such that Y = {φ ∈ CONS k ,0,X : v |= φ}, then there is D-valuation v : {x 1 , . . . , x k } → D such that v is an extension of v and Y = {φ ∈ CONS µ : v |= φ}.
Similar properties have been also introduced in [START_REF] Dechter | From local to global consistency[END_REF][START_REF] Balbiani | Computational Complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning[END_REF]Lutz et al., 2005a) known as global consistency.

When D is a constraint system satisfying the completion property, the set of symbolic models obtained by abstraction can be easily characterized.

Lemma 5.1. Let D be a constraint system with the completion property and µ be a measure. A symbolic model ρ wrt µ has a concrete model iff ρ is one-step consistent.

For instance, R, <, = , R + , <, = , Q, <, = , Q + , <, = as well as D, = for any non-empty set D satisfy the completion property. The above-mentioned symbolic model ρ 0 has therefore a concrete model. By constrast, ρ 0 has no concrete model with the constraint system N, <, = because of well-foundedness.

Let µ be a measure and φ be a formula in FOR µ . We write L µ (φ) to denote the set of symbolic models ρ wrt µ such that ρ, 0 |= µ φ and ρ has a concrete model. Observe that φ is satisfiable iff L µ (φ) is non-empty.

Lemma 5.2. Let D be a constraint system admitting a complete abstraction f and satisfying the completion property. Then, for every

CLTL(D) formula φ, L f (φ) (φ) is ω-regular.
The Büchi automaton accepting the language L f (φ) (φ) can be defined as the intersection of the Büchi automaton accepting one-step consistent symbolic models wrt f (φ) and, A

f (φ) φ .
Based on these properties, we can establish the following complexity result.

Theorem 5.3. [START_REF] Balbiani | Computational Complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning[END_REF]Demri et al., 2002) Let D be a constraint system with a finite amount of relations. Whenever D satisfies the completion property and, the implication and the maximally consistency problems are in PSPACE, then CLTL(D) satisfiability and model-checking are in PSPACE.

The proof in [START_REF] Balbiani | Computational Complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning[END_REF] uses arguments analogous to the ones used in [START_REF] Sistla | The complexity of propositional linear temporal logic[END_REF] to show that LTL is in PSPACE whereas the proof in (Demri et al., 2002) takes advantage of the automata-based approach for LTL [START_REF] Vardi | Reasoning about Infinite Computations[END_REF].

Corollary 5.4. Model-checking and satisfiability for CLTL(R, <, =), CLTL(Q, < , =) and CLTL(D, =) for any set D with at least two elements, are PSPACE-complete.

Adding to CLTL(Q, <, =) comparisons with constants in Q (encoded with a binary representation) of the form x ∼ c with ∼∈ {<, =} and c ∈ Q preserves the PSPACE upper bound. Indeed, constants in a formula can be encoded by variables that remain equal along the model and we need only to specify how the constants compare between each other.

Finite model case

For another class of constraint systems, we can provide complexity upper bounds for CLTL(D) problems, namely when D is finite. Finiteness means that D is of the form D, R 1 , . . . , R N where D is a finite set {d 1 , . . . , d M }. It should not come as a surprise that for such a restricted case, CLTL(D) satisfiability is in PSPACE since one can design a simple logspace reduction from CLTL(D) satisfiability to LTL satisfiability.

Theorem 5.5. Let D be a finite constraint system. The satisfiability problem for CLTL(D) is decidable in PSPACE.

A proof consists in introducing an auxiliary constraint system D = D, P 1 , . . . , P M such that P i = {d i } for each i. A logspace reduction from CLTL(D) to CLTL(D ) can be designed and CLTL(D ) satisfiability can be shown in PSPACE since D admits an easy complete abstraction and satisfies the completion property, see also (Demri, 2004, Theorem 4). The reduction is indeed homomorphic for Boolean and temporal operators and R(t 1 , . . . , t n ) is translated into

R(d i 1 ,...,d i n ) P i 1 (t 1 ) ∧ • • • ∧ P i n (t n ).
This atomic step still guarantees that the reduction is in logspace since the arities of the relations R i 's and the cardinal of D are parameters of the logic. PSPACE-hardness can be also easily shown by reducing LTL satisfiability [resp. model-checking] whenever D is non-trivial. This means that there is a relation R in D of arity n ≥ 1 such that either R = ∅ or R = D n .

Integer periodicity constraints

The language IPC ++ is a quite expressive fragment of Presburger arithmetic. This is witnessed by the PSPACE-completeness of its consistency problem whereas N, <, = is only NLOGSPACE-complete. For instance, formulae of CLTL(IPC ++ ) can encode calendars and slices from [START_REF] Niezette | An efficient symbolic representation of periodic time[END_REF]. A calendar C can be viewed as an ordered partition X 1 , X 2 , . . . of N such that (the partition can be finite but we omit this case here) (ordering) for all i, x and y, x ∈ X i and y ∈ X i+1 imply x < y, (consecution) for every i, there are x ∈ X i and y ∈ X i+1 such that y = x + 1.

A calendar C = X 1 , X 2 , . . . can be represented in CLTL(IPC ++ ) by the interpretation of a variable x in an CLTL(IPC ++ ) model σ : N × VAR → Z such that consecutive positions in σ having the same value for x belongs to the same class :

σ(0, x) = σ(1, x) = . . . = σ(i 1 , x) X 1 ={0,...,i 1 } = σ(i 1 + 1, x) = . . . = σ(i 2 , x) X 2 ={i 1 +1,...,i 2 } = . . .
In most cases, {σ(i, x) : i ∈ N} is naturally finite (minuts, hours, days in a week, months). This means that a class of such calendars can be alternatively encoded as consecutive positions having the same value modulo some integer.

Theorem 5.6. [START_REF] Demri | LTL over Integer Periodicity Constraints (Extended Abstract)[END_REF]) Satisfiability and model-checking for CLTL(IPC ++ ) is PSPACE-complete.

A key argument for such a proof is that IPC ++ admits a complete abstraction and it is possible to encode in polynomial-space the maximally consistent symbolic states. As an application of Theorem 5.6, we can characterize the complexity of the equivalence problem for extended single-string automata defined in (Lago et al., 2001, Sect.5), see other related automata in [START_REF] Bresolin | Time Granularities and Ultimately Periodic Automata[END_REF] and [START_REF] Puppis | Automata for branching and layered temporal structures[END_REF]. This problem is central to check whether two time granularities are equivalent (see also [START_REF] Wijsen | A string based-model for infinite granularities[END_REF]) when granularities are encoded by such automata that can be viewed as Büchi automata recognizing exactly one ω-word. Guards on transitions expressed by integer periodicity constraints and update maps on transitions provide conciseness of such constraint automata. Similarly, in [START_REF] Combi | A logical approach to represent and reason about calendars[END_REF], the authors advocate the need to design an extension of LTL that expresses quantitative temporal requirements, such as periodicity constraints. CLTL(IPC ++ ) with past-time operators (that is also PSPACE-complete) provides such an extension.

Let IPC be the fragment of IPC {∃} containing Boolean combinations of atomic constraints of the form either x ≡ k c or ∃z (x ≡ k z ∧ y ≡ k z). An update map g for the variable x i is defined as an expression of the form either x i := x i + c or x i := c with c ∈ Z. We write UP x 1 ,...,x n to denote the set of update maps that uses variables from {x 1 , . . . , x n }. An extended single-string automaton A (ESSA) over the finite set of variables {x 1 , . . . , x n } [START_REF] Lago | Calendars, time granularities, and automata[END_REF]) is a structure of the form Q, q 0 , v 0 , Σ, δ where -Q is a finite set of states and q 0 ∈ Q (initial state), -v 0 ∈ Z n (initial value of the variables x 1 , . . . , x n ), -Σ is a finite alphabet, -δ ⊆ Q × Σ × Q × ({ } ∪ IPC ) × P(UP x 1 ,...,x n ) and for every q ∈ Q, there are exactly two u such that q, u ∈ δ, say u 1 and u 2 , and in that case u 1 is of the form a 1 , q 1 , A, X 1 , u 2 is of the form a 2 , q 2 , ¬A, X 2 where A is a constraint in IPC * built over variables in {x 1 , . . . , x n } and in both X 1 and X 2 exactly one update map for x i is present.

The elements of δ are also denoted by q a,A,X ---→ q (A is the guard and X is the global update map).

A configuration is a member q, v ∈ Q × Z n . We define the one-step relation a -→ for a ∈ Σ as follows : q, v a -→ q , v iff there is q

a,A,X ---→ q ∈ δ such that [x 1 ← v 1 , . . . , x n ← v n ] |= A (in IPC ++ ) and for every g ∈ X, -if g is x i := x i + c then v i = v i + c ; -if g is x i := c then v i = c.
It is easy to check that there is exactly one sequence w = a 1 a 2 . . . ∈ Σ ω such that q 0 , v 0 a 1 -→ q 1 , v 1 a 2 -→ . . .. The unique ω-sequence generated from the ESSA A is denoted by w A . The equivalence problem for ESSA consists in checking whether w A = w A , given two ESSA A and A . This problem introduced in [START_REF] Lago | Calendars, time granularities, and automata[END_REF] is central to check the equivalence of time granularities when granularities are encoded by such automata.

For instance, the ω-word associated with the ESSA below is a 2 n • b ω with initial value 0 :

q 0 , x 0 = 0 q a, x ≡ 2 n 2 n -1, x := 0 a, ¬x ≡ 2 n 2 n -1, x := x + 1 b, , x := 0
Theorem 5.7. [START_REF] Demri | LTL over Integer Periodicity Constraints (Extended Abstract)[END_REF] The equivalence problem for ESSA is PSPACEcomplete.

In order to establish the PSPACE upper bound, given two ESSA A and A , one can build an IPC {∃} )-automaton B in logspace such that equivalent to B |= ∃ iff w A = w A . Actually l(B) will contain at most one ω-word. B is indeed a product between A and A . The PSPACE lower bound is obtained by adequately reducing QBF. The proof entails that checking whether w A = w A can be done in time

O(2 2×maxsize 2 ×n × |Q| × |Q |),
where n is the number of variables used in A, A and maxsize is the size of the greatest integer k in ≡ k -guards occurring in A, A . Hence, the greatest integer occuring in A, A has value in O(2 maxsize ). Actually, the proof also entails that the problem remains PSPACE-hard when the only integer k in ≡ k -guards occurring in A, A is 2 or when the integers are encoded with a unary representation. Similarly, the problem remains PSPACE-hard when only two distinct variables are used.

Another simpler problem which arises when dealing with time granularities, is to find the nth occurrence of a given symbol in a string (Lago et al., 2003, Sect. 4). Here is the definition of the occurrence problem for ESSA : input : An ESSA A, a ∈ Σ and n, m ∈ N (with a binary representation). question Is the nth occurrence of a in w A in position less than m ?

The proof of Theorem 5.7 can be easily adapted to prove the result below.

Theorem 5.8. [START_REF] Demri | LTL over integer periodicity constraints[END_REF] The occurrence problem for ESSA is PSPACEcomplete.

Decidability of CLTL(Z, <, =)

Even though the consistency problems for Z, <, = and R, <, = are identical, and both CLTL(Z, <, =) and CLTL(R, <, =) admit complete abstractions, respectively, the satisfiability problem for CLTL(Z, <, =) requires more sophisticated techniques to be shown in PSPACE than for CLTL(R, <, =). Indeed, not only Z, <, = does not satisfy the completion property, but also ω-regularity is not guaranteed which may invalidate the use of Büchi automata.

Lemma 5.9. [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF] There are a measure µ and a formula φ in FOR µ such that L µ (φ) is not ω-regular.

The very problem comes from the fact that for some measure µ, the class of onestep consistent symbolic models wrt µ that admit a concrete model is not necessarily ω-regular. In order to circumvent this difficult, we introduced in [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF] an over-approximation of this class that is ω-regular and we show that any ultimately periodic one-step consistent symbolic model wrt µ satisfying this new condition admit a concrete model. This allows us to show the result below.

Theorem 5.10. Satisfiability and model-checking for CLTL(N, <, =) and CLTL(Z, <, =) are PSPACE-complete.

The above result has been extended in (Demri et al., 2005a). The set of IPC * constraints A is defined as follows :

A ::= A | x < y | A ∧ A | ¬A A ::= x ≡ k [c 1 , c 2 ] | x ≡ k y + [c 1 , c 2 ] | x = y | x < d | x = d | A ∧ A | ¬A | ∃x A where x, y ∈ VAR, k ∈ N \ {0}, c 1 , c 2 ∈ N and d ∈ Z.
IPC * extends both Z, <, = and IPC ++ . Observe that the constraint language is defined in two layers in order to avoid an occurrence of x < y in the scope of ∃ which would make possible the encoding of incrementation.

So far, IPC * is the optimal known class of qualitative constraints on Z such that CLTL(IPC * ) is decidable in polynomial-space. By a qualitative constraint, we mean for instance a constraint that is interpreted as a non-deterministic binary relation, like x < y and x ≡ 2 k y + 5 (the relationship between x and y is not sharp). Constraint automata with qualitative constraints on Z are quite attractive operational models since they can be viewed as abstractions of counter automata where incrementations and decrementations are abstracted by operations modulo some power of two. Common programming languages perform arithmetic operators for integer types modulo 2 k (Müller- [START_REF] Müller-Olm | Analysis of Modular Arithmetic[END_REF], typically k is either 32 or 64. For example, x = y + 1 can be abstracted by x ≡ 2 k y + 1 ∧ y < x which is expressible in IPC * .

By extending adequately proof techniques from [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF][START_REF] Demri | LTL over Integer Periodicity Constraints (Extended Abstract)[END_REF], we can characterize CLTL(IPC * ) complexity. Observe that even though IPC * contains both Z, <, = and IPC ++ , the successor relation cannot be defined in IPC * .

Theorem 5.11. (Demri et al., 2005a) Satisfiability and model-checking for CLTL(IPC * ) are PSPACE-complete.

Surprisingly this allows to characterize the complexity of model-checking integral relational automata.

Corollary 5.12. The model-checking problem for integral relational automata restricted to the LTL fragment of CCTL * introduced in ( Čerans, 1994) is in PSPACE.

CLTL 1 1 (DL)

We have shown previously that both CLTL 1 2 (DL) and CLTL 2 1 (DL) are indecidable. When the number of variables and the X-length are both restricted to one, we regain the PSPACE upper bound.

Theorem 5.13. (Demri et al., 2006b) Model-checking and satisfiability for CLTL 1 1 (DL) are PSPACE-complete.

The proof is based on the fact that DL admits a complete abstraction and the class of symbolic models wrt to some measure of the form 1, 1, X that admit a concrete model can be recognized by one-counter automata where -the counter is interpreted in Z, -there are zero tests and sign tests, -accepted words are ω-sequences (Büchi acceptance condition), -updates of the counter are among 0,-1,1.

Standard Büchi automata form a specific subclass of such one-counter automata. Additionally, in order to get the PSPACE upper bound one needs to show that non-emptiness problem for this class of one-counter automata is NLOGSPACEcomplete (Demri et al., 2006b).

Model-checking CLTL

1 1 (QFP)
We have seen in Section 3.4 that CLTL 1 1 (QFP) satisfiability is highly undecidable. Consequently, so is CLTL 1 1 (QFP) model-checking. However, there is a relevant restriction of the CLTL ω 1 (QFP) model-checking problem that is decidable.

Indeed, consider as operational models one-counter automata where the counter is interpreted in Z, there are zero tests and sign tests, accepted words are ω-sequences and updates of the counter are in Z.

Theorem 5.14. (Demri et al., 2006b) The model-checking problem for CLTL ω 1 (QFP) over one-counter automata with updates in Z is PSPACE-complete.

Other decidable extensions

One of the nice features of Theorem 4.2 rests on the distinct treatments between symbolic satisfaction and existence of concrete models for symbolic models. Hence, let D be a constraint system such that CLTL(D) has been stated in PSPACE previously and LTL + be an extension of LTL for which formulae can be translated into Büchi automata in polynomial space. This includes for instance extensions -with past-time operators previous and since, see e.g. [START_REF] Lichtenstein | Propositional Temporal Logics : Decidability and Completeness[END_REF], -more generally, with a finite amount of MSO-definable temporal operators [START_REF] Gastin | Satisfiability and model checking for MSO-definable temporal logics are in PSPACE[END_REF], -with automata-based operators [START_REF] Wolper | Temporal logic can be more expressive[END_REF], -with fixpoint operator, see e.g. [START_REF] Vardi | A temporal fixpoint calculus[END_REF].

A quite remarkable feature of our proof technique is the following.

Theorem 5.15. CLTL + (D) model-checking and satisfiability are also in PSPACE.

Extensions of CLTL(D) by addition of MSO-definable temporal operators (not necessarily a finite amount) are decidable if CLTL(D) can be proved decidable with the above-mentioned proof techniques. It suffices to adapt the definition of A f (φ) φ from plain LTL to LTL + .

Ubiquous freeze operator

Atomic temporal D-constraints allow us to compare values of variables at bounded distance as in x < X 2 y. The languages presented previously have not the possibility to state a property of the form : "there is i ≥ 0 such that x < X i y holds true" which can be written " i x < X i y" with a generalized disjunction. Similarly, a property like "all the future values of x are different from the current value of x", which may be written i>0 ¬(x = X i x), cannot be expressed in the previous languages. In this section, we investigate extensions of CLTL(D) that can express such properties by adding the so-called freeze operator that allows to store a value from D (typically the value of a variable) and to test it later but possibly at some unbounded distance from the position it has been stored. This is a very weak form of existential first-order quantification. However, it is worth recalling that first-order LTL is known to be highly undecidable [START_REF] Abadi | The power of temporal proofs[END_REF][START_REF] Kröger | On the interpretability of arithmetic in temporal logic[END_REF] even in the case the uninterpreted domains are finite [START_REF] Trahtenbrot | Impossibility of an algorithm for the decision problem in finite classes[END_REF]. The extension of CLTL(D) with addition of the freeze quantifier ↓ is denoted by CLTL ↓ (D).

Definition

In order to define CLTL ↓ (D) formally, we divide the set VAR into the (countably infinite) set of rigid variables (VAR r ) and the (countably infinite) set of flexible variables (VAR f ). The clause ↓ y=X j x φ with y ∈ VAR r and x ∈ VAR f is added to the definition of CLTL(D). Atomic formulae are of the form R(t 1 , . . . , t n ) where each t i is either a rigid variable or a term of the form X i x with x ∈ VAR f . A model σ for CLTL ↓ (D) is an infinite sequence of valuations σ : N × VAR f → D over the set of flexible variables and the satisfaction relation is indexed by an environment e : VAR r → D. The definition of |= e is extended as follows :

σ, i |= e ↓ y=X j x φ def ⇔ σ, i |= e φ
where e is obtained from e by only modifying the value for y : e (y) = σ(i + j)(x).

Satisfaction of atomic formulae uses both σ and e depending whether variables are in VAR f or VAR r . Without any loss of generality, we can also assume that for all the formulae φ in CLTL ↓ (D), the free variables in φ are necessarily flexible.

A similar binding mechanism can be found in other logical formalisms :

-in real-time logics [START_REF] Henzinger | Half-order modal logic : how to prove real-time properties[END_REF]Alur et al., 1994b), -in modal logics with λ-abstraction [START_REF] Fitting | Modal logic between propositional and first-order[END_REF][START_REF] Lisitsa | Temporal logic with predicate λ-abstraction[END_REF], -in first-order logic over data words [START_REF] David | Mots et données infinies[END_REF][START_REF] Bojańczyk | Two-variable logic on words with data[END_REF], -in quantified propositional temporal logic with repeating [START_REF] French | Quantified Propositional Temporal Logic with Repeating States[END_REF].

A more detailed comparison can be found in (Demri et al., 2006d).

The formula below from CLTL ↓ (N, =) states that in the model all the values of the variable x are distinct :

ϕ 0 = G ↓ y=x XG(x = y).
We can indeed show that the freeze quantifier is really powerful since every satisfiable formula φ in CLTL(N, =) has a model which contains only finitely many distinct values (Demri et al., 2006d). By contrast, all the models of ϕ 0 contain an infinite amount of distinct values.

Undecidable fragments

Surprisingly, adding the freeze operator leads to undecidability even for the poor constraint system N, = . Hence, the effects of adding the freeze operator in full generality are quite devastating. Recall that N, = satisfies the completion property and CLTL(D) admits a complete abstraction. Theorem 6.1. [START_REF] Demri | On the freeze quantifier in constraint LTL : decidability and complexity[END_REF] Satisfiability for CLTL ↓ (N, =) restricted to two rigid variables and one flexible variable is Σ 1 1 -complete.

Undecidability with three rigid variables has been independently shown in [START_REF] Lisitsa | Temporal logic with predicate λ-abstraction[END_REF]. The Σ 1 1 upper bound is easily obtained. In order to get the hardness result, first one can show that satisfiability for CLTL ↓ (N, =) can be reduced in logspace into its restriction to a unique flexible variable. Then, the recurrence problem for nondeterministic 2-counter machines can be reduced to satisfiability for CLTL ↓ (N, =) restricted to two rigid variables and one flexible variable. Undecidability is a consequence of the fact that the freeze operator can express that if there are n consecutive distinct values (of the flexible variable) between two special markers (encoding that a counter has value n) then there are n + 1 consecutive distinct values between the next occurrences of the two special markers and the subsequence of n last distinct values is equal to the first sequence of n distinct values. This requires exactly the use of two rigid variables.

The above problem is also undecidable with finite models. When a single rigid variable is considered undecidability still holds but with a lower degree. Theorem 6.2. [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF] Satisfiability for CLTL ↓ (N, =) restricted to one rigid variable and one flexible variable is Π 0 1 -complete.

The proof is by reduction from infinitary nonemptiness problem for incrementing counter automata. This new class of automata are the counterpart of lossy counter automata (a special class of lossy channel systems (Schnoebelen, 2002)) in which counters can increment without notice.

Decidability but not PR

The undecidability results presented in Section 6.2 does not leave many hopes to use the freeze operator while being on the decidability side. Indeed, these results are obtained with quite poor constraint systems. By contrast, finite models and one rigid variable lead to decidability with very high complexity.

Theorem 6.3. [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF] Satisfiability for CLTL ↓ (N, =) restricted to one rigid variable over finite models is decidable but not primitive recursive.

The decidability proof is done in three steps :

1) There is a logspace reduction from CLTL ↓ (N, =) restricted to one rigid variable to CLTL ↓ (N, =) restricted to one rigid variable, one flexible variable y and the freeze operator is only used in subformulae of the form ↓ y=x ψ [START_REF] Demri | On the freeze quantifier in constraint LTL : decidability and complexity[END_REF].

2) Every formula in this fragment can be reduced to an equivalent alternating 1register automaton [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF].

3) Non-emptiness for alternating 1-register automaton can be reduced to decidable finitary non-emptiness problem for incrementing counter automata [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF].

Non primitive recursiveness is proved in two steps :

1) Finitary nonemptiness for incrementing counter automata can be shown non primitive recursive by adapting the proof in (Schnoebelen, 2002).

2) This latter problem can be reduced in logspace to satisfiability in CLTL ↓ (N, =) restricted to one rigid variable.

Finiteness, flatness and periodicity constraints

Theorem 5.5 has a counterpart in presence of the freeze operator possibly at the cost of one more exponential in space. Let D be a constraint system D, R 1 , . . . , R N where D is a finite set. Theorem 6.4. [START_REF] Demri | On the freeze quantifier in constraint LTL : decidability and complexity[END_REF] Let D be a finite constraint system. The satisfiability problem for CLTL ↓ (D) is decidable in EXPSPACE.

The proof is by designing an exponential-time reduction from CLTL ↓ (D) satisfiability into CLTL(D ) for some other finite constraint system D and then to take advantage of Theorem 5.5. It is natural to wonder whether the exponential space upper bound is optimal. After all, CLTL(D) satisfiability is only in polynomial space. For most domains D, the answer is positive as stated below. Theorem 6.5. [START_REF] Demri | On the freeze quantifier in constraint LTL : decidability and complexity[END_REF] Let D be a constraint system with equality such that the underlying domain D contains at least two elements. CLTL ↓ (D) satisfiability is EXPSPACE-hard.

CLTL ↓ (D) satisfiability can be also shown to be decidable when restricted to socalled flat formulae. For the rest of this section, D is not necessarily finite. 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 (Ibarra et al., 2001, Section 5) the design of a flat logical temporal language for model-checking pushdown machines) and the definition of flatness takes advantage of the polarity of 'until' subformulae occurring in a formula.

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 . This 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] Ten 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 future 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 t from the flat fragment CLTL ↓ (D) into CLTL(D) as follows : t replaces each y j by y new j in atomic formulae, it is homomorphic for Boolean and temporal operators, and

t(↓ y=X n x ψ) def = y new = X n x ∧ G(y new = Xy new ) ∧ t(ψ)
It is easy to show that t(φ) can be computed in logspace in the size of φ. Lemma 6.6. Let D be a constraint system with equality. For any formula φ of the flat fragment of

CLTL ↓ (D), φ is CLTL ↓ (D) satisfiable iff t(φ) is CLTL(D) satisfiable.
As a corollary, we obtain the following result. Theorem 6.7. [START_REF] Demri | On the freeze quantifier in constraint LTL : decidability and complexity[END_REF] Flat fragments of CLTL ↓ (Z, <, =), CLTL ↓ (N, <, =), CLTL ↓ (R, <, =), and CLTL ↓ (D) with D finite are PSPACEcomplete.

Even though flat CLTL ↓ (N, =) satisfiability can be reduced in logspace to CLTL(N, =) satisfiability, CLTL ↓ (N, =) is more expressive than CLTL(N, =), see details in (Demri et al., 2006d).

Finally, using ideas and techniques useful to prove above-mentioned results, we can show that the following result. Theorem 6.8. [START_REF] Demri | LTL over integer periodicity constraints[END_REF]

Satisfiability for CLTL ↓ (IPC + ) is EXPSPACE- complete.
By contrast, CLTL ↓ (IPC ++ ) is undecidable as a consequence of Theorem 6.1 and CLTL(IPC + ) is "only" PSPACE-complete.

An alternative binding mechanism is the existential quantification. In order to define CLTL ∃ (D) formally, we consider the same syntactic categories as for CLTL ↓ (D) except that we add the clause ∃ y φ with y ∈ VAR r to define formulae. When D contains equality, CLTL ↓ (D) can be viewed as a fragment of CLTL ∃ (D) but it is not always the case as in IPC + . Indeed, ↓ y=x φ is then equivalent to ∃ y x = y ∧ φ. Theorem 6.9. [START_REF] Demri | LTL over integer periodicity constraints[END_REF]

Satisfiability for CLTL ∃ (IPC + ) is EXPSPACE- complete.
The simple fragment of CLTL ↓ (N, =) with past-time operators is restricted to formulae with one flexible variable x and one rigid variable y such that -the only temporal operators are X, X -1 , XXF and X -1 X -1 F -1 , -every occurrence of such temporal operators is immediately preceded by ↓ y=x , -the only terms occurring in atomic formulae are x and y. X -1 is the "previous" operator and F -1 is the "sometimes in the past" operator. This simple fragment is known to be equivalent to a first-order logic with two variables, see e.g. [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF]) and consequently we can establish the following result by using the decidability for this first-order language shown in [START_REF] Bojańczyk | Two-variable logic on words with data[END_REF]. Theorem 6.10. [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF] Satisfiability for the simple fragment of CLTL ↓ (N, =) with past-time operators is decidable.

Related work

In this section, we provide useful pointers to works dealing with temporal logics and Presburger constraints in order to facilitate the comparison between the present framework and existing logical formalisms. Section 7.1 deals with first-order temporal logics whereas Section 7.2 presents LTL variants with quantitative aspects. Section 7.3 refers to quantitative branching-time temporal logics whereas Section 7.4 is dedicated to specification languages for expressing properties about counter systems. Logics with Presburger constraints on the number of children in tree-like models are described in Section 7.5 (see also the automata-based counterparts). Sections 7.6 and 7.7 present alternative temporal logics over concrete domains such as spatio-temporal logics and description logics over concrete domains.

First-order temporal logics

The different variants of LTL over constraint systems presented in this paper can be viewed as fragments of first-order LTL where the domain of interpretation of variables is fixed as well as the interpretation of predicate symbols. Moreover, flexible variables in CLTL(D) correspond to unary predicate symbols interpreted as singletons (the values of variables). However, CLTL(D) has no quantification over elements of the domain and in that sense it corresponds to a very weak first-order extension of plain LTL. It is worth recalling that first-order LTL is highly undecidable [START_REF] Abadi | The power of temporal proofs[END_REF][START_REF] Kröger | On the interpretability of arithmetic in temporal logic[END_REF]) even in the case the uninterpreted domains are finite [START_REF] Trahtenbrot | Impossibility of an algorithm for the decision problem in finite classes[END_REF]. Similarly, first-order LTL over finite time structures is highly undecidable [START_REF] Cerrito | First-Order Linear Temporal Logic over Finite Time Structures[END_REF]. In particular, the Σ 1 1 -hardness implies that no axiomatization with a countable set of axioms exists for this logic.

Since the freeze binding mechanism is a first-order 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 (Gabbay et al., 2003, Chapter 11)). To each flexible variable x one associates a unary predicate symbol P x in such a way that P x is interpreted as the singleton set containing the value of x.

A variant of first-order LTL has been introduced in [START_REF] Deutsch | Specification and verification of data-driven web services[END_REF] to verify data-driven web applications. The interplay between temporal operators and first-order quantifiers is restricted since no quantification can occur in the scope of temporal operators, which guarantees better computational properties.

Quantitative versions of LTL

The logics presented in this paper belong to the long tradition of quantitative versions of LTL. LTL-like logics having models non isomorphic to ω can be found in [START_REF] Alur | The benefits of relaxing punctuality[END_REF][START_REF] Reynolds | The complexity of the temporal logic with until over general linear time[END_REF][START_REF] Hirshfeld | Future temporal logic needs infinitely many modalities[END_REF][START_REF] Hirshfeld | Logics for real time : decidability and complexity[END_REF]Lutz et al., 2005b;Demri et al., 2005c). Temporal operators in the real-time logics from [START_REF] Alur | The benefits of relaxing punctuality[END_REF][START_REF] Hirshfeld | Logics for real time : decidability and complexity[END_REF]Lutz et al., 2005b) are indexed by intervals. By contrast, Constrained LTL defined in [START_REF] Bouajjani | On the verification problem of nonregular properties for nonregular processes[END_REF] have standard LTL models but the logical language is enriched with Presburger constraints about the number of occurrences of events. This extension of LTL is undecidable and decidable fragments are introduced in [START_REF] Bouajjani | On the verification problem of nonregular properties for nonregular processes[END_REF].

Branching-time temporal Logics

Integral relational automata defined in ( Čerans, 1994) form a subclass of IPC *automata and we have seen that the model-checking problem for CLTL(IPC * ) is PSPACE-complete. By contrast, it is shown in ( Čerans, 1994) that model-checking integral relational automata with a CTL version of CLTL(IPC * ) is undecidable roughly because quantification over natural numbers can be simulated by a quantification over paths. However, model-checking for the existential fragment of the CTL* version of CLTL(IPC * ) is shown decidable in [START_REF] Bozzelli | Branching-time temporal logic extended with Presburger constraints[END_REF] extending a weaker result from ( Čerans, 1994). The decidability proof is based on techniques for well-structured systems.

Very few classes of counter systems are decidable for CTL* (see e.g. [START_REF] Finkel | A Direct Symbolic Approach to Model Checking Pushdown Systems (Extended Abstract)[END_REF] for one-counter systems). Another logical formalism close to the ones presented in this paper is studied in [START_REF] Bultan | Symbolic model checking of infinite state systems using Presburger arithmetic[END_REF] where an undecidable temporal logic with CTL-like operators and atomic formulae in Presburger arithmetic is introduced and the models are counter systems.

Verification of counter systems

Analyzing the reachability problem for counter systems is ubiquitous for the verification of infinite-state systems, see e.g. [START_REF] Ibarra | Counter Machines : Decidable Properties and Applications to Verification Problems[END_REF] (reversal-bounded systems), [START_REF] Comon | Multiple counters automata, safety analysis and Presburger arithmetic[END_REF] (flat systems), [START_REF] Finkel | How to compose Presburger accelerations : Applications to broadcast protocols[END_REF] (flat Presburger transition systems), [START_REF] Dang | Presburger Liveness Verification of Discrete Timed Automata[END_REF] (discrete timed automata), see also the decidability of reachability for classes of 2-counter systems [START_REF] Finkel | Decidability of reachability problems for classes of two counters automata[END_REF]. It is worth noting that, even though decidability can be obtained only at the cost of making drastic restrictions on counter systems, there is a remarkable class of counter systems that are sufficiently expressive for modelling different case studies. For instance, the flattable systems [START_REF] Leroux | Flat counter systems are everywhere ![END_REF] admit a flat finite unfolding of the control graph with the same reachability set (see also (Demri et al., 2006a) for properties other than accessibility). On the logical side, temporal logics with Presburger constraints have been developed in [START_REF] Čerans | Deciding Properties of Integral Relational Automata[END_REF][START_REF] Bouajjani | On the verification problem of nonregular properties for nonregular processes[END_REF][START_REF] Bultan | Symbolic model checking of infinite state systems using Presburger arithmetic[END_REF][START_REF] Comon | Flatness is not a weakness[END_REF][START_REF] Bruyère | Durations, Parametric Model-Checking in Timed Automata with Presburger Arithmetic[END_REF], some of which have quite expressive decidable fragments. However, undecidability of the reachability problem can be proved for quite restricted counter systems, see e.g. [START_REF] Cortier | About the Decision of Reachability for Register Machines[END_REF][START_REF] Potapov | From Post Systems to the Reachability Problems for Matrix Semigroups and Multicounter Automata[END_REF].

The subclass of one-counter automata is obviously equivalent to pushdown systems with a singleton stack alphabet and many results on such systems can be therefore applied to one-counter automata. For instance, model-checking one-counter automata with the modal µ-calculus has been shown in EXPTIME in [START_REF] Walukiewicz | Pushdown processes : games and model-checking[END_REF] and this result has been refined in (Serre, 2004, Section 7.2) (see also [START_REF] Serre | Parity games played on transition graphs of one-counter processes[END_REF])) where it is proved that the problem is in PSPACE. It is worth mentioning that in these logics the atomic formulae can only speak about the control states and not about the content of the counter, a major difference with formalisms involved in Theorem 5.14. Similarly, in [START_REF] Bouajjani | Reachability Analysis of Pushdown Automata : Application to Model Checking[END_REF] model-checking pushdown automata over the linear µ-calculus is proved in EXPTIME. Surprisingly, one-counter automata have applications in various parts of theoretical computer science :

-for verification of cryptographic protocols [START_REF] Lafourcade | Intruder deduction for AC-like equational theories with homomorphisms[END_REF], -for validating XML streams (string representations of XML documents) by encoding recursive DTDs as one-counter automata [START_REF] Chitic | On validation of XML streams using finite state machines[END_REF], -to solve the identification problem [START_REF] Wakatsuki | Polynomial time identification of strict deterministic restricted one-counter automata in some class from positive data[END_REF].

Constraints on the number of children

In order to query XML documents with Presburger and/or regular constraints on the children of nodes, logical and automata-based formalisms have been recently introduced [START_REF] Seidl | Counting in Trees for free[END_REF][START_REF] Ohsaki | Monotone AC-Tree Automata[END_REF][START_REF] Zilio | XML schema, tree logic and sheaves automata[END_REF][START_REF] Boneva | Automata and Logics for Unranked and Unordered Trees[END_REF]Demri et al., 2006e) leading to various expressiveness and complexity results about logics and specialized tree automata. As usual, XML documents are viewed as finite labeled, unranked ordered trees. For instance, the computational complexity of a logic with fixed-point operators, Presburger and regularity constraints is studied in [START_REF] Seidl | Counting in Trees for free[END_REF], improving results for description logics with qualified number restrictions [START_REF] Hollunder | Qualifying number restrictions in concept languages[END_REF][START_REF] Calvanese | Expressive Description Logics », Description Logics Handbook[END_REF]. Graded modal logics from [START_REF] Fine | In so many possible worlds[END_REF][START_REF] Barnaba | Graded Modalities[END_REF][START_REF] Van Der Hoek | Counting objects[END_REF] have very elementary Presburger constraints compared to modal logic extended with all quantifier-free Presburger constraints that is shown to be in PSPACE in (Demri et al., 2006e), see also related logics in [START_REF] Pacuit | Majority logic[END_REF][START_REF] Schröder | PSPACE bounds for rank-1 modal logics[END_REF]. In those logics, Presburger formulae express constraints on the number of children.

Spatio-temporal logics

Spatio-temporal logics, see e.g. [START_REF] Wolter | Spatio-temporal representation and reasoning based on RCC-8[END_REF][START_REF] Gabbay | Many-dimensional modal logics : theory and practice[END_REF][START_REF] Hodkinson | On the computational complexity of decidable fragments of first-order linear temporal logics[END_REF][START_REF] Gabelaia | On the computational complexity of spatio-temporal logics[END_REF] are examples of versions of LTL with constraint systems for which the constraint system has indeed a spatial structure. Examples of such spatial systems verifying the completion property and examples of systems not verifying this property can be found in [START_REF] Balbiani | Computational Complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning[END_REF]. Complexity and decidability results for such logics can be found in [START_REF] Gabbay | Many-dimensional modal logics : theory and practice[END_REF].

Description logics over concrete domains

The introduction of concrete domains in description logics is due to (Baader et al., 1991) and since then, such logic-based formalisms for knowledge representation have been intensively studied, see e.g. [START_REF] Lutz | Description Logics with Concrete Domains-A Survey[END_REF][START_REF] Lutz | NEXPTIME-complete description logics with concrete domains[END_REF]. As expected, concept satisfiability with respect to general TBoxes with an arithmetic concrete domain is undecidable which is comparable to the undecidability of CLTL(N, =, +1) satisfiability. Hence, LTL over concrete domains can be technically viewed as a subclass of description logics over concrete domain in which the models are linear. Among the differences, it is worth observing that in LTL it is possible to access to any successor position with the always operator G whose counterpart in description logics is the presence of a transitive closure operator. Motivations are also quite different. In-deed, the introduction of LTL over Presburger constraints is motivated by the need to model-check counter systems whereas concrete domains in description logics have been introduced to integrate concrete qualities into description logic concepts.

Concluding remarks

In this paper, we have presented an overview of linear-time temporal logics with Presburger constraints and we have compared them with alternative formalisms. Because of lack of space, we have not provided the full technical details and they can be found in the original papers. It is worth observing that a great amount of work remains to be done to push the decidability border further in order to get effective procedures to verify programs with variables interpreted in fixed domains.

Among the open problems, let us mention a few of them. The first track is certainly to have more decidability results for richer classes of constraint systems. For instance, what is the decidability status of CLTL({0, 1} * , ⊂, =) where ⊂ is the subword [resp. prefix, factor] relation ? Obviously, CLTL({0} * , ⊂, =) behaves as CLTL(N, <, =). Developing model-checking techniques for such a logic might help to verify programs manipulating strings. Another line of research consists in extending known decidability proofs to heterogeneous constraint systems, for instance mixing strings and natural numbers. Finally, let us quote other interesting problems :

-How to refine the classification of constraint systems D such that CLTL(D) is decidable ? in PSPACE ? -What makes decidable branching-time extensions of decidable CLTL(D) ? -How to restrict further the use of the freeze binding quantifier in order to regain decidability ?

  and s 0 ∈ S 0 . Given a run c, we write inf (c) to denote the set of states that occur infinitely often in c. An accepting run c verifies inf (c) ∩ F = ∅. The word σ ∈ Σ ω is accepted by the accepting run c = s 0 a 0 -→ s 1 a 1

  CLTL ∃ (D) and CLTL ↓ (D) have the same models and the satisfaction relation is indexed by an environment e : VAR r → D. The relation |= e is defined as follows : σ, i |= e ∃ y φ def ⇔ there is a ∈ D such that σ, i |= e φ where e is obtained from e only modifying the value of y : e (y) = a.

Unlike what is done in the journal paper, we consider the existential version for the Σ 1 1 results.

Acknowledgements : Numerous results presented in this paper have been obtained with colleagues. I would like to thank Deepak D'Souza, Régis Gascon, Ranko Lazić and David Nowak for fruitful and friendly collaborations. I am grateful to the INTAS project members for their kind invitation to present such an overview. Finally, I thank the anonymous referee for suggestions that help me to improve the readability of this document.

Bibliographie

for the INTAS project "Algebraic and Deduction Methods in NonClassical Logics and their Applications to Computer Science". Work partially supported by the ACI "Sécurité et Informatique" CORTOS.