Stéphane Demri

D ' Souza

An Automata-Theoretic Approach to Constraint LTL

Keywords: temporal logic, logics of space and time, model-checking

We consider an extension of linear-time temporal logic (LTL) with constraints interpreted over a concrete domain. We use a new automata-theoretic technique to show pspace decidability of the logic for the constraint systems (Z, <, =) and (N, <, =). Along the way, we give an automata-theoretic proof of a result of [1] when the constraint system satisfies the completion property. Our decision procedures extend easily to handle extensions of the logic with past-time operators and constants, as well as an extension of the temporal language itself to monadic second order logic. Finally we show that the logic becomes undecidable when one considers constraint systems that allow a counting mechanism.

Introduction

Constraint temporal logics. In classical Linear-time Temporal Logic (LTL) [START_REF] Pnueli | The temporal logic of programs[END_REF], properties of a program state are captured using propositions. These propositions could stand for properties like "the value of variable x is non-negative", or that "the value of x is less than that of y", or even that "the value of x in the current state is less than the value of y in the next state". In a natural extension of the logic, one may consider allowing assertions directly on the value of variables, as in "x ≥ 0", "x < y", or "x < Oy". The type of variables and the kind of constraints allowed, leads us to the study of constraint temporal logics.

In this paper we consider constraint temporal logics which are parameterised by a constraint system D which comprises a concrete domain and an interpretation for relations. The logic is essentially obtained from LTL by replacing propositions by atomic constraints in D. In classical LTL variables represent propositions and models for its formulae are sequences of propositional valuations for these variables. These models can be viewed as having a "spatial" axis (here the elements true and false), along which the variables move. In constraint logics, the spatial axis for the models will comprise elements from the domain of D. For example, with the constraint system (N, <, =) one is allowed to use atomic constraints involving < and =, and variables which range over natural numbers. The formula 2(x < y) in the logic parameterised by (N, <, =) is interpreted over a sequence of N-valuations for the variables x and y, and asserts that at every point in the future, the value of the variable x is less than the value of y. This formula is of course satisfiable, a candidate satisfying model being ss • • • , where the valuation s assigns 1 to x and 2 to y.

Constraint temporal logics have been introduced and studied by logicians in the field of knowledge representation [START_REF] Bennett | Multi-dimensional modal logic as a framework for spatio-temporal reasoning[END_REF][START_REF] Wolter | Qualitative spatio-temporal representation and reasoning: a computational perspective[END_REF][START_REF] Baader | A scheme for integrating concrete domains into concept languages[END_REF][START_REF] Lutz | Interval-based temporal reasoning with general TBoxes[END_REF][START_REF] Lutz | Reasoning with the description logic ALCF(D)[END_REF]. Spatio-temporal logics, as they are better known there, involve a hybrid of temporal logic and constraint systems, with varying degrees of interaction. For instance, one may be permitted to refer to the value of a variable x in the next time instant, leading to constraints of the form (x < Ox). More generously, one may be permitted to refer to a future value of a variable, as in (x < 3y) which asserts that the current value of x is less than some future value of y.

While research in the area has focused mainly on logics involving constraint systems that have as domains intervals [START_REF] Allen | Maintaining knowledge about temporal intervals[END_REF][START_REF] Balbiani | Computational complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning[END_REF] and regions [START_REF] Randell | A spatial logic based on regions and connection[END_REF][START_REF] Bennett | Spatial reasoning with propositional logic[END_REF][START_REF] Wolter | Spatio-temporal representation and reasoning based on RCC-8[END_REF], with a variety of decidability and complexity results, there seems to have been little attention paid to commonly used constraint systems of the form (D, <, =), with D as the integers Z or natural numbers N. Comon and Cortier [START_REF] Comon | Flatness is not a weakness[END_REF] consider a constraint system with the natural numbers N as the underlying domain and constraints of the form x < Oy+2, and show that the corresponding constraint temporal logic is undecidable. They identify a decidable fragment of the logic by restricting the use of the "Until" operator. Balbiani and Condotta [START_REF] Balbiani | Computational complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning[END_REF] prove a general decidability result for constraint systems that satisfy a "completion" property and terms of the form O • • • Ox. The completion property says that given a finite consistent set of constraints X, a valuation for a subset of variables which satisfies the constraints in X involving only those variables, can be extended to a valuation which satisfies all of X. The constraint system (R, <, =) satisfies this property, and the decidability of the constraint logic based on (R, <, =) in pspace follows from this result.

Our contribution. In this paper we concentrate on a constraint temporal logic called CLTL(D), for Constraint LTL parameterised by a constraint system D, in which we restrict ourselves to terms of the form O • • • Ox.

Our main technical contribution is a decision procedure for the satisfiability problem for the logic over the constraint systems Z = (Z, <, =) and N = (N, <, =). These logics are interesting from a technical point of view. As a typical illustration, the formula 2(x > Ox) has no (infinite) N-models, while it does have R-models and Z-models. These constraint systems do not satisfy the completion property, and hence we cannot use the technique of [START_REF] Balbiani | Computational complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning[END_REF] here. Further, in contrast to classical LTL, we show in Sec. 6 that the set of models L(ϕ) of a formula ϕ in these logics is, in general, not ω-regular (i.e. it cannot be accepted by an automaton on infinite words). Nevertheless, we show that their satisfiability problems are decidable, and in fact pspace-complete. Our approach is automata-theoretic in that we associate with a given formula ϕ in CLTL(Z), an automaton A Z ϕ which is non-empty iff ϕ has a Z-model (and similarly for the N case). Roughly speaking, the technique used is as follows: we find an ω-regular superset M of L(ϕ), which has the property that all its ultimately periodic words (those of the form τ • δ ω ) are also in L(ϕ). This guarantees that M is non-empty iff L(ϕ) is. We can now check the emptiness of M -using standard automata theory techniques -to decide the satisfiability of ϕ.

The second contribution of this paper arises from the fact that we use a general automata-theoretic approach which is also modular in nature. The approach is automata-theoretic in the sense of [START_REF] Vardi | Reasoning about infinite computations[END_REF] in that we construct an automaton for a given formula whose language is non-empty if and only if the formula is satisfiable. It is modular in that the automaton we construct is the intersection of two separate automata, one corresponding to the underlying logical language, and the other for the constraint system under consideration. There are many benefits of such an approach and we hope these will be evident in the paper. In particular, this approach facilitates a transparent argument for the result of [START_REF] Balbiani | Computational complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning[END_REF] for constraint systems satisfying the completion property. For such constraint systems D we can further show that the set of models of formulas in this logic is ω-regular (more precisely we speak here of the set of induced "frame sequences" or symbolic models). The modular approach also makes it easy to generalize the decision procedure in a transparent manner to handle past operators in LTL as well as to augment the underlying logical language from LTL to Büchi's monadic second order logic [START_REF] Büchi | On a decision method in restricted second order arithmetic[END_REF].

The third part of our contribution is that we establish decidability and complexity results for some natural extensions of Constraint LTL. We consider an extension which allows constants to be used in constraints, and show that for "dense" constraint systems like (R, <, =) and for the discrete constraint systems (Z, <, =) and (N, <, =), we can reduce the satisfiability problem to the standard case by eliminating the constants. We also introduce a class of constraint systems having a "counting" mechanism and we establish that the satisfiability problem for CLTL(D) becomes undecidable when D has a "counting" mechanism. In particular the logic for the constraint system (N, =, = +1 , ) is undecidable. Finally, we make use of our modular approach to show the decidability of the satisfiability and model-checking problems for MSO extensions of CLTL(D).

Applications. Our main motivation in this work has been to examine decidability issues related to a natural extension of LTL. However, there are some potential applications of the work here. The constraint logics considered here can be viewed as a convenient specification language for the behaviour of non-terminating programs. Valuation sequences can be thought of as snapshots of a program's variables at specific points of time during its execution. The work in this paper can be used to tell whether the given specification is realizable, and if so, to synthesize a program that meets the specification. For example, for a CLTL(Z, <, =) specification ϕ, our technique enables us to tell whether ϕ is satisfiable, and if it is, gives us an ultimately periodic frame sequence τ • δ ω , along with a procedure to label it with integers, to obtain a model for the given specification. These finite frame sequences τ and δ, along with the labeling procedure, can be thought of as the required program whose behaviour satisfies the given specification.

Our modular automata-theoretic technique has also been useful in subsequent related work as detailed below, where it has been used as a fruitful starting point.

Related work.

The analysis of the reachability problem for counter systems is ubiquitous in the verification of infinite-state systems [START_REF] Comon | Multiple counters automata, safety analysis and Presburger analysis[END_REF][START_REF] Ibarra | Counter machines: Decidable properties and applications to verification problems[END_REF][START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF][START_REF] Dang | Presburger liveness verification of discrete timed automata[END_REF] and this partly motivates the versions of constraint LTL introduced in this paper. On the logical side, temporal logics with Presburger constraints have been developed in [START_REF] Čerans | Deciding properties of integral relational automata[END_REF][START_REF] Bouajjani | On the verification problem of nonregular properties for nonregular processes[END_REF][START_REF] Comon | Flatness is not a weakness[END_REF][START_REF] Bruyère | Durations, parametric model-checking in timed automata with presburger arithmetic[END_REF], some of which have quite expressive decidable fragments. Spatio-temporal logics, see e.g. [START_REF] Wolter | Spatio-temporal representation and reasoning based on RCC-8[END_REF][START_REF] Gabbay | Many-dimensional modal logics: theory and applications[END_REF][START_REF] Hodkinson | On the computational complexity of decidable fragments of first-order linear temporal logics[END_REF][START_REF] Gabelaia | On the computational complexity of spatio-temporal logics[END_REF] are also examples of versions of LTL with constraint systems for which the constraint system has indeed a spatial structure. Examples of such spatial systems satisfying the completion property and those not satisfying this property can be found in [START_REF] Balbiani | Computational complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning[END_REF] and [START_REF] Lutz | A tableau algorithm for description logics with concrete domains and GCIs[END_REF]. Incidentally, a property similar to completion is used in Constraint Satisfaction Problems [27]. Complexity and decidability results for such logics can be found in [START_REF] Gabbay | Many-dimensional modal logics: theory and applications[END_REF]. In the introduction of concrete domains in description logics is due to [START_REF] Baader | A scheme for integrating concrete domains into concept languages[END_REF] and since then, such logic-based formalisms for knowledge representation have been intensively studied, see e.g. [START_REF] Lutz | Description logics with concrete domains-a survey[END_REF][START_REF] Lutz | NEXPTIME-complete description logics with concrete domains[END_REF]. Hence, LTL over concrete systems can be technically viewed as a subclass of description logics over concrete domains in which the models are linear. However, the introduction of LTL over Presburger constraints is motivated by the need to model-check counter systems whereas concrete domains in description logics have been introduced to integrate concrete qualities into description logic concepts.

The general approach presented in [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF] and further developed in this long version, has been the starting point to further analyse temporal logics with constraint systems. Some of these are detailed below.

• Periodicity constraints are considered in [START_REF] Demri | LTL over integer periodicity constraints[END_REF] with applications for the automaton-based technique to define calendars. • An extension of CLTL(N, <, =) with constants and periodicity constraints is shown in pspace in [START_REF] Demri | Verification of qualitative Z-constraints[END_REF] generalizing the pspace upper bound of CLTL(N, < , =) established in this paper. • The branching-time extension of [START_REF] Demri | Verification of qualitative Z-constraints[END_REF] is explored in [START_REF] Bozzelli | Branching-time temporal logic extended with Presburger constraints[END_REF] that generalizes the decidability result. • Complexity and decidability issues for fragments of LTL with Presburger constraints are analyzed in [START_REF] Demri | The effects of bounding syntactic resources on Presburger LTL[END_REF]. • A survey on Constraint LTL over Presburger constraints can be found in [START_REF] Demri | Linear-time temporal logics with Presburger constraints: An overview[END_REF].

