Stéphane Demri
email: demri@lsv.ens-cachan.fr

Régis Gascon
email: gascon@lsv.ens-cachan.fr

Verification of qualitative Z constraints

We introduce an LTL-like logic with atomic formulae built over a constraint language interpreting variables in Z. The constraint language includes periodicity constraints, comparison constraints of the form x = y and x < y, is closed under Boolean operations and admits a restricted form of existential quantification. Such constraints are used for instance in calendar formalisms or abstractions of counter automata by using congruences modulo some power of two. Indeed, various programming languages perform arithmetic operators modulo some integer. We show that the satisfiability and model-checking problems (with respect to an appropriate class of constraint automata) for this logic are decidable in polynomial space improving significantly known results about its strict fragments. This is the largest set of qualitative constraints over Z known so far, shown to admit a decidable LTL extension.

Introduction

Model-checking infinite-state systems. The verification of systems with an infinite number of states has benefited from the numerous decidable model-checking problems for infinite-state systems, including timed automata [START_REF] Alur | A theory of timed automata[END_REF], infinite transition graphs [START_REF] Muller | The theory of ends, pushdown automata, and second-order logic[END_REF][START_REF]On infinite transition graphs having a decidable monadic theory[END_REF], or subclasses of counter systems (see e.g. [START_REF] Comon | Multiple counters automata, safety analysis and Presburger arithmetic[END_REF]). There exist numerous techniques to prove decidability such as finite partition of the infinite domain, well-structured systems, Presburger definable reachability sets or reduction to the monadic second-order theory of the binary tree. . . Since it is often possible to find a reduction from the halting problem for Minsky machines [START_REF] Minsky | Computation, Finite and Infinite Machines[END_REF], undecidability is often easy to prove. Decidability can sometimes be regained by naturally restricting the class of models (see e.g. the flatness condition in [START_REF] Comon | Multiple counters automata, safety analysis and Presburger arithmetic[END_REF][START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF]) or by considering fragments of the specification language (for instance reachability questions). Symbolic representations of infinite sets of states are often the key argument to get decidability (see e.g. [START_REF] Th | A classification of symbolic transitions systems[END_REF]).

Systems with variables interpreted in Z. Counter machines are operational models that have found numerous applications in the verification of infinite-state systems, including broadcast protocols (see e.g. [START_REF] Esparza | On the verification of broadcast protocols[END_REF][START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF]) and programs with pointer variables [BFLS06,BBH + 06]. They consist of a structure with a finite set of control states augmented with a finite set of variables interpreted either in Z or N (counters). Though this class of automata has numerous undecidable model-checking problems such as the reachability problem, many subclasses have been shown to be decidable:

1. reversal-bounded multicounter machines [START_REF] Ibarra | Reversal-bounded multicounter machines and their decision problems[END_REF], 2. flat counter systems with affine update functions forming a finite monoid (see e.g. [START_REF] Boigelot | Symbolic methods for exploring infinite state spaces[END_REF][START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF][START_REF] Bardin | Fast: Fast Acceleration of Symbolic Transition systems[END_REF]), 3. flat counter systems [START_REF] Comon | Multiple counters automata, safety analysis and Presburger arithmetic[END_REF][START_REF] Bozga | Flat parametric counter automata[END_REF] (weaker class of Presburger guards but no condition on the monoid), 4. admissible Presburger counter systems [START_REF] Demri | Towards a model-checker for counter systems[END_REF], 5. constraint automata with qualitative constraints on Z [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF].

Our motivation. Constraint automata with qualitative constraints on Z are quite attractive operational models since they can be viewed as abstractions of counter automata where increments and decrements are abstracted by operations modulo some power of two. Indeed, common programming languages perform arithmetic operators for integers modulo 2 k [START_REF] Müller-Olm | Analysis of modular arithmetic[END_REF], where k is typically equal to 32 or 64. So, such an abstraction is well-suited to check safety properties about the original counter system. In this paper, we introduce a class of constraint automata with a language of qualitative constraints as rich as possible and a companion LTLlike logic in order to perform model-checking on these models. Our framework should be able to deal both with modulo abstractions (see e.g. [START_REF] Clarke | Model checking and abstraction[END_REF][START_REF] Logothetis | Abstraction from counters: an application on real-time systems[END_REF]) and with integer periodicity constraints used in logical formalisms to deal with calendars [START_REF] Lago | Calendars, time granularities, and automata[END_REF]. By qualitative constraint, we mean constraints that are interpreted as a non-deterministic binary relation, like x < y or x ≡ 2 k y + 5 (the relationship between x and y is not sharp).

Our contribution. We introduce CLTL(IPC ⋆ ) as an extension of LTL over the constraint language IPC ⋆ , whose expressions are Boolean combinations of IPC ++ constraints from [START_REF] Demri | LTL over integer periodicity constraints[END_REF] and constraints of the form x < y. The language inherits from IPC ++ closure under Boolean operators and first-order quantification. We impose that no constraint of the form x < y occurs in the scope of a quantifier; otherwise incrementation is definable and this leads to undecidability. In this paper, we show that adding the single type of constraints x < y leads to many technical complications but not to undecidability. We also introduce the class of IPC ⋆ -automata defined as finite-state automata with transitions labelled by CLTL(IPC ⋆ ) formula à la Wolper [START_REF] Wolper | Temporal logic can be more expressive[END_REF]. Such structures can be viewed as labelled transition systems obtained by abstraction of counter automata.

Constraint LTL over IPC ++ is already known to be in pspace in [START_REF] Demri | LTL over integer periodicity constraints[END_REF] whereas constraint LTL over constraints of the form either x = y or x < y is shown to be also in pspace in [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF]. Though both proofs use reductions to the nonemptiness problem for Büchi automata, following the approach in [START_REF] Vardi | Reasoning about infinite computations[END_REF], they are of different nature: in [START_REF] Demri | LTL over integer periodicity constraints[END_REF] the complexity upper bound is obtained by a finite model property argument whereas in [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF] approximations of classes of symbolic models are considered because some formulae can generate non ωregular classes of symbolic models. We show that the model-checking and satisfiability problems for the logic CLTL(IPC ⋆ ) are still pspace-complete which generalizes and unifies these results. We improve what is done for constraint LTL over the domain Z, <, = by considering both new constraints of the form x ≤ d with d ∈ Z and periodicity constraints. The optimal treatment of the constants introduced in this language is our main technical contribution. As a corollary, we establish that LTL model-checking over integral relational automata [ Čer94] is pspace-complete. Hence, even though IPC ⋆ is a powerful language of qualitative constraints, the pspace upper bound is preserved in CLTL(IPC ⋆ ). Moreover, past-time operators can be added for free in our formalism thanks to [START_REF] Gastin | Satisfiability and model checking for MSOdefinable temporal logics are in PSPACE[END_REF] (the pspace bound is still preserved).

Related work. Reachability problems for subclasses of counter systems have been addressed in numerous works [Iba78,CJ98,FS00,FL02,BFLP03] (see also richer questions in [BEM97,DI02,DPK03,JKMS04]). In this paper, we consider a full LTL-like language used as a specification language which is not restricted to reachability questions, and we have no restriction on the structure of the models unlike [START_REF] Comon | Multiple counters automata, safety analysis and Presburger arithmetic[END_REF][START_REF] Demri | Towards a model-checker for counter systems[END_REF]. However, the atomic formulae of the specification language are restricted to qualitative constraints. If we give up the decidability requirement, other extensions of LTL with Presburger constraints can be found in [START_REF] Bouajjani | On the verification problem of nonregular properties for nonregular processes[END_REF][START_REF] Comon | Flatness is not a weakness[END_REF][START_REF] Ibarra | On removing the stack from reachability constructions[END_REF].

Extensions of LTL over concrete domains, not only restricted to variables interpreted in Z, have also been considered in [WZ00,BC02,DD07,GKK + 03,Dem06] where often pspace-completeness results are shown. The idea of building LTL over a language of constraints, although already present in first-order temporal logics, stems from the use of concrete domains for description logics [START_REF] Baader | A scheme for integrating concrete domains into concept languages[END_REF][START_REF] Lutz | NEXPTIME-complete description logics with concrete domains[END_REF]. The language CLTL(IPC ⋆ ) extends the different LTL-like fragments from the works [START_REF] Čerans | Deciding properties of integral relational automata[END_REF][START_REF] Lago | Calendars, time granularities, and automata[END_REF][START_REF] Demri | LTL over integer periodicity constraints[END_REF].

The underlying constraint language of CLTL(IPC ⋆ ) includes integer periodicity constraints, a special class of Presburger constraints that have found applications in many logical formalisms such as abstractions with congruences modulo an integer of the form 2 k (see e.g. [START_REF] Clarke | Model checking and abstraction[END_REF][START_REF] Müller-Olm | Analysis of modular arithmetic[END_REF]), logical formalisms dealing with calendars (see e.g. [START_REF] Lago | Calendars, time granularities, and automata[END_REF][START_REF] Puppis | Automata for Branching and Layered Temporal Structures[END_REF]) and temporal reasoning in database access control [START_REF] Bertino | An access control model supporting periodicity constraints and temporal reasoning[END_REF]. Such constraints can also be found in real-time logics, see e.g. [START_REF] Alur | A really temporal logic[END_REF]. Our approach of constraint LTL makes explicit the constraints on variables, similarly to the explicit clock approach from [START_REF] Harel | Explicit clock temporal logic[END_REF]. Furthermore, the class of IPC ⋆ -automata we introduce generalizes the class of integral relational automata from [ Čer94] (see details in Appendix A).

Finally, the concept of symbolic models used in the paper has similarities with untimed languages recognized by some classes of timed machines. In [START_REF] Bérard | Untiming timed languages[END_REF], sufficient conditions to get regular untimed languages from timed machines are exhibited.

