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

Alexander Rabinovich

The complexity of temporal logic with until and since over ordinals

We consider the temporal logic with since and until modalities. This temporal logic is expressively equivalent over the class of ordinals to first-order logic thanks to Kamp's theorem. We show that it has a pspace-complete satisfiability problem over the class of ordinals. Among the consequences of our proof, we show that given the code of some countable ordinal α and a formula, we can decide in pspace whether the formula has a model over α. In order to show these results, we introduce a class of simple ordinal automata, as expressive as Büchi ordinal automata. The pspace upper bound for the satisfiability problem of the temporal logic is obtained through a reduction to the nonemptiness problem for the simple ordinal automata.

Introduction

The main models for time are N, < , the natural numbers as a model of discrete time and R, < , the real line as the model for continuous time. These two models are called the canonical models of time. A major result concerning linear-time temporal logics is Kamp's theorem [START_REF] Kamp | Tense Logic and the theory of linear order[END_REF][START_REF] Gabbay | Temporal Logic -Mathematical Foundations and Computational Aspects[END_REF] which says that LTL(U, S), the temporal logic having "Until" and "Since" as only modalities, is expressively complete for first-order monadic logic of order over the class of Dedekind complete linear orders. The canonical models of time are indeed Dedekind-complete. Another important class of Dedekind-complete orders is the class of ordinals, see e.g. an axiomatization of LTL(U, S) over ordinals in [START_REF] Venema | Completeness via completeness: Since and until[END_REF]. In this paper the satisfiability problem for the temporal logic with until and since modalities over the class of ordinals is investigated. Our main results are the following: the satisfiability problem for LTL(U, S) over the class of ordinals is pspace-complete and a formula φ in LTL(U, S) has some α-model for some ordinal α iff it has an β-model for some β < ω |φ|+2 where |φ| is the size of φ.

In order to prove these results we use an automata-based approach [START_REF] Vardi | Reasoning about infinite computations[END_REF]. In Section 3, we introduce a new class of ordinal automata which we call simple ordinal automata. These automata are expressive equivalent to Büchi automata over ordinals [START_REF] Büchi | The monadic second order theory of all countable ordinals[END_REF]. However, the locations and the transition relations of these automata have additional structures as in [START_REF] Vardi | Reasoning about infinite computations[END_REF][START_REF] Rohde | Alternating Automata and The Temporal Logic of Ordinals[END_REF]. In particular, a location is a subset of a base set X. Herein, we provide a translation from formulae in LTL(U, S) into simple ordinal automata that allows to characterize the complexity of the satisfiability problem for LTL(U, S). However, the translation of the formula φ into the automaton A φ provides an automaton of exponential size in |φ| but the base of A φ has a cardinality linear in |φ|. Section 4 contains our main technical lemmas. We show there that every run in a simple ordinal automaton is equivalent to a short run. Consequently, we establish that a formula φ ∈ LTL(U, S) has an α-model iff it has a model of length trunc |φ|+2 (α) where trunc |φ|+2 (α) is a truncated part of α strictly less than ω |φ|+2 × 2 (see the definition of truncation in Section 2). In Section 5 we present two algorithms to solve the nonemptiness problem for simple ordinal automata. The first one runs in (simple) exponential time and does not take advantage of the short run property. The second algorithm runs in polynomial space and the short run property plays the main role in its design and its correctness proof.

In Section 6 we investigate several variants of the satisfiability problem and show that all of them are pspace-complete. Section 7 compares our results with related works. The satisfiability problem for LTL(U, S) over ω-models is pspacecomplete [START_REF] Sistla | The complexity of propositional linear temporal logic[END_REF]. Reynolds [START_REF] Reynolds | The complexity of the temporal logic with until over general linear time[END_REF][START_REF] Reynolds | The complexity of the temporal logic over the reals[END_REF] proved that the satisfiability problem for LTL(U, S) over the reals is pspace-complete. The proofs in [START_REF] Reynolds | The complexity of the temporal logic with until over general linear time[END_REF][START_REF] Reynolds | The complexity of the temporal logic over the reals[END_REF] are non trivial and difficult to grasp and it is therefore difficult to compare our proof technique with those of [START_REF] Reynolds | The complexity of the temporal logic with until over general linear time[END_REF][START_REF] Reynolds | The complexity of the temporal logic over the reals[END_REF] even though we believe cross-fertilization would be fruitful. We provide uniform proofs and we improve upper bounds for decision problems considered in [START_REF] Cachat | Controller synthesis and ordinal automata[END_REF][START_REF] Demri | Reasoning about transfinite sequences[END_REF][START_REF] Rohde | Alternating Automata and The Temporal Logic of Ordinals[END_REF]. We also compare our results and techniques with Rohde's thesis [START_REF] Rohde | Alternating Automata and The Temporal Logic of Ordinals[END_REF]. Finally we show how our results entail most of the results from [START_REF] Demri | Reasoning about transfinite sequences[END_REF] and we solve some open problems stated there.

Temporal logic with Until and Since

The formulae of LTL(U, S) are defined as follows:

φ ::= p | ¬φ | φ 1 ∧ φ 2 | φ 1 Uφ 2 | φ 1 Sφ 2
where p ∈ PROP for some set PROP of atomic propositions. Given a formula φ in LTL(U, S), we write sub(φ) to denote the set of subformulae of φ or their negation assuming that ¬¬ψ is identified with ψ. The size of φ is defined as the cardinality of sub(φ) and therefore implicitly we encode formulae as DAGs. This feature will be helpful for defining translations that increase polynomially the number of subformulae but for which the tree representation might suffer an exponential blow-up. We use the following abbreviations Gφ = φ ∧ ¬( U¬φ) and Fφ = ¬G¬φ that do cause only a polynomial increase in size.

The satisfaction relation is inductively defined below where σ is an α-model of the form α → P(PROP) for some ordinal α > 0 (β < α):

-σ, β |= p iff p ∈ σ(β), -σ, β |= ¬φ iff not σ, β |= φ, σ, β |= φ 1 ∧ φ 2 iff σ, β |= φ 1 and σ, β |= φ 2 , -σ, β |= φ 1 Uφ 2 iff there is γ ∈ (β, α) such that σ, γ |= φ 2 and for every γ ∈ (β, γ), we have σ, γ |= φ 1 , -σ, β |= φ 1 Sφ 2 iff there is γ ∈ [0, β) such that σ, γ |= φ 2 and for every γ ∈ (γ, β), we have σ, γ |= φ 1 .
The satisfiability problem for LTL(U, S) consists in determining, given a formula φ, whether there is a model σ such that σ, 0 |= φ.

We recall that well orders are particular cases of Dedekind complete linear orders. Indeed, a chain is Dedekind complete iff every non-empty bounded subset has a least upper bound. Kamp's theorem applies herein.

Theorem 1. (I) [START_REF] Kamp | Tense Logic and the theory of linear order[END_REF] LTL(U, S) over the class of ordinals is as expressive as the first-order logic over the class of structures α, < where α is an ordinal. (II) [START_REF] Büchi | The monadic second order theory of all countable ordinals[END_REF] The satisfiability problem for LTL(U, S) over the class of ordinals is decidable.

Hence, LTL(U, S) is a fundamental logic to be studied. Moreover, another key result is the pspace-completeness of LTL(U, S) restricted to ω-models [START_REF] Sistla | The complexity of propositional linear temporal logic[END_REF].

We recall below some definability results that will be used in Sections 6 and 7. Ordinals strictly below ω ω can be defined in LTL(U, S) with the truth constant (no propositional variable).

Lemma 2. Given an ordinal 0

< α = ω k 1 a k 1 + • • • ω k m a k m < ω ω with k 1 > . . . > k m ≥ 0, a k 1 , . . . a k m > 0, there is a formula def α in LTL(U, S) of linear size in Σ i (k i × a k i ) such that for any model σ, we have σ, 0 |= def α iff σ is of length α.
3 Translation from formulae to simple ordinal automata

In Section 3.1, we introduce a new class of ordinal automata which we call simple ordinal automata. These automata are expressive equivalent to Büchi automata over ordinals [START_REF] Büchi | The monadic second order theory of all countable ordinals[END_REF]. However, the locations and the transition relations of these automata have additional structures. In Section 3.2, we provide a translation from LTL(U, S) into simple ordinal automata which assigns to every formula in LTL(U, S) an automaton that recognizes exactly its models. We borrow the automata-based approach for temporal logics from [VW94,KVW00].

Simple ordinal automata Definition 3. A simple ordinal automaton

A is a structure X, Q, δ next , δ lim such that -X is a finite set (the basis of A), Q ⊆ P(X) (the set of locations), -δ next ⊆ Q × Q is the next-step transition relation, -δ lim ⊆ P(X) × Q is the limit transition relation.
A can be viewed as a finite directed graph whose set of nodes is structured. Given a simple ordinal automaton A, an α-path (or simply a path) is a map r : α → Q for some α > 0 such that -for every β + 1 < α, r(β), r(β + 1) ∈ δ next , -for every limit ordinal β < α, always(r, β), r(β) ∈ δ lim where always(r, β)