In [START_REF] Demri | LTL over integer periodicity constraints[END_REF][START_REF] Demri | On the freeze quantifier in constraint LTL: decidability and complexity[END_REF][START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF][START_REF] Lazić | Safely freezing LTL[END_REF], versions of Constraint LTL with the freeze operator that allow to express constraints of the form (x < 3y) are studied, leading to various complexity and decidability results. For instance, such an operator can be also encoded in logical formalisms for data words and XML documents [START_REF] Bojańczyk | Two-variable logic on words with data[END_REF] or for computations of systems with unboundedly many locations as resources [START_REF] Lisitsa | Temporal logic with predicate λ-abstraction[END_REF], to quote a few examples.

Finally, the different variants of LTL over constraint systems presented in this paper can be viewed as fragments of first-order LTL where the domain of interpretation of variables is fixed as well as the interpretation of predicate symbols. Moreover, variables in CLTL(D) correspond to unary predicate symbols interpreted as singletons (the values of variables). However, CLTL(D) has no quantification over elements of the domain and in that sense it corresponds to a very weak first-order extension of plain LTL. A variant of first-order LTL has been introduced in [START_REF] Deutsch | Specification and verification of data-driven web services[END_REF] to verify data-driven web applications. The interplay between temporal operators and first-order quantifiers is also restricted since no quantification can occur in the scope of temporal operators, which guarantees better computational properties.

Plan of the paper. In the next couple of sections we define our logic and state its important relation to classical LTL. Sec. 4 addresses constraint systems which satisfy the completion property, and Secs. 5-7 address the satisfiability problem for the constraint systems Z and N . In Sec. 9 & 10 we consider extensions to the logic. Though the emphasis in most of the paper is on the satisfiability problem for the logics, in Sec. 8 we also look at the model-checking problem for the logic CLTL(D).

Definitions

The set of natural numbers, integers, rationals, and reals, will be denoted by N, Z, Q, and R respectively. An infinite word (or sequence) over an alphabet Σ is a function α : N → Σ, written as α(0)α(1) • • • . For an infinite word α, we will use α[i, j] to denote the finite word α(i)α(i + 1) • • • α(j), and α[i, ∞] to denote the infinite suffix α(i)α(i + 1) • • • . The set of all infinite words over Σ is denoted by Σ ω . For a finite word τ and a finite or infinite word γ, we use τ • γ to denote the concatenation of τ and γ, and τ ω to denote the infinite word τ

• τ • • • . A (concrete) constraint system D is of the form (D, R 1 . . . , R n , I)
, where D is a non-empty set referred to as the domain, and each R i is a predicate symbol of arity a i , with I(R i ) ⊆ D a i being its interpretation. We will suppress the mention of I whenever it is clear from the context. Let us fix such a constraint system D for the rest of this section.

An (atomic) D-constraint over a finite set of variables U is of the form R(x 1 , . . . , x a ), where R is a predicate symbol of arity a in D and each x i ∈ U . A D-valuation over U is a map s : U → D. We will use the notation val D (U ) to denote the set of D-valuations over U . Let c = R(x 1 , . . . , x a ) be a D-constraint over U , and let s be a D-valuation over U . Then we say s satisfies c, written s |= D c, iff (s(x 1 ), . . . , s(x a )) ∈ I(R).

In the temporal logic we consider, we will allow terms of the form O • • • Ox to appear in an atomic constraint. The idea is that a term OOx, for example, will refer to the variable x, 2 steps ahead. Formally, an (atomic) D-term constraint over a set of variables U , is of the form

R(O n 1 x 1 , . . . , O n a x a )
where Let c be a D-term constraint over a set of variables U . By the O-length of c we will mean the value i + 1 where i is the largest j for which O j occurs in c. Thus the O-length of the term constraint x < Oy is 2. The truth of a term constraint c in a valuation sequence σ is clearly determined completely by σ[0, k -1], where k is the O-length of c.

A term constraint c over U of O-length k can also be viewed in a natural way as a constraint over the variables U × {0, . . . , k -1}, by identifying O i x with (x, i). Whenever it is convenient we will take the liberty of adopting this view.

We now introduce CLTL(D), the Constraint Linear-Time Temporal Logic parameterised by the constraint system D. Let Var be a countably infinite set of variables, which we fix for the rest of this paper. The syntax of CLTL(D) is given by: ϕ

::= c | ¬ϕ | (ϕ ∨ ϕ) | Oϕ | (ϕU ϕ)
where c is a D term constraint over the set of variables Var . The symbol 'O' is overloaded herein (used for D-terms and as a temporal operator) but this will not cause any confusion.

Models for CLTL(D) formulas are D-valuation sequences over the variables Var . Let ϕ be a CLTL(D) formula, and σ be D-valuation sequence over Var . The satisfaction relation σ |= ϕ is defined inductively below.

σ |= c iff σ |= D c σ |= ¬ϕ iff σ |= ϕ σ |= ϕ ∨ ψ iff σ |= ϕ or σ |= ψ σ |= Oϕ iff σ[1, ∞] |= ϕ σ |= ϕU ψ iff ∃k ∈ N such that σ[k, ∞] |= ψ and ∀i : 0 ≤ i < k, σ[i, ∞] |= ϕ.
We use the derived operators 3 and 2 which stand for "sometime" and "always", with the semantics 3ϕ ≡ ( U ϕ), and 2ϕ ≡ ¬( U ¬ϕ).

Let L D (ϕ) denote the set of models of a CLTL(D) formula ϕ.

Thus L D (ϕ) = {σ ∈ (val D (Var )) ω | σ |= ϕ}.
Let voc(ϕ) denote the finite set of variables that appear in ϕ. The truth of ϕ in a valuation sequence is thus determined completely by the values of the variables in voc(ϕ), and so we can describe models of ϕ by restricting them to the variables in voc(ϕ).

As an example, consider the constraint system N = (N, <, =) with the usual interpretation of the symbols '<' and '='. Let ϕ be the formula 2(x < Oy). Let us represent a valuation s restricted to voc(ϕ) = {x, y} as (s(x), s(y)). Then ϕ is satisfied by the N-valuation

sequence σ = (1, 2)(2, 4)(3, 6) • • • , but not by σ = (1, 1)(2, 2)(2, 2) • • • .
It is visually convenient to describe a valuation sequence like σ using the notation below:

y 2 4 6 8 • • • x 1 2 3 4 • • •
As another example, the valuation sequence below satisfies the formula 3(y < O 2 z) ∧ ¬2(y < O 2 z):

z 8 0 3 2 • • • y 5 1 0 1 • • • x 1 0 4 4 • • •
We recall briefly the definition of classical LTL. We are given a countable set of propositions P , and formulas are formed in much the same way as CLTL(D), except that instead of constraints c we have propositional assertions p from the set P . Models of LTL formulas are sequences of propositional valuations to variables in P . A propositional valuation over P can be represented as a subset of P , specifying the subset of propositions set to true. A propositional valuation sequence is thus a sequence over 2 P . The satisfaction relation α |= LTL ϕ, for a propositional valuation sequence α and LTL formula ϕ, is given as follows. α |= LTL p iff p ∈ α(0), with the semantics of the remaining operators being the same as that of CLTL(D).

We can view the logic CLTL(D) as a generalization of classical LTL. LTL is equivalent to the constraint logic CLTL({0, 1}, true) with I(true) = {1}. A translation from LTL into CLTL({0, 1}, true) consists of replacing the propositional variable p i by true(x i ). For instance,

{p 2 , p 3 } • {p 3 } • {p 1 , p 3 } . . . |= LTL 3(p 1 ∧ p 3 ) iff x 3 1 1 1 • • • x 2 1 0 0 • • • |= 3(true(x 1 ) ∧ true(x 3 )). x 1 0 0 1 • • • 3 Semantics via classical LTL
The semantics of CLTL(D) formulas can also be given in terms of classical LTL. This view of the logic will play an important role in the developments in this paper.

Before we proceed, we will assume for convenience of notation that the formulas in CLTL(D) are over a fixed, finite set of variables V . This assumption involves no loss of generality as far as our decision procedures are concerned, since a given formula can speak of only a finite number of variables in Var . Henceforth, unless explicitly stated, we will assume valuations, valuation sequences, and term constraints, to be over the fixed finite set of variables V .

Next we introduce some required terminology. A frame over a set of variables U , w.r.t. a constraint system D, is essentially a maximally consistent set of D-constraints over U . More precisely, let frame D (s, U ) denote the (possibly empty) set of D-constraints over U satisfied by a D-valuation s over U . Then a set of D-constraints X is a frame over the variables U , w.r.t. D, if there exists a D-valuation s over U such that X = frame D (s, U ).

In anticipation of a later need we define what we call the frame checking problem for a constraint system D. This is the problem of deciding whether a given set of D-constraints X, and a finite set of variables U , whether X is a frame over U , w.r.t. D.

We now want to refer to the frame induced by a k-length segment of a valuation sequence over V , which we will call a k-frame. Let σ be a D-valuation sequence and let k ∈ N. We use atc(D, k) to denote the set of all D-term constraints over V , of O-length at most k. Let k-frame D (σ) denote the set of all term constraints over V of O-length at most k, that are satisfied by σ.

Thus k-frame D (σ) = {c ∈ atc(D, k) | σ |= D c}. A k-frame w.r.t. D is a subset r of atc(D, k) such that r = k-frame D (σ)
, for some D-valuation sequence σ.

As an example, consider the constraint system N = (N, <, =), and the Nvaluation sequence σ of Sec. 2. We take V to be {x, y}. Then the following set is a 2-frame w.r.t. N , and coincides with 2-frame N (σ):

{ x < y, x < Ox, x < Oy, y < Oy, Ox < Oy, y = Ox, Ox = y, x = x, y = y, Ox = Ox, Oy = Oy }.

Extending the view of term constraints as constraints, a k-frame can be viewed as a frame over the set of variables V × {0, . . . , k -1} in the expected manner.

We say a pair of k-frames (r, r ) (w.r.t. D) is locally consistent, if for all R (of say arity a), and for all 1 ≤ n 1 , . . . , n a ≤ k -1:

R(O n 1 x 1 , . . . , O n a x a ) ∈ r iff R(O n 1 -1 x 1 , . . . , O n a -1 x a ) ∈ r .
Accordingly, a k-frame sequence ρ will be said to be locally consistent if for all i ∈ N, the pairs (ρ(i), ρ(i + 1)) are locally consistent.

A given D-valuation sequence σ induces, for a given k, a canonical locally consistent k-frame sequence ρ, w.r.t. D, denoted k-fs D (σ), and given by ρ

(i) = k-frame D (σ[i, ∞]).
The sequence σ is indeed a concrete model of CLTL(D) whereas k-fs D (σ) can be viewed as one of its symbolic representations by abstracting the values by D-terms.

We extend k-fs to act on sets of valuation sequences in the natural way; thus k-fs D (L) = {k-fs D (σ) | σ ∈ L}. Conversely, a k-frame sequence ρ will be said to admit a D-valuation sequence, if there exists a D-valuation sequence σ such that k-fs D (σ) = ρ. In that case, the concrete model σ is said to realize the symbolic model ρ.