Plan of the paper. The rest of the paper is organized as follows. In Section 2, we introduce the logic CLTL(IPC ⋆ ) and the class of IPC ⋆ -automata. We present the model-checking and satisfiability problems and discuss expressiveness issues.

In Section 3, we analyze the computational complexity of the satisfiability problem of the underlying constraint language IPC ⋆ . We also provide a symbolic representation of the valuations that is used later in the decidability proof. Section 4 contains a characterization of the sequences of symbolic valuations that admit concrete models (valuation sequence). We show that testing the existence of some concrete model is an ω-regular property when considering ultimately periodic sequences. In Section 5, we show that given a CLTL(IPC ⋆ ) formula φ, one can build a Büchi automaton A φ over the alphabet of symbolic valuations such that φ is CLTL(IPC ⋆ ) satisfiable iff L(A φ ) is non-empty. Moreover, we establish that nonemptiness of L(A φ ) can be checked in polynomial space in |φ|. Section 6 contains concluding remarks.

This paper is a completed version of [START_REF] Demri | Verification of qualitative Z-constraints[END_REF].

2 The logic CLTL(IPC ⋆ )

Language of constraints

Let VAR = {x 0 , x 1 , . . .} be a countably infinite set of variables (in some places for ease of presentation, VAR will denote a particular finite set of variables). The language of constraints IPC ⋆ is defined by the following grammar:

ξ ::= θ | x < y | ξ ∧ ξ | ¬ξ θ ::= x ≡ k [c 1 , c 2 ] | x ≡ k y + [c 1 , c 2 ] | x = y | x < d | x = d | θ ∧ θ | ¬θ | ∃x θ where x, y ∈ VAR, k ∈ N\{0}, c 1 , c 2 ∈ N and d ∈ Z.
In the following, the symbol ∼ is used to mean either = or <. We write IPC ++ to denote the restriction of the language to constraints ranged over by θ, Z c to constraints of the form either x ∼ y or x ∼ d and Z to constraints of the form x ∼ y where x, y ∈ VAR, d ∈ Z and ∼∈ {<, =}. A valuation v : VAR → Z is a map that associates a value to each variable and the satisfaction relation v |= ⋆ ξ is defined in the standard way:

-v |= ⋆ x ∼ y iff v(x) ∼ v(y); -v |= ⋆ x ∼ d iff v(x) ∼ d; -v |= ⋆ x ≡ k [c 1 , c 2 ] iff v(x) -c = kd for some c 1 ≤ c ≤ c 2 and d ∈ Z; -v |= ⋆ x ≡ k y + [c 1 , c 2 ] iff v(x) -v(y) -c = kd for some c 1 ≤ c ≤ c 2 and d ∈ Z; -v |= ⋆ ξ ∧ ξ ′ iff v |= ⋆ ξ and v |= ⋆ ξ ′ ; -v |= ⋆ ¬ξ iff v |= ⋆ ξ; -v |= ⋆ ∃x ξ iff there is d ∈ Z such that v[x ← d] |= ⋆ ξ where v[x ← d](x ′ ) = v(x ′ ) if x = x ′ and v[x ← d](x) = d.
We will shortly write (II) IPC ++ admits quantifier elimination [START_REF] Demri | LTL over integer periodicity constraints[END_REF] and therefore so does IPC ⋆ since Z is quantifier-free. ⊓ ⊔

x ≡ k c instead of x ≡ k [c, c] and x ≡ k y + c instead of x ≡ k y + [c, c]. Given a set of IPC ⋆ -constraints X, we note v |= ⋆ X whenever v |= ⋆ ξ for every ξ ∈ X. A constraint ξ is satisfiable iff there is a valuation v such that v |= ⋆ ξ.

Logical language

We consider the extension of the linear-time temporal logic LTL whose atomic formulae are defined from constraints in IPC ⋆ (denoted by CLTL(IPC ⋆ )). So, the language includes boolean operators as well as the classical temporal operators next (X) and until (U) of LTL. The atomic formulae are of the form ξ[x 1 ← X l1 x j1 , . . . , x r ← X lr x jr ], where ξ is a constraint of IPC ⋆ with free variables x 1 . . . x r . We substitute each occurrence of the variable x i by X li x ji , which corresponds to the variable x ji preceded by l i next symbols. Each expression of the form X l x j is called a term and represents the value of the variable x j at the l th next state. For example, Xy ≡ 2 32 x + 1 and x < Xy are atomic formulae of the logic. The set of CLTL(IPC ⋆ ) formulae φ is defined by the grammar below

φ ::= ξ[x 1 ← X i1 x j1 , . . . , x r ← X ir x jr ] | ¬φ | φ ∧ φ | Xφ | φUφ,
where ξ belongs to IPC ⋆ . The integers are encoded with a binary representation (this is important for complexity considerations). A one-step constraint is a constraint where all the terms are of the form x and Xx only (for some x ∈ VAR). Given a set of constraints X included in IPC ⋆ , we write CLTL(X) to denote the restriction of CLTL(IPC ⋆ ) in which the atomic constraints are built over elements of X.

A model σ : N × VAR → Z for CLTL(IPC ⋆ ) is an ω-sequence of valuations. The satisfaction relation is defined as follows:

-σ, i |= ξ[x 1 ← X i1 x j1 , . . . , x r ← X ir x jr ] iff [x 1 ← σ(i + i 1 , x j1 ), . . . , x r ← σ(i + i r , x jr )] |= ⋆ ξ; -σ, i |= φ ∧ φ ′ iff σ, i |= φ and σ, i |= φ ′ ; -σ, i |= ¬φ iff σ, i |= φ; -σ, i |= Xφ iff σ, i + 1 |= φ;
σ, i |= φUφ ′ iff there is j ≥ i s.t. σ, j |= φ ′ and for every i ≤ l < j, σ, l |= φ.

Satisfiability and model-checking problems

We define below the problems we consider in this paper. The definition of the satisfiability problem is standard.

Satisfiability problem :

Given a CLTL(IPC ⋆ ) formula φ, is there a model σ such that σ, 0 |= φ?

Note that if we extend IPC ⋆ to allow constraints of the form x < y in the scope of an existential quantifier, then the satisfiability problem for the corresponding extension of CLTL(IPC ⋆ ) is undecidable since the relation x = y + 1 is then definable and the halting problem for Minsky machines can be easily encoded. The model-checking problem which is defined in a moment rests on a particular class of constraint automata [START_REF] Revesz | Introduction to Constraint Databases[END_REF]. An IPC ⋆ -automaton is defined as a Büchi automaton over a finite alphabet made of CLTL(IPC ⋆ ) formulae. In such an automaton, letters on transitions may 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]. Hence, guards and update functions are expressed in the same formalism. We are however a bit more general since we allow formulae on transitions as done in [START_REF] Wolper | Temporal logic can be more expressive[END_REF]. Formally, an IPC ⋆ -automaton is a structure A = Q, I, F, δ such that:

-Q is a finite set of locations, -I ⊆ Q is a set of initial locations and F ⊆ Q a set of final locations, -δ ⊆ Q × Σ × Q where Σ is a finite set of IPC ⋆ -constraints.
We say that A is a restricted IPC ⋆ -automaton when Σ is a set of Boolean combination of one-step constraints. A run is an infinite sequence q 0 φ0 -→ q 1 φ1 -→ q 2 φ2 -→ . . . such that for every i ∈ N, q i , φ i , q i+1 ∈ δ. Such a run is accepting iff there is a state q f ∈ F such that q i = q f for infinitely many i ∈ N. In this case, the word φ 0 • φ 1 • φ 2 • . . . is accepted by A and we write L(A) to denote the language recognized by A made of ω-sequences φ 1 • φ 2 • • • ∈ Σ ω obtained from accepting runs. We say that a valuation sequence σ realizes a word

φ 0 • φ 1 • φ 2 • . . . in Σ ω iff for every i ≥ 0, σ, i |= φ i .
As an illustration, we present a (restricted) IPC ⋆ -automaton in Figure 1 which is an abstraction of the pay-phone controller from [CC00, Example 1] (x is the number of quarters that have been inserted and y measures the total communication time). An increment of a variable z is abstracted by Xz ≡ 2 32 z + 1 ∧ Xz > z. The formula φ = denotes Xx = x ∧ Xy = y. Messages are omitted because they are irrelevant here (simplifications are then possible).

Model-checking problem :

Given an IPC ⋆ -automaton A and a CLTL(IPC ⋆ ) formula φ, are there an ω-word φ 0 • φ 1 • . . . accepted by A and a model σ for φ that realizes φ 0 • φ 1 • . . .. Note that the equivalence problem for Extended Single-String automata [START_REF] Lago | Calendars, time granularities, and automata[END_REF] can be encoded as a model-checking problem for CLTL(IPC ⋆ ) (see [START_REF] Demri | LTL over integer periodicity constraints[END_REF]).

q1 q2 q3 q4 q6 q5 x = 0 ∧ y = 0 φ= x > 0 ∧ φ= y ≤ x ∧ φ= φ= φ= x = y ∧ Xx = 0 ∧ Xy = 0 Xx ≡ 2 32 x + 1 ∧ Xx > x ∧ Xy = y Xx ≡ 2 32 x + 1 ∧ Xx > x ∧ Xy = y y ≤ x ∧ Xy ≡ 2 32 y + 1 ∧ Xy > y ∧ Xx = x Xy ≤ x, Xy ≡ 2 32 y + 1 ∧ Xy > y ∧ Xx = x Fig. 1. A restricted IPC ⋆ -automaton
The satisfiability problem and the model-checking problem are reducible to each other in logspace following techniques from [START_REF] Sistla | The complexity of propositional linear temporal logic[END_REF]. Indeed, satisfiability can be seen as a particular case of model-checking problem since one can build an IPC ⋆ -automaton such that every valuation sequence realizes some execution of this automaton (consider for instance the automaton that accepts the sequence ⊤ ω ). The converse reduction relies on a standard encoding of the executions of an IPC ⋆ -automaton by a CLTL(IPC ⋆ ) formula, possibly introducing a new variable to encode the control states of the automaton. In the following, we only refer to the satisfiability problem but the results we prove also hold for the model-checking problem.