def = {a ∈ X : ∃ γ < β such that a ∈ ∩ γ ∈(γ,β) r(γ )}.
The set always(r, β) contains exactly the elements of the basis that belong to every location from some γ < β until β. We sometimes write always(r) instead of always(r, α) when α is a limit ordinal or always(r) instead of always(r, α -1) when α is a successor ordinal and α -1 is a limit ordinal.

Given an α-path r, for β, β < α we write r ≥β to denote the restriction of r to positions greater or equal to β, r ≤β to denote the restriction of r to positions less or equal to β, r [β,β ) to denote the restriction of r to positions in [β, β ) (half-open interval).

A simple ordinal automaton with acceptance conditions is a structure of the form X, Q, I, F, F, δ next , δ lim where -I ⊆ Q is the set of initial locations, -F ⊆ Q is the set of final locations for accepting runs whose length is some successor ordinal, -F ⊆ P(X) encodes the accepting condition for runs whose length is some limit ordinal.

Given a simple ordinal automaton with acceptance conditions, an accepting run is a path r : α → Q such that r(0) ∈ I and

-if α is a successor ordinal, then r(α -1) ∈ F , -otherwise {a ∈ X : ∃ γ < α such that a ∈ ∩ γ ∈(γ,α) r(γ )} ∈ F.
The nonemptiness problem for simple ordinal automata consists in checking whether A has an accepting run.

Our current definition for simple ordinal automata does not make them language acceptors since they have no alphabet. It is possible to add in the definition a finite alphabet Σ and to define the next-step transition relation as a subset of Q × Σ × Q. If we do so, our model of automata can recognize the same languages as the usual ordinal automata with Muller acceptance conditions in the limit transitions. The proof is not very difficult. Additionally, the current definition can be viewed as the case either when the alphabet is a singleton or when the read letter is encoded in the locations through the dedicated elements of the basis. This second reading will be in fact used implicitly in the sequel.

We also write A to denote either a simple ordinal automaton or its extension with acceptance conditions.

Translation from LTL(U, S) formulae to simple ordinal automata

As usual, a set Y is a maximally Boolean consistent subset of sub(φ) when the following conditions are satisfied: for every ψ ∈ sub(φ), ¬ψ ∈ Y iff ψ ∈ Y and for every

ψ 1 ∧ ψ 2 ∈ sub(φ), ψ 1 ∧ ψ 2 ∈ Y iff ψ 1 , ψ 2 ∈ Y . Given a formula φ, the simple ordinal automaton A φ = X, Q, I, F, F, δ next , δ lim is defined as follows: -X = sub(φ).
-Q is the set of maximally Boolean consistent subsets of sub(φ).

-I is the set of locations that contain φ and no since formulae. -F is the set of locations with no elements of the form

ψ 1 Uψ 2 . -F is the set of sets Y such that not {ψ 1 , ¬ψ 2 , ψ 1 Uψ 2 } ⊆ Y , for every ψ 1 Uψ 2 ∈ X.
-For all q, q ∈ Q, q, q ∈ δ next iff the conditions below are satisfied:

(next U ) for ψ 1 Uψ 2 ∈ sub(φ), ψ 1 Uψ 2 ∈ q iff either ψ 2 ∈ q or ψ 1 , ψ 1 Uψ 2 ∈ q , (next S ) for ψ 1 Sψ 2 ∈ sub(φ), ψ 1 Sψ 2 ∈ q iff either ψ 2 ∈ q or ψ 1 , ψ 1 Sψ 2 ∈ q.
-For all Y ⊆ X and q ∈ Q, Y, q ∈ δ lim iff the conditions below are satisfied:

(lim U 1) if ψ 1 , ¬ψ 2 , ψ 1 Uψ 2 ∈ Y , then either ψ 2 ∈ q or ψ 1 , ψ 1 Uψ 2 ∈ q, (lim U 2) if ψ 1 , ψ 1 Uψ 2 ∈ q and ψ 1 ∈ Y , then ψ 1 Uψ 2 ∈ Y , (lim U 3) if ψ 1 ∈ Y , ψ 2 ∈ q and ψ 1 Uψ 2 is in the basis X, then ψ 1 Uψ 2 ∈ Y , (lim S ) for every ψ 1 Sψ 2 ∈ sub(φ), ψ 1 Sψ 2 ∈ q iff (ψ 1 ∈ Y and ψ 1 Sψ 2 ∈ Y ).
Even though the conditions above can easily be shown correct, at this stage it might sound mysterious how they have been made up. For some of them, their justification comes with the proof of Lemma 4.

Let σ be an α-model and φ be a formula in LTL(U, S). The Hintikka sequence for σ and φ is an α-sequence H σ,φ defined as follows: for every β < α,

H σ,φ (β) def = {ψ ∈ sub(φ) : σ, β |= ψ}.

Short run properties

Let A be a simple ordinal automaton and Y be a subset of its basis. Y is said to be present in A iff there is a limit transition of the form Y, q in A. Given a set Y present in A, its weight, noted weight(Y ), is the maximal l such that

Y 1 ⊂ Y 2 ⊂ • • • ⊂ Y l is a sequence of present subsets in A and Y 1 = Y . Obviously, weight(Y ) ≤ |X| + 1.
Given a path r : α → Q in A with α ≥ ω + 1, its weight, noted weight(r), is the maximal value in the set {weight(always(r, β)) : β < α, β is a limit ordinal}.

By convention, if a path is of length strictly less than ω + 1, then its weight is zero (no limit transition is fired). Furthermore, we write exists(r) to denote the set β<α r(β) and all(r) to denote the set β<α r(β). For example, all(r) corresponds to the set of elements from the basis that are present in all locations of the run r. Let r, r be two paths of respective length α+1 and α +1, we say that they are congruent (noted r ∼ r ) iff the conditions below are meet: r(0) = r (0), r(α) = r (α ), exists(r) = exists(r ) and all(r) = all(r ). We can easily adapt the congruence relation to runs r and r of length some limit ordinal by requiring that always(r) = always(r ) instead of the condition on final locations for runs of length some successor ordinal.

Let r 1 be a path of length α + 1 and r 2 be a path of length β such that r 1 (α) = r 2 (0). The concatenation r 1 • r 2 is the path r of length α + β such that for γ ∈ [0, α], r(γ) = r 1 (γ) and for γ ∈ [0, β), r(α + γ) = r 2 (γ). For every ordinal α, the concatenation of α-sequences of paths is defined similarly. The relation ∼ can be viewed as a congruence for the concatenation operation on paths.

Lemma 5. (I) Let r • r 0 • r , r 1 be two paths such that r 0 ∼ r 1 . Then, r • r 1 • r is a path that is congruent to r • r 0 • r . (II) Let r 0 0 , r 1 0 , r 2 0 , . . . and r 0 1 , r 1 1 , r 2 1 , .
. . be two ω-sequences of pairwise consecutive paths such that for i ≥ 0, r i 0 ∼ r i 1 and their length is a successor ordinal.

If r • r 0 0 • r 1 0 • r 2 0 • . . . • r is a path, then it is congruent to r • (r 0 1 • r 1 1 • r 2 1 • . . .) • r .
The proof of the above lemma is by an easy verification.

Lemma 6. Let r : α → Q be a path in A. Then, there is a path r : α → Q such that α < ω weight(r)+1 and r ∼ r .

Lemma 6 states a crucial property for most of complexity results established in the sequel. Indeed, for usual ordinal automata, it is not possible to get this polynomial bound as an exponent of ω for the length of the short paths. Actually, the exponent is linear in the cardinal of its basis and can be logarithmic in the number of locations for large automata. By combination of Lemma 4 and Lemma 6, we obtain the following interesting result.

Corollary 7. If φ is satisfiable, then φ has an α-model with α < ω |φ|+2 .
This can be still be refined a little more by observing that for each ω i × a occurring in the Cantor normal form of the length of a small model of φ (strictly less than ω |φ|+2 ), a is bounded by 2 |φ|-1 since the cardinal of the set of locations of A φ is bounded by 2 |φ|-1 .

For n ∈ N, let trunc n be the function that assigns to every ordinal α > 0 an ordinal in (0, ω n 2) as follows. α can be written in the form

α = ω n γ + β with β ∈ [0, ω n ). Then trunc n (α) = ω n × min(γ, 1) + β.
Lemma 8. Let A be a simple ordinal automaton.

(I) If r is a path of length ω weight(r)+1 × α for some countable ordinal α > 0, then there is a path r of length ω weight(r)+1 such that r ∼ r . (II) If a path r has length ω weight(r)+1 , then for every ordinal α > 0, there is a path r of length ω weight(r)+1 × α such that r ∼ r . (III) If r is a path of length α and β ≈ |X|+1 α, then there is a path r of length β such that r ∼ r .