As an illustration, consider once again the constraint system N , with V = {x}. The 2-frame sequence r ω , where r = {x < Ox, x = x, Ox = Ox}, admits the N-valuation sequence

x 0 1 2 3 • • • .
However the 2-frame sequence r ω where r = {x > Ox, x = x, Ox = Ox} does not admit any N-valuation sequence, since we cannot have an infinite strictly decreasing sequence of natural numbers.

We say a CLTL(D) formula

ϕ has O-length k if the largest O-length of term constraints in ϕ is k. Thus the O-length of the formulae 2(O(x < Oy)) and 2(x < Oy) is 2.
Consider now a CLTL(D) formula ϕ, and let k be its O-length. We can view ϕ as an LTL formula over the set of "propositions" atc(D, k), by viewing each term constraint c that appears in ϕ syntactically as a proposition p c , or just c for notational convenience. Thus, for a sequence ρ ∈ (2 atc(D,k) ) ω , we have the (symbolic) satisfaction relation ρ |= LTL ϕ defined by the usual semantics of LTL. We use L LTL (ϕ) to denote the set

{ρ ∈ (2 atc(D,k) ) ω | ρ |= LTL ϕ}.
The following proposition is now a direct consequence of the semantics of CLTL(D) and LTL, and summarizes the link between the two logics:

Lemma 3.1 Let ϕ be a CLTL(D) formula of O-length k. Let σ be a D- valuation sequence, and let ρ = k-fs D (σ). Then σ |= ϕ iff ρ |= LTL ϕ. 2
For a formula ϕ in CLTL(D) of O-length k, let L D fs (ϕ) denote the set of k-frame sequences induced by the valuation sequence models of ϕ. That is

L D fs (ϕ) = {k-fs D (σ) | σ |= ϕ}.
In the light of Lemma 3.1, L D fs (ϕ) is the set of all k-frame sequences (w.r.t.

D) that satisfy ϕ as an LTL formula, and admit a D-valuation sequence. Equivalently, L D fs (ϕ) contains the symbolic models having a concrete model satisfying ϕ.

A general decidability result

Let D = (D, R 1 , . . . , R n ) be a constraint system. The satisfiability problem for CLTL(D) is: given a CLTL(D) formula ϕ, does there exist a D-valuation sequence which satisfies ϕ? In other words, is

L D (ϕ) = ∅? (equivalently, is L D fs (ϕ) = ∅?).
From Lemma 3.1 we have the following corollary. This suggests a way to answer the satisfiability problem for the logic. Recall the automata-theoretic approach to solving the satisfiability problem for classical LTL [START_REF] Vardi | An automata theoretic approach to automatic program verification[END_REF]. One builds an automaton A LTL ϕ which accepts precisely the models of the given formula φ. This automaton can then be checked for nonemptiness to decide the satisfiability of the given formula. In our case we can build the formula automaton A LTL ϕ corresponding to the LTL version of the given formula ϕ. If we could now construct automata that (1) filter out k-frame sequences that are not locally-consistent and (2) filter out k-frame sequences that do not admit D-valuations; then we can intersect them and check the resulting automaton for nonemptiness to decide the satisfiability of ϕ. This approach has structural similarities with [START_REF] Bérard | Untiming timed languages[END_REF] where nonemptiness of timed languages is checked by considering untimed languages.

As we will see in Sec. 6, there are constraint systems for which (2) above is not possible, and one has to adopt a slightly different approach for them. However, there are constraint systems for which it suffices to ensure (1), and ( 2) is automatically taken care of. Constraint systems that satisfy a "completion" property are one class of such constraint systems. In the rest of this section we elaborate on these ideas.

A constraint system D is said to satisfy the completion property if, essentially, given a consistent set of constraints X over a set of variables U , any partial valuation which respects the constraints in X involving only the assigned variables, can be extended to a valuation which respects all the constraints in X. More precisely, for a set of constraints X and a subset of variables U , let us use the notation X U to denote the set of constraints in X which use only variables in U . Then, the constraint system D satisfies completion if given • a frame X over a finite set of variables U w.r.t. D, • a subset U of U , and • a valuation s over U , such that frame D (s , U ) = X U . there exists a valuation s over U which extends s and satisfies frame D (s, U ) = X.

The constraint system (R, <, =) is one example of a system that satisfies the completion property. We will prove this fact in the next section where we show that the completion property is closely related to "denseness" of the domain.

An example of a constraint system which does not satisfy the completion property is (Z, <, =), since for the set of constraints X = {x < y, x < z, z < y, x = x, y = y, z = z} over the set of variables U = {x, y, z}, the partial valuation s : x → 0, y → 1 satisfies the constraints in X involving x and y, but cannot be extended to a valuation which satisfies the constraints x < z and z < y in X.

We now observe that: Lemma 4.2 Let D be a constraint system which satisfies the completion property. Then every locally consistent k-frame sequence w.r.t. D admits a Dvaluation sequence.

Proof Let ρ = r 0 r 1 . . . be a locally consistent k-frame sequence w.r.t.

D = (D, R 1 , . . . , R n ). We define a D-valuation sequence σ = s 0 s 1 • • • with the property that ρ = k-fs D (σ).
We take the liberty of viewing each r i as a frame over the variables U i = V × {i, . . . , i + k -1}. Since each r i is a k-frame, for each i there exists a Dvaluation t i over U i such that r i = frame D (t i , U i ). For each i ∈ {0, . . . , k -1} and x ∈ V , we define s i (x) = t 0 (x, i). Now suppose that s i is defined for 0 ≤ i ≤ j with j ≥ k -1. Let us define s j+1 . Consider the set of constraints r j+1 . We know that r j+1 is a frame over U j+1 . Further consider the subset

U = V × {j + 1, . . . , j + k -1} of U j+1 .
The restriction t of the valuation t j to U , is such that r j+1 U = frame D (t , U ). Thus, by the completion property we have a D-valuation t which extends t to the variables V ×{j+1, . . . , j+k}, and satisfies r j+1 = frame D (t , U j+1 ). We can now define s j+1 (x) = t (x, j + 1) for each x ∈ V .

The sequence σ = s 0 s 1 • • • can be completely defined and σ has the property that k-fs D (σ) = ρ. Hence ρ admits the D-valuation sequence σ.

2

Here is an interesting property of the language of k-frames defined by a CLTL(D) formula, which we had alluded to in the beginning of this section. Recall that a Büchi automaton over an alphabet Σ is simply a classical automaton A = (Q, q 0 , -→, F ) over Σ, but with the set of final states F used as an acceptance condition on infinite words α ∈ Σ ω . A run ρ : N → Q on α is accepting if ρ(i) ∈ F for infinitely many i ∈ N. L(A) is the set of infinite words accepted by A, and L ⊆ A ω is termed ω-regular if L = L(A) for some Büchi automaton A over Σ. The class of w-regular languages are known to be effectively closed under the boolean operations of union, intersection, and complement. Further, the nonemptiness problem for these automata is easily decidable, being essentially a graph reachability problem. We refer the reader to [START_REF] Thomas | Automata on infinite objects[END_REF] for further details. Proof Let ϕ be of O-length k. We define a Büchi automaton

A D ϕ over the alphabet 2 atc(D,k) , such that L(A D ϕ ) = L D fs (ϕ). Define A D ϕ = A LTL ϕ ∩ A D,k lc (i.
e. the automaton which accepts the intersection of the languages of the two automata), where A LTL ϕ is the Vardi-Wolper automaton [START_REF] Vardi | An automata theoretic approach to automatic program verification[END_REF] for the LTL formula ϕ, and A D,k lc is a Büchi automaton over 2 atc(D,k) , defined below, which accepts locally consistent k-frame sequences.

Define A D,k lc = (Q, q 0 , -→, F ) where Q is the set of k-frames w.r.t. D, along with a separate start state q 0 ; -→ is given by q 0 r -→ r, and r r -→ r iff (r, r ) is locally consistent (here r and r range over k-frames w.r.t. D); and F = Q. 2 Thus, if A D ϕ can be constructed effectively, Lemma 4.3 gives us a way to decide the satisfiability problem for a constraint system D which satisfies the completion property: construct A D ϕ and check it for nonemptiness. We know that A LTL ϕ can indeed be constructed [START_REF] Vardi | An automata theoretic approach to automatic program verification[END_REF]. However, whether automaton A D,k lc can be constructed effectively depends on the decidability of the frame-checking problem for D, since the transition relation of the automaton must be computable and for this one needs to recognize whether a set of constraints constitutes a frame.

In particular, if D is such that frame checking can be done in pspace (in the size of the frame), then the satisfiability problem for CLTL(D) can be solved in pspace in the size of the given formula. The automata A LTL ϕ and A D,k lc have sizes exponential in the length of ϕ. However, they are both implicitly defined graphs whose adjacency relation can be checked in pspace in the length of ϕ. For A D,k lc we need the assumption that frame checking for D can be done in pspace. Now checking emptiness of the language accepted by a Büchi automaton essentially requires checking whether there is a final state reachable from the initial state, which is again reachable from itself. It is well-known that reachability on an n-node graph can be done nondeterministically in nlogspace. Thus, emptiness checking for A D ϕ can be done non-deterministically in pspace in the length of ϕ. Since deterministic and non-deterministic pspace coincide, we can conclude that it can be done deterministically in polynomial space. This is essentially the result of [START_REF] Balbiani | Computational complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning[END_REF], presented in an automata-theoretic manner. Finally, if D is non-trivial in the sense that at least one of the relations R is not ∅ or D a (where a is the arity of R), the satisfiability problem of classical LTL (which is known to be pspace-hard [START_REF] Sistla | The complexity of propositional linear temporal logics[END_REF]) can be reduced to the satisfiability problem for CLTL(D). We can do this by translating an LTL formula ψ into a CLTL(D) formula ϕ as follows. With each proposition p we associate a set of distinct variables {x p 1 , . . . , x p a }. Further, these sets are disjoint for each pair of propositions. We now replace each proposition p in ψ by R(x p 1 , . . . , x p a ). The formula ψ is now LTL satisfiable iff ϕ is CLTL(D) satisfiable.

To summarize: In this section we consider domains of the form (D, <, =), where D is an infinite set, '<' is any strict total ordering on D, and '=' is the equality relation. We introduce a natural way of representing frames over such domains as labelled directed graphs. This representation will play a useful role in subsequent arguments in this paper. We then give a characterisation of such domains that satisfy the completion property. For a constraint system of the form (D, <, =) it is convenient to visualise a frame as a labelled, directed graph. For the rest of this section let us fix a constraint system D = (D, <, =) with D an infinite set, and '<' a strict total ordering on D. We represent a frame X over a finite set of variables U by a {<, =}-labelled, directed graph G X over the vertices U , where we place a '∼'-labelled edge (for ∼∈ {<, =}) from x to y precisely when x ∼ y ∈ X.

Such a graph clearly satisfies the conditions that:

(1) There is an edge between every pair of vertices;

(2) If there is a '='-labelled edge from x to y then there is also one from y to x; (3) There are no strict cycles -i.e. directed cycles containing a '<'-labelled edge.

We call such a graph (i.e. a {<, =}-labelled directed graph over a set of vertices U which satisfies the conditions 1-3 above) a frame graph over U .

Conversely, given a frame graph H over a finite set of vertices U , the set of constraints gtof (H) = {x ∼ y | x ∼ -→ y in H} constitutes a frame over U . To see this, observe that we can label the vertices of H by natural numbers via a labelling l : U → N, which respects the edges in