Let CCTL * (IPC ⋆ ) denote the CTL * extension of CLTL(IPC ⋆ ). The modelchecking problem of the LTL fragment of the logic introduced in [ Čer94] against integral relational automata is a subproblem of the model-checking problem for CLTL(IPC ⋆ ). Full CCTL * (IPC ⋆ ) model-checking can be shown to be undecidable by using developments in Appendix A and [ Čer94]. This is actually true even for its CTL-like fragment. However in [START_REF] Bozzelli | Branching-time temporal logic extended with presburger constraints[END_REF], it has been shown that its existential and universal fragments are decidable even though the proof does not allow to obtain any tight bound on the computational complexity of the problem. Here, we show that the LTL fragment is decidable in polynomial space, a result not captured by these two works.

Expressive power and conciseness of the language

By definition, CLTL(IPC ⋆ )-models interpret variables but not propositional variables. However, it is not difficult to encode propositional variables by using atomic formulae of the form x = 0 where x is a new variable introduced for this purpose. The model-checking problems for CLTL(IPC ++ ) and CLTL(Z) are shown to be pspace-complete respectively in [START_REF] Demri | LTL over integer periodicity constraints[END_REF] and in [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF]. However, the proof for IPC ++ uses an ω-regular property of the set of models that does not hold when introducing constraints of the form x < y. The problem for CLTL(Z c ) is shown to be in expspace in [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF] by translation into CLTL(Z) that increases exponentially the size of formulae with a binary encoding of the integers.

Let WIPC ⋆ (weak IPC ⋆ ) denote the restriction of IPC ⋆ to constraints of the form either x ∼ y, x ∼ d or x ≡ k c where x, y ∈ VAR, ∼∈ {<, =}, d ∈ Z and k, c ∈ N. Though WIPC ⋆ is a fragment of IPC ⋆ , the logic CLTL(WIPC ⋆ ) is as expressive as CLTL(IPC ⋆ ).

Lemma 2. For every φ ∈ CLTL(IPC ⋆ ), there exists an equivalent formula ψ ∈ CLTL(WIPC ⋆ ).

Proof. This a direct consequence of the facts below:

-IPC ⋆ admits quantifier-elimination. -x ≡ k [c 1 , c 2 ] is equivalent to c1≤c ′ ≤c2 x ≡ k c -x ≡ k y + [c 1 , c 2 ] is equivalent to c1≤c ′ ≤c2 { c ′ 1 ,c ′ 2 ∈{0,...,k-1} 2 |c ′ 1 +c ′ 2 ≡ k c ′ } (x ≡ k c ′ 1 ∧ y ≡ k c ′ 2 ) .

⊓ ⊔

The size of ψ is exponential in the size of φ in the worst case (for an infinite amount of formulae φ). In spite of this exponential blow-up, we shall prove that both CLTL(WIPC ⋆ ) and CLTL(IPC ⋆ ) have pspace-complete model-checking problems.

Note also that adding constraints of the form ax + by ≡ k c with a, b, c ∈ Z in CLTL(IPC ⋆ ) does not add expressiveness since we can translate such constraints in CLTL(IPC ⋆ ). Let S = { c x , c y ∈ {0, . . . , k -1} 2 | c x + c y ≡ k c}. We have the following logical equivalence:

ax + by ≡ k c ⇔ cx,cy ∈S (ax ≡ k c x ∧ by ≡ k c y ).
Then we can translate the constraints of the form ax ≡ k c x into CLTL(IPC ⋆ ) by solving a simple diophantine equation. The constraint ax ≡ k c x reduces either to false if gcd(a, k) does not divide c x or to x ≡ k ′ c ′ with k ′ × gcd(a, k) = k for some c ′ that can be computed in polynomial-time in the respective sizes of a, k and c x . The addition of such constraints may cause a gain of conciseness. However, because the sizes of k ′ and c ′ are bounded by the maximum of the sizes of a, k and c and k is a multiple of k ′ , the forthcoming pspace upper bounds for CLTL(IPC ⋆ ) problems can be also obtained when constraints of the form Σ i a i x i ≡ k c are added.

Properties of the constraint language

In this section, we establish results about the constraint language underlying the logic CLTL(IPC ⋆ ). We define a symbolic representation of the valuations in order to build automata that recognize symbolic representations of CLTL(IPC ⋆ )models. Given a finite set X of IPC ⋆ constraints, typically the set of constraints occurring in a given CLTL(IPC ⋆ ) formula, we introduce the following notations:

-K is the least common multiple of the integers k 1 , . . . , k n such that periodicity constraints with relations ≡ k1 , . . . , ≡ kn occur in X. -CONS is the finite set of constants d occurring in the constraints of X of the form x ∼ d (where ∼∈ {<, =}). m is the minimal element of CONS and M is its maximal element.

-CONS ′ denotes the set of constants {m, m + 1, . . . , M }.

-VAR is the finite set of variables occurring in X.

In the remaining, we consider that the above objects are always defined (possibly by adding dummy valid constraints in order to make the sets non-empty). In the sequel, we write |O| to denote the size of the finite object O for some reasonably succinct encoding (in particular binary encoding of integers). Observe that A maximally consistent set Y of Z c constraints with respect to VAR and CONS is a set of Z c constraints using only the variables from VAR and the constants from CONS such that there is a valuation v verifying v |= ⋆ Y and for any proper extension Z of Y , there is no valuation v ′ verifying v ′ |= ⋆ Z. A valuation is abstracted by three disjoint finite sets of IPC ⋆ constraints similar to regions for timed automata.