Only in (I), α is supposed to be countable. Because of the translation from formulae to automata, we can also establish a pumping lemma at the level of formulae.

Lemma 9.

(I) Let A be a simple ordinal automaton with acceptance conditions and α, β be ordinals such that α ≈ |X|+1 β. Then, A has an accepting run of length α iff A has an accepting run of length β. (II) Let φ be a formula in LTL(U, S) and α, β be ordinals such that α ≈ |φ|+2 β.

Then φ has an α-model iff φ has a β-model.

Proof. (I) Direct consequence of Lemma 6 and Lemma 8 since accepting runs can be viewed as paths.

(II) By Lemma 4, φ has an α-model iff A φ has an accepting run r of length α.

Since |φ| + 1 bounds the weight of any path in A φ and by (I), we get that A φ has an accepting run r of length α iff A φ has an accepting run r of length β.

Equivalently, φ has a β-model.

Checking nonemptiness of simple ordinal automata

In this section, we provide algorithms to check whether a simple ordinal automata admits accepting runs. The first one is in exptime. Our optimal algorithm runs in polynomial space in the size of the basis.

Let A be a simple ordinal automaton X, Q, I, F, F, δ next , δ lim . We provide below an algorithm to check given q, q ∈ Q and n ∈ N whether there is path r : α + 1 → Q such that r(0) = q, r(α) = q and α < ω n . Given an (α + 1)-path we write abs(r) to denote the quadruple r(0), exists(r), all(r), r(α) . We define a family of relations containing the quadruples of the form abs(r). Each relation

R i below is therefore a subset of R i ⊆ Q × P(X) 2 × Q.
-R 0 = { q, q ∪ q , q ∩ q , q : q, q ∈ δ next }, -For i ∈ N,

R i = { q 0 , m i=0 E i , m i=0 A i , q m+1 : ∃ q 0 , E 0 , A 0 , q 1 R i q 1 , E 1 , A 1 , q 2 R i • • • R i q m , E m , A m , q m+1 } -For i ∈ N, R i+1 is defined from R i as follows: q, E, A, q ∈ R i+1 iff
• either q, E, A, q ∈ R i

• or there exist a limit transition Y, q ∈ δ lim and a path

q 0 , E 0 , A 0 , q 1 R i q 1 , E 1 , A 1 , q 2 R i • • • R i q m , E m , A m , q m+1
such that (a) q 0 = q m+1 , (b)

m i=0 A i = Y , (c) q, E , A , q 0 ∈ R i for some E , A , (d) E = (E ∪ q ) ∪ m i=0 E i , A = (A ∩ q ) ∩ m i=0 A i . Because R i ⊆ R i+1 for all i, for some N ≤ 2 4×|X| + 1, R N +1 = R N .
The bound 2 4×|X| + 1 takes simply into account that Q ⊆ P(X).

Lemma 10. (I) If q, E, A, q ∈ R n , then there is an (α + 1)-path such that abs(r) = q, E, A, q and α < ω n . (II) Conversely, let r : α + 1 → Q be a path such that α < ω n . Then abs(r) ∈ R n .

We provide below a first complexity result.

Lemma 11. nonemptiness problem for simple ordinal automata with acceptance conditions can be checked in exponential time in |X|.

Proof. Let A be of the form X, Q, I, F, F, δ next , δ lim . A has an accepting run iff either (A) there are q 0 ∈ I, q f ∈ F and E, A ⊆ X such that q 0 , E, A, q f ∈ R n for some n or (B) there are q 0 ∈ I, and a run r from q 0 such that always(r) ∈ F. (A) deals with accepting runs of length some successor ordinal, whereas (B) deals with accepting runs of length some limit ordinal.

By Lemma 6 and Lemma 10(II), in order to check (A), it is sufficient to test for q 0 , E, A, q f ∈ I × P(X) 2 × F whether q 0 , E, A,

q f ∈ R |X|+2 ⊆ R |X|+3 . Since |Q| is in O(2 |X| ), computing R |X|+3 takes |X| + 3
steps that requires polynomial time in |A| and exponential time in |X|, we obtain the desired result. Observe that we can take advantage of the fact that computing the transitive closure of a relation and the maximal strongly connected components can be done in polynomial time in the size of the relations.

By Ramsey theorem, (B) is equivalent to the following condition: there are q ∈ Q, E, E , A ⊆ X, A ∈ F and runs r 1 and r 2 such that abs(r 1 ) = q 0 , E, A, q and abs(r 2 ) = q, E , A , q .

Hence. in order to check these, it is enough to check whether there are q 0 ∈ I, q ∈ Q and E, A ⊆ X such that q 0 , E, A, q ∈ R |X|+2 , q, E , A , q ∈ R |X|+2 and A ∈ F. This can be done in exponential time as for (A).

The proof of Lemma 11 mentions Lemma 6 but the exponential time upper bound can be obtained by observing that an exponential number of steps, such as 2 4×|X| + 1 would provide the same bound in the worst case. As a corollary of Lemma 11, satisfiability for LTL(U, S) is in exptime. Moreover, this can be improved as shown in the proof of Theorem 13 presented in Section 6.

We improve below the bound in Lemma 11.

Theorem 12. The nonemptiness problem for simple ordinal automata can be checked in polynomial space in |X|.