H -i.e. if u ∼ -→ v then l(u) ∼ l(v).
The map l is said to be an edge-respecting labelling. This follows since we can quotient H by equating vertices joined by edges labelled by '=' to get a DAG (in fact a total order) on U , which can then be linearized. Since U is finite, this gives us a natural edge-respecting labelling l of U by numbers in N. From a finite non-decreasing sequence of natural numbers we can always obtain a corresponding (order preserving) sequence in D, which gives us an edge-respecting D-labelling l of H. Viewing l as a D-valuation over U , it is immediate that frame (l , U ) = gtof (H). Thus gtof (H) is a frame.

Frame graphs are thus a faithful representation of frames in the following sense:

Lemma 5.1 Let X be a frame over U w.r.t. D. Then (1) G X is a frame graph over U . (2) If H is a frame graph over U then gtof (H) is a frame over U . (3) gtof (G X ) = X. (4) A D-valuation s over U is such that frame (s, U ) = X iff s is an edge- respecting labelling of G X . 2
Observe that the frame-checking problem for D amounts to checking whether the graph corresponding to the given frame satisfies the conditions 1-3 in the definition of a frame graph above. Since cycle detection in a directed graph can be done in nlogspace, we conclude that the frame checking problem for D is in nlogspace. Extending the representation of frames as frame graphs, a locally consistent k-frame sequence ρ can be represented as a single {<, =}-labelled, directed graph G ρ . The graph G ρ is essentially the superimposition (in an overlapping manner) of the graphs corresponding to the successive k-frames. Fig. 1 shows the first two 3-frames of a locally consistent k-frame sequence represented as a single graph. In the figure we have left out self-loops on the vertices, as well as '<' labels on edges, for brevity. More precisely, G ρ has V × N as its set of vertices, and an edge (x, i)

∼ -→ (y, j) (∼∈ {<, =}) iff either i ≤ j and (x ∼ O j-i y) ∈ ρ(i), or, i > j and (O i-j x ∼ y) ∈ ρ(j).
In a natural way, a D-valuation sequence σ can be viewed as a D-labelling l of the vertices of G ρ by defining l(x, i) = σ(i)(x). Conversely, a D-labelling l of G ρ gives us a D-valuation sequence σ given by σ(i)(x) = l(x, i). It thus follows that: (d,d ) is an edge-respecting labelling of G X restricted to U . By the completion property, we should be able to extend l to an edge-respecting D-labelling l over U . We thus have an element l(z) ∈ D with d < l(z) < d . Similarly for openness, given a d ∈ D we can consider the trivial edge-respecting labelling of the single vertex y, which assigns d to y. This labelling must be extendable to a labelling of U , which gives us elements l(x) and l(z) of D satisfying l(x) < d < l(z).

Conversely, let D be open and dense. We show that it satisfies the completion property. Let X be a frame over a finite set of variables U . Let U be a nonempty subset of U , and l an edge-respecting labelling for the subgraph of G X induced by U . Let x be a vertex in U \ U . We will label x with d ∈ D, such that the resulting labeling l = s ∪ {(x, d)} of U ∪ {x} is an edge-respecting labelling of the subgraph induced by U ∪ {x}. This will suffice to prove the completion property, since this procedure can be repeatedly applied to obtain a labelling of U which extends l . Let X =x be the set of vertices in U to which there is an '='-labelled edge from x in G X ; X <x the set of vertices in U from which there is a '<'-labelled edge to x; and X x< the set of vertices in U to which there is a '<'-labelled edge from x. Let p = max{l (y) | y ∈ X <x } and q = min{l (z) | z ∈ X x< } (we will use the values of p and q only when the sets X <x and X x< , are respectively non-empty.) Note that p and q are values in D, and by denseness and openness of D there exist elements p , q , r in D such that p < p , q < q and p < r < q.

We label x as follows:

(1) if X =x is non-empty, label x by l (y) for any y ∈ X =x , (2) if X <x is non-empty and both X =x and X x< are empty, label x by p , (3) if X x< is non-empty and both X =x and X <x are empty, label x by q . (4) if X <x and X x< are non-empty and X =x is empty, label x by r.

To argue that d is an acceptable label for x, suppose to the contrary, that it was not. Then there must exist a vertex y in U and an edge between x and y which is inconsistent with the labels of x and y. Two cases arise here: We have x < -→ y but l(x) ≥ l(y) (and the symmetric case of y

< -→ x), or x = -→ y and l(x) = l(y).
For the first case, it must have been the case that x was labelled by clause 1. Thus there must be another vertex z in U with x = -→ z in G X , and l(x) = l(z). But since l was an edge-respecting labelling, we must have y

< -→ z or y = -→ z in G X . This gives us a strict cycle x < -→ y < -→ z = -→ x or x < -→ y = -→ z = -→ x in G X , which is a contradiction.
For the second case to have arisen, it must again be the case that x was labelled by clause 1. Thus there is a vertex z such that x = -→ z and l(z) = l(x). Once again this gives us a strict cycle in G X which is a contradiction. 2

It now follows that: Corollary 5. [START_REF] Bennett | Multi-dimensional modal logic as a framework for spatio-temporal reasoning[END_REF] The following constraint systems are non-trivial and satisfy the completion property [START_REF] Balbiani | Computational complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning[END_REF]:

(1) (R, <, =), (Q, <, =). Constraint systems satisfying the completion property can be found in [START_REF] Allen | Maintaining knowledge about temporal intervals[END_REF][START_REF] Vilain | Constraint propagation algorithms for temporal reasoning[END_REF]. Other constraint domains used in spatio-temporal logics as spatial domains lead to a pspace upper bound, see e.g. [START_REF] Gabbay | Many-dimensional modal logics: theory and applications[END_REF]Chapter 16] and [START_REF] Gabelaia | On the computational complexity of spatio-temporal logics[END_REF].

Finally, we point out an important property of G ρ which is that it does not contain any strict cycles: Corollary 5.6 Let D = (D, <, =) be such that < is a strict total order on D. Then, for a locally consistent k-frame sequence ρ w.r.t. D, the graph G ρ has no strict cycles.

Proof It is not difficult to see that a k-frame with respect to D is also one w.r.t. (R, <, =). Thus ρ is also a locally consistent k-frame sequence w.r.t. (R, <, =). Now by Corollary 5.4 and Lemma 4.2, ρ admits an R-valuation sequence. Equivalently, there is an edge-respecting R-labelling of G ρ . Thus a strict cycle in G ρ would imply a label in G ρ is less than itself, which is a contradiction. 2 6 Satisfiability for CLTL(Z, <, =)

In this section we consider the constraint system Z = (Z, <, =). It follows from Lemma 5.3 that Z does not satisfy the completion property. As a result we cannot appeal to Theorem 4.4 to solve the satisfiability problem for the logic CLTL(Z). In fact, we will show that unlike the case for R, the language L Z fs (ϕ) is not ω-regular in general (Corollary 6.5). Nonetheless, we can still solve the satisfiability problem for CLTL(Z) automata-theoretically. The idea is to define a Büchi automaton A Z ϕ which accepts a superset of L Z fs (ϕ) with the property that all ultimately periodic words in it are also in L Z fs (ϕ). It will then follow that L(A Z ϕ ) is non-empty iff ϕ is CLTL(Z)-satisfiable.

We begin with a characterisation of locally consistent k-frame sequences which admit a Z-valuation sequence, along the lines of [START_REF] Čerans | Deciding properties of integral relational automata[END_REF]Lemma 5.5]. Let ρ be a locally consistent k-frame sequence (which in this section we understand to be w.r.t. Z). For a directed path p in G ρ , let slen(p) denote the strict length of p -i.e. the number of '<'-labelled edges in p if this number is finite, and ω otherwise. For any two vertices u, v in G ρ , define slen(u, v) to be the supremum of slen(p) over directed paths p from u to v, if it exists, and ω otherwise. Whenever there is no directed path from u to v, slen(u, v) takes the value 0 by convention.

Lemma 6.1 Let ρ be a locally consistent k-frame sequence. Then ρ admits a Z-valuation sequence iff for all u, v ∈ G ρ , slen(u, v) < ω.

Proof If ρ admits a Z-valuation sequence σ, let l be the corresponding edgerespecting labelling of G ρ . Then clearly slen(u, v) ≤ |l(v)-l(u)| for all vertices u, v in G ρ . Thus, there cannot exist vertices u and v with slen(u, v) = ω.

Conversely, suppose G ρ satisfies the given condition. We assume that k is at least 2 (for k = 1, it is clear that ρ always admits a Z-valuation). One can verify that the procedure given below produces an edge-respecting Z-labelling l of G ρ . This in turn implies that ρ admits a Z-valuation sequence. We assume an ordering ≺ on variables, and use it to define an ordering of vertices in G ρ given by (x, i) ≺ (y, j) iff i < j, or i = j and x ≺ y.

(1) Label the vertices in order. Begin by labelling the first, say (x, 0), by 0.

(2) In general, if X is the portion of the graph already labelled, and u is the next vertex to be labelled: (a) if there is a directed path from u to a vertex in X, set l

(u) = min{l(v) -slen(u, v) | v ∈ X, ∃ a path from u to v}, else, (b) set l(u) = max{l(v) + slen(v, u) | v ∈ X, ∃ a path from v to u}.
Note that with k ≥ 2 every vertex other than (x, 0) has a vertex preceding it in the ordering above, to which it is connected by an edge (from the relation (

< -→ ∪ = -→ ∪ > -→) * ).
Hence case (2a) or (2b) is always applicable, and the procedure never gets stuck.

To argue that the procedure does give us a valid Z-labelling for G ρ , let us assume the contrary. Then there must be a first time where the procedure labels a vertex, say u, with a value which contradicts the strict length of a path from or to this vertex u. Moreover, since there are no strict cycles in G ρ , this path must be from u to an already labelled vertex, or from an already labelled vertex to u. Let the vertex at the other end of the offending path be v, and let the vertices labelled up to this point be X. Note that v ∈ X. There are two cases to examine:

(1) The offending path p is from u to v, and slen(p) > l(v)l(u). But in this case, step (2a) of the procedure is applicable, and hence l(u) ≤ l(v)slen(p). Thus this case is not possible. (2) The offending path p is from v to u with slen(p) > l(u)l(v). Here again two possibilities arise.

In the first possibility vertex u was labelled by an application of step (2a) of the procedure. So there must have been a vertex w in X with a path q from u to w, and l(u) = l(w)slen(q). But since v and w were labelled without any discrepancy, it must be the case that l(w)l(v) ≥ slen(p)+slen(q). Thus l(u) = l(w)-slen(q) ≥ l(v)+slen(p). This contradicts our assumption that slen(p) > l(u)l(v), and hence this possibility is ruled out too.

The second possibility is that u was labelled by an application of step (2b) of the procedure. But then it must be the case that l(u) ≥ l(v) + slen(p). Thus this case is ruled out too.

2

The natural question is now: can we characterize, by means of automata, the locally consistent k-frame sequences that admit a Z-valuation? Consider the condition (C Z ) below on a locally consistent k-frame sequence ρ. In what follows, by an infinite forward (respectively backward ) path in G ρ we will mean a sequence d : N → V × N satisfying:

(1) for all i ∈ N, there is an edge from d(i) to d(i + 1) (respectively, an edge from d(i + 1) to d(i)), (2) for all i ∈ N, if d(i) is in level j, then d(i + 1) is in a level greater than or equal to j + 1. By the "level" of a vertex (x, j) we mean j.

Such a path d will be called strict if there exist infinitely many i for which there is a '<'-labelled edge from d(i) to d(i + 1) (respectively, from d(i + 1) to d(i)).

Two vertices are in the same k-frame iff the difference of levels between them is strictly less than k. Here is the condition (C Z ).