|K| is in O(|k 1 | + • • • + |k n |) and the cardinality of CONS is polynomial in the size of X. The cardinality of CONS ′ is in O(2 |M|
Definition 1. Given a finite set X of IPC ⋆ constraints, a symbolic valuation sv is a triple Y 1 , Y 2 , Y 3 such that -Y 1 is a maximally consistent set of Z c constraints with respect to VAR and CONS. -Y 2 is a set of constraints of the form x = d with x ∈ VAR and d ∈ CONS ′ \ CONS. Moreover, we impose that for every

x ∈ VAR, (x = d) ∈ Y 2 for some unique d ∈ CONS ′ \ CONS iff for every d ′ ∈ CONS, (x = d ′ ) ∈ Y 1 and {m < x, x < M } ⊆ Y 1 . Note that, each x ∈ VAR occurs at most once in Y 2 . -Y 3 is a set of constraints of the form x ≡ K c with x ∈ VAR and c ∈ {0, . . . , K -1}. Each x ∈ VAR occurs exactly once in Y 3 . A consequence of Definition 1 is that in a symbolic valuation sv = Y 1 , Y 2 , Y 3 , no constraint occurs in more than one set. Given an IPC ⋆ constraint ξ, we write ξ ∈ sv instead of ξ ∈ Y 1 ∪ Y 2 ∪ Y 3 . A symbolic valuation is satisfiable iff there is a valuation v : VAR → Z such that v |= ⋆ Y 1 ∪ Y 2 ∪ Y 3 .
Lemma 3. Let X be a finite set of IPC ⋆ constraints and sv = Y 1 , Y 2 , Y 3 be a triple composed of IPC ⋆ constraints such that Y 1 is a set of Z c constraints built over VAR and CONS, Y 2 is a set of Z c constraints of cardinality at most |VAR| built over VAR and CONS ′ \CONS, Y 3 is a set of constraints of the form x ≡ K c of cardinality |VAR|. Checking whether sv is a satisfiable symbolic valuation can be done in polynomial-time in the sum of the respective size of X and sv.

To prove this result, we have to check several things. Maximal consistency of Y 1 can be checked in polynomial-time by using developments from [ Čer94, Lemma 5.5]. A set Y 1 of Z c constraints is maximally consistent w.r.t. VAR and CONS iff the associated graph

G Y1 = VAR ∪ CONS, = -→, < -→ such that n ∼ -→ n ′ def ⇔ (n ∼ n ′ ) ∈ Y 1 (
where ∼∈ {<, =}) satisfies the conditions below:

(MC1) For all n, n ′ , either n ∼ -→ n ′ or n ′ ∼
-→ n for some ∼∈ {<, =}.

(MC2) = -→ is a congruence relation compatible with < -→. (MC3) There is no path n 0 ∼0 -→ n 1 ∼1 -→ . . . ∼α-1 --→ n α such that n 0 = n α and one of the symbols ∼ 0 , . . . , ∼ α-1 is equal to < (no strict cycle). (MC4) For all d 1 , d 2 ∈ CONS, d 1 ∼ d 2 implies d 1 ∼ -→ d 2 . (MC5) For all d 1 , d 2 with d 1 ≤ d 2 , there is no path n 0 ∼0 -→ n 1 ∼1 -→ . . . ∼α-1 --→ n α with n 0 = d 1 and n α = d 2 such that the number of occurrences of the symbol < in ∼ 0 , • • • , ∼ α-1 is strictly greater than d 2 -d 1 .
Note that this graph does not take into account the constraints in Y 2 and Y 3 .

Checking that a variable occurs at most once in Y 2 or exactly once in Y 3 can be done in linear time. It is also easy to verify that the equality relations of Y 2 do not contradict the constraints in Y 1 .

Finally, we need to check that the set of congruence relations Y 3 is compatible with the sets of constraints Y 1 and Y 2 :

(MC6) (a) For all n, n ′ such that n = -→ n ′ , for every c ∈ {0, . . . , K -1}, n ≡ K c ∈ Y 3 iff n ′ ≡ K c ∈ Y 3 . (b) For all x = d in Y 2 , the corresponding constraint x ≡ K c belonging to Y 3 is such that c ≡ K d.
As illustrated by the following lemma, the symbolic representations of valuations contain the relevant information to evaluate constraints. Lemma 4. Let X be a finite set of IPC ⋆ constraints.

(I) For every valuation v : VAR → Z there is a unique symbolic valuation Y 1 , Y 2 , Y 3 built w.r.t. X and denoted by sv(v) such that v |= ⋆ Y 1 ∪ Y 2 ∪ Y 3 . (II) For all valuations v, v ′ such that sv(v) = sv(v ′ ) and for every ξ ∈ X, v |= ⋆ ξ iff v ′ |= ⋆ ξ.
Proof. (I) Given a symbolic valuation sv , let V sv be the set of tuples d 1 , .

(v) = sv , v |= ⋆ ξ.
Lemma 5. Given a symbolic valuation sv built w.r.t. a set of constraints X (fixing VAR, CONS and K) and a constraint ξ ∈ X, checking whether sv |= symb ξ is pspace-complete.

Proof. pspace-hardness can be obtained by reducing QBF. The only constants used are 0 and 1.

Each QBF formula φ = Q 1 p 1 Q 2 p 2 . . . Q n p n φ ′ with φ ′ a
propositional formula in CNF built over the propositional variables {p 1 , . . . , p n } and {Q 1 , . . . , Q n } ⊆ {∀, ∃} is translated via the map t as follows

-t(∃ p i φ i ) = ∃ x i (x i = 0 ∨ x i = 1) ∧ t(φ i ), -t(∀ p i φ i ) = ∀ x i (x i = 0 ∨ x i = 1) ⇒ t(φ i ), -t is homomorphic for Boolean connectives, -t(p i ) = (x i = 1).
One can show that φ is QBF satisfiable iff for all symbolic valuations sv, sv |= symb t(φ) which is equivalent to check that an arbitrary symbolic valuation symbolically satisfies t(φ), since t(φ) has no free variable.

The proof for the upper bound is similar to the proof of the pspace upper bound for first-order model-checking [START_REF] Chandra | Optimal implementation of conjunctive queries in relational databases[END_REF]. We can define a function MC(sv, ξ ′ , ξ) where ξ ′ is a subconstraint occurring in the IPC ⋆ constraint ξ, sv is a symbolic valuation over the syntactic resources of ξ ′ (VAR, CONS, K defined above), which returns true iff sv |= symb ξ ′ . Observe that if a variable occurs in sv but is not free in ξ ′ then the satisfaction of sv |= symb ξ ′ is independent of its value. The function MC is defined as a case analysis on the form of ξ ′ . For instance, MC(sv, ∃ x ξ ′ , ξ) returns true iff there is a satisfiable symbolic valuation sv ′ extending sv by addition of x-constraints, such that MC(sv ′ , ξ ′ , ξ) returns true.

The symbolic valuations sv

′ = Y ′ 1 , Y ′ 2 , Y ′ 3 and sv = Y 1 , Y 2 , Y 3 are related as follows:
sv ′ is a satisfiable symbolic valuation over the free variables of ξ ′ . This can be checked in polynomial-time in |ξ|.

-Y 1 ⊆ Y ′ 1 , Y 2 ⊆ Y ′ 2 and Y 3 ⊆ Y ′ 3 . -The only variable in sv ′ but not in sv is x.
Even if the number of symbolic valuations over the free variables of ξ ′ is exponential in |ξ|, it is possible to enumerate them in polynomial space in order to check the existence of some sv ′ verifying the above conditions.

⊓ ⊔

Satisfiable ω-sequences of symbolic valuations

Given a CLTL(IPC ⋆ ) formula φ, we write IPC ⋆ (φ) to denote the set of IPC ⋆ constraints ξ such that some atomic formula of the form ξ[x 1 ← X i1 x j1 , . . . , x r ← X ir x jr ] occurs in φ. We associate to IPC ⋆ (φ) the objects relative to any finite set of IPC ⋆ constraints: the set VAR of variables and the set CONS of constants occurring in φ, and K the least common multiple of the integers k i that occur in the congruence relations. This induces a unique set CONS ′ = {m, . . . , M } where m is the minimal element of CONS and M the maximal element.

We define the X-length of φ, denoted by |φ| X , as the maximal number i such that a term of the form X i x occurs in φ. In the following, we assume that VAR = {x 1 , . . . , x s } and |φ| X = l ≥ 1. We write Terms(φ) to denote the set of terms of the form X β x α with β ∈ {0, . . . , l} and α ∈ {1, . . . , s}.

Let VAR ′ be a set of fresh variables of cardinality |Terms(φ)|. For technical convenience, we need to introduce a bijection f : Terms(φ) → VAR ′ such that f and f -1 can be computed in polynomial time. By extension, for every subformula ψ of φ, f (ψ) is obtained from ψ by replacing each occurrence of X β x α by f (X β x α ). The map f -1 is used in a similar fashion. A symbolic valuation with respect to φ is a symbolic valuation built over the set of variables VAR ′ , CONS and K.

We say that a pair

Y 1 , Y 2 , Y 3 , Y ′ 1 , Y ′ 2 , Y ′ 3
of symbolic valuations with respect to φ is one-step consistent iff for every j, j ′ ≥ 1,

x i , x i ′ ∈ VAR, d ∈ CONS ′ and c ∈ {0, . . . , K -1} we have 1. f (X j x i ) ∼ f (X j ′ x i ′ ) ∈ Y 1 iff f (X j-1 x i ) ∼ f (X j ′ -1 x i ′ ) ∈ Y ′ 1 , 2. f (X j x i ) ∼ d ∈ Y 1 ∪ Y 2 iff f (X j-1 x i ) ∼ d ∈ Y ′ 1 ∪ Y ′ 2 , 3. f (X j x i ) ≡ K c ∈ Y 3 iff f (X j-1 x i ) ≡ K c ∈ Y ′
3 . An ω-sequence ρ of satisfiable symbolic valuations w.r.t. φ is one-step consistent iff for every j ∈ N, ρ(j), ρ(j + 1) is one-step consistent, where ρ(j) denotes the jth symbolic valuation of the sequence. We say that a symbolic valuation sequence ρ is satisfied by a CLTL(IPC ⋆ )-model σ iff for all j ∈ N and ξ ∈ ρ(j), σ, j |= f -1 (ξ). In order to simplify the future developments, we will write ρ f (or sometimes ρ f -1 ) to denote the ω-sequence of IPC ⋆ -constraints obtained from ρ by substituting each occurrence of x by f -1 (x) for every variable x used in ρ.

One-step consistent ω-sequences of symbolic valuations w.r.t. φ define abstractions of models for φ. We represent a one-step consistent sequence ρ by an infinite labeled structure

G ρ = (VAR ∪ CONS ′ ) × N, = -→, < -→, mod where mod : (VAR ∪ CONS ′ ) × N → {0, . . . , K -1} and for all ∼ ∈ {<, =}, x, y ∈ VAR, d ′ , d 1 , d 2 ∈ CONS ′ and i, j ∈ N such that |i -j| ≤ l we have: x, i ∼ -→ y, j iff either i ≤ j and x ∼ X j-i y ∈ ρ f (i) or i > j and X i-j x ∼ y ∈ ρ f (j), x, i = → d, j iff x = d ∈ ρ f (i), d, i = → x, j iff x = d ∈ ρ f (j), x, i < → d, j iff there is d ′ ∼ d s.t. x ∼ ′ d ′ ∈ ρ f (i) for some ∼ ′ ∈ {<, =} and either ∼ or ∼ ′ is equal to <, d, i < → x, j iff there is d ∼ d ′ s.t. d ′ ∼ ′ x ∈ ρ f (j) for some ∼ ′ ∈ {<, =} and either ∼ or ∼ ′ is equal to <, d 1 , i ∼ -→ d 2 , j iff d 1 ∼ d 2 , mod( x, i ) = c iff x ≡ K c ∈ ρ f (i), mod( d, i ) = c iff d ≡ K c.
By construction of G ρ , the variables and constants are treated in a similar fashion. It is worth observing that G ρ is well-defined because ρ is one-step consistent. Moreover, the construction ensures that the "local" representation of every ρ(i) verifies the conditions (MC1)-(MC6) introduced Section 3.

We say that a vertex represents the constant d ∈ CONS ′ if it is of the form d, i for some i ∈ N. The level of a node n = a, t in G ρ is defined by lev(n) = t. There is some redundancy in G ρ for the nodes of the form d, i but this turn out to be helpful to establish tight relationships between ρ and G ρ .

As an example, assume that VAR = {y}, CONS = {2, 4}, K = 2, l = 1, VAR ′ = {x, x ′ } (f (y) = x and f (Xy) = x ′ ) and l = 1. We consider the sequence ρ = sv 0 • (sv 1 • sv 2 ) ω where

-sv 0 = Y 0 1 , Y 0 2 , Y 0 3 with • Y 0 1 = {x = x, x ′ = x ′ , x < x ′ , 2 < x, x < 4, 2 < x ′ , x ′ = 4}, • Y 0 2 = {x = 3}, • Y 0 3 = {x ≡ 2 1, x ′ ≡ 2 0}, -sv 1 = Y 1 1 , Y 1 2 , Y 1 3 with • Y 1 1 = {x = x, x ′ = x ′ , x < x ′ , 2 < x, x = 4, 2 < x ′ , 4 < x ′ }, • Y 1 2 = ∅, • Y 1 3 = {x ≡ 2 0, x ′ ≡ 2 1}, -sv 2 = Y 2 1 , Y 2 2 , Y 2 3 with • Y 2 1 = {x = x, x ′ = x ′ , x < x ′ , 2 < x, 4 < x, 2 < x ′ , 4 < x ′ }, • Y 2 2 = ∅, • Y 2 3 = {x ≡ 2 1, x ′ ≡ 2 1}.
The graph G ρ is presented in Figure 2. In order to simplify the representation, closure by transitivity for < -→ and the fact that = -→ is a congruence are omitted. The function mod is directly encoded in the node label.

A path in G ρ is a sequence (possible infinite) of the form n 0

∼0 -→ n 1 ∼1 -→ n 2 ∼2 -→ . . . (each ∼ i belongs to {<, =}). A finite path w = n 0 ∼0 -→ n 1 ∼1 -→ n 2 ∼2 -→ . . . ∼α-1 --→ n α such that n 0 = n α is called a cycle. For any finite path w = n 0 ∼0 -→ n 1 ∼1 -→ n 2 ∼2 -→ . . . ∼α-1
--→ n α , its strict length slen(w) is the number of indices i ∈ {0, . . . , α -1} such that ∼ i is equal to <. We say that w is strict if slen(w) > 0. The strict length between two nodes n 1 and n 2 , written slen(n 1 , n 2 ), is the least upper bound (possibly equal to ω) of the strict lengths of finite paths between n 1 and n 2 . By convention, if there is no path between from n 1 to n 2 , slen(n 1 , n 2 ) takes the value -∞. For example, in Figure 2 slen( 2, 2 , y, 3 ) = 4 (see the transitions in boldface). --→ n α , n 0 = n α implies slen(w) = 0. The proof is by induction on α. The base case with either α = 1 or α = 2 is by an easy verification since the subgraph corresponding to the symbolic valuation ρ(min{lev(n i ) : 1 ≤ i ≤ α}) contains all the nodes of the path and satisfies (MC3). In the induction step, suppose that w is a cycle with α > 2 and let n β be a node of the path with the greatest level. Without any loss of generality, we can assume that 0 < β < α since one can choose the first node of the cycle. As lev(n β ) is maximal, |lev(n β-1 )lev(n β+1 )| ≤ l and so the subgraph corresponding to ρ(min{lev(n β-1 ), lev(n β+1 )}) contains the nodes n β-1 , n β and n β+1 . Since this subgraph satisfies (MC2), this implies that n β-1

< -→ n β+1 iff n β-1 < -→ n β or n β < -→ n β+1 .
As a consequence, slen(w) = 0 iff slen(w ′ ) = 0 where the path w ′ is obtained from w by replacing the subpath from n β-1 to n β+1 by the edge n β-1 ∼ -→ n β+1 . By induction hypothesis, slen(w ′ ) = 0 and therefore slen(w) = 0.

(II) We show that for every path w = n 0

∼0 -→ n 1 ∼1 -→ n 2 ∼2 -→ . . . ∼α-1 --→ n α such that n 0 = d, i , we have d, lev(n α )
∼ -→ n α with ∼ equal to < if w is strict and to = otherwise. The proof is by induction on α. The base case with α = 1 is obvious. Let us consider a path w = n 0

∼0 -→ n 1 ∼1 -→ n 2 ∼2 -→ . . . ∼α-1 --→ n α with n 0 = d, i and α > 1. Suppose that d, lev(n α-1 ) ∼ -→ n α-1 with ∼ equals to < if n 0 ∼0 -→ n 1 ∼1 -→ n 2 ∼2 -→ . . . ∼α-2
--→ n α-1 is strict and ∼ equals to = otherwise. We only treat the case lev(n α-1 ) ≤ lev(n α ), the other case is similar. Since lev(n α )lev(n α-1 ) ≤ l, the nodes n α-1 and n α belong to the subgraph corresponding to ρ(lev(n α-1 )). This subgraph satisfies (MC2) and so d, lev(n α-1 )

∼ ′ -→ n α with ∼ ′ equal to < if either d, lev(n α-1 ) < -→ n α-1 or n α-1 < -→ n α .
Hence, by using induction hypothesis we obtain that d, lev(n α-1 ) (IV) Suppose that two nodes n and n ′ are such that slen(n, n ′ ) = 0. So there is a path,

∼ ′ -→ n α and ∼ ′ is equal to < if w is strict. Since d, lev(n α-1 ) = -→ d,
w = n = -→ n 0 = -→ . . . = -→ n α-1 = -→ n α with n α = n ′ .
We proceed by induction on α. If α ≤ 1 then the local representation of ρ(min{lev(n 0 ), lev(n α ))} contains both n 0 and n α and we can conclude using (MC6). Otherwise, suppose that α > 1 and mod(n 0 ) = mod(n α-1 ). Since n α-1 = -→ n α the local representation of ρ(min{lev(n α-1 ), lev(n α ))} contains both n α-1 and n α . Since, this symbolic valuation satisfies (MC6), we have mod(n α ) = mod(n α-1 ) = mod(n 0 ).

⊓ ⊔ Corollary 1. Let ρ be a one-step consistent sequence of symbolic valuations and G ρ its graph representation. Then, for all nodes d 1 , i and

d 2 , j in G ρ representing constants such that d 1 ≤ d 2 , slen( d 1 , i , d 2 , j ) = d 2 -d 1 .
Proof. Let d 1 , i and d 2 , j be vertices of G ρ representing respectively the constants d 1 and d 2 . Without any loss of generality, we can assume that i ≤ j (the case j > i has a similar treatment). Obviously, slen( d 1 , i , d 2 , j ) ≥ d 2d 1 as witnessed by the path below of strict length d 2d 1 :

d 1 , i = -→ d 1 , i+1 = -→ d 1 , i+2 • • • d 1 , j < -→ d 1 +1, j < -→ d 1 +2, j • • • < -→ d 2 , j .
Now suppose that there is a path w between d 1 , i and d 2 , j such that slen(w) > d 2d 1 . Consider the restriction of the transitive closure of = -→ to the nodes appearing in w. This relation is an equivalence relation having exactly slen(w) + 1 equivalence classes. Let X 0 , . . . , X slen(w) be an enumeration of these equivalence classes. As a consequence of Lemma 6(II,III), every node n in w of

level j is such that d 1 , j ∼ -→ n ∼ ′ -→ d 2 , j for some ∼, ∼ ′ ∈ {<, =}.
By definition of CONS ′ (which contains all the integers of the interval [m, M ]) and by maximal consistency of the local representations, for every i ∈ {0, . . . , slen(w)}, there is

d ′ i ∈ CONS ′ such that d 1 ≤ d ′ i ≤ d 2
and every node n of level j in X i has an outgoing edge n = -→ d ′ i , j . Moreover the constants d ′ 0 , . . . , d ′ slen(w) should be mutually distinct since all the X i represents distinct equivalence classes. This leads to a contradiction since the cardinality of {d 1 , . . . ,

d 2 } is (d 2 -d 1 ) + 1. ⊓ ⊔
So far, we have stated properties about the graph G ρ . Below, we establish simple conditions on G ρ equivalent to the existence of a CLTL(IPC ⋆ ) model satisfying ρ. An edge-respecting labeling for G ρ is a map lab : (VAR ∪ CONS ′ ) × N → Z such that -for all nodes n 1 , n 2 and ∼ ∈ {<, =}, we have n 1

∼ -→ n 2 implies lab(n 1 ) ∼ lab(n 2 ), -for every node n, lab(n) ≡ K mod(n).
Additionally, lab is said to be strict if for every d, i in G ρ , lab( d, i ) = d.

Lemma 7. A one-step consistent sequence of symbolic valuations ρ has a model iff G ρ has an edge-respecting labeling.

Proof. Let σ be a model for ρ and lab : (VAR ∪ CONS ′ ) × N → Z be the map defined as follows:

lab( x, i ) = σ(i, x); lab( d, i ) = d for all x ∈ VAR, d ∈ CONS ′ and i ∈ N.
It is not difficult to show that lab is a strict edge-respecting labeling for G ρ . For instance, we have implications between the propositions below (x, y ∈ VAR, i, j ∈ N, ∼ ∈ {<, =}): σ(i,x) ∼ σ(j, y) (by definition of |=), -lab( x, i ) ∼ lab( y, j ) (by definition of lab).

-x, i ∼ -→ y, j and i ≤ j, -x ∼ X j-i y ∈ ρ f (i) (by definition of G ρ ), -f (x ∼ X j-i y) ∈ ρ(i) (by definition of ρ f ), -σ, i |= f -1 (f (x ∼ X j-i y)) (since σ is a model for ρ), -σ, i |= x ∼ X j-i y (f is a bijection),
Hence, x, i ∼ -→ y, j and i ≤ j implies lab( x, i ) ∼ lab( y, j ). Satisfaction of periodicity constraints is based on the same development (x ∈ VAR, c ∈ {0, . . . , K -1}):

-mod( x, i ) = c, -x ≡ K c ∈ ρ f (i) (by definition of G ρ ), -σ, i |= x ≡ K c (arguments as above), -σ(i, x) ≡ K c (by definition of |=), -lab( x, i ) ≡ K c (by definition of lab).
Conversely, let lab be an edge-respecting labeling of G ρ . First, we build from lab a strict edge-respecting labeling lab ′ of G ρ . The values greater than M are divided in consecutive blocks of K consecutive values in such a way that if lab(n)lab( M, lev(n) ) = β > 0 then lab ′ (n) takes its value in the βth block.

0 z}|{ M block 1 z }| { M + 1 • • • M + K block 2 z }| { M + K + 1 • • • M + 2K . . . block γ z }| { M + (γ -1)K + 1 • • • M + γK . . .
Then the constraint mod(n) insures the unicity of lab ′ (n) such that lab ′ (n) ≡ K mod(n). A similar division is performed for the values smaller than m.

-For every n = x, i such that x, i

< -→ m, i , then lab ′ ( x, i ) def = α with • α ≡ K mod( x, i ), • m -(lab( m, i ) -lab( x, i )) × K ≤ α ≤ m -((lab( m, i ) -lab( x, i ) - 1) × K -1.
-For every x, i such that M, i

< -→ x, i , then lab ′ ( x, i ) def = α with • α ≡ K mod( x, i ), • M + ((lab( x, i ) -lab( M, i ) -1) × K + 1 ≤ α ≤ M + (lab( x, i ) - lab( M, i )) × K.
In both above cases, α is unique since it belongs to an interval of length K with a periodicity constraint that forces a unique value in this interval.

-For every x, i such that x, i

= -→ d, i for some d ∈ CONS ′ , lab ′ ( x, i ) = d. -For every d, i , lab ′ ( d, i ) = d.
lab ′ is well-defined because ρ is a sequence of satisfiable symbolic valuations with respect to φ. Moreover, lab ′ is a strict edge-respecting labeling. By way of example, suppose that n

< -→ n ′ , lev(n) ≤ lev(n ′ ), M, lev(n) < -→ n and M, lev(n ′ ) < -→ n ′ . We have lab( M, lev(n) ) < lab(n) < lab(n ′ )
because lab is edge-respecting and so, since the values of the (lab(n)lab( M, lev(n) )th block after M are greater than the values of (lab

(n ′ ) -lab( M, lev(n) )th block, lab ′ (n) < lab ′ (n ′ ).
Now, we show that the model σ defined by σ(i, x) = lab ′ ( x, i ) for all x ∈ VAR and i ∈ N satisfies ρ. By way of example, we show that X j x ∼ X k y ∈ ρ f (i) and j ≤ k implies σ, i |= X j x ∼ X k y. We have implications between the propositions below:

-X j x ∼ X k y ∈ ρ f (i) and j ≤ k, -x, i + j ∼ -→ y, i + k in G ρ (by definition of G ρ ), -lab( x, i + j ) ∼ lab ′ ( y, i + k ) (lab ′ is edge-respecting), -σ(i + j)(x) ∼ σ(i + k)(y) (by definition of σ), -σ, i |= X j x ∼ X k y (by definition of |=). ⊓ ⊔
Lemmas 7 states correspondences between ρ and its graphical representation G ρ . We now define a more abstract characterization of the one-step consistent sequences admitting a model. Lemma 8. Let ρ be a one-step consistent sequence. The graph G ρ has an edgerespecting labeling iff for all nodes n 1 , n 2 in G ρ , slen(n 1 , n 2 ) < ω.

Note that, by construction of G ρ , for all nodes d 1 , i and d 2 , j representing constants such that d 1 ≤ d 2 we have slen( d 1 , i , d 2 , j ) = d 2d 1 (see Corollary 1). That is why it suffices to consider nodes n 1 and n 2 that are not both constants.

Proof. If G ρ has an edge-respecting labeling lab, then one can easily show that for all nodes n 1 , n 2 in G ρ slen(n 1 , n 2 ) ≤ lab(n 2 )lab(n 1 ).

Conversely, if for all nodes n 1 , n 2 in G ρ , slen(n 1 , n 2 ) < ω, we define the following map lab : (VAR ∪ CONS ′ ) × N → Z:

-lab( d, i ) def = d. -If x, i = -→ d, i then lab( x, i ) def = d. -Otherwise, • If x, i < -→ m, i then lab( x, i ) def = α with 1. α ≡ K mod( x, i ). 2. m-slen( x, i , m, i )×K ≤ α ≤ m-(slen( x, i , m, i )-1)×K -1. • If M, i < -→ x, i then lab( x, i ) def = α with 1. α ≡ K mod( x, i ). 2. M + (slen( M, i , x, i ) -1) × K + 1 ≤ α ≤ M + slen( M, i , x, i ) × K.
Similarly to the proof of Lemma 7, each α is uniquely defined since it belongs to an interval of length K and the map mod forces a unique value in this interval. We now show that lab is a strict edge-respecting labeling of G ρ . If the labeling is not edge-respecting, then one of the following cases arises:

-Suppose n = -→ n ′ . We treat the case lev(n) < lev(n ′ ) (the symmetrical case has an analogous treatment).

Case 1: M, lev(n) < -→ n and M, lev(n ′ ) < -→ n ′ . Since n = -→ n ′ and M, lev(n) = -→ M, lev(n ′ ) , we have slen( M, lev(n) , n) = slen( M, lev(n ′ ) , n ′ ).
Hence lab(n) and lab(n ′ ) belong to the same block of size K after M . Moreover, ρ(lev(n)) is maximally consistent which entails mod(n) = mod(n ′ ) (by (MC6)) and lab(n) = lab(n ′ ).

Case 2: n < -→ m, lev(n) and n ′ < -→ m, lev(n ′ ) . Similar to Case 1. Case 3: M, lev(n) < -→ n and n ′ ∼ -→ M, lev(n ′ ) . Since ρ(lev(n)) is maximally consistent, by (MC2) we have n ∼ -→ M, lev(n ′ ) . So we obtain the path M, lev(n) < -→ n ∼ -→ M, lev(n ′ ) = -→ M, lev(n) ,
which leads to a contradiction using (MC3). ⊓ ⊔ So we have a characterization of the set of sequences having a model but what we really want is to recognize them with automata. The main difficulty rests on the fact that the set of satisfiable one-step consistent ω-sequences of satisfiable symbolic valuations is not ω-regular, as shown in [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF] for the fragment CLTL(Z). However, we can define an ω-regular condition such that every one-step consistent ultimately periodic sequence ρ is satisfiable iff G ρ satisfies this condition. An infinite word is ultimately periodic if it is of the form τ • δ ω for some finite words τ and δ. We will see in the following section that this approximation condition is enough for our purpose since satisfiable CLTL(IPC ⋆ ) formulas always have a ultimately periodic (symbolic) model. Let ρ be a onestep consistent symbolic valuation sequence and G ρ its graphical representation. An infinite forward (resp. backward) path in G ρ is defined as a sequence w : N → (VAR ∪ CONS ′ ) × N such that:

-for every i ∈ N, we have w(i)

∼ -→ w(i + 1) (resp. w(i + 1) ∼ -→ w(i)) in G ρ , -for every i ∈ N, we have lev(w(i)) < lev(w(i + 1)).
The path w is infinitely often strict iff for every i ≥ 0, there is j ≥ i such that w(j) < -→ w(j + 1) (resp. w(j + 1)

< -→ w(j)).
Definition 2. A graph G ρ satisfies the condition (C) iff there do not exist vertices n 1 and n 2 in G ρ with |lev(n 1 )lev(n 2 )| ≤ l satisfying (AP1) there is an infinite forward path w for from n 1 , (AP2) there is an infinite backward path w back from n 2 , (AP3) either w for or w back is infinitely often strict, and (AP4) for all i, j ∈ N, whenever |lev(w for (i))lev(w back (j))| ≤ l, w for (i)

< -→ w back (j) in G ρ .
A graph representation of some ρ not satisfying (C) is presented in Figure 3 where n 1 is a constant node.

n1 n2 < < < < < = = = = = < < < < Fig. 3. Gρ does not satisfy (C)
If ρ admits a model, then necessarily G ρ satisfies (C). Indeed, if G ρ does not satisfy (C), then slen(n 1 , n 2 ) = ω which entails that ρ has no model by Lemma 7 and 8. The converse does not hold in general. However, when ρ is ultimately periodic, the condition (C) is sufficient.

Lemma 9. Let ρ be a one-step consistent ω-sequence of satisfiable symbolic valuations which is ultimately periodic. Then ρ admits a model iff G ρ satisfies (C).

Thanks to the way G ρ is built from ρ, (C) does not explicitly refer to the constants in CONS and the constraints of the form x ≡ K c. Hence, Lemma 9 can be proved as [DD07, Lemma 6.2]: the map mod in G ρ is ignored and a uniform treatment for all nodes in (VAR ∪ CONS ′ ) × N is provided.

Let ρ = τ • δ ω be an ultimately periodic one-step consistent ω-sequence. If ρ admits a model then by Lemma 8 it satisfies the condition (C). Conversely, if ρ has no model then by Lemma 8 there exist two vertices n 1 and n 2 such that slen(n 1 , n 2 ) = ω. Intuitively, the proof uses this property to claim the existence between these two nodes of a finite path w long enough so that two paths w for and w back satisfying the conditions (AP1)-(AP4) can be deduced. The construction of w for and w back from w uses the periodicity of ρ by repeating infinitely finite subpaths and can be done smoothly by using the properties established in this section (see e.g. Lemma 6). This witnesses that G ρ does not satisfy (C).

As the proof is not essentially different from [DD07, Lemma 6.2] modulo slight changes mentioned above, we omit it here (see details in [START_REF] Gascon | Spécification et vérification de propriétés quantitatives sur des automates à contraintes[END_REF]).

Büchi automata and PSPACE upper bound

Based on the previous results and following the approach in [START_REF] Vardi | Reasoning about infinite computations[END_REF], we show that given a CLTL(IPC ⋆ ) formula φ, one can build a standard Büchi automaton A φ such that φ is CLTL(IPC ⋆ ) satisfiable iff L(A φ ) is non-empty. Moreover, we establish that nonemptiness of L(A φ ) can be checked in polynomial space in the size of φ (denoted by |φ|). The automaton A φ is precisely the intersection of three Büchi automata and its construction can be done quite smoothly thanks to the previous results. In the following, VAR, VAR ′ , CONS and CONS ′ are the sets of variables and constants associated to φ as defined in Section 4. Moreover, K, m and M are constants with their usual meaning and we use the map f : Terms(φ) → VAR ′ as previously.

Unlike LTL, the language recognized by the Büchi automaton A φ is not a set of models but rather a set of symbolic models. The alphabet Σ of this automaton is the set of symbolic valuations w.r.t. φ. As a consequence, a symbolic model for φ is an ω-sequence ρ : N → Σ. We naturally extend the symbolic satisfaction to sequences. The relation |= ′ is defined as |= except at the atomic level:

ρ, i |= ′ ξ def ⇔ ρ(i) |= symb f (ξ)
where |= symb is the satisfaction relation between symbolic valuations and constraints (see Section 3).

By Lemma 5 and using standard techniques for LTL [START_REF] Vardi | Reasoning about infinite computations[END_REF], checking whether there is a symbolic model ρ satisfying ρ |= ′ φ can be done in pspace (see more details below). Because every model for φ generates a unique symbolic model for φ (consequence of Lemma 4), we obtain the result below.

Lemma 10. A CLTL(IPC ⋆ ) formula φ is satisfiable iff there is a one-step consistent symbolic valuation ρ such that ρ |= ′ φ and ρ has a model. Proof. Let σ be a model that satisfies φ. Consider the symbolic valuation sequence ρ defined by: ρ(i) = sv (v i ) where for every i ∈ N, v i is the valuation such that v i (f (X j x)) = σ(i + j)(x). By construction, we have σ |= ρ. Using Lemma 4(II) we can show that for every v such that sv (v) = ρ(i) we have σ(i) |= ξ iff v |= ξ for every atomic subformula ξ of φ. By definition of the symbolic satisfaction relation, this implies that if σ |= ξ then ρ |= ′ ξ. Consequently, ρ |= ′ φ (induction on the structure of φ).

Conversely, suppose that ρ |= ′ φ and σ |= ρ for some σ and ρ. Since for every i ∈ N we have σ, i |= ρ(i), ρ(i) is the symbolic valuation corresponding to the valuation v i such that v i (f (X j x)) = σ(i + j)(x). By definition of |= ′ , this implies that for every atomic subformula ξ of φ, if ρ, i |= ′ ξ then σ, i |= ξ. Thus, we can show that ρ |= φ and σ |= ρ imply σ |= φ.

⊓ ⊔

The automaton A φ is formally defined as the intersection A LTL ∩ A 1cons ∩ A C of Büchi automata where -L(A LTL ) is the set of symbolic models satisfying φ, -L(A 1cons ) is the set of one-step consistent sequences of symbolic valuations, -L(A C ) is the set of sequences of symbolic valuations verifying (C).

We briefly explain below how these different automata are built. All of them are built over the alphabet Σ which is of exponential size in |φ|. The automaton A LTL is obtained from [START_REF] Vardi | Reasoning about infinite computations[END_REF] with a difference for atomic formulae. We define cl (φ) the closure of φ as usual, and an atom of φ is a maximally consistent subset of cl (φ). We define A LTL = (Q, Q 0 , δ, F ) as the generalized Büchi automaton below:

-Q is the set of atoms of φ and Q 0 = {X ∈ Q : φ ∈ X}, -X sv → Y is in δ iff (atomic constraints) for every atomic formula ξ in X, sv |= symb f (ξ), (one step) for every Xψ ∈ cl (φ), Xψ ∈ X iff ψ ∈ Y , -let {φ 1 Uψ 1 , . . . , φ r Uψ r } be the set of until formulas in cl (φ). We define F as the set {F 1 , . . . , F r } such that for every i ∈ {1, . . . , r},

F i = {X ∈ Q : φ i Uψ i ∈ Xor ψ i ∈ X}.
By Lemma 5, the condition about atomic formulae can be checked in pspace and so the transition relation can also be computed in pspace.

We define

A 1cons = Q, Q 0 , δ, F as a Büchi automaton such that Q = Q 0 = F = Q = Σ and the transition relation satisfies: sv sv ′′ -→ sv ′ is in δ def ⇔ sv
, sv ′ is one-step consistent and sv ′ = sv ′′ . Since checking whether a triple of sets of IPC ⋆ -constraints is a symbolic valuation and checking whether a pair of symbolic valuations is one-step consistent can both be done in polynomial time (see Lemma 3), the transition relation of A 1cons can be computed in polynomial time.

It remains to define A C that recognizes ω-sequences of symbolic valuations satisfying (C). As done in [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF], instead of building A C , it is easier to construct the Büchi automaton A ¬ C that recognizes the complement language of L(A C ). The automaton A ¬ C is essentially the automaton B defined in [DD07, Sect.6] except that we work with an extended alphabet. We need to consider vertices in the graph that represent constants in CONS ′ and equality between constants does not need to be explicitly present in the symbolic valuations. Apart from this point, the variables in VAR and the constants in CONS have a uniform treatment in the definition of A ¬ C . The automaton A ¬ C non-deterministically guesses in the first part of the run the vertices n 1 , n 2 and which path among w for and w back is infinitely often strict. Then it checks that the sequence fails to meet (C). The Büchi acceptance condition guarantees that <-labeled edges are infinitely often visited. We store all these pieces of information in the locations. For instance, if the automaton is in the location a, i, b, j, for , 0 at the position α ≥ 0 of the run, this means that:

-the position of the current vertex of the forward path is a, α + i , -the position of the current vertex of the backward path is b, α + j , -the forward path is infinitely often strict.

The last component is only used to note when the forward path visits a strict edge. It takes the value 1 (respectively 0) when the previous transition is (respectively is not) a <-transition.

Before defining formally A ¬ C , for a, a ′ ∈ VAR ∪ CONS ′ , ∼ ∈ {<, =} and i, j ∈ {0, . . . , l}, we write (X i a ∼ -→ X j a ′ ) ∈ G sv if there is an edge from the node representing X i a at the current position to the node representing X j a ′ (according to the definition of the edge relation in Section 4) which means that one of the following cases arises:

a, a ′ ∈ VAR and f (X i a) ∼ f (X j a ′ ) ∈ sv (see definition of f in Section 4).

-a ∈ VAR, a ′ ∈ CONS and f (X i a) ∼ a ′ ∈ sv . -a ′ ∈ VAR, a ∈ CONS and a ∼ f (X j a ′ ) ∈ sv . -a, a ′ ∈ CONS ′ and a ∼ a ′ . -a ∈ CONS ′ \ CONS, a ′ ∈ VAR and either ∼ is equality and a = f (X j a ′ ) ∈ sv or there is d ∈ CONS such that a < d and d ∼ f (X j a ′ ) ∈ sv or there is d ∈ CONS ′ such that a < d and d = f (X j a ′ ) ∈ sv . -a ′ ∈ CONS ′ \ CONS, a ∈ VAR and either ∼ is equality and f (X i a) = a ′ ∈ sv or there is d ∈ CONS such that d < a ′ and f (X i a) ∼ d ∈ sv or there is d ∈ CONS ′ such that d < a ′ and f (X i a) = d ∈ sv . Formally, A ¬ C = Q, Q 0 , →, F is defined as follows: -Q = {q 0 } ⊎ {(VAR ∪ CONS ′ ) × {0, . . . , l} × (VAR ∪ CONS ′ ) × {0, . . . , l} × {for , back } × {0, 1}} where l = |φ| X , -I = {q 0 },
-The transition relation → is defined as follows.

(a) q 0 sv -→ q 0 for every sv ∈ Σ.

(b) q 0 sv -→ a, i, b, j, for , 0 and q 0 sv -→ a, i, b, j, back , 0 for every a, b ∈ VAR ∪ CONS ′ , i, j ∈ {0, . . . , l}, sv ∈ Σ and X i a < X j b ∈ G sv .

(c) a, i, b, j, p, bin sv -→ a, i -1, b, j -1, p, bin for every p ∈ {for , back }, bin ∈ {0, 1}, i, j ≥ 1 and sv ∈ Σ.

(d) a, 0, b, j, for , bin sv -→ a ′ , i ′ -1, b, j -1, for , bin ′ s.t. i ′ > 0, j > 0 and • (a < -→ X i ′ a ′ ) ∈ G sv and bin ′ = 1; or (a = -→ X i ′ a ′ ) ∈ G sv and bin ′ = 0; • (X i ′ a ′ < -→ X j b) ∈ G sv .
These rules just check that there is a forward edge from the current node to the next node of the forward path. (e) a, i, b, 0, for, bin sv -→ a, i -1, b, j ′ -1, for , bin ′ if i > 0, j ′ > 0 and the conditions of (d) are verified when doing the following substitutions

a ← b, a ′ ← b ′ , b ← a.
This corresponds to check that there is a backward edge from the current node to the next node of the backward path. (f ) a, 0, b, 0, for, bin sv -→ a ′ , i ′ , b ′ , j ′ , for , bin ′ if the obvious combination of the constraints (d) and (e) is verified. (g) Similar conditions are needed to consider the case where the backward path is infinitely often strict.

-F is the set of states of the form a, i, b, j, p, 1 for every a, b ∈ VAR∪CONS ′ , i, j ∈ {0, . . . , l} and p ∈ {for , back }.

Lemma 11. A CLTL(IPC ⋆ ) formula φ is satisfiable iff L(A φ ) is nonempty.

The proof of this lemma is similar to [DD07, Lemma 6.3]. The main trick is to observe that if L(A φ ) is nonempty then A φ accepts an ultimately periodic ω-sequence so that Lemma 9 can be applied. Since given a formula φ we can effectively construct A φ and check whether L(A φ ) is nonempty, the model-checking and satisfiability problems for CLTL(IPC ⋆ ) are decidable. We also have all the arguments to establish the pspace upper bound by using arguments from [START_REF] Safra | On the complexity of ω-automata[END_REF].

Theorem 1. The satisfiability problem for CLTL(IPC ⋆ ) is pspace-complete.

Proof. pspace-hardness is a consequence of the pspace-hardness of LTL [START_REF] Sistla | The complexity of propositional linear temporal logic[END_REF]. As far as the pspace upper bound is concerned, the automata A LTL , A 1cons and A ¬ C are of exponential size in |φ| and can be built in polynomial space in |φ|.

The automaton A C is obtained from A ¬ C by Safra's construction [START_REF] Safra | On the complexity of ω-automata[END_REF] to complement a Büchi automaton. A ¬ C has a number of states polynomial in |φ|, say P (|φ|). From this, we can build a deterministic Streett automaton which accepts the complement of the language accepted by A ¬ C and has O(2 P (|φ|)×log(|φ|) ) states. These are the same arguments as in the proof of [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF]Theorem 6.6]. This automaton can be converted to an equivalent Büchi automaton A C with the same order of states. Hence, A C can be built in polynomial space in |φ|.

So, computing the intersection automaton A φ = A LTL ∩ A 1cons ∩ A C can be done in polynomial space in |φ|. Since the emptiness problem for Büchi automata is nlogspace-complete, by [BDG88, Corollary 3.36], we finally get that testing emptiness of L(A φ ) can be done non-deterministically in polynomial space in |φ|. As usual, by Savitch's theorem we get the pspace upper bound.

⊓ ⊔

Note that, all the temporal operators in CLTL(IPC ⋆ ) are definable in monadic second order logic (MSO). By using [START_REF] Gastin | Satisfiability and model checking for MSOdefinable temporal logics are in PSPACE[END_REF], it is immediate that any extension of CLTL(IPC ⋆ ) obtained by adding a finite amount of MSO-definable temporal operators remains in pspace. Only the automaton A LTL needs to be updated.

Another corollary is that the model-checking of the linear-time fragment of the logic of [ Čer94] against integral relational automata is in pspace (only decidability is established by [ Čer94]).

Corollary 2. The model-checking problem for integral relational automata restricted to the LTL fragment of CCTL * introduced in [ Čer94] is in pspace.

Conclusion

In this paper, we have introduced the logic CLTL(IPC ⋆ ) extending formalisms in [ Čer94,LM01,DD07,Dem06] and we have shown that both model-checking over IPC ⋆ -automata and satisfiability are decidable in polynomial space. The proof heavily relies on a translation into the nonemptiness problem for standard Büchi automata and on the approximation of non ω-regular sets of symbolic models. As a by-product, the model-checking problem over the integral relational automata defined in [ Čer94] is also pspace-complete when restricted to its LTL fragment. The logic CLTL(IPC ⋆ ) supports a rich class of constraints including those of the form x < y unlike periodicity constraints from [START_REF] Demri | LTL over integer periodicity constraints[END_REF] (which are quite useful to compare absolute dates) and comparison with constants unlike logics shown in pspace in [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF]. Abstraction of counter automata by performing reasoning modulo can be encoded in CLTL(IPC ⋆ ) thanks to the presence of integer periodicity constraints.

To conclude, we mention a few open problems that are worth investigating.

-The model checking of CTL* for integral relational automata is undecidable [ Čer94] whereas we have shown that its LTL fragment is pspacecomplete. Moreover, it is shown in [START_REF] Bozzelli | Branching-time temporal logic extended with presburger constraints[END_REF] that the existential and universal fragments have a decidable model checking problem (complexity is not known). It would be interesting to design other decidable branching-time extensions of CLTL(IPC ⋆ ). -The decidability status of the satisfiability problem of the full CTL * extension is also an open question.

-The decidability status of constraint LTL over the domain {0, 1} * , ⊆ is open either with the subword relation or with the prefix relation. Note that constraint LTL over the domain {0} * , ⊆ is already equivalent to constraint LTL over N, <, = that is a strict fragment of CLTL(IPC ⋆ ).

A Integral relational automata are restricted IPC ⋆ -automata

An integral relational automata (RA) is defined in [ Čer94] as a program with a finite amount of variables interpreted in Z. The set OP of operations is composed of the following instructions and guards:

- Observe that equality between variables can be tested by performing two negative tests on a < b and b < a.

comparisons
From a relational automaton A = Q, δ, op, g , we build a restricted IPC ⋆automaton A ′ , having an isomorphic configuration graph in a sense to be precised below. Given A = Q, δ, op, g , the restricted IPC ⋆ -automaton A ′ = Q ′ , Q ′ 0 , δ ′ , F ′ is defined as follows:

1. Q ′ = Q ′ 0 = F ′ = Q.
Without any loss of generality, we can assume that Q is a finite set of Z constants not occurring in op. 2. To each e = n, n ′ in A, we associate n φe -→ n ′ in δ ′ , where φ e is a conjunction of constraints defined as follows:

  ) and each element of CONS ′ can be encoded in binary representation with O(|M |) bits.

Fig. 2 .∼0-→ n 1 ∼1-→ n 2 ∼2-

 212 Fig. 2. A graph Gρ

  lev(n α ) and using the property (MC2), we getd, lev(n α ) ∼ ′-→ n α and ∼ ′ equals < if w is strict (and = otherwise).(III) Similar to (II).

  block

  , lev(n) and m, lev(n ′ ) ∼ -→ n ′ . Similar to Case 3. Case 5: n = -→ d, lev(n) and n ′ = -→ d ′ , lev(n ′ ) with d < d ′ . Since ρ(lev(n)) is maximally consistent, by (MC2) and (MC3) we have d = d ′ which leads to a contradiction. -The case n < -→ n ′ can be done in a similar fashion.

  of the form x < y, x < d, d < y, -assignments of the form x ← y, x ← d, -input value ?x, -output value !x or !d, -dummy operation NOP, where x, y are variables and d is a constant in Z. A relational automaton A = Q, δ, op, g[ Čer94] is a finite directed graph where-Q is a finite set of control states, δ ⊆ Q × Q, op : Q → OP, g : δ → {+, -}.Let Var (A) and Cons(A) be respectively the sets of variables and constants occuring in op. A configuration of A is a pair n, v where n ∈ Q and v is a map v : Var (A) ∪ Cons(A) → Z equal to identity for its restriction to Cons(A). The configuration graph of A is defined as the pair S, → where S is the set of configurations of A and n, v → n ′ , v ′ iff there exists e = n, n ′ ∈ δ such that 1. v and v ′ are related depending on the nature of op(n):-if op(n) is ?x, then for every y ∈ Var (A) \ {x}, v ′ (y) = v(y), -if op(n) is an output value or the dummy operation, then v ′ = v, -if op(n) is x ← a, then v ′ = v[x ← v(a)], -if op(n) is a < b, then v = v′ and either g(e) = + and v(a) < v(b), or g(e) =and v(a) ≥ v(b), where a, b ∈ Var (A)∪Cons(A), v(x) denotes the value of x in v and v[x ← a] is such that v[x ← z](y) = z if x = y and v[x ← z](y) = v(y) otherwise.

  Two constraints are equivalent iff they are satisfied by the same valuations.Lemma 1. (I)The satisfiability problem for IPC ⋆ is pspace-complete. (II) For every constraint in IPC ⋆ there exists an equivalent quantifier-free constraint in IPC ⋆ .Proof. (I) Satisfiability for IPC ++ is pspace-complete [Dem06] whereas satisfiability for Z is nlogspace-complete. Since constraints in IPC ⋆ are Boolean combinations of IPC ++ and Z constraints, IPC ⋆ satisfiability is in pspace by simply adapting the proof of [Dem06, Theorem 3]. pspace-hardness is a consequence of the pspace-hardness of IPC ++ .

  . . , d n in Z |VAR| (viewed as maps VAR → Z) such that d 1 , . . . , d n |= sv . It is easy to show that {V sv : sv is a symbolic valuation built w.r.t. X and V sv = ∅} is a partition of Z |VAR| . (II) By structural induction on ξ. The proof is similar to the proof of [Dem06, Lemma 1]. ⊓ ⊔ Note that by Lemma 4, a symbolic valuation is an equivalence class of valuations. Given a symbolic valuation sv and a constraint ξ, we write sv |= symb ξ

	def ⇔ for
	every valuation v such that sv

Acknowledgments. We would like to thank the anonymous referees for their numerous and useful suggestions, remarks, etc. improving significantly the quality of the paper.

-Xic = n ′ is a conjunct of φ e where ic is a new variable taking care of the instruction counter, -if op(n) =?x then y∈VAR(A)\{x} y = Xy belongs to φ e , -if op(n) is an output or a dummy operation, then y∈VAR(A) y = Xy belongs to φ e ,

The configuration graphs of A and A ′ are isomorphic with the following property. The transition n, v -→ n ′ , v ′ belongs to the configuration graph of A iff n, v -→ n ′ , v ′ belongs to the configuration graph of A ′ where v :

The map v ′ is defined similarly. As a corollary, the LTL fragment of CLTL* defined in [ Čer94] where the atomic formulae are of the form n, x < y and x = y, can be reduced to the model-checking problem for restricted IPC ⋆automata (just replace n by ic = n to obtain CLTL(IPC ⋆ ) formulae).