Proof. Following the proof of Lemma 11, A has an accepting run iff (A) there are q 0 ∈ I, q f ∈ F and E, A ⊆ X such that q 0 , E, A, q f ∈ R |X|+3 or (B) there are q 0 ∈ I, q ∈ Q and E , A ⊆ X such that q 0 , E , A , q ∈ R |X|+3 , q, E , A , q ∈ R |X|+3 and A ∈ F. X denotes the basis of A. In order to check (A), the nondeterministic algorithm guesses q 0 ∈ I, q f ∈ F and E, A ⊆ X (encoded in polynomial space in O(|X|) and test whether PATH(A, q 0 , E, A, q f , |X| + 3) returns true. Condition (B) admits a similar treatment. The non-deterministic algorithm PATH defined below works in polynomial space in |X| assuming that the last argument is polynomial in |X| which is the case with |X| + 3. Figure 1 contains the definition of the function PATH (some details are omitted).

PATH(A, q, E, A, q , N )

-If N = 0 then (if (either E = q ∪ q or A = q ∩ q or q, q ∈ δ next ) then abort else return ); -If N > 0 then go non-deterministically to 1.,2. or 3.

(1.) Return PATH(A, q, E, A, q , N -1) (2.) Guess on-the-fly a sequence

q 0 , E 0 , A 0 , q 1 , q 1 , E 1 , A 1 , q 2 , . . . , q m , E m , A m , q m+1 such that • m < 2 4×|X|+1 + 1, • for 0 ≤ i ≤ m, PATH(A, q i , E i , A i , q i+1 , N -1) returns , • E = S j E j and A = T j A j • q = q 0 , q = q m+1 ;
(3.) We guess here two long sequences:

(3.1) Guess on-the-fly a sequence q 0 , E 0 , A 0 , q 1 , q 1 , E 1 , A 1 , q 2 , . . . , q m , E m , A m , q m+1 such that

• m < 2 4×|X|+1 + 1, • for 0 ≤ i ≤ m, PATH(A, q i , E i , A i , q i+1 , N -1) returns , • E = S j E j and A = T j A j ; • q 0 = q;
(3.2) Guess a limit transition Y, q ∈ δ lim and on-the-fly a sequence q 0 , E 0 , A 0 , q 1 , q 1 , E 1 , A 1 , q 2 , . . . , q m , E m , A m , q m +1 such that In (2.), guessing on-the-fly a long sequence means that only two consecutive quadruples are kept in memory at any time. We need a counter to guarantee that m < 2 4×|X|+1 and it requires only space in O(|X|). Moreover, in order to check E = j E j and A = j A j we need two auxiliary variables that bookkeep the E j and A j so far respectively. Similar techniques are used in (3.) to guarantee that this non-deterministic algorithm requires only polynomial space in O(|X| + N ) (we only need more variables and steps). It is straightforward to show that PATH(A, q, E, A, q , N ) has a computation that returns (all the guesses were correct) iff q, E, A, q ∈ R N . Finally Savitch's Theorem allows to conclude that nonemptiness can be checked in deterministic polynomial space in |X|.

• m < 2 4×|X|+1 , • for 0 ≤ i ≤ m , PATH(A, q i , E i , A i , q i+1 , N -1) returns , • E = (E ∪ q m +1 ) ∪ S j E j , • A = (A ∩ q m +1 ) ∩ T j A j , Y = T j A j , q 0 = q m+1 ; -Return .

Complexity of satisfiability problems

We establish new complexity results for problems related to LTL(U, S) satisfiability thanks to the intermediate results we have established so far.

Complexity of LTL(U, S)

Here is the main result of the paper.

Theorem 13. The satisfiability problem for LTL(U, S) over the class of ordinals is pspace-complete.

Proof. By Lemma 4, given a formula φ in LTL(U, S), there is an automaton A φ whose accepting runs correspond exactly to models of φ. In order to check nonemptiness of A φ , we do not build it explicitly (as usual) but we run the algorithm from the proof of Theorem 12 and we compute the locations, and transition relations of A φ on demand. Hence, we obtain a polynomial space non-deterministic algorithm since the basis of A φ has a cardinality in O(|φ|) and checking whether a subset of X is a location of A φ or q, q ∈ δ next or Y, q ∈ δ lim can be done in polynomial space in O(|φ|). Again by Savitch's Theorem, we get that the satisfiability problem for LTL(U, S) is in pspace. The pspace lower bound can be easily shown inherited from LTL.

Thanks to Kamp's theorem, we get the following corollary.

Corollary 14. Let LTL(U, S, O 1 , . . . , O k ) be an extension of LTL(U, S) with k first-order definable temporal operators. Then the satisfiability problem for the logic LTL(U, S, O 1 , . . . , O k ) over the class of ordinals is in pspace. Indeed, every formula O i (p 1 , . . . , p n i ) encoded as a DAG can be translated into an equivalent formula in LTL(U, S) encoded as a DAG over the propositional variables p 1 , . . . , p n i . Since O 1 , . . . , O k and their definition in LTL(U, S) are constant of LTL(U, S, O 1 , . . . , O k ) we obtain a translation in polynomial-time (with our definition for the size of formulae).

A family of satisfiability problems

The satisfiability problem for LTL(U, S) asks for the existence of a model for a given formula. A natural variant of this problem consists in fixing the length of the models in advance as for LTL. The satisfiability problem for LTL(U, S) over α-models, noted SAT(α, LTL(U, S)), is defined as follows: given a formula φ in LTL(U, S), is φ satisfiable over an α-model? In this subsection we prove that SAT(α, LTL(U, S)) is in pspace for every countable ordinal α. First we consider the case of ordinals strictly less than ω ω . Recall that for every α < ω ω there is a formula def α in LTL(U, S) such that for every β-model σ, we have σ, 0 |= def α iff β = α.

Corollary 15. For every α < ω ω , the problem SAT(α, LTL(U, S)) is in pspace.

Proof. φ has a α-model iff ψ = φ ∧ def α is satisfiable over the class of ordinals. Thanks to Lemma 2 and Theorem 13, we obtain the pspace upper bound. Now we consider the case of a countable ordinal α ≥ ω ω . Let α be the unique ordinal strictly less than ω ω such that α = ω ω × γ + α for some ordinal γ. Note that for every k,

trunc k (α) = trunc k (ω k + α ) < ω ω . By Lemma 9, φ has an α- model iff φ has a α |φ| -model with α |φ| = trunc |φ|+2 (α) = trunc |φ|+2 (ω |φ|+2 + α ).
Hence, φ has an α-model iff φ ∧ def α |φ| is satisfiable (over the class of countable ordinals). Since the size of def α |φ| is polynomial in the size of φ, we derive from Theorem 13 the following result.

Corollary 16. For every countable α ≥ ω ω , the problem SAT(α, LTL(U, S)) is in pspace.

Corollaries 15, 16 and the arguments similar to the arguments in the proof of Corollary 14 imply the result below.

Theorem 17. For every finite set {O 1 , . . . , O k } of first-order definable temporal operators and every countable ordinal α, the satisfiability problem for the logic LTL(O 1 , . . . , O k ) restricted to α-models is in pspace.

Observe that (1) if α is finite, then SAT(α, LTL(O 1 , . . . , O k )) is np-complete whereas (2) if α is infinite, then pspace-hardness for SAT(α, LTL(U, S)) follows from the pspace-completeness of SAT(ω, LTL(U, S)).

Uniform satisfiability

Büchi (see, e.g., [START_REF] Büchi | The monadic second order theory of all countable ordinals[END_REF]) has shown that there is a finite amount of data concerning any countable ordinal that determines its monadic theory.

Definition 18 (Code of an ordinal). Let α be a countable ordinal and let m be in [1, ω].

1. Write α = ω m α + ζ with ζ < ω m (this can be done in a unique way), and let

p m (α) := -2 if α = 0 -1 if 0 < α < ω 1 . 2. If ζ = 0, write ζ = i≤n ω n-i • a n-i
where a i ∈ ω for i ≤ n and a n = 0 (this can be done in a unique way), and let t m (α) := (a n , . . . , a 0 ). If ζ = 0, let t(α) = -3. 3. The m-code of α is the pair (p m (α), t m (α)).

The following is implicit in [START_REF] Büchi | The monadic second order theory of all countable ordinals[END_REF].

Theorem 19 (Code Theorem). There is an algorithm that, given a monadic second-order sentence φ and the ω-code of a countable ordinal α, determines whether α, < |= φ.

Lemma 9 can be rephrased as "the (|φ| + 2)-code of an ordinal α determines whether φ has a model of length α".

Let C = (b, a n , . . . a 0 ) be an m-code. Its size is defined as n+a 0 +a 1 +• • •+a n . It is clear that for m 1 < m 2 the m 2 -code of an ordinal determines its m 1 -code and there is a linear time algorithm, that given m 2 -code of an ordinal and m 1 < m 2 computes the m 1 -code of the ordinal.

The arguments used in the proof of Corollary 16 show the following theorem.

Theorem 20 (Uniform Satisfiability).

(I) There is a polynomial-space algorithm that, given an LTL(U, S) formula φ and the ω-code of a countable ordinal α, determines whether φ has an αmodel. (II) There is a polynomial-space algorithm that, given an LTL(U, S) formula φ and the (|φ| + 2)-code of a countable ordinal α, determines whether φ has an α-model.

Related work

In this section, we compare our results with those from the literature. Because of lack of place, we omit to cite works in which models of length higher than ω are considered for formal verification of computer systems, see e.g. [START_REF] Godefroid | A partial approach to model checking[END_REF].

Comparison with Rohde's thesis

In [START_REF] Rohde | Alternating Automata and The Temporal Logic of Ordinals[END_REF], it is shown that an uniform satisfiability problem for temporal logic with until (and without since) can be solved in exponential-time. The inputs of this problem are a formula in LTL(U) and the representation of an ordinal. The satisfiability problem is also shown in exptime. In order to obtain this upper bound, formulae are shown equivalent to alternating automata and a reduction from alternating automata into a specific subclass of non-deterministic automata is given. Finally, a procedure for testing nonemptiness is provided. Here are the similarities between [Roh97] and our results.

2. Existence of α-paths in the automata depends on some truncation of α. 3. The logical decision problems can be solved in exponential-time.

However, our work improves considerably some results from [START_REF] Rohde | Alternating Automata and The Temporal Logic of Ordinals[END_REF].

1. Our temporal logic includes the until and since operators (instead of until only) and it is therefore as expressive as first-order logic. 2. We establish a tight pspace upper bound (instead of exptime) thanks to the introduction of a class of simple ordinal automata. 3. Our proofs are much shorter and transparent (instead of the lengthy developments from [START_REF] Rohde | Alternating Automata and The Temporal Logic of Ordinals[END_REF]).

Consequently, the developments from [START_REF] Rohde | Alternating Automata and The Temporal Logic of Ordinals[END_REF] and ours follow the same approach with different definitions for automata, different intermediate lemmas and distinct final complexity bounds. On the other hand, the structure of the whole proof to obtain the main complexity bounds is similar.

Comparison with Reynolds' results

Even though the results for linear-time temporal logics from [START_REF] Reynolds | The complexity of the temporal logic with until over general linear time[END_REF][START_REF] Reynolds | The complexity of the temporal logic over the reals[END_REF] involve distinct models, our automata-based approach has similarities with these works that uses a different proof method, namely mosaics. Indeed, equivalence classes of the relation ∼ between runs of length a successor ordinal roughly correspond to mosaics from [START_REF] Reynolds | The complexity of the temporal logic with until over general linear time[END_REF]. We recall the main results below.

Theorem 21. (I) The satisfiability problem for the temporal logic with until and since over the reals is pspace-complete. (II) The satisfiability problem for LTL(U) over the class of all linear orders is pspace-complete.

The proofs in [START_REF] Reynolds | The complexity of the temporal logic with until over general linear time[END_REF][START_REF] Reynolds | The complexity of the temporal logic over the reals[END_REF] are much more involved than our proofs since the orders are more complex than the class of ordinals. Unfortunately, we do not understand these proofs fully and find it difficult to compare to our proof.

Quantitative temporal operators

In this section, we show that the main results from [START_REF] Demri | Reasoning about transfinite sequences[END_REF] are subsumed by the current paper. We also solve an open problem from [START_REF] Cachat | Controller synthesis and ordinal automata[END_REF][START_REF] Demri | Reasoning about transfinite sequences[END_REF]. For every fixed countable ordinal α ≤ ω, let us introduce the logic LTL(O α ) where the set of temporal operators O α is defined as follows:

{X β : β < ω α } ∪ {U β : β ≤ ω α }.
The models of LTL(O α ) as those of LTL(U, S) and the formulae of LTL(O α ) are precisely defined by: φ

::= p | ¬φ | φ 1 ∧ φ 2 | X β φ | φ 1 U β φ 2 .
The size of a formula φ is the number of subformulae occurring in φ plus the sum of all the natural numbers occurring in φ either as a coefficient or as an exponent of ω. The satisfaction relation is inductively defined below where σ is a model for LTL(O α ) (we omit the obvious clauses):

-σ, β |= X β φ iff β + β is a position of σ and σ, β + β |= φ, -σ, β |= φ 1 U β φ 2 iff there is 0 < γ < β such that β + γ is a position of σ,
σ, β + γ |= φ 2 and for every 0 < γ < γ, we have σ, β + γ |= φ 1 .

The satisfiability problem for LTL(O α ) consists in determining, given a formula φ, whether there is a model σ such that σ, 0 |= φ. The main results of [START_REF] Cachat | Controller synthesis and ordinal automata[END_REF][START_REF] Demri | Reasoning about transfinite sequences[END_REF] are the following: for every k ≥ 1, the satisfiability problem for LTL(O k ) restricted to models of length ω k is pspace-complete and LTL(O ω ) restricted to models of length ω ω is decidable.

Observe that LTL(O k ) cannot express the temporal operator U over the class of countable ordinals but it can do it on models of length ω k . Hence, each logic LTL(O k ) is less expressive than LTL(U, S).

Moreover, it is easy to show that for every α ≤ ω, the logic LTL(O α ) is expressive equivalent (over the class of countable ordinals) to its sublogic over the following set O α of temporal operators:

O α = {X ω i : ω i < ω α , i ∈ N} ∪ {U ω β : ω β ≤ ω α , β ≤ ω}.
This set is finite when α is finite. Moreover, there is a linear time (and logarithmic space) meaning preserving translation from LTL(O α ) into LTL(O α ).

We obtain alternative proofs for known results and we get new results.

Theorem 22. For every k ≥ 1, (I) the satisfiability problem for LTL(O k ) over ω k -models is in pspace, (II) the satisfiability problem for LTL(O k ) restricted to ω k -models is pspacecomplete, (III) for every countable infinite ordinal α, the satisfiability problem for LTL(O k ) restricted to α-models is pspace-complete.

(III) is an instance of Theorem 17. (II) is an instance of (III). (I) can be shown by observing that there is logarithmic space meaning preserving translation from LTL(O k ) to LTL(O k ). (I) is the main result of [START_REF] Demri | Reasoning about transfinite sequences[END_REF] with the unary encoding of natural numbers occurring in ordinal expressions.

Finally, the corollary below improves the non-elementary bounds obtained in [START_REF] Cachat | Controller synthesis and ordinal automata[END_REF][START_REF] Demri | Reasoning about transfinite sequences[END_REF] for LTL(O ω ) by reducing this temporal logic to the monadic second order logics, and then to the Buchi ordinal automata.

Corollary 23. Satisfiability for LTL(O ω ) over the class of ω ω -models is pspacecomplete.

Conclusion

In the paper, we have shown that the linear-time temporal logic with until and since over the class of ordinals, namely LTL(U, S) has a pspace-complete satisfiability problem. Thanks to Kamp's theorem [START_REF] Kamp | Tense Logic and the theory of linear order[END_REF], we know that LTL(U, S) is a fundamental temporal logic since it is as expressive as first-order logic over the class of ordinals. In order to establish this tight complexity characterization, we have introduced the class of simple ordinal automata. This class of automata is more structured than usual ordinal automata and the sets of locations have some structural properties, typically it is a subset of the powerset of some set (herein called the basis). As a consequence, we are also able to improve some results from [START_REF] Rohde | Alternating Automata and The Temporal Logic of Ordinals[END_REF][START_REF] Demri | Reasoning about transfinite sequences[END_REF]. For instance the uniform satisfiability problem is pspace-complete and we obtain alternative proofs for results in [START_REF] Demri | Reasoning about transfinite sequences[END_REF].

Extensions of our results include that the satisfiability problem for the language LTL(O 1 , . . . , O k ) where the O i s form a finite set of MSO definable temporal operators is in pspace by adapting the developments from [START_REF] Vardi | Reasoning about infinite computations[END_REF] and showing that our simple ordinal automata augmented with alphabet has the expressive power of standard ordinal automata. Furthermore, our results can be extended to scattered linear orderings, see e.g. [START_REF] Bruyère | Automata on linear orderings[END_REF]. Indeed, one should add right limit transitions, using the terminology from [START_REF] Bruyère | Automata on linear orderings[END_REF] and adapt the developments herein.

  Now we can state the correctness lemma.Lemma 4.(I) If σ, 0 |= φ, then H σ,φ is an accepting run of A φ . (II) If r is an accepting run of A φ , then there is a model σ such that σ, 0 |= φ and r is the Hintikka sequence for σ and φ. (III) φ is satisfiable iff A φ has an accepting run.

Fig. 1 .

 1 Fig. 1. Algorithm PATH

We follow an automata-based approach and the class of non-deterministic automata in[START_REF] Rohde | Alternating Automata and The Temporal Logic of Ordinals[END_REF] and ours have a structured set of locations and limit transitions use elements that are true from some position.

Acknowledgments: We would like to thank the anonymous referees for helpful suggestions and remarks.

Partially supported by an invited professorship from ENS de Cachan and project AutoMathA (ESF).


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, it is closed under Boolean operations and it admits a restricted form of existential quantification. This is the largest set of qualitative constraints over Z known so far, shown to admit a decidable LTL extension. Such constraints are those used for instance in calendar formalisms or in 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. As a by-product, LTL model-checking over integral relational automata is proved complete for polynomial space which contrasts with the known undecidability of its CTL counterpart.

Introduction

Model-checking infinite-state systems. The verification of systems with an infinite amount 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]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]). Even though decidability can be obtained via numerous proof techniques (finite partition of the infinite domain, well-structured systems, Presburger definable reachability sets, reduction to the second-order theory of the binary tree), showing undecidability of model-checking for some classes of infinite-state systems is often easy. After all, the halting problem for Minsky machines is already undecidable. Decidability is more difficult to establish and it can be sometimes 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]) or by considering fragments of the specification language (to consider only reachability or repeated reachability for instance).