(C Z ): There do not exist vertices u and v in the same k-frame in G ρ satisfying:

(1) there is an infinite forward path d from u, (2) there is an infinite backward path e from v, there is an edge labelled '<' from d(i) to e(j).

It follows from Lemma 6.1 that condition (C Z ) is necessary for ρ to admit a Z-valuation sequence: if ρ does not satisfy (C Z ) -i.e. there are vertices u and v satisfying the conditions (1)-( 4) above -then u and v are such that slen(u, v) = ω, and hence by Lemma 6.1 ρ does not admit a Z-valuation sequence.

But it is not sufficient as witnessed by the 2-frame sequence ρ Z bad in Fig. 2. In the figure we have shown only the relevant edges. Essentially from the vertex (x, i), for i of the form j(j+1)

2 , we have a strict path of strict length j + 1 by going from (x, i) to (y, i + 1), and then on to (y, i + j + 1). The frame sequence ρ Z bad can be defined formally as follows. We have V = {x, y, z} and:

• {x < y < z, x < Oy, x < Oz, z > Ox, z > Oy, Ox < y < Oz, x = Ox, z = Oz} ⊆ ρ Z bad (i) for every i ≥ 0; • y > Oy ∈ ρ Z bad ( i×(i+1)
2

) for every i ≥ 0;

• y < Oy ∈ ρ Z bad (i) for every i ≥ 0 such that i = i ×(i +1) 2
for some i .

ρ Z bad clearly satisfies condition (C Z ): there are no strict forward or backward paths from any vertex in G ρ . However, note that the vertices u = (x, 0) and v = (z, 0) have unbounded strict length -i.e. slen(u, v) = ω, and hence ρ cannot admit a Z-valuation sequence.

However, when ρ is an ultimately periodic word condition (C Z ) is indeed sufficient. We say an infinite word α is ultimately periodic if it is of the form τ • δ ω for some finite words τ and δ. Lemma 6.2 Let ρ be an ultimately periodic, locally consistent, k-frame sequence. Then ρ admits a Z-valuation sequence iff ρ satisfies (C Z ).

Before we proceed with the proof, here are a few observations which can be readily verified. In what follows, ρ = τ • δ ω is an ultimately periodic, locally consistent k-frame sequence.

(1) We term a level in

G ρ a δ-boundary if it is of the form |τ | + i • |δ| for some i ∈ N. An l-suffix of G ρ , denoted G ρ [l, ∞],
is the subgraph of G ρ on the vertices V × {l, l + 1, . . .}. Let l and m be δ-boundaries in G ρ , with l < m. Then there is an isomorphism between the suffixes G ρ [l, ∞] and G ρ [m, ∞], given by (x, n) → (x, n + (ml)), where n ≥ l. Accordingly, w w v Fig. 3. Short-circuiting a backward loop we say vertices (x, n) and (x, n+i) are isomorphic if (x, n+i) is the image of (x, n) under one of the isomorphisms above (i.e. n is on or to the right of a δ-boundary, and i is a multiple of |δ|). (2) A forward path between two isomorphic vertices implies an infinite forward path in G ρ . Say there is a forward path p from u to u and u, u are isomorphic. Then u is isomorphic to a vertex u ahead of it, under the same isomorphism. Thus there is an isomorphic copy of the path p, which goes from u to u . This argument can be repeatedly used to concatenate copies of p to obtain an infinite forward path from u.

In a similar manner, a backward path between two isomorphic vertices implies an infinite backward path in G ρ .

(3) Here is a property of G ρ which holds even in the absence of periodicity.

Let p be a path from u to v in G ρ , with v at a level ahead of u. Then can obtain a forward path p from u to v in G ρ . This is done by "short-circuiting" the portions of the path p that loop backward. With reference to Fig 3, if p does not take a forward edge at a vertex w, then let w be the first vertex it visits to the right of w (if it exists). Since this edge to w is from a vertex either to the left or at the same level as w, it must be the case that w and w are in a common k-frame, and hence there must be an edge between w and w . This edge must be either an '=' or '<'-labelled edge from w to w , since otherwise G ρ would contain a strict cycle. Furthermore, if the backward loop contained a strict edge, the edge from w to w is strict.

A similar argument holds when p is a path from u to v with u ahead of v. In this case we have a backward path p from v to u.

We return now to the proof of Lemma 6.2.

Proof If ρ admits a Z-valuation sequence, then by Lemma 6.1 ρ must satisfy the condition (C Z ).

Conversely, let ρ = τ • δ ω be a locally consistent, ultimately periodic k-frame sequence. Suppose ρ does not admit a Z-valuation sequence. Then we will show that ρ fails to meet condition (C Z ). By Lemma 6.1 there must exist two vertices u and v in G ρ with slen(u, v) = ω. We will use this property to produce a picture in G ρ which violates (C Z ). Let l be a level to the right of the first δ-boundary and the vertices u and v. Let m be the level l Such a path exists because slen(u, v) = ω. Without any loss of generality we can assume p has no non-strict cycles (and hence no cycles at all), since a non-strict cycle can be eliminated without affecting the strict length of the path. Thus p never re-visits a vertex in G ρ . It now follows that there must be at least |δ| • |V | strict edges in p which occur to the right of level m. Now consider the portion p from the time it first crosses to the right of m, till the time it crosses back to the left of m for the last time. Since there are only |δ| • |V | non-isomorphic vertices to the right of m, it must be the case that this portion of the path visits two isomorphic vertices w 1 and w 2 , both to the right of m, such that w 1 is visited first, and w 2 is visited next via a strict path. Using the observation on short-circuiting a path, we can now produce a path p in G ρ that begins at u, goes to w 1 via a forward path q, then visits w 2 via a strict path r, then goes back to v via a backward path s.

+ k • |δ| • |V |. l τ δ m u w 1 w 2 w 3 w 4 q r s t t v
Two cases arise at this point: (a) w 1 is to the left of w 2 , and (b) w 1 is to the right of w 2 .

We deal with case (a) first. In this case r must be a strict forward path from w 1 to w 2 . Notice also that the backward path s spans across the levels l to m. Since an edge in s can span at most k levels, by the choice of m, s must visit two isomorphic vertices w 3 and w 4 which lie between the levels l and m. Without loss of generality we assume w 3 is to the right of w 4 . Let this backward path from w 4 to w 3 be t. Let us write the path s as s tt . This is shown in Fig. 4.

Since w 1 and w 2 are isomorphic, we have a strict forward path d from u (given by q followed by r, followed by isomorphic copies of r ad infinitum). Similarly, since w 4 and w 3 are isomorphic, we have an infinite backward (not necessarily strict) path e from v.

Further, we can assume that u and v lie in the same k-frame, since if this were not the case, with say v ahead of u, we can choose u to be any vertex along the path q that lies in the same k-frame as v. It remains now to argue that for any two vertices w on d and w on e, which are in the same k-frame, there is a strict edge from w to w . Now note that the number of levels spanned by the paths r and t are a multiple of |δ|; say k 1 • |δ| and k 2 • |δ| respectively (by isomorphism of (w 1 , w 2 ) and (w 3 , w 4 )). Let w 1 = (x, n 1 ) and w 4 = (y, n 4 ). Then the vertices (x, n 1 + ik 1 k 2 |δ|) and (y, n 4 + ik 1 k 2 |δ|), for any i, are images of w 1 and w 4 under the same isomorphism. Hence there is a strict path isomorphic to rs tt between these vertices as well.

Further, these vertices also lie on the paths d and e respectively. Now given w and w on d and e respectively, consider the next occurrence of the two isomorphic copies of w 1 and w 4 described above, to the right of both w and w (see Fig. 5). Then there is a strict path between w and w obtained by going right to the copy of w 1 , then taking the strict copy of rs tt to the copy of w 4 , and then back to w . Hence there must be a strict edge from w to w (or else we would have a strict cycle in G ρ , see Corollary 5.6).

This completes the proof that in this case there is a picture in G ρ which contradicts (C Z ).

Coming now to case (b), where we assume w 1 is to the right of w 2 . Then the path r is a strict backward path from w 2 to w 1 . Then the path p from u to v appears as shown in figure Fig. 6, with q 2 being a forward path between two isomorphic vertices. Once again this gives us an infinite forward path from u given by q 1 followed by q 2 ad infinitum, and a strict backward path from v given by s followed by r ad infinitum. Using an argument similar to case (a) above, we once again get a picture in G ρ which contradicts (C Z ).

this we conclude the proof of Lemma 6. Let B be a Büchi automaton over the alphabet of k-frames, which simply checks the negation of condition (C Z ). Thus B non-deterministically guesses the vertices u and v, and then verifies the conditions ( 1)-( 4). We non-deterministically choose in the beginning, whether to signal (via the Büchi condition) each time the d or e path sees an edge labelled '<'. Here is a more precise definition of the automaton B:

Define B = (Q, S 0 , -→, F ), over the alphabet of k-frames, where

• S 0 = {q 0 }; • Q = {q 0 } ∪ (V × {0, . . . , (k -1)} × V × {0, . . . , (k -1)} × {d, e} × {0, 1});
• -→ is given by: • q 0 v -→ q 0 • (guess (x, i) as u, and (y, j) as v, as well as which of d or e is strict) q 0 v -→ (x, i, y, j, d, 0) and q 0 v -→ (x, i, y, j, e, 0) for all x, i, y, j. • (wait till x or y is at the edge of the frame)

(x, i, y, j, f, b) v -→ (x, i -1, y, j -1, f, b) for f ∈ {d, e} and b ∈ {0, 1}, provided i, j ≥ 2. • (guess a forward edge from (x, 1)) (x, 1, y, j, d, b) v -→ (z, i, y, j -1, d, ) provided j > 1, (x, 0) < -→ (z, i) ∈ v and b = 1, or (x, 0) = -→ (z, i) ∈ v and b = 0, (z, i) < -→ (y, j -1) ∈ v.
• similarly for (y, 1), and for (x, 1) and (y, 1) simultaneously.

• similar clause for e.

• F comprises all states of the form (x, i, y, j, f, 1).

The automaton A Z

k is now just the complement of B.

Lemma 6.3 A CLTL(Z) formula ϕ is satisfiable iff L(A Z ϕ ) is non-empty.
Proof Suppose ϕ is satisfiable. Let σ be a Z-valuation sequence such that

σ |= ϕ. Let ρ = k-fs Z (σ),
where k is the O-length of ϕ. By Lemma 3.1, ρ ∈ L(A LTL ϕ ). We know that ρ is a locally consistent k-frame sequence and hence ρ ∈ L(A Z,k lc ). Further, by Lemma 6.1, G ρ satisfies (C Z ) and hence

ρ ∈ L(A Z ϕ ). Thus ρ ∈ L(A LTL ϕ ) ∩ L(A Z,k lc ) ∩ L(A Z k ). Hence ρ ∈ L(A Z ϕ ).
Conversely, suppose A Z ϕ accepts a word ρ. Then it must accept an ultimately periodic word ρ (by nature of the acceptance condition). Since ρ ∈ L(A Z ϕ ), we know that ρ is such that ρ |= LTL ϕ, ρ is locally consistent, and satisfies (C Z ). By Lemma 6.2, ρ admits a Z-valuation sequence σ. Further, since ρ |= LTL ϕ, by Lemma 3.1, σ |= ϕ. Thus ϕ is CLTL(Z) satisfiable. 2 This lets us conclude that Theorem 6. [START_REF] Bennett | Multi-dimensional modal logic as a framework for spatio-temporal reasoning[END_REF] The satisfiability problem for CLTL(Z) is decidable.