Systems with variables interpreted in Z. Structures with a finite set of control states augmented with a finite set of variables interpreted either in Z or in N (counters) are operational models of numerous 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]). The class of counter machines has numerous undecidable model-checking problems such as the reachability problem but many classes of counter systems have been shown to be decidable: reversal-bounded multicounter machines [START_REF] Ibarra | Reversal-bounded multicounter machines and their decision problems[END_REF], flat counter systems with affine update functions forming a finite monoid [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], flat counter systems [START_REF] Comon | Multiple counters automata, safety analysis and Presburger arithmetic[END_REF] (weaker class of Presburger guards but no condition on the monoid) and 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 incrementations and decrementations are abstracted by operations modulo some power of two. Common programming languages perform arithmetic operators for integer types modulo 2 k [MOS05], typically k is either 32 or 64. For example, x = y + 1 can be abstracted by x ≡ 2 k y + 1 ∧ y < x. Such an abstraction is well-suited to check safety properties about the original counter system. In the paper, we study a class of constraint automata with a language of qualitative constraints as rich as possible and a companion LTL-like logic to perform model-checking on such operational models. Our framework should be able to deal both with abstractions modulo (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], i.e. constraints of the form x ≡ k y + c. 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).

Our contribution. We introduce a version of constraint 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 IPC ++ is already closed under Boolean operators and first-order quantification. No constraint of the form x < y occurs in the scope of a quantifier. Otherwise incrementation is definable and it leads to undecidability of the logic. So, as shown in this paper, adding the single type of constraints x < y leads to many technical complications, but not to undecidability. We call CLTL(IPC ) the specification language built over IPC constraints. 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 shown 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 also shown to be in pspace in [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF]. Both proofs use reductions to the emptiness problem for Büchi automata following the approach in [START_REF] Vardi | Reasoning about infinite computations[END_REF]. However, the proofs 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 model-checking and satisfiability problems for the logic CLTL(IPC ) are decidable (which was open so far) and moreover in pspace (pspace-hardness is easy). The proof substantially generalizes what is done for constraint LTL over the domain Z, <, = by con-sidering both new constraints of the form x ≤ d, d ∈ Z and integer periodicity constraints. The optimal treatment of constants occurring in such constraints is our main technical contribution. As a corollary, we establish that LTL modelchecking 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 ). To our opinion, we provide a definite complexity characterization of LTL with qualitative constraints over Z.

Related work.

Reachability problems for subclasses of counter systems have been addressed for instance in [Iba78,CJ98,FL02,BFLP03] (see also richer questions in [START_REF] Bouajjani | Reachability analysis of pushdown automata: application to model-checking[END_REF][START_REF] Jančar | DP lower bounds for equivalence-checking and model-checking of one-counter automata[END_REF]). In our work, we have a full LTL-like language, not restricted to reachability questions, used as a specification language and no restriction on the structure of the models. However, atomic formulae of the specification language are qualitative constraints. If we give up the decidability requirement, LTL over 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].

Constraint LTL over concrete domains (not only restricted to Z) has been considered in [WZ00,BC02,DD03,GKK + 03,Dem04] where often pspace-completeness is 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, see e.g. [START_REF] Lutz | NEXPTIME-complete description logics with concrete domains[END_REF]. The language CLTL(IPC ) extends the different LTL-like fragments from [ Čer94,LM01,DD03,Dem04] (pasttime operators can be added for free in our formalism thanks to [START_REF] Gastin | Satisfiability and model checking for MSO-definable temporal logics are in PSPACE[END_REF]). The class of IPC -automata introduced in the paper generalizes the class of integral relational automata from [ Čer94] (see details in [START_REF] Demri | Verification of qualitative Z-constraints[END_REF]).

Integer periodicity constraints, a special class of Presburger constraints, have found applications in many 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]), DATALOG with integer periodicity constraints [START_REF] Toman | Datalog with integer periodicity constraints[END_REF] and in real-time logics [START_REF] Alur | A really temporal logic[END_REF].

Omitted proofs can be found in [START_REF] Demri | Verification of qualitative Z-constraints[END_REF].

The logic CLTL(IPC )

Language of constraints

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

p ::= pmod | x < y | p ∧ p | ¬p pmod ::= x ≡ k [c 1 , c 2 ] | x ≡ k y + [c 1 , c 2 ] | x = y | x < d | x = d | pmod ∧ pmod | ¬pmod | ∃x pmod where x, y ∈ V , k ∈ N \ {0}, c 1 , c 2 ∈ N and d ∈ Z.
This language is denoted by IPC . We write IPC ++ to denote its restriction to constraints ranged over by pmod, and Z c its restriction to constraints of the form either x ∼ y or x ∼ d. The symbol ∼ is used to mean either = or <. The language Z is the restriction of Z c to constraints of the form x ∼ y. We define a valuation v as a map v : V → Z and the satisfaction relation v |= p is defined as follows in the standard way:

-v |= x ∼ y def ⇔ v(x) ∼ v(y); v |= x ∼ d def ⇔ v(x) ∼ d; -v |= x ≡ k [c 1 , c 2 ] def ⇔ v(x) is equal to c modulo k for some c 1 ≤ c ≤ c 2 ; -v |= x ≡ k y + [c 1 , c 2 ] def ⇔ v(x) -v(y) is equal to c modulo k for some c 1 ≤ c ≤ c 2 ; -v |= p ∧ p def ⇔ v |= p and v |= p ; v |= ¬p def ⇔ not v |= p; -v |= ∃x p def ⇔ there is z ∈ Z such that v[x ← z] |= p where v[x ← z](x ) = v(x ) if x = x and v[x ← z](x) = z. We recall that x is equal to y modulo k if there is z ∈ Z such that x -y = k × z. We write x ≡ k c instead of x ≡ k [c, c], x ≡ k y + c instead of x ≡ k y + [c, c] and v |= X
where X is a set of IPC -constraints, whenever v |= p for every p ∈ X.

A constraint p is satisfiable iff there is a valuation v such that v |= p. Two constraints are equivalent iff they are satisfied by the same valuations.

Lemma 1. (I) The satisfiability problem for IPC is pspace-complete. (II) Every constraint in IPC admits an equivalent quantifier-free constraint in IPC .

Hence, IPC is a quite well understood fragment of Presburger arithmetic.

Logical language

We consider the linear-time temporal logic CLTL(IPC ) whose atomic formulae are defined from constraints in IPC . The atomic formulae are of the form p[x 1 ← X i 1 x j 1 , . . . , x r ← X i r x j r ], where p is a constraint of IPC with free variables x 1 . . . x r . We substitute each occurrence of the variable x l with X i l x j l , which corresponds to the variable x j l preceded by i l next symbols. Each expression of the form X β x α is called a term and represents the value of the variable x α at the β th next state. Here are examples of atomic formulae: Xy ≡ 2 32 x + 1 and x < Xy.

The set of CLTL(IPC ) formulae φ is defined by

φ ::= p[x 1 ← X i 1 x j 1 , . . . , x r ← X i r x j r ] | ¬φ | φ ∧ φ | Xφ | φUφ,
where p belongs to IPC . The operators next (X) and until (U) are the classical operators used in temporal logics. In the language, all the integers are encoded with a binary representation (this is important for complexity considerations). 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 × V → Z for CLTL(IPC ) is an ω-sequence of valuations. The satisfaction relation is defined as follows (we omit the Boolean cases):

-σ, i |= p[x 1 ← X i 1 x j 1 , . . . , x r ← X i r x j r ] iff [x 1 ← σ(i + i 1 , x j 1 ), . . . , x r ← σ(i + i r , x j r )] |= p; -σ, i |= Xφ iff σ, i + 1 |= φ; -σ, i |= φUφ iff there is j ≥ i s.t. σ, j |= φ and for every i ≤ l < j, σ, l |= φ.
By definition, CLTL(IPC )-models interpret variables but not propositional variables. However, it is easy to encode propositional variables by using atomic formulae of the form x = 0 where x is a new variable introduced for this purpose.

Satisfiability and model-checking problems

We recall below the problems we are interested in.

Satisfiability problem for CLTL(IPC ): Given a CLTL(IPC ) formula φ, is there a model σ such that σ, 0 |= φ?

If we extend IPC to allow constraints of the form x < y in the scope of ∃, then the satisfiability problem for the corresponding constraint LTL-like logic is undecidable since the successor relation is then definable and the halting problem for Minsky machines can be easily encoded.

The model-checking problem rests on IPC -automata which are constraint automata. An IPC -automaton A is defined as a Büchi automaton over the infinite alphabet composed of CLTL(IPC ) formulae. In an IPC -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]. As an illustration, we present an IPC -automaton in Fig. 1 which is an abstraction of the pay-phone controller from [CC00, Example 1] (x is the number of quarters which have been inserted and y measures the total communication time). Incrementation 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). 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], by possibly introducing a new variable. In the following sections, we prove results for the satisfiability problem but they also extend to the model-checking problem.