C Z + lc L LTL (ϕ) L(A Z ϕ ) ρ Z bad L Z fs (ϕ)
Fig. 7. The languages L Z fs (ϕ) and L(A Z ϕ ).

Proof Given ϕ ∈ CLTL(Z) we can effectively construct the automaton A Z ϕ and check it for emptiness. 2

The decision procedure can be shown to run in pspace. Before that, as a consequence of Lemma 6.2 and the existence of the automaton A Z ϕ , we observe that: Corollary 6.5 There are formulas ϕ in CLTL(Z) for which L Z fs (ϕ) is not ω-regular.

Proof Consider the formula ϕ = 3((x < Oy) ∧ (y < z)). We will show that L Z fs (ϕ) is not ω-regular.

Let us suppose L Z fs (ϕ) was ω-regular. Then, since ω-regular are under boolean operations,

L = ((2 atc(2,Z) ) ω -L Z fs (ϕ)) ∩ L(A Z ϕ
) is also ω-regular. This is the lightly shaded region in Fig. 7. Note that L is disjoint from L Z fs (ϕ). Now consider the frame sequence ρ Z bad of Fig. 2. ρ Z bad satisfies (C Z ) and is a locally consistent 2-frame sequence. Further it satisfies ϕ as an LTL formula (i.e. ρ Z bad |= LTL ϕ). Hence it belongs to L(A Z ϕ ). However, as observed earlier, ρ Z bad does not admit a Z-valuation sequence, and hence ρ Z bad ∈ L Z fs (ϕ). Hence ρ Z bad ∈ L.

But since L is ω-regular, there must exist an ultimately periodic word ρ in L. ρ ∈ L(A Z ϕ ) and hence is locally consistent, satisfies (C Z ), and satisfies ϕ as an LTL formula. By Lemma 6.2, ρ admits a Z-valuation sequence. Since we also have that ρ ∈ L(A LTL ϕ ), by Lemma 3.1 we must have ρ ∈ L Z fs (ϕ). But this contradicts the fact that L and L Z fs (ϕ) are disjoint. Hence L Z fs (ϕ) could not have been ω-regular. 2

Complexity of the decision procedure. We now want to argue that the satisfiability problem for CLTL(Z) can be solved in pspace. Given a CLTL(Z) formula ϕ of O-length k, we show that the decision procedure above runs in space polynomial in n = |ϕ|.

A Z ϕ C A Z k A Z,k lc A LTL ϕ B Fig. 8. A Z
ϕ and component automata

Recall that we need to check if the language accepted by the automaton

A Z ϕ = A LTL ϕ ∩ A Z,k lc ∩ A Z k , is empty.
We briefly describe the construction of the automaton A Z k . It is obtained from the automaton B above by Safra's construction [START_REF] Safra | On the complexity of ω-automata[END_REF] to complement Büchi automaton. Note that the automaton B has a number of states which is polynomial in n, say p(n). From this Safra's method constructs a deterministic Streett automaton C which accepts the complement of the language accepted by B, and has 2 O(p(n) log n) states. This automaton can then be converted to an equivalent Büchi automaton A Z k with the same order of states.

Though the automaton A Z ϕ is exponential in n (note that both component automata A Z k and A LTL ϕ are exponential in n), we can still check its nonemptiness non-deterministically in pspace in n, as argued below. Using Savitch's theorem, it then follows that its nonemptiness can be checked deterministically in pspace in n.

To argue that A Z ϕ can be checked for nonemptiness non-deterministically in pspace, we note that A Z ϕ has an implicitly defined transition relation that can be checked in pspace in n. Fig. 8 depicts the fact that the transition relation of A Z ϕ is implicitly defined in terms of the transition relations of its component automata. Each of the component automata have implicitly defined transition relations, that can be computed in pspace. For A LTL ϕ the argument is standard and can be found in [START_REF] Vardi | An automata-theoretic approach to linear temporal logic[END_REF]. For A Z k one can verify in [START_REF] Safra | On the complexity of ω-automata[END_REF] that the construction of the automata C and A Z k are indeed such that their states can be described in space polynomial in n and their transition relation can be checked in space polynomial in n.

Thus we can conclude that checking nonemptiness of the automaton A Z

ϕ can be done in pspace in n. pspace-hardness follows from that of classical LTL as in the proof of Theorem 4.5. Hence we have: Proof Suppose ρ does not admit an N-valuation. Then by Lemma 7.1 there must exist a vertex u with unbounded strict descending length. We now choose the levels l and m, and a backward path p from u of suitable strict length, as in the Z case. Once again, we must visit two isomorphic vertices w 1 and w 2 (in that order, as we go along the path in the backward direction), with both w 1 and w 2 to the right of level m, and with a strict path between them. Again, two cases arise: either w 1 is to the left of w 2 , or w 2 is the left of w 1 .

If w 1 is to the left of w 2 , then we have the situation in Fig. 10, and we have an infinite backward path from u given by q followed by r ad infinitum. This contradicts condition (C N ).

If w 2 is visited before w 1 , then the situation in Fig. 11 arises. We now have a strict infinite forward path d from w 2 given by r followed by r ad infinitum. We also have an infinite backward path e from w 3 given by q 2 repeated ad infinitum. As in the case of Z we can argue that for any two vertices w and w on d and e respectively, there is a strict edge from w to w . This picture violates (C Z ) and hence (C N ). 2

We can now define an automaton A N ϕ as in the Z case, so that the CLTL(N ) formula ϕ is satisfiable iff L(A N ϕ ) is non-empty. We can define A N ϕ to be the intersection of A Z ϕ and an automaton that rejects k-frame sequences which contain a vertex with a strict backward path from it.

In a similar manner to the Z case, we can thus conclude that:

Theorem 7.3 The satisfiability problem for CLTL(N ) is pspace-complete.
Finally, the frame sequence ρ N bad of Fig. 9 allows us to argue that there is a CLTL(N ) formula ϕ (for example x < Ox) for which L N fs (ϕ) is not ω-regular. Once again the argument is similar to the Z case.

Model-Checking

A natural model-checking problem for CLTL(D) one may study would be to consider a Kripke structure M whose states are labelled by D-valuations, and a CLTL(D) formula ϕ; and to ask if every valuation sequence generated by M satisfies ϕ. However this problem easily reduces to the classical LTL model-checking problem, since we can transform M into a Kripke structure M k labelled by k-frames (where k is the O-length of ϕ) corresponding to the k-frame induced by k-length valuation sequences in M. Whether M satisfies ϕ is now equivalent to checking whether M k satisfies ϕ as a classical LTL formula.

Hence, in this section we focus on a more interesting model-checking problem which has been proposed earlier in the literature in the context of counter automata [START_REF] Comon | Flatness is not a weakness[END_REF] (see also [START_REF] Fribourg | Concurrent constraint automata[END_REF][START_REF] Roger | Log auditing through model-checking[END_REF] and [START_REF] Revesz | Introduction to Constraint Databases[END_REF]Chap. 6]). As in the case of classical LTL, this model-checking problem will be shown to be equivalent to the satisfiability problem for the logic.

Let D be a constraint system. A D-automaton A is a Büchi automaton A over an alphabet comprising CLTL(D) formulae. Thus transitions in A are of the form q ϕ -→ q , see similar structures in [START_REF] Wolper | Temporal logic can be more expressive[END_REF]. Fig. 12 shows a N -automaton with variables {x, y, z}. q 0 q 1 q 2 q 3

x < Ox The N -automaton A in Fig. 12 is such that L vs (A) = ∅. However, if we consider it as an Z-automaton, L vs (A) contains the Z-valuation sequence 0, 0, 0 , 0, 0, 0 , -1, -1, 0 , -2, -2, 0 , -3, -3, 0 , . . .

2(x = y) (y = Oz) ∨ 3(x = O 4 x) Ox < x
The model-checking problem for CLTL(D) is defined as follows: Given a Dautomaton A and a CLTL(D) formula ϕ, is there a σ ∈ L vs (A) that σ |= ϕ? (in symbols A |= ∃ ϕ?)

Note that for convenience we have defined the existential version of the problem. The universal version of the problem can be phrased in terms of the version above. We also note that the nonemptiness problem for D-automata is a restriction of the model-checking problem for CLTL(D), by taking ϕ = .

The problems are in fact inter-reducible to each other.

We now show that the satisfiability and model-checking problems for CLTL(D) are inter-reducible. This is analogous to the situation for classical LTL.

Theorem 8.1 Let D be a non-trivial constraint system. Then the modelchecking and satisfiability problems for CLTL(D) are inter-reducible with respect to logspace transformations.

Proof Let us reduce the satisfiability problem to the model-checking problem for CLTL(D). We only need to observe that ϕ is CLTL(D) satisfiable iff A |= ∃ ϕ where A is a one-state D-automaton such that q 0 -→ q 0 and Q 0 = F = {q 0 }.

To reduce the model-checking problem to the satisfiability problem, we use the idea behind the reduction from the model-checking problem to the satisfiability problem for classical LTL from [START_REF] Sistla | The complexity of propositional linear temporal logics[END_REF]. Let A = (Q, Q 0 , F, →) be a D-automaton and ϕ be a CLTL(D) formula. By non-triviality of D, there is R of arity a such that R = ∅ or R = D a . For every state q ∈ Q, we consider an exclusive set of new variables x q 1 , . . . , x q a from Var , distinct from those in V . In that way, for each q ∈ Q, R(x q 1 , . . . , x q a ) behaves as an independent atomic formula that can be locally set to either true or false. Now, let us encode A by a CLTL(D) formula. For every q ∈ Q, let next q be the formula that encodes the successors of q:

next q def = q ψ -→q ∈δ (ψ ∧ R(Ox q 1 , . . . , Ox q a )).
Let uni be the formula stating the unicity of the current state:

uni def = q∈Q (R(x q 1 , . . . , x q a ) ∧ q ∈Q\{q}
¬R(x q 1 , . . . , x q a )).

Let ϕ A be the formula encoding the accepting runs of A:

ϕ A def = q∈Q 0 R(x q 1 , . . . , x q a ) ∧ 2uni
∧ 2( q∈Q R(x q 1 , . . . , x q a ) ⇒ next q ) ∧ 23( q∈F R(x q 1 , . . . , x q a )).

One can show that

A |= ∃ ϕ iff ϕ ∧ ϕ A is CLTL(D) satisfiable. 2
Observe that in the second part of the above proof, we use the fact that we have a countably infinite supply of variables in Var .

As a consequence of Theorem 8.1, the pspace-completeness results for the satisfiability problem carry over for the model-checking problem too. In particular, from Theorem 4.5 we get that the model-checking problem for CLTL(D) when D satisfies completion, non-triviality, and allows frame-checking in pspace (and hence for all the constraint systems in Corollary 5.4), is pspace-complete. Also, from Theorems 6.6 and 7.3 we have that the model-checking problem for Z and N are also pspace-complete.

Decidable Extensions

In this section we outline some extensions of the logic CLTL(D) for which the satisfiability and model checking problems remain decidable.

Monadic second order logic

We define a Constraint Monadic Second Order Logic, parameterized by the constraint system D, and denoted CMSO(D). Here the underlying logic is generalized from LTL to MSO [START_REF] Büchi | On a decision method in restricted second order arithmetic[END_REF].

We assume a supply of individual variables x, y, . . ., and set variables X, Y, . . .. These variables will range over positions (respectively sets of positions) of a given sequence. The syntax of CMSO(D) is given by:

ϕ ::= Q c (x) | x ∈ X | x ≺ y | ¬ϕ | (ϕ ∨ ϕ) | ∃xϕ | ∃Xϕ.
Here c is an atomic D-term constraint, and Q c is a unary predicate with the semantics below.