q 1 q 2 q 3 q 4 q 6 q 5 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
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 ) [START_REF] Demri | LTL over integer periodicity constraints[END_REF]. Furthermore, the model-checking problem for integral relational automata restricted to the LTL fragment of CCTL * introduced in [ Čer94] is a subproblem of the modelchecking problem for CLTL(IPC ) (see details in [START_REF] Demri | Verification of qualitative Z-constraints[END_REF]). The model-checking problem for CLTL(IPC ++ ) (resp. CLTL(Z)) is shown to be pspace-complete in [START_REF] Demri | LTL over integer periodicity constraints[END_REF] (resp. 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 we introduce 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 a translation into CLTL(Z) that increases exponentially the size of formulae (with a binary encoding of the natural numbers).

A restricted IPC -automaton is defined as an IPC -automaton such that the labels on transitions are Boolean combinations of atomic formulae with terms of the form x and Xx (see Fig. 1). The logic CCTL * (IPC ) (constraint CTL * over IPC constraints) is defined as the extension of CLTL(IPC ) with the path quantifiers ∃ and ∀ but restricted to atomic formulae with no variables in V preceded by X. The models of CCTL * (IPC ) are the configuration graphs of restricted IPC -automata. The satisfaction relation A, q, x |= φ is defined in the usual way. The model-checking problem for CCTL * (IPC ) takes as inputs a restricted IPC -automaton A, an initial configuration q, 0 (q is a control state and 0 is the initial valuation with null values for the variables) and a CCTL * (IPC ) formula φ and checks whether A, q, 0 |= φ. Full CCTL * (IPC ) model-checking can be shown to be undecidable by using developments in [START_REF] Demri | Verification of qualitative Z-constraints[END_REF] and [ Čer94] (even its CTL-like fragment) and one can show that its LTL fragment is decidable in polynomial space, a new result not captured by [ Čer94].

Properties of the constraint language

In this section, we establish results about the constraint language underlying the logic CLTL(IPC ). In order to define automata that recognize symbolic representations of CLTL(IPC )-models, the valuations v of the form V → Z are represented by symbolic valuations. 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 lcm of k 1 , . . . , k n where periodicity constraints with relations -V is the finite set of variables occurring in X.

≡ k 1 , . . . , ≡ k n occur in X. Observe that |K| is in O(|k 1 | + • • • + |k n |). -C
In the remaining, we assume that the above objects are always defined (possibly by adding dummy valid constraints in order to make the sets non-empty).

A maximally consistent set Y of Z c constraints with respect to V and C is a set of Z c constraints using only the variables from V and the constants from C such that there is a valuation v : V → Z verifying v |= Y and for any proper extension Z of Y , there is no valuation v : V → Z verifying v |= Z. A valuation is abstracted by three disjoint finite sets of IPC constraints like regions for timed automata.

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 wrt V and C. -Y 2 is a set of constraints of the form x = d with x ∈ V and d ∈ C \ C. Each x ∈ V occurs at most in one constraint of the form x = d in Y 2 . Moreover, for every x ∈ V , (x = d) ∈ Y 2 for some unique d ∈ C \ C iff for every d ∈ C, (x = d ) ∈ Y 1 and {m < x, x < M } ⊆ Y 1 . -Y 3 is a set of constraints of the form x ≡ K c with x ∈ V and 0 ≤ c ≤ K -1. Each x ∈ V occurs exactly in one constraint of the form x ≡ K c 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. That is why, given an IPC constraint p, we write p

∈ sv instead of p ∈ Y 1 ∪ Y 2 ∪ Y 3 . A symbolic valuation is satisfiable iff there is a valuation v : V → Z such that v |= Y 1 ∪ Y 2 ∪ Y 3 . Lemma 2. 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 V and C, Y 2 is a set of Z c constraints of cardinality at most |V | built over V and C \ C, Y 3 is a set of constraints of the form x ≡ K c of cardinality |V |.
Checking whether sv is a satisfiable symbolic valuation can be done in polynomialtime in the sum of the respective size of X and sv.

Maximal consistency of Y 1 can be checked in polynomial-time by using developments from [ Čer94, Lemma 5.5]. Indeed, given a set Y of Z c constraints built over V and C, a graph G Y can be built such that Y is maximally consistent wrt

V and C iff G Y satisfies the conditions below. G Y is a structure V ∪ C, = -→, < -→ such that n ∼ -→ n def ⇔ n ∼ n belongs to Y . Following [ Čer94, Lemma 5.5], Y is maximally consistent iff G Y 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 α with n 0 = n α and < occurs in {∼ 0 , ∼ 1 , . . . , ∼ α-1 }. (MC4) For all d 1 , d 2 ∈ C, 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 cardinality of {i :∼ i equals <, 1 ≤ i ≤ α -1} is strictly more than d 2 -d 1 .
The symbolic representations of valuations contain the relevant information to evaluate constraints. Lemma 3. Let X be a finite set of IPC constraints. (I) For every valuation v : V → Z there is a unique symbolic valuation sv

(v) = Y 1 , Y 2 , Y 3 such that v |= Y 1 ∪ Y 2 ∪ Y 3 . (II) For all valuations v, v such that sv(v) = sv(v ) and for every p ∈ X, v |= p iff v |= p.
The proof of (I) is by an easy verification whereas (II) is shown by structural induction on p similarly to the proof of [Dem04, Lemma 1]. By Lemma 3, a symbolic valuation is an equivalence class of valuations.

Given a symbolic valuation sv and p a constraint, we write sv |= symb p def ⇔ for every valuation v such that sv(v) = sv, v |= p.

Lemma 4. The problem of checking whether sv |= symb p is pspace-complete (given that the syntactic resources used in p are included in those used for the symbolic valuation sv ).

Satisfiable ω-sequences of symbolic valuations

Given a CLTL(IPC ) formula φ, we write IPC (φ) to denote the set of IPC constraints p such that some atomic formula of the form p[x 1 ← X i x j 1 , . . . , x r ← X i r x j r ] occurs in φ. To IPC (φ) we associate the objects relative to any finite set of IPC constraints. The set V denotes the set of variables occurring in φ. We write |φ| X to denote the maximal natural number i such that X i x occurs in φ for some variable x. |φ| X is called the X-length of φ. Without any loss of generality, we can assume that |φ| X ≥ 1. In the following, we assume that V = {x 1 , . . . , x s } and |φ| X = l. We write Terms(φ) to denote the set of terms of the form X β x α with β ∈ {0, . . . , l} and α ∈ {1, . . . , s}.

Let V be a set of variables of cardinality |Terms(φ)| and f : Terms(φ) → V be an unspecified bijection such that f and f -1 can be computed in polynomial time. By extension, for every atomic subformula p of φ, f (p) is obtained from p by replacing each occurrence of X β x α by f (X β x α ). The map f -1 is used in a similar fashion. A symbolic valuation wrt φ is a symbolic valuation built over the set of variables V , C and K.

We say that a pair

Y 1 , Y 2 , Y 3 , Y 1 , Y 2 , Y 3 of symbolic valuations wrt φ is one-step consistent def ⇔ 1. f (X j x i ) ∼ f (X j x i ) ∈ Y 1 and j, j ≥ 1 imply 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 and j ≥ 1 imply f (X j-1 x i ) ∼ d ∈ Y 1 ∪ Y 2 , 3. f (X j x i ) ≡ K c ∈ Y 3 and j ≥ 1 imply f (X j-1 x i ) ≡ K c ∈ Y 3 .
An ω-sequence ρ of satisfiable symbolic valuations wrt φ is one-step consistent def ⇔ for every j ∈ N, ρ(j), ρ(j+1) is one-step consistent. A model for ρ is defined as a CLTL(IPC )-model σ such that for all j ∈ N and p ∈ ρ(j), σ, j |= f -1 (p). In order to simplify the future developments, we write ρ f to denote the ω-sequence obtained from ρ by substituting each occurrence of some variable x by f -1 (x).

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

G ρ = (V ∪ C ) × N, = -→, < -→, mod where mod : (V ∪ C ) × N → {0, . . . , K -1}: 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 such that x ∼ d ∈ ρ f (i) and <∈ {∼, ∼ }, d, i < → x, j iff there is d ∼ d such that d ∼ x ∈ ρ f (j) and <∈ {∼, ∼ }, d 1 , i ∼ → d 2 , j iff d 1 ∼ d 2 , mod( x, i ) = c iff x ≡ K c ∈ ρ f (i) and mod( d, i ) = c iff d ≡ K c.
for all x, y ∈ V , d 1 , d 2 ∈ C and i, j ∈ N such that |i -j| ≤ l. 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. The construction ensures that the "local" representation of every ρ(i) verifies the conditions (MC1) to (MC5) of Sect. 3.

In the following, we say that a vertex represents the constant d if it is of the form d, i for some i. The level of a node n = a, t in G ρ is t, and is denoted by lev(n). There is some redundancy in G ρ for the nodes of the form d, i . However, this is useful to establish strict relationships between ρ and G ρ . A path in G ρ is a sequence (possible infinite) of the form n 0

Example 1. Assuming that C = {2, 4}, K = 2, V = {x, x } (f (x) = x and f (Xx) = x ) and l = 1, let us define the sequence ρ = sv 0 • (sv 1 • sv 2 ) ω where sv 0 = Y 0 1 , Y 0 2 , Y 0 3 such that Y 0 1 = {x = x, x = x , x < x , 2 < x, x < 4, x = 4, x > 2}, Y 0 2 = {x = 3} and Y 0 3 = {x ≡ 2 1, x ≡ 2 0}. The symbolic valuation sv 1 = Y 1 1 , Y 1 2 , Y 1 3 satisfies: Y 1 1 = (Y 0 1 \ {2 < x, x < 4, x = 4, x > 2}) ∪ {4 < x, 4 < x }, Y 1 2 = ∅ and Y 1 3 = {x ≡ 2 0, x ≡ 2 1}. The symbolic valuation sv 2 = Y 2 1 , Y 2 2 , Y 2 3 verifies Y 2 1 = Y 1 1 , Y 2 2 = Y 2 1 and Y 2 3 = Y 0 3 . The graph G ρ is presented in Fig.
∼ 0 -→ n 1 ∼ 1 -→ n 2 ∼ 2 -→ . . .. For any finite path w = n 0 ∼ 0 -→ n 1 ∼ 1 -→ n 2 ∼ 2 -→ . . . ∼ α-1
--→ n α , its strict length slen(w) is the cardinality of {i : 0 ≤ i ≤ α-1, ∼ i equals <}. When w has a strict length greater than 1, we say that w is strict. A finite path w such that n 0 = n α is called a cycle. The strict length between two nodes n 1 and n 2 , written slen(n 1 , n 2 ), is the least upper bound of the strict lengths of finite paths between n 1 and n 2 . By convention, if there is no path between n 1 and n 2 , slen(n 1 , n 2 ) takes the value -∞. In Fig. 2, slen( 2, 2 , x, 3 ) = 4.

In Lemma 5 below, the one-step consistency of ρ implies global constraints on its graph representation that already hold true locally. By a global constraint, we mean a constraint on the whole graph and not only on the local representation of a single symbolic valuation or on two successive satisfiable symbolic valuations.

2, 0 3, 0 4, 0 x, 0 ≡ 2 1 2, 1 3, 1 4, 1 x, 1 ≡ 2 0 2, 2 3, 2 4, 2 x, 2 ≡ 2 1 2, 3 3, 3 4, 3 x, 3 ≡ 2 0 . . . < < < < < < = < = < = < = = < < < < = < = < = < < < < < = < = < = < < Fig. 2. A graph G ρ Lemma 5.
Let ρ be a one-step consistent sequence.

(I) G ρ has no strict cycle. (II) If there is a finite path w starting at d, i and ending at the node n of level j, then: if w is strict then d, j

< -→ n, otherwise d, j = -→ n. (III)
If there is a finite path w starting at the node n of level j and ending at d, i , then: if w is strict then n

< -→ d, j , otherwise n = -→ d, j .
Corollary 1. Let ρ be a one-step consistent sequence 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 .
So far, we have stated properties about the graph G ρ . Below, we establish simple conditions on G ρ equivalent to the existence of a model for ρ. An edgerespecting labeling for G ρ is a map lab : (V ∪ C ) × N → Z such that for all nodes n 1 , n 2 , n 1 ∼ -→ n 2 implies lab(n 1 ) ∼ lab(n 2 ) and 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 6. A one-step consistent sequence ρ has a model iff G ρ has a strict edge-respecting labeling.

The proof is quite direct by unfolding the definitions. A refinement is possible.

Lemma 7. A one-step consistent sequence ρ has a model iff G ρ has an edgerespecting labeling (not necessarily strict).

Lemmas 6 and 7 state correspondences between ρ and its graphical representation G ρ . However, we need a more abstract characterization of the one-step consistent sequences admitting a model (see Lemma 8 below).

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 ) < ω.

By construction of G ρ , for all nodes d 1 , i and d 2 , j representing constants such that d 1 ≤ d 2 , slen( d 1 , i , d 2 , j ) = d 2d 1 (see Corollary 1). That is why, in Lemma 8, there is no additional constraint for nodes of the graph representing constants.

Lemma 8 characterizes the set of sequences having a model but what we really need 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, a consequence of [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF] for the fragment CLTL(Z). In order to approximate this class of sequences, we define below a condition (C) shown to be ω-regular such that for every one-step consistent ωsequence ρ of satisfiable symbolic valuations that is ultimately periodic, ρ has a model iff G ρ satisfies (C).

An infinite forward (resp. backward) path in G ρ is defined as a sequence w : N → (V ∪ C ) × N such that: for every i ∈ N, there is an edge w(i) ∼ -→ w(i + 1) (resp. w(i + 1) ∼ -→ w(i)) in G ρ and if lev(w(i)) = j, then lev(w(i + 1)) ≥ j + 1. The path w is infinitely often strict def ⇔ for every i ≥ 0, there is j ≥ i such that w(j) < -→ w(j + 1) (resp. w(j + 1) < -→ w(j)). The condition (C) on the graph G ρ is: 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 ρ .
We say an infinite word is ultimately periodic if it is of the form τ • δ ω for some finite words τ and δ.

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

Thanks to the way G ρ is built from ρ, (C) does not explicitly mention the constants in C and the constraints of the form x ≡ K c. Hence, Lemma 9 can be proved as [DD03, Lemma 6.2]: the map mod in G ρ is ignored and a uniform treatment for all nodes in (V ∪ C ) × N is provided. In [DD03, Lemma 6.2], there are no nodes of the form C × N but we take into account their specificity in our construction of G ρ . If ρ admits a model then by Lemma 8 it satisfies the condition (C). Conversely, let ρ = τ • δ ω be an ultimately periodic one-step consistent ω-sequence. We can show that if ρ has no model then it does not satisfy (C). By Lemma 8, if ρ has no model, then there exist two vertices n 1 and n 2 such that slen(n 1 , n 2 ) = ω. One can construct a finite path w between n 1 and n 2 long enough so that paths w for and w back satisfying the conditions (AP1)-(AP4) can be constructed, witnessing that G ρ does not satisfy (C). The construction of w for and w back from w uses the fact that ρ is ultimately periodic by repeating infinitely finite subpaths. The construction of such infinite paths can be done smoothly by using the properties established in this section (see e.g. Lemma 5). As the proof is not essentially different from [DD03, Lemma 6.2] modulo slight changes mentioned above, we omit it here.

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 emptiness of L(A φ ) can be checked in polynomial space in |φ|. From the technical viewpoint, the construction of A φ as the intersection of three Büchi automata can be done quite smoothly thanks to the previous results. In the following, V , V , C and C are the sets of variables and constants associated to φ as defined in Sect. 4. Moreover, K, m and M are constants with their usual meaning and we use the map f : Terms(φ) → V 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. We write Σ to denote the set of satisfiable symbolic valuations wrt φ. A symbolic model for φ is an ω-sequence ρ : N → Σ. We write ρ |= φ where the symbolic satisfaction relation |= is defined as |= except at the atomic level: ρ, i |= p def ⇔ ρ(i) |= symb f (p) where |= symb is the satisfaction relation between symbolic valuations and constraints.

By Lemma 4 and by 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). Since every model for φ generates a unique symbolic model for φ, 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.

All the following automata are built over the alphabet Σ which is of exponential size in |φ|. 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 satisfiable symbolic valuations, L(A C ) is the set of sequences of symbolic valuations verifying (C). We briefly explain below how these automata are built. 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 iff ( atomic
constraints) for every atomic formula p in X, sv |= symb f (p), (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 pose F equal to {F 1 , . . . , F r } with for every i ∈ {1, . . . , r},

F i = {X ∈ Q : ψ i Uϕ i ∈ Xor ϕ i ∈ X}.
By Lemma 4, the condition about atomic formulae can be checked in pspace.

Hence, the transition relation can 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 def ⇔ sv , sv is onestep consistent and sv = sv . Since checking whether a symbolic valuation is satisfiable can be done in P (Lemma 2) and checking whether a pair of symbolic valuations is one-step consistent can be also done in P, the transition relation of A 1cons can be computed in P.

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 [DD03, page 20] except that we work with a different type of alphabet. We need to consider vertices in the graph that represent in C and equality between constants does not need to be explicitly present in the symbolic valuations (see details in [START_REF] Demri | Verification of qualitative Z-constraints[END_REF]).

Lemma 11. A CLTL(IPC ) formula φ is satisfiable iff L(A φ ) is non-empty.

The proof of this lemma is similar to [DD03, Lemma 6.3]. The main trick is to observe that if L(A φ ) is non-empty 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 empty, 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 subtle arguments from complexity theory and [START_REF] Safra | Complexity of Automata on Infinite Objects[END_REF].

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

All the temporal operators in CLTL(IPC ) are definable in monadic second order logic (MSO) and by using [START_REF] Gastin | Satisfiability and model checking for MSO-definable 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.

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 the paper, we have introduced the logic CLTL(IPC ) extending formalisms in [ Čer94,LM01,DD03,Dem04] 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 emptiness 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.

-CTL* for integral relational automata is undecidable [ Čer94]

Fig. 1 .

 1 Fig. 1. An IPC -automatonModel-checking problem for CLTL(IPC ): Given an IPC -automaton A and a CLTL(IPC ) formula φ, are there a symbolic ω-word v = φ 0 • φ 1 • . . . accepted by A and a model σ (a realization of v) such that σ, 0 |= φ and for every i ≥ 0, σ, i |= φ i ?

  is the set of constants d occurring in constraints of the form x ∼ d. m is the minimal element of C and M is its maximal element. -C denotes the set of constants {m, m -1, . . . , M }. The cardinality of C is in O(2 |m|+|M | ) and each element of C can be binary encoded in binary representation with O(|m| + |M |) bits.

  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.

  whereas we have shown that its LTL fragment is pspace-complete. It is interesting to design other fragments of CTL* strictly more expressive than Boolean combinations of LTL formulae. -The decidability status of constraint LTL over the domain {0, 1} * , ⊆ is open either with the subword relation or with the prefix relation. Constraint LTL over the domain {0} * , ⊆ is already equivalent to constraint LTL over N, <, = that is a strict fragment of CLTL(IPC ). -The decidability status of CLTL(IPC ) extended with constraints of the form 3x + 2Xy ≡ 5 3 is open. They are considered in [MOS05] but not integrated in any LTL-like language.