A structure for the logic will be a pair (σ, J) where σ is a D-valuation sequence, and J is an assignment of individual variables to a position of σ (i.e. an element of N), and set variables to a set of positions of σ. The predicate '≺' is interpreted as the usual ordering on N. The satisfaction relation σ, J |= ϕ for atomic formulas ϕ is given below.

σ, J |= Q c (x) iff σ[J(x), ∞] |= D c σ, J |= x ∈ X iff J(x) ∈ J(X) σ, J x ≺ y iff J(x) < J(y)
The operators ¬, ∨, and the existential quantifiers ∃x and ∃X are interpreted in the usual manner. In particular the quantifier ∃X is interpreted as follows. Let i ∈ N. will use the notation J[i/x] to denote the assignment which maps x to i and agrees with J on all other individual and set variables. Similarly, for a subset S of N, the notation J[S/X] will denote the interpretation which sends X to S, and agrees with J on all other variables. Then: σ, J |= ∃Xϕ iff there exists S ⊆ N such that σ, J[S/X] |= ϕ.

As an illustration, the CMSO(N ) formula ∀x Q x<Oy (x) rephrases the CLTL(N ) formula 2(x < Oy). By analogy to CLTL(D), the O-length of some CMSO(D) ϕ is the maximal O-length of D-terms occurring in unary predicates of ϕ.

Recall that classical monadic second order logic over a set of propositions P is defined similar to CMSO(D) above, except that instead of Q c we have predicates of the form Q p for each p ∈ P . A model for the logic is an ωword α over 2 P , and the formula Q p (x) is interpreted as: α, J |= MSO Q p (x) iff p ∈ α(J(x)). Just as in Lemma 3.1 it is easy to show the following result.

Adding constants

We can extend the language of constraints by allowing constants to be used, leading to term constraints of the form (Ox < 3). The model checking problem for this extension can be handled as in Sec. 8, so we focus here on the satisfiability problem. We restrict ourselves to domains of the form (D, <, =) introduced in Sec. 5, and denote the version of the logic extended with constants by CLTL con (D, <, =). For reasons of effectiveness, we assume the constants are from D ∩ Q.

Consider first the case of domains which are dense and open (or equivalently which satisfy the completion property). Let ϕ be a formula with constants K 1 , . . . , K n . Without loss of generality we assume that K

1 ∼ 1 K 2 ∼ 2 . . . ∼ n-1 K n with ∼ i ∈ {<, =}. Consider the CLTL(R, <, =) formula ϕ : ϕ[K 1 ← y 1 , . . . , K n ← y n ] ∧ n-1 i=1 (y i ∼ i y i+1 ) ∧ 2( n i=1 y i = Oy i )
where y 1 , . . . , y n are new variables not occurring in ϕ and K i ← y i denotes the operation of replacing every occurrence of K i by y i . ϕ is now satisfiable iff ϕ is. To see this, note that if ϕ is satisfiable, the same valuation extended by labelling y i 's by K i 's satisfies ϕ . Conversely, given a D valuation sequence σ which satisfies ϕ , we can re-label the variables y 1 , . . . , y n with K 1 , . . . , K n , and repeatedly use the completion property to label the remaining variables so that we get an edge-respecting labelling of the underlying frame sequence. This gives us a valuation sequence which satisfies ϕ. We now consider CLTL con (Z). Once again we can reduce the satisfiability for CLTL con (Z) to that of CLTL(Z). Let ϕ be a CLTL con (Z) formula, and let m and M be respectively the minimum and maximum constants used in ϕ. Let x m , x m+1 , . . . , x M be new variables that do not occur in voc(ϕ). Consider the CLTL(Z) formula ϕ which is the conjunction of:

(1) ϕ[m ← x m , . . . , M ← x M ] (2) 2 M i=m (x i = Ox i ) (3) (x m < . . . < x M ) (4) y∈voc(ϕ) 2((y < x m ) ∨ (y > x M ) ∨ (y = x m ) ∨ . . . ∨ (y = x M )).
The claim is now that ϕ is satisfiable iff ϕ is. Given a model for ϕ we can extend it to a model for ϕ by assigning the value K to x K for each K between m and M . Conversely, consider a model σ for ϕ . Then σ may not be a model for ϕ for two reasons: first, the values assigned to x m , . . . , x M may not be contiguous, and secondly, they may not begin at m. The first problem can be taken care of by observing that the values assigned to x m , . . . , x M in σ can be "compressed" without contradicting the formula. Thus, if d m , . . . , d M were the values assigned to x m , . . . , x M in σ, then we relabel all vertices which are labelled with these values, by the values d m , d m + 1, . . . , d m + (Mm) respectively. Clause 4 of the formula ensures that this is still a model of the formula. It is now easy to see that the values of all vertices can be shifted down uniformly by the value (d mm) to get a model for ϕ and hence also for ϕ.

Assuming a binary encoding for the constants, the size of ϕ can be exponential in ϕ. Hence we have: Corollary 9.4 The satisfiability problem for CLTL con (Z, <, =) is solvable in expspace.

Few remarks about the logic CLTL con (Z, <, =) are in order.

(1) We conjectured in [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF][START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF] that satisfiability for CLTL con (Z, <, =) is indeed still in pspace. By an appropriate extension of the notion of symbolic models, we have shown in [START_REF] Demri | Verification of qualitative Z-constraints[END_REF] that it is the case. (2) We note that the satisfiability problem for CLTL(N ) and CLTL con (N ) can be reduced to that of CLTL con (Z) by adding the constraint

2( x∈voc(ϕ) (x > 0)).
Thus this gives us an alternate solution to the satisfiability problem for CLTL(N ) and provides a pspace upper bound. (3) A CTL variant of CLTL con (Z, <, =) is known to be undecidable [20, Theorem 1] and our complexity upper bound in Corollary 9.4 refines results in [START_REF] Čerans | Deciding properties of integral relational automata[END_REF].

Other extensions

The satisfiability results of this paper can be easily extended to handle the past-time operators O -1 (previous) and S (since) in the temporal language. Indeed, since we use automata-based techniques, the treatment of LTL with those past-time operators from [START_REF] Markey | Temporal logic with forgettable past[END_REF] can be used in our framework to obtain a pspace upper bound. This answers an open question from [START_REF] Balbiani | Computational complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning[END_REF].

Actually, for any extension L of LTL obtained by adding a finite amount of MSO-definable temporal operators, one can show that L(D) satisfiability is in pspace as soon as D satisfies completion, non-triviality, and allows frame-checking in pspace. Indeed, instead of considering the Büchi automaton A LTL ϕ , one builds the automaton A L ϕ based on the developments in [START_REF] Gastin | Satisfiability and model checking for MSO-definable temporal logics are in PSPACE[END_REF].

Undecidable Extensions

As seen in the previous section, the decidability results from Secs. 4-7 are quite robust when the logical language is enriched. However, adding even basic quantitative relations (like = +1 ) to the constraint system quickly leads to undecidability.

More generally, we define below three abstract conditions for a constraint system to admit implicitly a counting mechanism which leads to undecidability.

A constraint system D is said to admit an implicit counting mechanism if the following conditions are met:

(1) D contains the equality predicate,

(i.e. d R -→ f 1 (d) R -→ . . . f i (d) R -→ . . .) is isomorphic to (N, <).
For every D ∈ {N, Z, Q, R} and for every i ∈ D \ {0}, the constraint system (D, =, = +i ) has an implicit counting mechanism, where n = +i n iff n = n + i.

Similarly, the constraint system (D \ {0}, =, = ×i ) admits an implicit counting mechanism where n = ×i n iff n = n × i with i = -1, A nondeterministic 2-counter machines consists of two counters C 0 and C 1 , and a sequence of n instructions. The lth instruction is either of the form • add l, C i , l , l meaning "add 1 to the counter C i and go to either instruction l or instruction l " or of the form • sub l, C i , l , l meaning "if C i = 0, then subtract 1 from the counter C i and go to the instruction l , otherwise go to the instruction l ".

A configuration is a triple ic, n 0 , n 1 ∈ {1, . . . , n} × N × N where ic is the instruction counter and n i is the value of the counter C i . A computation is an infinite sequence of configurations starting at the initial configuration 1, 0, 0 and such that two successive configurations are admissible according to the instructions of the machine. A computation is recurring iff it contains infinitely many configurations with the value counter being 1 (Büchi acceptance condition).

In order to encode the configurations, we shall use the variables ic, n 1 , and n 2 . However, since D does not necessarily have constant values, we shall introduce additional variables with constant values throughout the models:

• It remains to specify how the values of the current configurations evolve along the ω-sequence of states. We need to specify how to encode the relationships between two successive configurations. For each instruction l, we will define a formula ψ l that specifies its effects on the instruction counter and on the counters. For instance, adding one to a counter C i will be encoded by the atomic formula R(n i , On i ).

If the lth instruction is of the form add l, C i , l , l , the formula µ l is defined as follows: Similarly, if the lth instruction is of the form sub l, C i , l , l , the formula µ l is defined as follows:

( It remains to express that a computation is recurring with the formula ϕ rec below: 23(ic = d 1 ). We define the final formula ϕ M to be the formula below:

C i =0 ¬(n i = d n+1+i ) ⇒
ϕ inst ∧ ϕ init-c ∧ ∧ϕ rec ∧ 2( 1≤l≤n ((ic = d l ) ⇒ µ l )).
Using the fact that D has an implicit counting mechanism, it is easy to see that M has a recurring computation iff ϕ M is CLTL(D) satisfiable. 2 Corollary 10.2 For each D ∈ {N, Z, Q, Q + R, R + } and for every i ∈ D \ {0}, satisfiability for CLTL(D, =, = +i ) is undecidable.

The above Σ 1 1 -hardness results implies that CLTL(D) is not recursively enumerable and therefore there cannot be complete proof systems for it.

A slight adaptation of the proof of Theorem 10.1 allows us to show the following result. Proof The only difference with the proof of Theorem 10.1 is that we have to enforce that d n+1 and d n+2 are not equal to zero which can be expressed by the formula ¬(d n+1 = ×i d n+1 ) ∧ ¬(d n+2 = ×i d n+2 ). 2 Finally, we show that Theorem 10.1 holds even when we restrict ourselves to just two variables. This follows from the general result below. Lemma 10.4 Let D = (D, =, . . .) be a concrete domain equipped with equality. Then CLTL(D)-satisfiability can be reduced in logarithmic space to CLTL(D)satisfiability restricted to formulas with at most two variables.

Proof Let ϕ be a CLTL(D) formula of O-length m with variables x 1 , . . . , x n for some n ≥ 3. We set M = n × m. We shall build a CLTL(D) formula ϕ (in logarithmic space in |ϕ|) such that ϕ is CLTL(D) satisfiable iff ϕ is CLTL(D) satisfiable.

If D is a singleton, every variable in ϕ can be replaced by x leading to ϕ . In the sequel, we assume that D has at least two elements.

A sequence v 0 , . . . , v m-1 of valuations of the form {x 1 , . . . , x n } → D, viewed as a sequence of m states in a model for ϕ, will be encoded by M successive valuations u 1 , . . . , u M over {x, y} such that • for every 1 ≤ i ≤ M , u i (x) = v j (x k+1 ) where j and k are such that i = j × n + k and k < n. • u 1 (y) = u 1 (x) and for every 2 ≤ i ≤ M , u i (y) = u i (x).

The second variable y has a unique function: to be able to count the positions of the states modulo M with the satisfiability of the atomic constraint x = y. The first formula that we consider allows us to access states whose positions are multiple of M . Basically, the first states of n × m states sequences are exactly the states satisfying x = y. The formula ϕ mult does the job:

ϕ mult def = (x = y) ∧ 1≤i≤M -1 ¬(O i x = O i y) ∧ 2(x = y ⇔ O M x = O M y).
Indeed, we have σ |= ϕ mult iff for all i, (σ[i, ∞] |= x = y iff i = 0 mod M ). The formula ϕ shift below states that for 2 × M consecutive valuations over {x, y} u 1 , . . . , u M , u 1 , . . . , u M , u n+1 , . . . , u M = u 1 , . . . , u M -n :

2(x = y ⇒ M -n i=1 O n+i x = O M +i x)
We now define the map t from subformulas of ϕ to formulas over {x, y}:

• t is homomorphic with respect to the Boolean operators; • t(R(O j 1 x i 1 , . . . , O j α x i α )) = R(O (j 1 -1)×n+i 1 x, . . . , O (j α -1)×n+i α x); • t(Oψ) = O(¬(x = y)U ((x = y) ∧ t(ψ))); • t(ψU µ) = ((x = y) ⇒ t(ψ))U ((x = y) ∧ t(µ)). Now one can easily show that ϕ is CLTL(D) satisfiable iff ϕ mult ∧ t(ϕ) is CLTL(D) satisfiable. 2

When only one variable is involved, undecidability can still be established following [START_REF] Demri | The effects of bounding syntactic resources on Presburger LTL[END_REF].

Conclusion

We have studied some natural satisfiability and model-checking problems related to a simple constraint temporal logic. The technique used in this pa-per is automata-theoretic and its novelty lies in its applicability in the face non-regularity of the set of models described by formulas in the logics. The automata-theoretic approach also leads to transparent generalizations of the techniques for some extensions of the logic.

Among the issues we have not paid much attention to are applications of these results, particularly in the area of automated program verification. For example one could consider model-checking properties of finitely presented infinite state programs like timed automata [START_REF] Alur | A theory of timed automata[END_REF] (where clocks can be modelled as real-valued variables) or integer-valued programs [START_REF] Müller-Olm | Computing interprocedurally valid relations in affine programs[END_REF]. Another application one could investigate would be in the area of program synthesis. As mentioned in the the introduction, the developed here can in principle be used to synthesize programs satisfying a given CLTL specification.

Another interesting problem we would like to investigate is the decidability of the logic when we allow more expressive quantifiers like y = 3x expressing that some future value of x is equal to the current value of y. These quantifiers are related to the "freeze quantifiers" used in some real-time logics [START_REF] Alur | A really temporal logic[END_REF] (see also recent developments in [START_REF] Demri | On the freeze quantifier in constraint LTL: decidability and complexity[END_REF][START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF]), and one may be able to exploit the techniques used there.

  x 1 , . . . , x a ∈ U , and n 1 , . . . , n a ∈ N. Here O i stands for the juxtaposition of the next-state operator O i times, with O 0 x representing just x. A Dterm constraint is interpreted over a sequence of D-valuations. A D-valuation sequence over a set of variables U is an infinite sequence σ of D-valuations over U . We say a D-valuation sequence σ over U satisfies a D-term constraint c = R(O n 1 x 1 , . . . , O n a x a ) over U , written σ |= D c, iff (σ(n 1 )(x 1 ), . . . , σ(n a )(x a )) ∈ I(R).

Corollary 4 . 1 A

 41 CLTL(D) formula ϕ of O-length k is satisfiable iff there exists a locally consistent k-frame sequence which (symbolically) satisfies ϕ as a classical LTL formula, and which admits a D-valuation sequence, i.e. a concrete model.

Lemma 4 . 3

 43 Let D be a constraint system satisfying the completion property. Let ϕ be a CLTL(D) formula. Then L D fs (ϕ) is ω-regular.

Theorem 4 . 4 (

 44 [START_REF] Balbiani | Computational complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning[END_REF]) The satisfiability problem for CLTL(D) when D satisfies completion and allows frame-checking in pspace, is in pspace. 2

Theorem 4 . 5

 45 The satisfiability problem for CLTL(D) when D is non-trivial, satisfies completion, and allows frame-checking in pspace, is pspace-complete. 2Examples of constraint systems satisfying the completion property can be found in Corollary 5.4 (including (R, <, =), (Q, <, =) and (D, =) for any infinite set D).5 Domains of the form (D, <, =)

Fig. 1 .

 1 Fig. 1. A 3-frame sequence over the variables {x, y}

Lemma 5 . 2 A

 52 locally consistent k-frame sequence ρ admits a D-valuation sequence σ iff σ is an edge-respecting D-labelling of G ρ . We now show that the completion property for domains of the form (D, <, =) is strongly related to denseness of the domain. As usual we say D is dense (with respect to the ordering <) if for each d, d in D with d < d , there exists d in D, such that d < d < d . We say D is open iff for each d ∈ D, there exist d , d ∈ D with d < d < d . Lemma 5.3 Let D be a constraint system of the form (D, <, =) where D is infinite and < is a total order. Then, D satisfies completion iff D is dense and open.Proof We will make use of the representation of frames as graphs here.Let D satisfy completion. Then D must be dense and open. To see this consider the frame X = {x < y, y < z, x < z}, over the variables U = {x, y, z} (we have suppressed the mention of the identity constraints x = x etc, for brevity). Let d, d ∈ D with d < d . Then the labelling l over U = {x, z} given by

( 2 )

 2 (D, <, =) where D is any dense open subset of R. (3) (D n , ≺, =) for n ≥ 1, and D ∈ {Q, R}, where ≺ is for instance a lexicographical ordering based on (D, <, =). (4) (D, =) for any infinite set D. 2 It now follows from Theorem 4.5 that: Corollary 5.5 The satisfiability problem for CLTL(D) for each of the constraint systems D in Corollary 5.4 (in particular (R, <, =)) is pspace-complete. 2

Fig. 2 .

 2 Fig. 2. ρ Z bad satisfies (C Z ) but does not admit a Z-valuation sequence.

Fig. 4 .

 4 Fig. 4. The path p for case (a) Now consider a u-v path p with

Fig. 5 . 2 vFig. 6 .

 526 Fig. 5. Strict edge from w to w

2 . 2

 22 Now let ϕ be the given CLTL(Z) formula. Let k be the O-length of ϕ. Let us defineA Z ϕ = A LTL ϕ ∩ A Z,k lc ∩ A Z k , where A LTLϕ and A Z,k lc are as in Sec. 4, and A Z k -described below -accepts k-frame sequences which satisfy (C Z ).

Theorem 6 . 6

 66 The satisfiability problem for CLTL(Z) is pspace-complete.

Fig. 10 . 2 Fig. 11 .

 10211 Fig. 10. The case (a)

Fig. 12 .

 12 Fig. 12. An example of a D-automaton

Lemma 9 . 1 Theorem 9 . 2

 9192 Let ϕ be an CMSO(D) formula of O-length k. Let σ be a Dvaluation sequence, and let ρ = k-fs D (σ). Then σ |= ϕ iff ρ |= MSO ϕ. 2 Using Büchi's well-known result that for every classical MSO formula we can construct a Büchi automaton A MSO ϕ which accepts precisely the models of ϕ, we can now follow the same route as in the previous sections to conclude that: The satisfiability (and model-checking) problem for CMSO(D) is decidable for D = N , Z, and for any D which satisfies completion, nontriviality, and has a decidable frame checking problem. 2

Corollary 9 . 3

 93 The satisfiability problem for CLTL con (D, <, =) when D is dense and open, is solvable in pspace.

  D contains a binary relation R such that (a) R = {(x, y) ∈ D 2 : f (x) = y} for some injective map f : D → D, (b) (D, R) is a DAG.Observe that for any d in D, the set {f i (d) : i ∈ N} with the relation R

  d 1 , . . . , d n to encode the n different possible values of the instruction counter; • d n+1 and d n+2 the initial values of the counters C 0 and C 1 , respectively. Now, we define a formula that enforces that the interpretation of d 1 , . . . , d n are distinct and constant throughout the model. The formula ϕ inst does the job:ϕ inst def = d 1 ,...,d n are distinct 1≤i<j≤n (¬(d i = d j )) ∧2( 1≤i≤n d i = Od i ).In a similar way, we define a formula that enforces that d n+1 and d n+2 are constant values. The formula ϕ init-c does the job:ϕ init-c def = 2(d n+1 = Od n+1 ∧ d n+2 = Od n+2 ).Observe that for these values of the counters, we do not require that d n+1 = d n+2 . Now we define a formula stating what is the first instruction counter and what are the initial values of the counters: ϕ init def = (ic = d 1 ) ∧ (n 0 = d n+1 ) ∧ (n 1 = d n+2 ).

go to either l or l (

 l (d l = Oic) ∨ (d l = Oic)) ∧ add 1 to C i R(n i , On i ) ∧ C 1-i does not change (On 1-i = n 1-i ) .

  go to l (d l = Oic) ∧ sub 1 from C i R(On i , n i ) ∧ C 1-i does not change (On 1-i = n 1-i ) ) ∧( C i =0 (n i = d n+1+i ) ⇒ go to l (d l = Oic) ∧ C 0 does not change (On 0 = n 0 ) ∧ C 1 does not change (On 1 = n 1 ) ).

Corollary 10 . 3

 103 For every D ∈ {N, Z, Q, Q + , R, R + } and for every i ∈ D \ {0, 1, -1}, satisfiability CLTL(D, =, = ×i ) is undecidable.

7 Satisfiability for CLTL(N, <, =)

In this section we outline a decision procedure for the satisfiability problem for CLTL over the constraint system N = (N, <, =). The decidability of this logic actually follows from the fact that CLTL(Z) extended with constants is decidable (cf. Sec. 9). However for reasons of independent interest, we sketch a decision procedure for this logic, which in fact is very much along the lines of the one for CLTL(Z) in the previous section. It is hoped that this will emphasize the fact that a simple-minded approach to rule out infinite backward chains will not work, and further that the languages corresponding to these formulas could in fact be non-ω-regular.

We begin with a notion similar to that of slen in the previous section. For a vertex u in G ρ , we define sdlen(u) to be the supremum of slen(p) over directed paths p from some vertex v to u in G ρ .

Lemma 7.1 Let ρ be a locally consistent k-frame sequence. Then ρ admits an N-valuation sequence iff for all u ∈ G ρ , sdlen(u) < ω.

Proof If ρ admits an N-valuation σ, then clearly sdlen(u) ≤ l(u), where l is the N-labelling of G ρ corresponding to σ. Thus, there cannot exist a vertex u with sdlen(u) = ω.

Conversely, if G ρ satisfies the given condition, then one can verify that the N labelling l given by l(u) = sdlen(u) is an edge-respecting labelling of G ρ . Hence ρ admits an N-valuation. 2

Let (C N ) denote the following condition on a locally consistent k-frame sequence ρ: G ρ satisfies (C Z ) and it does not contain a strict backward path.

Condition (C N ) is once again necessary but not sufficient to ensure that a locally consistent k-frame sequence admits an N-valuation sequence. One can see that it is not sufficient by considering the 2-frame sequence ρ N bad of Fig. 9. It clearly satisfies condition (C N ), but does not admit an N-valuation sequence because the vertex u = (y, 0) is such that sdlen(u) = ω.

However, we can assert that: Lemma 7.2 Let ρ be an ultimately periodic, locally consistent, k-frame sequence. Then ρ admits an N-valuation sequence iff ρ satisfies (C N ).