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

LTL over Integer Periodicity Constraints

Keywords: Presburger LTL, periodicity constraints, computational complexity, Büchi automaton, QBF

Periodicity constraints are used in many logical formalisms, in fragments of Presburger LTL, in calendar logics, and in logics for access control, to quote a few examples. In the paper, we introduce the logic PLTL mod , an extension of Linear-Time Temporal Logic LTL with past-time operators whose atomic formulae are defined from a first-order constraint language dealing with periodicity. Although the underlying constraint language is a fragment of Presburger arithmetic shown to admit a pspace-complete satisfiability problem, we establish that PLTL mod model-checking and satisfiability problems remain in pspace as plain LTL (full Presburger LTL is known to be highly undecidable). This is particularly interesting for dealing with periodicity constraints since the language of PLTL mod has a language more concise than existing languages and the temporalization of our first-order language of periodicity constraints has the same worst case complexity as the underlying constraint language. Finally, we show examples of introduction the quantification in the logical language that provide to PLTL mod , expspacecomplete problems. As another application, we establish that the equivalence problem for extended single-string automata, known to express the equality of time granularities, is pspace-complete by designing a reduction from QBF and by using our results for PLTL mod .

Introduction

Presburger Constraints. Presburger constraints (see e.g., [START_REF] Presburger | Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt[END_REF]) are present in many logical formalisms including extensions of Linear-Time Logic LTL. We quote below some examples:

-Timed Propositional Temporal Logic(s) [START_REF] Alur | A really temporal logic[END_REF], -CTL* dedicated to automata with variables interpreted in Z [ Čer94], -Constrained LTL named CLTL defined with LTL models but with Presburger occurrences constraints [START_REF] Bouajjani | On the verification problem of nonregular properties for nonregular processes[END_REF], -Flat fragment of Presburger LTL [START_REF] Comon | Flatness is not a weakness[END_REF] (see also [START_REF] Comon | Multiple counters automata, safety analysis and Presburger arithmetic[END_REF]).

Other formalisms more dedicated to formal verification can be found in -model-checking of (discrete) timed automata [START_REF] Choffrut | Timed automata with periodicity clock constraints[END_REF][START_REF] Dang | Presburger liveness verification of discrete timed automata[END_REF], -verification of infinite-state systems with linear arithmetic constraints, see e.g. [BH99,WB00,Wol01,FS00,FL02,BB03].

In the paper, we are interested in models of Presburger LTL that are ωsequences of valuations for a given set VAR of integer variables taking their values in Z and the atomic formulae are Presburger arithmetic constraints with free variables in VAR (the models in [START_REF] Bouajjani | On the verification problem of nonregular properties for nonregular processes[END_REF] are quite different since they are just plain LTL models). For instance, φ = 2(Xx = x) states that the value of the variable x is constant over the time line where Xx denotes the value of x at the next state. A model of φ is simply an ω-sequence in (Z) ω . The counterpart of the highly expressive power of Presburger LTL rests on its Σ 1 1 -completeness, shown by a standard encoding of the recurrence problem for nondeterministic two-counter machines. However, to regain decidability one can either restrict the underlying constraint language, see e.g. [START_REF] Alur | A really temporal logic[END_REF]Sect. 3] and [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF], or restrict the logical language, see e.g. a decidable flat fragment of Presburger LTL in [START_REF] Comon | Flatness is not a weakness[END_REF]. Herein, we shall consider versions of LTL with Presburger constraints with the full logical language (mainly LTL with past-time operators sometimes augmented with first-order quantifiers) but with strict fragments of Presburger arithmetic. As a consequence, all the constraint languages we will consider are closed under Boolean operations.

Our motivations. Integer periodicity constraints, a special class of Presburger constraints, have found applications in many logical formalisms such as -DATALOG with integer periodicity constraints [START_REF] Toman | DATALOG with integer periodicity constraints[END_REF], -logical formalisms dealing with calendars, see e.g. [Ohl94,Wij00,CFP02], -temporal reasoning in database access control [START_REF] Bertino | Supporting periodic authorizations and temporal reasoning in database access control[END_REF][START_REF] Bertino | An access control model supporting periodicity constraints and temporal reasoning[END_REF], -periodic time in generalized databases, see e.g. [START_REF] Wolper | Representing periodic temporal information with automata[END_REF][START_REF] Niezette | An efficient symbolic representation of periodic time[END_REF].

Moreover, abstracting programs with integer variables by constraint automata with periodicity constraints can be viewed as a way to handle the analysis of such programs. Although we will not elaborate on it in this paper, we believe it is a promising continuation of the current paper, in the line of [START_REF] Müller-Olm | Program analysis through linear algebra[END_REF] for instance. In view of the ubiquity of integer periodic constraints, the main motivation of the current work is to design a variant of LTL over a language for integer periodicity constraints that satisfies the following properties.

1. The logical language contains at least LTL (no flatness restriction). 2. The constrained language is expressive enough to capture most integer periodicity constraints used in calendar logics and in database access control. For instance, in [START_REF] Combi | A logical approach to represent and reason about calendars[END_REF], the authors advocate the need to design an extension of LTL that expresses quantitative temporal requirements, such as periodicity constraints. We provide in the paper such an extension. 3. Model-checking and satisfiability remain in pspace. For this new extension of LTL, we would like also to adapt the technique from [START_REF] Vardi | Reasoning about infinite computations[END_REF] that has been so successful in the past.

Last but not least, as a long-term project, we wish to understand what are the decidable fragments of Presburger LTL by restricting the constraint language but with the full logical language.

Our contribution. We introduce a decidable fragment of Presburger LTL that satisfies the above-mentioned requirements. Let us be a bit more precise.

1. We introduce a first-order theory of integer periodicity constraints IPC ++ and we show its pspace-completeness. This is a fragment of Presburger arithmetic that extends the one from [START_REF] Toman | DATALOG with integer periodicity constraints[END_REF]. 2. We show the pspace-completeness of PLTL (LTL with past-time operators) over IPC ++ using Büchi automata (logic denoted by PLTL mod in the paper) along the lines of [START_REF] Vardi | Reasoning about infinite computations[END_REF]. 3. We demonstrate why adding the existential operator ∃ [resp. the freeze oper-

ator ↓] at the logical level (∃ is already present at the constraint level) leads to an exponential blow-up of the complexity. IPC + is a fragment of IPC ++ without constraints of the form x = y. We show that PLTL over IPC + constraints but augmented with ∃ [resp. with ↓] is expspace-complete.

It is difficult to get tighter decidability results in view of the recent results [START_REF] Demri | On the freeze quantifier in constraint LTL: decidability and complexity[END_REF][START_REF] Lisitsa | Temporal logic with predicate λ-abstraction[END_REF]. 4. As an application, we show the pspace-completeness of the equivalence problem for the extended single-string automata [START_REF] Lago | Calendars, time granularities, and automata[END_REF]Sect. 5]. Extended singlestring automata are Büchi automata that recognize exactly one ω-word and guards involving periodicity constraints are present on the transitions. This formalism has been introduced as a concise means to define time granularities and the equivalence problem for such automata is central to check the equality of time granularities, see also [START_REF] Wijsen | A string based-model for infinite granularities[END_REF]. Roughly speaking, a time granularity is a mapping from integer numbers to subsets of a time domain.

Related work. Apart from the above-mentioned works dealing with (fragments of) Presburger LTL, we list below some related works involving periodicity constraints, fragments of Presburger arithmetic, versions of LTL over concrete domains, and constraint automata.

1. In [START_REF] Toman | DATALOG with integer periodicity constraints[END_REF] a version of DATALOG with integer periodicity constraints is studied. Our constraint language extends the one from [START_REF] Toman | DATALOG with integer periodicity constraints[END_REF] but is used in a different way since it serves as a basis for the atomic formulae of our studied fragment of Presburger LTL. Similar periodicity constraints can be found in [START_REF] Bertino | Supporting periodic authorizations and temporal reasoning in database access control[END_REF][START_REF] Bertino | An access control model supporting periodicity constraints and temporal reasoning[END_REF]. 2. Complexity issues for versions of LTL over concrete domains have been studied in [BC02,DD03,GKWZ03,GKK + 03] (see also [START_REF] Lutz | Interval-based temporal reasoning with general TBoxes[END_REF][START_REF] Lutz | NEXPTIME-complete description logics with concrete domains[END_REF]). Unlike most of these works, we use a computationally expensive constraint language (satisfiability is pspace-complete) while preserving the pspace upper bound of the corresponding fragment of Presburger LTL. 3. Various fragments of Presburger arithmetic have been introduced in the literature, very often for quite different purposes. By way of example, let us mention the pspace-complete fragment of Presburger arithmetic introduced in [START_REF] Koubarakis | Complexity results for first-order theories of temporal constraints[END_REF] with quantifier elimination. OCP "One counter Properties" [START_REF] Jančar | Equivalence-checking with one-counter automata: a generic method for proving lower bounds[END_REF] is also a fragment of Presburger arithmetic that is DP-hard (see e.g. [START_REF] Ch | Computational Complexity[END_REF]), and in Π p 2 (level 2 of polynomial hierarchy). A peculiarity of OCP is that it lacks the closure under negation. 4. Constraint automata similar to the one we shall consider in this paper are introduced in [START_REF] Lago | Calendars, time granularities, and automata[END_REF] (extended single-string automata). The underlying constraint language L I from [START_REF] Lago | Calendars, time granularities, and automata[END_REF] is actually a fragment of the language IPC + (see Sect. 6 for more details). Decidability of the equivalence problem between two such constraint automata is shown in [START_REF] Lago | Calendars, time granularities, and automata[END_REF] by using an exponential space decision procedure. We shall explain why the extended single-string automata can be viewed as a subclass of LTL(IPC + )-automata (defined in Sect. 2.4). 5. First-order temporal logics of actions such as TLA [START_REF] Lamport | The temporal logic of actions[END_REF] (see also extensions in [START_REF] Merz | A more complete TLA[END_REF][START_REF] Estrin | The expressive power of temporal logic of actions[END_REF]) can be viewed as variants of LTL over concrete domains in which the domain is not fixed.

Plan of the paper. The rest of the paper is structured as follows. In Sect. 2 we introduce fragments of Presburger arithmetic involving periodicity constraints and the corresponding versions of LTL with past defined upon them. Sect. 3 is dedicated to the most expressive constraint language considered in the paper, namely IPC ++ . We show that IPC ++ admits quantifier elimination in polynomial space, satisfiability is pspace-complete and we provide a symbolic representation for solutions of IPC ++ constraints. In Sect. 4 we show that the satisfiability and model-checking problems for our main logic PLTL mod are pspace-complete problems by taking advantage of results from Sect. 3 to abstract PLTL mod models of a given PLTL mod formula. These problems are reduced to the emptiness problem for Büchi automata. Sect. 5 analyses the complexity of the logic PLTL(IPC + ), a fragment of PLTL mod , augmented with the quantifier ∃ [resp. with ↓] at the logical level. We show that PLTL(IPC + ) augmented with ∃ [resp. with ↓] has an expspace-complete satisfiability problem. Sect. 6 presents the proof of the pspace-completeness of the equivalence problem for extended single-string automata. In Sect. 7, we provide concluding remarks.

This paper is a completed version of [START_REF] Demri | LTL over integer periodicity constraints (extended abstract)[END_REF].

PLTL over periodicity constraints

Constraint languages

Let VAR = {x 0 , x 1 , . . .} be a countably infinite set of variables. We define below languages of the first-order theory of integer periodicity constraints. The constraint language IPC is defined by the grammar below:

p ::= x ≡ k y + c | x ≡ k c | p ∧ p | ¬p,
where k, c ∈ N, x, y ∈ VAR. A simple periodicity constraint is a conjunction of constraints of the form either x ≡ k y + c or x ≡ k c for some k, c ∈ N and x ∈ VAR. Given X ⊆ {∃, [], <, =}, we define an extension of IPC, namely IPC X , by adding clauses to the definition of IPC:

-if ∃ ∈ X, then the clause ∃ x p is added (existential quantification), -if [] ∈ X, then the clause x ≡ k y + [c 1 , c 2 ] with c 1 , c 2 ∈ N is added, -if =∈ X, then the clause x = y with x, y ∈ VAR is added, -if <∈ X, then the clauses x < d | x > d | x = d with x ∈ VAR and d ∈ Z are added.
Below, IPC + denotes IPC {∃,[],<} whereas IPC ++ denotes IPC {∃,[],<,=} , which is actually the richest constraint language considered in the paper. IPC ++ is the extension of the language of the first-order theory of integer periodicity constraints introduced in [TC98]1 but with the inclusion of negation as considered in [START_REF] Bertino | Supporting periodic authorizations and temporal reasoning in database access control[END_REF]. Unlike [START_REF] Toman | DATALOG with integer periodicity constraints[END_REF], we shall not use periodicity graphs as symbolic representation of sets of tuples definable by constraints in IPC (see also the complementation of periodicity graphs in [START_REF] Bertino | Supporting periodic authorizations and temporal reasoning in database access control[END_REF]). Instead, we shall represent periodicity constraints by sets of triples of natural numbers. The cardinality of such sets will be exponential in the size of the corresponding constraints (see details in Sect. 3).

Observe that constraints of the form x ∼ d with ∼∈ {=, >, <} allow to compare variables to absolute time values. A semi-simple periodicity constraint is a conjunction between a simple periodicity constraint and a conjunction of atomic constraints of the form x ∼ d with ∼∈ {<, >, =}.

The interpretation of the constraints is the standard one. A valuation v is a map v : VAR → Z. The satisfaction relation v |= p is inductively defined in Figure 1. It is worth observing that x ≡ k y + [c 1 , c 2 ] is not symmetrical with respect to x and y. However,

-v |= x ∼ d def ⇔ v(x) ∼ d with ∼∈ {<, >, =}, v |= x = y def ⇔ v(x) = v(y), -v |= x ≡ k c def ⇔ v(x) is equal to c modulo k, i.e. there is z ∈ Z such that v(x) - v(y) = z × k + c, -v |= x ≡ k y + c def ⇔ v(x) -v(y) is equal to c modulo k, -v |= x ≡ k y + [c 1 , c 2 ] def ⇔ v(x) -v(y) is equal to c modulo k for some c 1 ≤ c ≤ c 2 , -v |= p ∧ p def ⇔ v |= p and v |= p , v |= ¬p def ⇔ not v |= p, -v |= ∃ x p def ⇔ there is z ∈ Z such that v[x ← z] |= p where v[x ← z](x ) = v(x ) if x = x, and v[x ← z](x) = z.
y ≡ k x + [c 1 , c 2 ] is equivalent to x ≡ k y + [k -c 2 , k -c 1 ].
Given p in IPC ++ with free variables x 1 , . . . , x k (in the order of enumeration of the variables), sol(p) denotes the set of k-tuples z 1 , . . . , z k ∈ Z k such that [x 1 ← z 1 , . . . , x k ← z k ] |= p. sol(p) is a semilinear set of k-tuples since IPC ++ is obviously a fragment of Presburger arithmetic [START_REF] Ginsburg | Semigroups, Presburger formulas and languages[END_REF]. Given a constraint language L, the L-satisfiability problem is to decide given a constraint p ∈ L whether sol(p) is non-empty. Without any loss of generality, we can assume that p contains at least one free variable (otherwise consider (x 1 ≡ 1 0) ∧ p and x 1 does not occur in p), if ∃x 1 p 1 and ∃x 2 p 2 are distinct subconstraints of p, then x 1 is distinct from x 2 and, in p a variable cannot occur both free and bounded.

The expressive power of a constraint language L can be measured by the set {sol(p) : p ∈ L}. For instance, IPC {∃,<} is as expressive as

IPC + since x ≡ k y + [c 1 , c 2 ] is equivalent to c 1 ≤c≤c 2 x ≡ k y + c.
However, because all the natural numbers are encoded with a binary representation, IPC + may be more concise than IPC {∃,<} . The introduction of the succinct atomic constraints of the form x ≡ k y + [c 1 , c 2 ] is motivated by the existence of similar constraints in the calendar logic developed in [START_REF] Ohlbach | Calendar logic[END_REF].

Definition of PLTL mod

The atomic formulae of PLTL mod are the constraints of IPC ++ except that the variables are of the form X j x i . A term X j x i , the variable x i followed by j "X" symbols, represents the value of x i at the jth next state and its size is in O(j + log i). The atomic formulae of PLTL mod are expressions of the form

p[x 1 ← X i 1 x j 1 , . . . , x k ← X i k x j k ]
where p is a constraint of IPC ++ with free variables x 1 , . . . , x k (in the order of enumeration of the variables) and p[x 1 ← X i 1 x j 1 , . . . , x k ← X i k x j k ] is obtained from p by replacing every occurrence of x u by x j u preceded by i u next symbols for 1 ≤ u ≤ k. For instance, the formula x ≡ 2 0 ∧ 2(Xx ≡ 2 x + 1) states that the value of x is even on states of even indices.

The formulae of PLTL mod are defined by the following grammar:

φ ::= p[x 1 ← X i 1 x j 1 , . . . , x k ← X i k x j k ] | ¬φ | φ∧φ | Xφ | φUφ | X -1 φ | φSφ,
where p belongs to IPC ++ . As usual, X is the next-time operator, X -1 is the previous past-time operator, U is the until operator, and S is the since past-time operator (see below the semantics). More generally, we write PLTL(L) to denote the variant of PLTL mod where the atomic formulae are built from the constraint language L. Hence, PLTL mod is simply PLTL(IPC ++ ). We write LTL(L) to denote the restriction of PLTL(L) to the future-time operators X and U. We include past-time operators to the logic in order to capture the conciseness of LTL with past considered in [START_REF] Combi | A logical approach to represent and reason about calendars[END_REF][START_REF] Combi | Representing and reasoning about temporal granularities[END_REF]. However, the addition of a finite amount of MSO-definable temporal operators still guarantees the (forthcoming) pspace upper bound thanks to more general results from [START_REF] Gastin | Satisfiability and model checking for MSOdefinable temporal logics are in PSPACE[END_REF].

A model σ for PLTL mod is an ω-sequence of valuations of the form σ : N × VAR → Z. The satisfaction relation |= is inductively defined in Figure 2.

-σ, i |= p[x 1 ← X i 1 x j 1 , . . . , x k ← X i k x j k ] iff [x 1 ← σ(i + i 1 , x j 1 ), . . . , x k ← σ(i + i k , x j k )] |= p (the second occurrence of |= denotes the satisfaction relation in IPC ++ ), -σ, i |= φ ∧ φ iff σ, i |= φ and σ, i |= φ ; σ, i |= ¬φ iff not σ, i |= φ, -σ, i |= Xφ iff σ, i + 1 |= φ, σ, i |= X -1 φ iff i > 0 and σ, i -1 |= φ, -σ, i |= φUφ iff
there is j ≥ i such that σ, j |= φ and for every i ≤ k < j, σ, k |= φ, σ, i |= φSφ iff there is 0 ≤ j ≤ i such that σ, j |= φ and for every j < k ≤ i, σ, k |= φ.

Fig. 2. Semantics for PLTL mod formulae

A very important aspect of PLTL mod rests on the fact that the values of variables at different states can be compared. We use the standard abbreviations 3φ, F -1 φ, 2φ, . . . The satisfiability problem for PLTL mod is to decide given a formula φ whether there is σ such that σ, 0 |= φ. It is worth observing that adding to IPC ++ constraints of one of the forms below leads to undecidability of the satisfiability problem of the corresponding extension of PLTL mod :

-x = y + 1 with x, y ∈ VAR, see e.g. [CC00], -x < y with x, y ∈ VAR, -xy ≥ c with x, y ∈ VAR and c ∈ N \ {0}.

A few other remarks are in order. No propositional variables are part of PLTL mod but they can be easily simulated, for instance each P i can be encoded by x i = 1 if x i is not used for other purposes in the formula. When complexity issues are considered, all the integers are taken to be coded in binary representation.

Observe that because of the presence of the past-time operator X -1 , we can also simulate the access to past values of variables (which we would write X -n x for instance if n times X -1 . . . X -1 holds true). Typically, X -2 x = x can be concisely translated into X -1 X -1 ∧X -1 X -1 (x = X 2 x) assuming that if X -2 x is undefined, then the atomic constraint is interpreted by false.

PLTL mod and calendar formalisms

In [START_REF] Combi | A logical approach to represent and reason about calendars[END_REF], LTL with past is used for reasoning about calendars based on consistent granularities: this amounts to require that the truth values of propositional variables along the time line encode consistent granularities. As a major drawback, the encoding a period of n units requires a formula of size O(n) whereas the formula 2(Xx ≡ n x + 1) in PLTL mod does the job with only O(log(n)) symbols (remember that we encode the integers with a binary representation). A similar blow up occurs in the translation of pure Calendar Logic [START_REF] Ohlbach | Calendar logic[END_REF] into propositional calculus with an exponential increase of the size of formulae, which leads to a decision procedure in double exponential-time (to be compared with our pspace decision procedure in Sect. 4). Other advantages of our formalism in comparison with [START_REF] Ohlbach | Calendar logic[END_REF][START_REF] Combi | A logical approach to represent and reason about calendars[END_REF] is that we specify in the logical language the granularities.

Calendars. Formulae of PLTL mod can encode calendars and slices from [START_REF] Niezette | An efficient symbolic representation of periodic time[END_REF]. For instance, a calendar C can be viewed as an ordered partition X 1 , X 2 , . . . of N such that (the partition can be finite but we omit this case here) (ordering) for all i, x and y, x ∈ X i and y ∈ X i+1 imply x < y, (consecution) for every i, there are x ∈ X i and y ∈ X i+1 such that y = x + 1.

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

σ(0, x) = σ(1, x) = . . . = σ(i 1 , x) X 1 ={0,...,i 1 } = σ(i 1 + 1, x) = . . . = σ(i 2 , x) X 2 ={i 1 +1,...,i 2 } = . . .
In most cases, {σ(i, x) : i ∈ N} is naturally finite (minuts, hours, days in a week, months). This means that a class of such calendars can be alternatively encoded as consecutive positions having the same value modulo some integer. Assuming that the time unit is a second, let us define the calendar minuts using the notations from [START_REF] Niezette | An efficient symbolic representation of periodic time[END_REF]: duration(minuts / seconds) = [60] and synchronization(minuts / seconds) = 1. synchronization sec ≡ 60 0 ∧ min ≡ 60 0 ∧2(Xsec ≡ 60 sec + 1)∧ 2(sec ≡ 60 59 ⇒ Xmin ≡ 60 min + 1 ∧ (¬sec ≡ 60 59) ⇒ Xmin ≡ 60 min).

More complex calendars can be encoded in a similar fashion, possibly by introducing auxiliary variables (apart from the one to define the calendars) in order to be able to count in binary in some places.

Encoding Gregorian calendar. By way of example, we provide a partial encoding of Gregorian calendar with PLTL mod formulae.

-sec ≡ 60 0 ∧ 2(Xsec ≡ 60 sec + 1 ∧ 0 ≤ sec < 60). The second is the time unit (granularity).

-min ≡ 60 0 ∧ 2(0 ≤ min < 60)∧ 2((sec = 59 ⇒ Xmin ≡ 60 min + 1) ∧ (sec = 59 ⇒ Xmin = min)). -hour ≡ 24 0 ∧ 2(0 ≤ hour < 24)∧ 2((min = 59 ∧ sec = 59 ⇒ Xhour ≡ 24 hour + 1) ∧ (min = 59 ∨ sec = 59 ⇒ Xhour = hour)).
-

(hour ≡ 24 12 ∧ lunch -time)) ⇒ X(day ≡ 7 XdayUring)
It is worth observing that this PLTL mod formula is in polynomial size in the size of the original statement from Calendar Logic [START_REF] Ohlbach | Calendar logic[END_REF] even if one includes the encoding of Gregorian calendar.

Model Checking

The languages of the form PLTL(L) are of course well-designed to perform model checking of counter automata, similarly to what is done in [START_REF] Čerans | Deciding properties of integral relational automata[END_REF][START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF] and [START_REF] Revesz | Introduction to Constraint Databases[END_REF]Chap. 6]. Given a constraint language L (herein a fragment of IPC ++ ), a PLTL(L)-automaton is a Büchi automaton A over the alphabet Σ made of a finite subset of PLTL(L) formulas: transitions are of the form q φ -→ q where q, q are control states and φ is an PLTL(L) formula . As in [START_REF] Wolper | Temporal logic can be more expressive[END_REF][START_REF] Vardi | Reasoning about infinite computations[END_REF], we allow formulae on transitions. ω-words w

= φ 0 φ 1 • • • in Σ ω are indeed sym- bolic models. A symbolic model w has a concrete model σ : N × VAR → Z def ⇔ for every i ≥ 0, σ, i |= φ i . The model σ is simply a realization of the ω-sequence φ 0 φ 1 • • • . Let l(A) denote the set l(A) = {σ : N × VAR → Z | ∃w accepted by A such that σ, i |= w(i)
for each i}. The set l(A) is precisely the set of models for which there is a symbolic model accepted by A.

The model-checking problem for PLTL(L) is defined as follows:

input : A PLTL(L)-automaton A and a PLTL(L) formula φ, question : Is there a σ ∈ l(A) such that σ |= φ? (in symbols A |= ∃ φ?)

A natural relaxed version of the problem consists in restricting the labels on transitions to Boolean combinations of PLTL(L) atomic formulae.

Theorem 1. The model checking and satisfiability problems for PLTL mod are inter-reducible with respect to logspace transformations.

From model checking to satisfiability, the proof is similar to the proof of [DD03, Theorem 8.3] (which is itself based on a proof in [START_REF] Sistla | The complexity of propositional linear temporal logic[END_REF]). Indeed, control states of PLTL(L)-automata can be encoded by propositional variables, transitions by PLTL mod formulae. From satisfiability to model-checking, one can observe that φ is satisfiable iff A |= ∃ φ where A is a single-state automaton such that l(A) is precisely the set of all PLTL mod models. In Sect. 6 we shall show how LTL(IPC ++ )automata naturally encode extended single-string automata from [LM01, Sect. 5].

In the rest of the paper, only satisfiability problems are explicitly treated thanks to Theorem 1.

First-order theory of integer periodicity constraints

Given p in IPC ++ with free variables x 1 , . . . , x k , we shall construct a finite partition of Z k such that -every region can be represented by a semi-simple periodicity constraint; -for all k-tuples z and z in a given region of the partition, z ∈ sol(p) iff z ∈ sol(p).

In this way, we shall be able to finitely represent the set of solutions sol(p) and such a representation will be easy to manipulate since it can be viewed as a disjunction of semi-simple periodicity constraints. This is actually a standard requirement when an infinite set of tuples has to be finitely abstracted, see e.g. the clock regions for timed automata in [START_REF] Alur | A theory of timed automata[END_REF], the quantifier elimination procedure for discrete point constraint language in [START_REF] Koubarakis | Complexity results for first-order theories of temporal constraints[END_REF] and the reducibility of extended single-string automata in [START_REF] Lago | Calendars, time granularities, and automata[END_REF], to quote a few examples (see also the symbolic transition systems of the class one in [START_REF] Th | A classification of symbolic transitions systems[END_REF]).

Quantifier elimination

Quantifier elimination (QE) is a known method to show decidability of logical theories, see e.g. [START_REF] Presburger | Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt[END_REF][START_REF] Tarski | A Decision Method for Elementary Algebra and Geometry[END_REF][START_REF] Kreisel | Elements of Mathematical Logic[END_REF][START_REF] Ferrante | A decision procedure for the first order theory of real addition with order[END_REF]. In this section, we establish such a property to prove the pspace upper bound of the IPC ++ -satisfiability problem. Let p be a constraint in IPC ++ such that -d 1 < . . . < d n are the constants in p occurring in constraints of the form

x ∼ d with ∼∈ {<, >, =}; we fix d 0 = -∞ and d n+1 = +∞, this is done to simplify the notations in some places, -K is the least common multiple of every number k that appears in any ≡ k operator in the formula. K is in 2 O(|p|) .

We define from p an equivalence relation ∼ p between elements of Z as follows:

z ∼ p z def ⇔ 1. for all i ≤ j ∈ {0, . . . , n + 1}, d i ≤ z ≤ d j iff d i ≤ z ≤ d j , 2. for every l ∈ {0, . . . , K -1}, z ≡ K l iff z ≡ K l.
Hence, the number of equivalence classes of ∼ p is bounded by (n + 1) × K, that is in O(2 |p| ). The idea behind the definition of ∼ p is simply that z ∼ p z iff z and z cannot be distinguished by constraints of IPC + that use only d 1 , . . . , d n and k 1 , . . . , k u . For instance, it is easy to check that for every j ∈ {1, . . . , n}, {d i } is an equivalence class of ∼ p . The relation ∼ p extended to tuples will not be a simple component-wise extension because of the presence of equality in IPC ++ . For k ≥ 1, we say that z 1 , . . . ,

z k = z ∼ k p z = z 1 , . . . , z k iff -for every i ∈ {1, . . . , k}, z i ∼ p z i , -for all i, j ∈ {1, . . . , k}, z i = z j iff z i = z j .
If x 1 , . . . , x k are the free variables in p, we write z ∼ p z instead of z ∼ k p z . The number of equivalence classes of ∼ p (on k-tuples) is bounded by

(n + 1) × K × 2 k 2 .
Given 1 ≤ i 1 < . . . < i l ≤ k, we write z 1 , . . . , z k {i 1 ,...,i l } to denote the subsequence z i 1 , . . . , z i l .

Lemma 1. Let p be a constraint in IPC ++ with k free variables and z, z ∈ Z k . z ∈ sol(p) and z ∼ p z imply z ∈ sol(p).

Proof. Let p be a constraint in IPC ++ with k free variables x 1 , . . . , x k and k bounded variables y 1 , . . . , y k . For any subconstraint p of p, we write sol p (p ) to denote the set of (k

+ k )-tuples z 1 , . . . , z k+k ∈ Z k+k such that [x 1 ← z 1 , . . . , x k ← z k , y 1 ← z k+1 , . . . , y k ← z k+k ] |= p . The equivalence relation ∼ p on Z k is extended on Z k+k by considering ∼ k+k p
. By structural induction, we shall show that for every subconstraint p of p, for all z, z ∈ Z k+k , z ∈ sol p (p ) and z ∼ p z imply z ∈ sol p (p ). By taking p = p , we then get the statement of the lemma since sol p (p) = sol(p) × Z k .

Base case 1: p is of the form x ∼ d with x ∈ {x 1 , . . . , x k , y 1 , . . . , y k } and ∼∈ {<, >, =}. Suppose z ∈ sol p (x ∼ d), z ∼ p z and x equals some x i . By definition of ∼ p ,

z i ∼ d iff z i ∼ d. Hence, z ∈ sol p (x ∼ d). Base case 2: p is of the form x = x with x, x ∈ {x 1 , . . . , x k , y 1 , . . . , y k }. Suppose z ∈ sol p (x = x ), z ∼ p z , x = x i and x = y j . By definition of ∼ p , z i = z k+j iff z i = z k+j . Hence, z ∈ sol p (x = x ).
Base case 3: p is of the form x ≡ l c with x ∈ {x 1 , . . . , x k , y 1 , . . . , y k }. Suppose z ∈ sol p (x ≡ l c), z ∼ p z and x equals some y i . Let l 1 , . . . , l s be all the numbers appearing in some ≡ l operator of p. Recall that K is the lcm of all such numbers. By definition of ∼ p , z k+i ≡ K z k+i . By the Generalized Chinese Remainder Theorem, (z k+i ≡ l 1 z k+i and • • • and z k+i ≡ l s z k+i ) iff z k+i ≡ K z k+i . Consequently, z k+i ≡ l z k+i and therefore z ∈ sol p (x ≡ l c).

The other base cases are treated analogously. Now let us consider the different cases of the induction step.

Case 1: p = p 1 ∧ p 2 . Suppose z ∈ sol p (p 1 ∧ p 2 ) and z ∼ p z . Since each free variable occurring in some p i , is also free in p 1 ∧ p 2 , z ∈ sol p (p 1 ) and z ∈ sol p (p 2 ). By the induction hypothesis, z ∈ sol p (p 1 ) and z ∈ sol p (p 2 ). Hence, z ∈ sol p (p 1 ∧ p 2 ). Case 2: p = ¬p 1 . Suppose z ∈ sol p (¬p 1 ) and z ∼ p z . Hence, z ∈ sol p (p 1 ). By the induction hypothesis, z ∈ sol p (p 1 ), whence z ∈ sol p (¬p 1 ). Case 3: p = ∃ y p 1 for some y ∈ {y 1 , . . . , y k }. Suppose z ∈ sol p (∃ y p 1 ), z ∼ p z and y equals some y i . By definition of the satisfaction relation |=,

there is t ∈ Z such that [x 1 ← z 1 , . . . , x k ← z k , y 1 ← z k+1 , . . . , y i ← t, . . . y k ← z k+k ] |= p 1 . Let z 0 = z 1 , .
. . , z k , . . . , z k+i-1 , t, z k+i+1 , . . . , z k+k and z 0 = z 1 , . . . , z k , . . . , z k+i-1 , t, z k+i+1 , . . . , z k+k . Since z 0 ∼ p z 0 and z 0 ∈ sol p (p 1 ), by the induction hypothesis z 0 ∈ sol p (p 1 ). So every t ∈ Z, [x 1 ← z 1 , . . . , x k ← z k , y 1 ← z k+1 , . . . , y i ← t , . . . y k ← z k+k ] |= ∃ y p 1 . In particular, z ∈ sol p (∃ y p 1 ) by taking t = z k+i .

Each equivalence class of ∼ p on Z can be represented by a triple i, j, l with i ∈ {0, . . . , n}, j ∈ {0, 1}, and l ∈ {0, . . . , K -1} such that -if j = 0 and i ∈ {1, . . . , n}, then i, j, l represents the equivalence class {d i }, -if j = 1 and i ∈ {0, . . . , n}, then i, j, l represents the equivalence class {z ∈ Z : d i < z < d i+1 , and z ≡ K l} if this set is non empty.

We introduce the map

[•] : Z → {0, . . . , n} × {0, 1} × {0, . . . , K -1} such that [z]
is the representation of the equivalence class of ∼ p containing z. For instance, if

d i ≡ K 1, then [d i ] = i, 0, 1 .
By extension, given Y a non-empty finite subset of N of cardinality k representing a set of variable indices, we introduce the map

[•] Y : Z k → ({0, . . . , n} × {0, 1} × {0, . . . , K -1}) k × P(Y 2 ) such that [ z 1 , . . . , z k ] Y = [z 1 ], . . . , [z k ] , { J i , J j ∈ Y 2 : z i = z j } ,
where Y = {J 1 , . . . , J k } and J 1 < . . . < J k . If p has free variables x 1 , . . . , x k , the finite set ({0, . . . , n} × {0, 1} × {0, . . . , K -1}) k × P({1, . . . , k} 2 ) will represent the equivalence classes of ∼ p on k-tuples.

The proof of Lemma 2 below is by an easy verification.

Lemma 2. Let Y = {J 1 , . . . , J k } be a non-empty finite subset of N with J 1 < . . . < J k . Checking whether u ∈ ({0, . . . , n} × {0, 1} × {0, . . . , K -1})

k × P(Y 2 ) belongs to the image of [•] Y can be done in polynomial-time in |p| + |Y |. In Lemma 2 above, |u| is of polynomial size in |p| + |Y | with |Y | = Σ k i=1 (1 + log(J i )).
If p contains k free variables x 1 , . . . , x k , we write D p to denote the domain ({0, . . . , n} × {0, 1} × {0, . . . , K -1}) k × P({1, . . . , k} 2 ) and D sat p to denote the set {[z] {1,...,k} ∈ D p : z ∈ sol(p)}. The set D p is indeed a finite abstraction of the infinite domain Z k with respect to the constraint p (only depends on the syntactic resources in p) and D sat p is a finite representation of the possibly infinite set sol(p).

To each i, j, l ∈ {0, . . . , n} × {0, 1} × {0, . . . , K -1}, and variable index α ∈ N, we associate a semi-simple periodicity constraint IPC < ( i, j, l , α) in IPC {<} with free variable x α defined as follows:

IPC < ( i, j, l , α) = (x α ≡ K l) ∧        x α = d i if j = 0 and i ∈ {1, . . . , n}, (d i < x α ) ∧ (x α < d i+1 ) if j = 1 and i ∈ {0, . . . , n}, ⊥ otherwise.
The following lemma makes explicit the relationship between the constraints generated by the map IPC < and the map [•].

Lemma 3. For all z ∈ Z and i, j, l ∈ {0, . . . , n} × {0, 1} × {0, . . . , K -1}, we have

[x α ← z] |= IPC < ( i, j, l , α) iff [z] = i, j, l .
We are now able to show that IPC ++ satisfies (QE) by appropriately extending the map IPC < . To each t 1 , . . . , t k , X ∈ D p we associate a semi-simple periodicity constraints IPC ++ ( t 1 , . . . , t k , X ) defined by

( 1≤i≤k IPC < (t i , i)) ∧ ( i,j ∈X x i = x j ) ∧ ( i,j ∈X ¬(x i = x j )).
The following lemma (also not difficult to show) makes explicit the relationship between the constraints generated by the map IPC ++ (•) and the map [•] {1,...,k} .

Lemma 4. For all z 1 , . . . , z k ∈ Z k and u ∈ D p , we have [x 1 ← z 1 , . . . , x k ← z k ] |= IPC ++ (u) iff [ z 1 , . . . , z k ] {1,...,k} = u.
Theorem 2. IPC ++ admits quantifier elimination.

Proof. Let p be a constraint in IPC ++ with free variables x 1 , . . . , x k . We define below a constraint p in IPC ++ such that sol(p) = sol(p ):

p = t 1 ,...,t k ,X ∈D sat p IPC ++ ( t 1 , . . . , t k , X ).
Equality between sol(p) and sol(p ) can be proved by using Lemma 4.

PSPACE-complete satisfiability problem

We establish that IPC ++ -satisfiability is decidable in polynomial space.

Theorem 3. IPC ++ -satisfiability is pspace-complete.

Proof. pspace-hardness is obtained by reducing QBF. Let φ be an instance of QBF of the form below:

∀ x 1 ∃ x 2 . . . ∀ x 2n-1 ∃ x 2n φ m i=1 (l i 1 ∨ l i 2 ∨ l i 3 )
where the l i j 's are literals over the propositional variables in x 1 , . . . , x 2n . In spite of the prenex form of φ, the strict alternation between ∀ and ∃, and the fact that φ is in 3CNF, QBF restricted to such QBF formulae can be easily shown to be pspace-hard. We define, in logarithmic space in |φ|, a formula t(φ) such that φ is QBF satisfiable iff x 0 = 0 ∧ t(φ) is IPC ++ satisfiable (x 0 = 0 is artificially added to have at least one free variable). To each propositional variable x i , we associate an IPC ++ variable x i .

-t(∀ x ψ)

def = ∀ x (x = 0) ∨ (x = 1) ⇒ t(ψ), -t(∃ x ψ) def = ∃ x ((x = 0) ∨ (x = 1)) ∧ t(ψ), -t(ψ ∧ ψ ) def = t(ψ) ∧ t(ψ ), t(ψ ∨ ψ ) def = t(ψ) ∨ t(ψ ), t(¬ψ) = ¬t(ψ), -t(x) def = x = 1, -t(¬x) def = x = 0.
Satisfiability in pspace can be shown via a procedure similar to first-order model-checking [START_REF] Chandra | Optimal implementation of conjunctive queries in relational databases[END_REF], details are given below.

First, some preliminary definitions. Given a sequence s 1 , . . . , s k , we write s 1 , . . . , s k [i 1 ← t 1 , . . . , i u ← t u ] to denote the sequence obtained from s 1 , . . . , s k by replacing s i j by t j for every j ∈ {1, . . . , u}. We shall define a function SAT(p) that checks satisfiability of the constraint p in IPC ++ . To do so, we introduce an auxiliary function MC which is indeed the core of our procedure. Let p be a constraint in IPC ++ with occurrences of the variables x 1 , . . . , x k . The free variables of p are x i 1 , . . . , x i s with 1 ≤ i 1 < i 2 < . . . < i s ≤ k. The function SAT is defined in Figure 3.

SAT(p):

if there is t 1 , . . . , t s , X ∈ ({0, . . . , n}×{0, 1}×{0, . . . , K -1}) s ×P({i 1 , . . . , i s } 2 ) such that 1. t 1 , . . . , t s , X belongs to the image of [•] {i 1 ,...,i s } and 2. MC(p, p,

k times z }| { -, . . . , -[i 1 ← t 1 , . . . , i s ← t s ], X , {i 1 , .
. . , i s }) returns "Yes"; then return "Yes" otherwise return "No".

Fig. 3. Function SAT

Observe that condition 1. in the definition of SAT can be checked in polynomialtime in |p| by Lemma 2. Moreover, it will not be difficult to show that MC (defined below) runs in pspace: polynomial recursion depth and quantification over exponential size sets (which requires only polynomial space) guarantees this upper bound. MC has four arguments:

1. a constraint p of IPC ++ , 2. a subconstraint p of p, 3. an interpretation of the free variables of p represented in an abstract fashion with the use of a padding symbol '-', 4. the set of indices of the free variables of p .

There is certainly a bit of redundancy in the arguments: the positions of the third argument with values different from the padding symbol '-' are precisely the elements of the fourth argument. However, this is not crucial for the result we want to establish. MC is indeed a model-checking procedure since the third argument provides an interpretation for the free variables of the second argument. MC returns "Yes" iff this interpretation forces the second argument to hold true. The function MC is defined by a simple case analysis as shown in Figure 4.

In the case p = ∃x i p , condition 1. can be checked in polynomial-time in |p|.

In order to get a pspace-complete extension of LTL with a subclass of Presburger constraints, the best we can do is to design a constraint language with a pspace-hard satisfiability problem, like IPC ++ .

Corollary 1. Let p be a constraint in IPC ++ . Checking whether u ∈ D p belongs to D sat p can be done in pspace.

Proof. Let u ∈ D p . One can show that u ∈ D sat p iff p ∧ IPC ++ (u) is satisfiable.
Hence, the pspace upper bound.

Observe also that IPC ++ ( t 1 , . . . , t k , X ) is indeed a set of signed atomic constraints of the form s (x i = x j ), s (x i ∼ d j ), and s (x i ≡ K l) with the sign s in { , ¬} and ∼∈ {<, >, =}.

MC(p, p , s 1 , . . . , s k , X , Y ):

if p = "x i = x j " and i, j ∈ X then return "Yes";

-if p = "x i ≡ α x j + [c 1 , c 2 ]" and there is c ∈ [c 1 , c 2 ] such that l i ≡ α l j + c then
return "Yes" (s i = min i , max i , l i and s j = min j , max j , l j ); -the other base cases from the atomic formulae of IPC ++ are treated in a similar fashion and one can check that this requires only polynomial-time in p; -in the case p = p 1 ∧ p 2 , let x i 1 , . . . , x i α be the free variables of p 1 and x j 1 , . . . , x j β be the free variables of p 2 . If the two calls below returns "Yes" 1. MC(p, p 1 , -, . . . ,

-[i 1 ← s i 1 , . . . , i α ← s i α ], X ∩ {i 1 , . . . , i α } 2 , {i 1 , . . . , i α }) 2. MC(p, p 2 , -, . . . , -[j 1 ← s j 1 , . . . , j β ← s j β ], X ∩{j 1 , . . . , j β } 2 , {j 1 , . . . , j β }) then return "Yes". -in the case p = ¬p , if MC(p, p , s 1 , . . . , s k , X , Y ) returns "No", then return "Yes"; -if p = ∃x i p then if there are t ∈ {0, . . . , n} × {0, 1} × {0, . . . , K -1} and X ⊆ X ⊆ (Y ∪ {i}) 2 such that 1. X = X ∩ Y 2 ; 2. ( s 1 , . . . , s k [i ← t]) Y ∪{i} , X belongs to the image of [•] Y ∪{i} ; 3. MC(p, p , s 1 , . . . , s k [i ← t],
X , Y ∪ {i}) returns "Yes"; then return "Yes".

Return "No".

Fig. 4. Function MC

The problem described in Corollary 1 is actually a model-checking problem (easily solvable with the procedure MC) where the interpretation of the variables is done modulo the equivalence classes of ∼ p . By Lemma 1, this reasoning modulo is sufficient.

Corollary 2. Given a constraint p in IPC ++ , one can compute an equivalent quantifier-free p in polynomial space in |p|

(but |p | is in O(2 |p| )).
This is a mere consequence of the proof of Theorem 2, Corollary 1, and the fact that all the elements of D p can be enumerated using only polynomial space in |p|.

Complexity of PLTL mod

Let φ be a PLTL mod formula with -free variables x 1 , . . . , x s , -constants d 1 < . . . < d n (d 0 = -∞ and d n+1 = +∞), -natural numbers k 1 , . . . , k u occurring in the context of ≡-atomic formulae and their lcm is denoted by K.

Without any loss of generality, we can assume that the above sets of integers/variables are non-empty. Let |φ| X be one plus the greatest i with some term X i x j occurring in φ. For instance, |φ| X with φ = 2(Xx ≡ n x + 1) is equal to two. In the sequel, we let l = |φ| X . l is the maximal number of consecutive states necessary to evaluate an atomic subformula of φ.

We shall provide in the sequel a procedure to decide satisfiability of φ using polynomial space in |φ|.

Abstraction of PLTL mod models

By definition, a model σ of φ is a structure σ : N × {x 1 , . . . , x s } → Z such that σ, 0 |= φ. However, each local valuation σ(i) : {x 1 , . . . , x s } → Z can take an infinite amount of values. By contrast, for classical LTL, there is a finite amount of interpretations over a finite set of propositional variables. That is why we shall abstract such valuations as elements of a finite set, more precisely as elements of the set Σ φ = ({0, . . . , n} × {0, 1} × {0, . . . , K -1}) k × P({1, . . . , k} 2 ) with k = s × l. This provides evidence that PLTL(IPC ++ )-automata are in the class one of symbolic transitions systems following the classification in [START_REF] Th | A classification of symbolic transitions systems[END_REF]. The rest of this section is dedicated to the construction of such abstractions by using Sect. 3.

Another way to understand a structure σ : N × {x 1 , . . . , x s } → Z with the PLTL mod semantics is to view it as a structure σ : N×({x 1 , . . . , x s }×{0, . . . , l -1}) → Z such that (C1) for all i ∈ N, α ∈ {1, . . . , s}, and β ∈ {1, . . . , l -1}, σ (i, x α , β ) = σ (i + 1, x α , β -1 ).

In that way, the pair x α , β plays the rôle of the term X β x α . So far, the profile of σ depends on φ by the value l and by the number of variables s but one has also to relate σ with σ. The condition (C2) below does the job:

(C2) for all i ∈ N and α ∈ {1, . . . , s}, σ (i, x j , 0 ) = σ(i, x j ).

Each map σ satisfying conditions (C1) and (C2) can be viewed as a variant of σ where the states are grouped by l consecutive states. The following lemma is now easy to establish. Lemma 5.

(I) Given σ : N × {x 1 , . . . , x s } → Z, there is a unique σ : N × ({x 1 , . . . , x s } × {0, . . . , l -1}) → Z satisfying (C1) and (C2). (II) Given σ : N × ({x 1 , . . . , x s } × {0, . . . , l -1}) → Z satisfying (C1), there is a unique σ : N × {x 1 , . . . , x s } → Z satisfying (C2).

By way of example, in the proof of Lemma 5(II), we define σ(i, x α ) as the value σ (i, x α , 0 ).

In order to state Lemma 6 below, a straightforward corollary of Lemma 5, we need a preliminary definition. Let (PLTL mod ) be the syntactic variant of PLTL mod where each term X β x α is replaced by the pair x α , β . The models of (PLTL mod ) are maps of the form N × ({x 1 , . . . , x s } × {0, . . . , l -1}) → Z. The satisfaction relation is defined inductively as for PLTL mod except at the atomic level where we require: Hence, (PLTL mod ) is a variant of PLTL mod (depending on φ because of s and l) for which the satisfiability problem is related to PLTL mod as shown below.

(*) σ , i |= p[x 1 ← x j 1 ,
Lemma 6. φ is satisfiable iff there is a structure σ : N × ({x 1 , . . . , x s } × {0, . . . , l -1}) → Z satisfying (C1) such that σ , 0 |= φ where φ is obtained from φ by replacing every occurrence of X β x α by x α , β .

Let us now abstract the structures of the form σ : N × ({x 1 , . . . , x s } × {0, . . . , l -1}) → Z. We pose k = s × l and we write Σ φ to denote the set ({0, . . . , n} × {0, 1} × {0, . . . , K -1}) k × P({1, . . . , k} 2 ) by similarity to the developments made in Sect. 3. The set Σ φ is a finite abstraction of maps σ : {x 1 , . . . , x s } × {0, . . . , l -1} → Z where σ (x j , i) is the value of the variable x j at the ith next state. Similarly, Σ sat φ is defined as the subset of Σ φ that corresponds to elements of Σ φ that are really abstractions of maps σ : {x 1 , . . . , x s } × {0, . . . , l-1} → Z (there are dummy abstract values in Σ φ ). Actually, Σ sat φ is the codomain of [•] {1,...,k} . In order to relate terms of the form X β x α and "new" variables x i (i ∈ {1, . . . , k}), we introduce the map f : {x 1 , . . . , x s }×{0, . . . , l -1} → {1, . . . , k} as the bijection defined by f ( x α , β ) = s×β +α. The inverse function f -1 can be easily defined with the operations of the Euclidean division. Details are omitted here. One can check that f -1 (1), f -1 (2), . . . , f -1 (k) is precisely the sequence

x 1 , 0 , x 2 , 0 , . . . , x s , 0 , x 1 , 1 , . . . , x 1 , l -1 , x 2 , l -1 , . . . , x s , l -1 .

Hence, first the variables at the current state are enumerated, then the variables at the next state are enumerated and so on.

Another way to understand a structure σ : N×({x 1 , . . . , x s }×{0, . . . , l-1}) → Z is to view it as a structure σ : N → Σ sat φ such that

(C3) for every i ∈ N, if σ (i) = t 1 , . . . ,
= { u + s, v + s : u, v ∈ X , u + s ≤ k, v + s ≤ k}
(preservation in X of X restricted to the indices in {s + 1, . . . , k}).

One has also to relate σ with σ. The condition (C4) below does the job. We need again a preliminary definition. Given g : {x 1 , . . . , x s } × {0, . . . , l -1} → Z, we write g k to denote the k-tuple g(f -1 (1)), . . . , g(f -1 (k)) . g k is simply a representation of g as a k-tuple of Z k with k = s × l.

(C4) for all i ∈ N, σ (i) = [σ(i) k ] {1,...,k} .
The following lemma can be established.

Lemma 7.

(I) Given σ : N × ({x 1 , . . . , x s } × {0, . . . , l -1}) → Z satisfying (C1), there is a unique σ : N → Σ sat φ satisfying (C3) and (C4). (II) Given σ : N → Σ sat φ satisfying (C3), there is a map σ : N × ({x 1 , . . . , x s } × {0, . . . , l -1}) → Z satisfying (C1) and (C4).

Lemma 7(I) is easily shown by using the equality in (C4) to construct σ . Observe that in Lemma 7(II), σ is not necessarily unique. The proof of Lemma 7(II) uses the existence of a map h :

Σ sat φ → Z k such that for every u ∈ Σ sat φ , [h(u)] {1,...,k} = u since Σ sat φ is the image of [•] {1,.
..,k} (Axiom of Choice). In order to state Lemma 8 below, we need another preliminary definition. Let (PLTL mod ) be the syntactic variant of PLTL mod where each term X β x α is replaced by the variable x f ( x α ,β ) . The models of (PLTL mod ) are maps of the form N → Σ sat φ . The satisfaction relation is defined inductively as for PLTL mod except at the atomic level where we require:

The cardinality of cl (φ) is polynomial in |φ|. We define an atom of φ to be a maximally consistent subset of cl (φ) defined as follows. X is an atom of φ iff -X ⊆ cl (φ) and ∈ X, -for every ψ ∈ cl (φ), ψ ∈ X iff not ¬ψ ∈ X; -for every ψ ∧ ψ ∈ cl (φ), ψ ∧ ψ ∈ X iff ψ ∈ X and ψ ∈ X, -for every ψUψ ∈ cl (φ), ψUψ ∈ X iff either ψ ∈ X or {ψ, X(ψUψ )} ⊆ X, -for every ψSψ ∈ cl (φ), ψSψ ∈ X iff either ψ ∈ X or {ψ, X -1 (ψSψ )} ⊆ X, -for every X -1 ψ ∈ cl (φ), X -1 ψ ∈ X implies X -1 ∈ X.

We can now define the generalized Büchi automaton A PLTL = (Q, Q 0 , -→ , F) with F = {F 1 , . . . , F m } ⊆ P(Q). A run ρ : N → Q is accepting according to F iff for each i ∈ {1, . . . , m}, ρ(j) ∈ F i for infinitely many j ∈ N. A generalized Büchi condition can be easily converted to a Büchi condition by augmenting the states with a 0-m counter, see e.g. [CGP00, Chapter 9]. The elements of A PLTL are defined as follows:

-Q = P(cl (φ)); Q 0 = {X ∈ Q : {φ, ¬X -1 } ⊆ X}. -X u -→ Y iff
(ATOM) X and Y are atoms of φ. (IPC ++ ) for every atomic p in X, p ∧ IPC ++ (u) is IPC ++ -satisfiable where p is obtained from p by replacing the occurrences of

X β x α by x f ( x α ,β ) . (NEXT) for each Xψ ∈ cl (φ), Xψ ∈ X iff ψ ∈ Y . (PREVIOUS) for each X -1 ψ ∈ cl (φ), X -1 ψ ∈ Y iff ψ ∈ X.
-Let {ψ 1 Uϕ 1 , . . . , ψ m Uϕ m } be the set of until formulae in cl (φ). F = {F 1 , . . . , F m } with for every i ∈ {1, . . . , m},

F i = {Z ∈ Q | ψ i Uϕ i ∈ Z or ϕ i ∈ Z}.
In A PLTL , one can check whether X u -→ Y holds true in polynomial space in |φ|. The conditions (ATOM), (NEXT), and (PREVIOUS) can be checked in polynomial-time in |φ|. However, the above condition (IPC ++ ) requires polynomial space by Corollary 1. The main difference with LTL with past remains in the condition at the atomic level, involving here an IPC ++ -satisfiability check.

Theorem 4. φ is satisfiable iff L(A φ ) is non-empty.
This is a consequence of Lemma 8 and of the construction of Büchi automata from formulae in LTL with past [START_REF] Laroussinie | Temporal logic with forgettable past[END_REF].

Viewing a model of φ as an ω-sequence of elements from Σ φ , every formula φ defines an ω-regular subset of Σ ω φ , which can be also viewed as an ω-regular set of constraints by using the map IPC ++ (u). By contrast, in LTL({x = y, x < y}), the extension of LTL where the atomic formulae are of the form X n 1 x 1 ∼ X n 2 x 2 with ∼∈ {<, =}, there exist formulae that define non ω-regular sets of constraints [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF].

Complexity bounds

It is now standard to prove Theorem 5 below.

Theorem 5. Satisfiability for PLTL mod is in pspace.

Proof. A φ is defined as A Σ sat φ ∩ A (C3) ∩ A PLTL . By the above considerations even though A φ has an exponential amount of states in |φ|, checking the emptiness of L(A φ ) can be done on the fly in polynomial space in |φ| with a non-deterministic algorithm. As usual, by Savitch's theorem, this provides the required pspace upper bound.

The pspace-hardness of the satisfiability problem for PLTL mod is a mere consequence of the pspace-hardness of plain LTL [START_REF] Sistla | The complexity of propositional linear temporal logic[END_REF]. Moreover, it is worth observing that all the temporal operators in PLTL mod are MSO-definable and by using [START_REF] Gastin | Satisfiability and model checking for MSOdefinable temporal logics are in PSPACE[END_REF], it is not difficult to show that any extension of PLTL mod obtained by adding a finite amount of MSO-definable temporal operators remains in pspace.

This pspace upper bound is quite remarkable: in [BC02,DD02,DD03] pspacecompleteness has been mainly established for extensions of LTL over concrete domains with satisfiability problem in P(only) at the constraint level.

Corollary 3. Model checking for PLTL mod is pspace-complete.

Adding logical first-order quantifiers

In this section, we investigate the extension of PLTL(IPC + ) with the existential quantifier ∃, i.e. temporal operators can be in the scope of the existential quantifier ∃. This extension is denoted by PLTL ∃ (IPC + ). In full generality, first-order LTL is known to be highly undecidable [START_REF] Abadi | The power of temporal proofs[END_REF][START_REF] Kröger | On the interpretability of arithmetic in temporal logic[END_REF] even in the case the uninterpreted domains are finite [START_REF] Trahtenbrot | Impossibility of an algorithm for the decision problem in finite classes[END_REF]. Similarly, first-order LTL over finite time structures is highly undecidable [START_REF] Cerrito | First-order linear temporal logic over finite time structures[END_REF]. The decidability/complexity results obtained in this section are due to the fact that we can interpret any first-order formula φ of PLTL ∃ (IPC + ) in a fixed concrete (infinite) domain that can be abstracted by a finite domain whose cardinality is nevertheless exponential in |φ|. A similar argument cannot be used for PLTL mod augmented with the quantifier ∃, denoted by PLTL ∃ (IPC ++ ), as shown by the recent undecidability results from [START_REF] Demri | On the freeze quantifier in constraint LTL: decidability and complexity[END_REF][START_REF] Lisitsa | Temporal logic with predicate λ-abstraction[END_REF].

Existential quantifier

In order to define PLTL ∃ (IPC ++ ) formally, we divide the set VAR into the (countably infinite) set of rigid variables (VAR r ) and the (countably infinite) set of flexible variables (VAR f ). The clause ∃ y φ with y ∈ VAR r is added to the definition of PLTL(IPC ++ ) formulae in order to obtain PLTL ∃ (IPC ++ ) formulae. A model σ for PLTL ∃ (IPC ++ ) is of the form σ : N × VAR → Z where for every x ∈ VAR r , for all i, j ∈ N, σ(i, x) = σ(j, x). In other words, the rigid variables never change their value in a model. By contrast, the variables in VAR f for PLTL ∃ (IPC ++ ) behave as the variables in VAR for PLTL(IPC ++ ). The definition of |= is extended as follows:

σ, i |= ∃ y φ def ⇔ there exists z ∈ Z such that σ , i |= φ,
where σ is defined as follows:

-for all j ∈ N and x ∈ VAR \ {y}, σ (j, x) = σ(j, x), -for every j ∈ N, σ (j, y) = z.

Without any loss of generality, we can assume that for all the formulae φ in PLTL ∃ (IPC ++ ), the free variables in φ are necessarily flexible. The logic PLTL ∃ (IPC + ) is defined as the fragment of PLTL ∃ (IPC ++ ) restricted to contraints in IPC + .

Freeze quantifier

A very interesting restriction of the existential operator consists of the so-called freeze quantifier that acts as a mechanism to remember a past value (register). In this section, we consider the freeze quantifier ↓ that allows to bind the values of variables to a fixed value. This is a powerful binder mechanism used in real-time logics [START_REF] Alur | Real-time logics: complexity and expressiveness[END_REF][START_REF] Alur | A really temporal logic[END_REF], in hybrid logics [START_REF] Goranko | Hierarchies of modal and temporal logics with references pointers[END_REF][START_REF] Blackburn | Representation, reasoning, and relational structures: a hybrid logic manifesto[END_REF], in logics with λabstraction [START_REF] Fitting | Modal logic between propositional and first-order[END_REF][START_REF] Lisitsa | Temporal logic with predicate λ-abstraction[END_REF], and in temporal logics [START_REF] Laroussinie | Temporal logic with forgettable past[END_REF][START_REF] Demri | On the freeze quantifier in constraint LTL: decidability and complexity[END_REF]. Adding this kind of operator can easily lead to undecidability (see e.g., [START_REF] Goranko | Hierarchies of modal and temporal logics with references pointers[END_REF]) when no restriction is required on the Kripke structures. In this section, we treat a very particular case with integer periodicity constraints for which decidability follows from decidability of PLTL mod .

In order to define PLTL ↓ (IPC ++ ), we also divide the set VAR into VAR r and VAR f . The clause ↓ y=X j x φ with y ∈ VAR r and x ∈ VAR f is added to the definition of PLTL(IPC ++ ) formulae in order to obtain PLTL ↓ (IPC ++ ) formulae. A model σ for PLTL ↓ (IPC ++ ) is defined as a model for PLTL ∃ (IPC ++ ). The definition of |= is extended as follows:

σ, i |=↓ y=X j x φ def ⇔ σ , i |= φ,
where σ is defined as follows:

-for all k ∈ N and x ∈ VAR \ {y}, σ (k, x) = σ(k, x); -for every k ∈ N, σ (k, y) = σ(i + j, x).

Without any loss of generality, we can also assume that for all the formulae φ in PLTL ↓ (IPC ++ ), the free variables in φ are necessarily flexible. The logic PLTL ↓ (IPC + ) is defined as the fragment of PLTL ↓ (IPC ++ ) restricted to contraints in IPC + .

The logic PLTL ↓ (IPC ++ ) is a fragment of PLTL ∃ (IPC ++ ) since ↓ y=X j x φ and ∃ y y = X j x ∧ φ are equivalent formulae whatever the context is. Since constraints of the form y = X i x cannot be generated from IPC + (IPC + has no equality between variables), PLTL ↓ (IPC + ) is not a fragment of PLTL ∃ (IPC + ).

It is however open whether PLTL ↓ (IPC + ) is as expressive as PLTL ∃ (IPC + ) even through as shown below, both logics have the same complexity. Formally, PLTL ∃ (IPC + ) is as expressive as PLTL ↓ (IPC + ) def ⇔ for every φ in PLTL ∃ (IPC + ), there is φ in PLTL ↓ (IPC + ) such that for every model σ : N×VAR → Z, σ, 0 |= φ iff σ, 0 |= φ . The proof of Lemma 11 entails that PLTL ↓ (IPC + ) is as expressive as PLTL ∃ (IPC + ) and for every φ in PLTL ↓ (IPC + ), the equivalent formula φ in PLTL ∃ (IPC + ) can be computed in polynomial-time.

EXPSPACE lower bound

Adding the existential operator ∃ to PLTL(IPC + ) leads to an exponential blowup even if only future-time operators and simple periodicity constraints are used.

Lemma 9. Satisfiability for PLTL ∃ (IPC + ) and PLTL ↓ (IPC + ) restricted to futuretime operators and simple periodicity constraints are expspace-hard.

Proof. In order to prove the result for PLTL ∃ (IPC + ), we present a reduction from the 2 n -corridor tiling problem that is expspace-complete, see [START_REF] Van Emde | The convenience of tilings[END_REF] and references therein. A tile is a unit square of one of the several tile-types and the tiling problem we considered is specified by means of a finite set T of tile-type (say T = {t 1 , . . . , t m }), two binary relations H and V over T and two distinguished tile-types t init , t f inal ∈ T . The tiling problem consists in determining whether, for a given number n in unary, the region [0, . . . , 2 n -1] × [0, . . . , k -1] of the integer plane for some k can be tiled consistently with H and V , t init is the left bottom tile, and t f inal is the right upper tile.

Given an instance I = T, t init , t f inal , n of the tiling problem, we build a formula φ I such that I = T, t init , t f inal , n has a solution iff φ I is PLTL ∃ (IPC + ) satisfiable. We introduce below the variables in PLTL ∃ (IPC + ) used in the proof:

-pos is a flexible variable that allows to count until 2 n . There is a corresponding rigid variable pos . Each element α, i of a row [0, . . . , 2 n -1] × {i} satisfies pos ≡ 2 n α. The finite region [0, . . . , 2 n -1] × [0, . . . , k -1] will be encoded by the following prefix of a PLTL ∃ (IPC + ) model

({pos ≡ 2 n 0} • {pos ≡ 2 n 1} • . . . • {pos ≡ 2 n 2 n -1}) k .
-For t ∈ T , z t is a flexible variable such that D t := z t ≡ 2 0 is the formula encoding the fact that at a certain position of the integer plane the tile t is present. There is also a rigid variable z t and D t def = (z t ≡ 2 0). -end is a flexible variable and we define END def = (end ≡ 2 0).

The formula φ I is the conjunction of the following formulae:

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

¬END ∧ (¬ENDU(pos ≡ 2 n 0 ∧ 2END)).
-Exactly one tile per element of the plane region:

2(¬END ⇒ t∈T (D t ∧ t =t ¬D t )).
-Constraint on the right upper tile:

3(pos ≡ 2 n (2 n -1) ∧ ¬END ∧ D t f inal ∧ XEND).
-Constraint on the left bottom tile:

pos ≡ 2 n 0 ∧ D t init .
-Incrementation of the counter pos modulo 2 n : 2(Xpos ≡ 2 n pos + 1).

-Horizontal consistency:

2(( not the last element of a row (¬pos ≡ 2 n (2 n -1)) ∧¬END) ⇒ t∈T (D t ⇒ t,t hor ∈H XD t hor )).
-Vertical consistency:

2( t∈T (D t ∧ not on the last row ¬END ∧ 3(X¬END ∧ pos ≡ 2 n (2 n -1))) ⇒ ∀ x (x ≡ 2 n pos ⇒ X((¬x ≡ 2 n pos)U
go to the same position one row above

(x ≡ 2 n pos ∧ t,t ver ∈V D t ver ) ))).
The last part of the above formula allows us to go exactly to the cell above a given cell and check the vertical consistency. Observe that ∃ is present in φ I only to express the vertical consistency.

One can show that the instance I = T, t init , t f inal , n has a solution iff φ I is PLTL ∃ (IPC + ) satisfiable.

In order to get the expspace-hardness for PLTL ↓ (IPC + ), it is sufficient to consider the above formula for PLTL ∃ (IPC + ) and to replace the subformula about the vertical consistency by the formula below:

2( t∈T (D t ∧ not on the last row ¬END ∧ 3(X¬END ∧ pos ≡ 2 n (2 n -1))) ⇒ ↓ x=pos X((¬x ≡ 2 n pos)U
go to the same position one row above

x ≡ 2 n pos ∧ t,t ver ∈V D t ver )).

EXPSPACE upper bound

An exponential-time translation from PLTL ∃ (IPC + ) to PLTL(IPC + ) allows us to show the following result.

Lemma 10. Satisfiability for PLTL ∃ (IPC + ) is in expspace.

Proof. Let φ be a formula of PLTL ∃ (IPC + ) with -free variables x 1 , . . . , x k , -d 1 < . . . < d n are the constants in φ occurring in constraints of the form

x ∼ d with ∼∈ {<, >, =}, -natural numbers k 1 , . . . , k u occurring in the context of ≡-atomic formulae and their lcm is denoted by K.

Let D be the set { i, j, l ∈ {0, . . . , n} × {0, 1} × {0, . . . , K -1} : IPC < ( i, j, l , 1)) is satisfiable}.

To each i, j, l ∈ D, we associate a constant d i,j,l such that |d i,j,l | is polynomial in |φ| and [x 1 ← d i,j,l ] |= IPC < ( i, j, l , 1).

We reduce PLTL ∃ (IPC + ) satisfiability to PLTL(IPC + ) satisfiability. Basically, we replace logical existential quantification ∃ x α ψ by a disjunction where for each disjunct the variable x α takes a value d i,j,l for some i, j, l ∈ D. The number of disjuncts may be exponential in |φ|. The translation t is defined as follows. Suppose we want to translate a formula φ in PLTL ∃ (IPC + ) with flexible variables x 1 , . . . , x k and rigid variables y 1 , . . . , y s . The translation of φ is defined from the map t(ψ, a) where ψ is a subformula of φ and a ∈ ({d i,j,l : i, j, l ∈ D} ∪ {⊥}) s . The tuple a stands for a valuation of the variables y 1 , . . . , y s . The element ⊥ is the undefined value. The translation of φ is precisely t(φ, ⊥, . . . , ⊥ ).

-t(p, a 1 , . . . , a s ) = p where p is atomic and p is obtained from p by replacing each occurrence of y i by a i with adequate simplifications, see below.

The expression x ≡

k a i + [c 1 , c 2 ] with a i = s × k + c, s ∈ Z, and c ∈ {0, . . . , k -1} is simplified into c 1 ≤α≤c 2 x ≡ k (c + α). 2. The expression a i ≡ k [c 1 , c 2 ] with a i = s × k + c, s ∈ Z, and c ∈ {0, . . . , k -1} is simplified into c 1 ≤α≤c 2 c = α. 3.
The expression a i ∼ d with ∼∈ {=, <, >} takes either the value or ⊥ depending whether

a i ∼ d holds true. -t(φ 1 ∧ φ 2 , a 1 , . . . , a s ) = t(φ 1 , a 1 , . . . , a s ) ∧ t(φ 2 , a 1 , . . . , a s ), -t(¬φ 1 , a 1 , . . . , a s ) = ¬t(φ 1 , a 1 , . . . , a s ), -t(φ 1 Uφ 2 , a 1 , . . . , a s ) = t(φ 1 , a 1 , . . . , a s )Ut(φ 2 , a 1 , . . . , a s ), -t(φ 1 Sφ 2 , a 1 , . . . , a s ) = t(φ 1 , a 1 , . . . , a s )St(φ 2 , a 1 , . . . , a s ), -t(Xφ 1 , a 1 , . . . , a s ) = Xt(φ 1 , a 1 , . . . , a s ), -t(X -1 φ 1 , a 1 , . . . , a s ) = X -1 t(φ 1 , a 1 , . . . , a s ), -t(∃ y α φ 1 , a 1 , . . . , a s ) = i,j,l ∈D t(φ 1 , a 1 , . . . , a α-1 , d i,j,l , a α+1 , . . . , a s ). One can check that |t(φ)| is in 2 O(|φ| 2 )
. Even if we add atomic constraints of the form x ≡ k [c 1 , c 2 ] in the definition of IPC + (with the obvious interpretation), one cannot avoid the quadratic exponent in 2 O(|φ| 2 ) .

We show that φ is PLTL ∃ (IPC + ) satisfiable iff t(φ, ⊥, . . . , ⊥ ) is PLTL(IPC + ) satisfiable. We describe below the main steps of the proof. First observe that there is σ : N × VAR → Z such that σ, 0 |= φ iff there is σ : N × VAR → {d i,j,l : i, j, l ∈ D} such that σ , 0 |= φ. Indeed, atomic formulae in φ cannot distinguished d i,j,l from any d such that [x 1 ← d ] |= IPC < ( i, j, l , 1). Second, one can show by structural induction that for every subformula ψ of φ, for every a 1 , . . . , a s such that a i =⊥ implies y i is not free in ψ, for every PLTL ∃ (IPC + ) model σ, for every j ∈ N, σ, j |= ψ iff σ x 1 ,...,x k , j |= t(ψ, a 1 , . . . , a s ) where σ x 1 ,...,x k is the restriction of σ to the flexible variables x 1 , . . . , x k . As a consequence, φ is PLTL ∃ (IPC + ) satisfiable iff t(φ, ⊥, . . . , ⊥ ) is PLTL(IPC + ) satisfiable.

By way of example, the case in the induction step with ψ = ∃ y α ψ is treated as follows. We have the following equivalences:

-σ, j |= ψ, -there is d ∈ Z such that σ , j |= ψ where σ equals σ except that σ (l, y α ) = d for all l, -there is d ∈ {d i,j,l : i, j, l ∈ D} such that σ d , j |= ψ where σ equals

σ d except that σ d (l, y α ) = d for all l, -there is d ∈ {d i,j,l : i, j, l ∈ D} such that (σ d ) x 1 ,...,x k |= t(ψ, a 1 , . . . , a α-1 , d, a α+1 , . . . , a s ) (by the induction hypothesis), -σ x 1 ,...,x k , j |= d∈{d i,j,l : i,j,l ∈D} t(ψ, a 1 , . . . , a α-1 , d, a α+1 , . . . , a s ) since (σ d ) x 1 ,...,x k = (σ d ) x 1 ,...,x k = σ x 1 ,...,x k for all d, d ∈ {d i,j,l : i, j, l ∈ D}.
As a corollary: Theorem 6. PLTL ∃ (IPC + ) satisfiability is expspace-complete.

The above reduction does not work if we allow atomic constraints of the form x = y (belonging to IPC ++ ) as in the formula 2 ↓ x =x X2(x = x ) that characterizes models where all the values for x are different. Such a formula is particularly interesting since in cryptographic protocols, nonces, ideally variables that never take twice the same value, are often used to guarantee freshness properties. Hence, this can be specified in PLTL mod with ↓.

We show for PLTL ↓ (IPC + ) a result analogous to Lemma 10. Lemma 11. PLTL ↓ (IPC + ) satisfiability is in expspace.

Proof. Let us reduce in logarithmic space PLTL ↓ (IPC + ) satisfiability to PLTL ∃ (IPC + ) satisfiability. Let φ be a PLTL ↓ (IPC + ) formula with -d 1 < . . . < d n are the constants in φ occurring in constraints of the form

x ∼ d with ∼∈ {<, >, =}, -natural numbers k 1 , . . . , k u occurring in the context of ≡-atomic formulae and their lcm is denoted by K.

The translation t is defined as follows -t(p) = p for p atomic, -t(¬φ 1 ) = ¬t(φ 1 ), t(φ

1 ∧ φ 2 ) = t(φ 1 ) ∧ t(φ 2 ), -t(Xφ 1 ) = Xt(φ 1 ), t(φ 1 Uφ 2 ) = t(φ 1 )Ut(φ 2 ), -t(X -1 φ 1 ) = X -1 t(φ 1 ), t(φ 1 Sφ 2 ) = t(φ 1 )St(φ 2 ), -t(↓ y=X j x φ 1 ) = ∃ y ((y ≡ K X j x) ∧ ( n i=1 ∼∈{<,>,=} (y ∼ d i ) ⇔ (X j x ∼ d i ))) ∧ t(φ 1 )).
It is then easy to show that φ is PLTL ↓ (IPC + ) satisfiable iff t(φ) is PLTL ∃ (IPC + ) satisfiable. We sketch below the main steps of the proof. Given a, b ∈ Z, we write a ≡ φ b def ⇔ a ≡ K b and for all j ∈ {1, . . . , n} and ∼∈ {<, >, =}, a ∼ d j iff b ∼ d j . It is easy to show that (*) for all σ, σ : N × VAR → Z such that for all i ∈ N and x ∈ VAR, σ(i, x) ≡ φ σ (i, x), we have that for every subformula ψ of φ, for every i ∈ N, σ, i |= ψ iff σ , i |= ψ.

The proof is by a simple structural induction. Based on (*), we show again by structural induction that for every σ : N × VAR → Z, for every i ∈ N, for every subformula ψ of φ, σ, i |= ψ iff σ, i |= t(ψ). By way of example, we treat the case with ψ =↓ y=X j x ψ . We have the following equivalences:

-σ, i |= ψ, -σ , i |= ψ where σ equals σ except that σ (l, y) = σ(i + j, x) for all l, -for every σ : N × VAR → Z such that σ equals σ except that σ (l, y) ≡ φ σ(i + j, x) for all l, σ , i |= ψ (by the property (*)), -for every σ : N × VAR → Z such that σ equals σ except that σ (l, y) ≡ φ σ(i + j, x) for all l, σ , i |= ψ ∧ ( n i=1 ∼∈{<,>,=} (y ∼ d i ) ⇔ (X j x ∼ d i ))), -for every σ : N × VAR → Z such that σ equals σ except that σ (l, y) ≡ φ σ(i + j, x) for all l, σ , i |= t(ψ ) ∧ ( n i=1 ∼∈{<,>,=} (y

∼ d i ) ⇔ (X j x ∼ d i ))) (by the induction hypothesis), -σ, i |= ∃ y t(ψ ) ∧ ( n i=1 ∼∈{<,>,=} (y ∼ d i ) ⇔ (X j x ∼ d i ))).
As a corollary: Theorem 7. PLTL ↓ (IPC + ) satisfiability is expspace-complete.

6 Application to the equivalence problem for extended single-string automata

In this section, we characterize the complexity of the equivalence problem for extended single-string automata defined in [LM01, Sect. 5], see other related automata in [START_REF] Bresolin | Time granularities and ultimately periodic automata[END_REF]. This problem is central to check whether two time granularities are equivalent (see also [START_REF] Wijsen | A string based-model for infinite granularities[END_REF]) when granularities are encoded by such automata that can be viewed as Büchi automata recognizing exactly one ω-word. Guards on transitions expressed by integer periodicity constraints and update maps on transitions provide conciseness of such constraint automata. Unlike timed automata, no synchronization between variables is performed and the languages for guards and update maps are quite different, see e.g. [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Bouyer | Are timed automata updatable?[END_REF]. We improve the known expspace upper bound from [START_REF] Lago | Calendars, time granularities, and automata[END_REF] into a pspace upper bound by reducing the equivalence problem to the model-checking problem for PLTL mod -automata. Moreover, we also show the pspace-hardness by reducing QBF.

Let IPC * be the fragment of IPC {∃} containing Boolean combinations of atomic constraints of the form either x ≡ k c or ∃z (x ≡ k z ∧ y ≡ k z). Elements of IPC * will be guards on transitions. An update map g for the variable x i is defined as an expression of the form either x i := x i + c or x i := c with c ∈ Z.

We write UP x 1 ,...,x n to denote the set of update maps that uses variables from {x 1 , . . . , x n }.

An extended single-string automaton A (ESSA) over the finite set of variables {x 1 , . . . , x n } [LM01] is a structure of the form Q, q 0 , v 0 , Σ, δ where -Q is a finite set of states and q 0 ∈ Q (initial state), -v 0 ∈ Z n (initial value of the variables x 1 , . . . , x n ), -Σ is a finite alphabet, -δ ⊆ Q × Σ × Q × ({ } ∪ IPC * ) × P(UP x 1 ,...,x n ) and for every q ∈ Q, 1. either there is a unique u such that q, u ∈ δ, u is of the form a, q , , X , and X contains exactly one update map per variable x i , 2. or there are exactly two u such that q, u ∈ δ, say u 1 and u 2 , and in that case u 1 is of the form a 1 , q 1 , p, X 1 , u 2 is of the form a 2 , q 2 , ¬p, X 2 where p is a constraint in IPC * built over variables in {x 1 , . . . , x n } and in both X 1 and X 2 exactly one update map for x i is present.

Case 1. is subsumed by Case 2. by taking p = . The elements of δ are also denoted by q a,p,X ---→ q (p is the guard and X is the global update map). A configuration is a member q, v ∈ Q × Z n . We define the one-step relation a -→ for a ∈ Σ as follows: q, v a -→ q , v iff there is q, a, q , p, X ∈ δ such that [x 1 ← v 1 , . . . , x n ← v n ] |= p (in IPC ++ ) and for every g ∈ X,

-if g is x i := x i + c then v i = v i + c; -if g is x i := c then v i = c.
It is easy to check that there is exactly one sequence w = a 1 a 2 . . . ∈ Σ ω such that q 0 , v 0 For instance, the ω-word associated with the ESSA below is a 2 n • b ω with initial value 0:

a 1 -→ q 1 , v 1
q 0 , x 0 = 0 q a, x ≡ 2 n 2 n -1, x := 0 a, ¬x ≡ 2 n 2 n -1, x := x + 1 b, , x := 0
Lemma 12. The equivalence problem for ESSA can be solved in pspace.

Proof. Given two ESSA A and A , one can build an LTL(IPC {∃} )-automaton B in polynomial time such that l(B) is non-empty (equivalent to B |= ∃ ) iff w A = w A . Actually l(B) will contain at most one ω-word. The LTL(IPC {∃} )automaton B is indeed a product between A and A . Let A = Q, q 0 , v 0 , Σ, δ and A = Q , q 0 , v 0 , Σ, δ be ESSA over the (disjoint) sets of variables {x 1 , . . . , x n 1 } and {x n 1 +1 , . . . , x n 1 +n 2 }, respectively. We build an LTL(IPC {∃} )-automaton B such that l(B) is non-empty iff w A = w A . We write K to denote the lcm of all the constants k occurring in one of the two input automata in the context of ≡ k . The constructed automaton B has a quite restricted form since the labels on transitions are atomic formulae from LTL(IPC {∃} ).

With each update map g occurring in one of the two input automata, we associate an atomic formula PLTL mod (g) in PLTL mod as follows:

-if g is of the form x i := x i + c, then PLTL mod (g) is equal to Xx i ≡ K x i + c K where c K is the unique element of {0, . . . , K -1} such that c = c K + α × K for some α ∈ Z; -if g is of the form x i := c, then PLTL mod (g) is equal to Xx i ≡ K c K .
Let B = Q , init, F, δ be the LTL(IPC {∃} )-automaton defined as follows:

-Q = (Q × Q ) ∪ {init} and F = Q ; -init φ -→ q 1 ,
q 1 iff the following conditions are verified: • q 0 , a 1 , q 1 , p 1 , X 1 , q 0 , a 2 , q 1 , p 2 , X 2 ∈ δ with a 1 = a 2 (the same letter is read); • φ is the conjunction of the following formulae:

1.

n 1 i=1 x i ≡ K c i where for each i, c i ∈ {0, . . . , K -1} and v 0,i ≡ K c i (initial condition of A); 2. n 2 i=n 1 +1 x i ≡ K c i where for each i, c i ∈ {0, . . . , K-1} and v 0,i-n 1 ≡ K c i (initial condition of A ); 3. g∈X 1 ∪X 2 PLTL mod (g) (synchronization of A and A for update maps); 4. p 1 ∧ p 2 (synchronization of A and A for guards).

-q 1 , q 1 φ -→ q 2 , q 2 iff the following conditions are verified:

• q 1 , a 1 , q 2 , p 1 , X 1 , q 1 , a 2 , q 2 , p 2 , X 2 ∈ δ with a 1 = a 2 ; • φ is g∈X 1 ∪X 2 PLTL mod (g) ∧ p 1 ∧ p 2 .
It is easy to check that B can be built in polynomial-time in the size of A and A . Moreover, l(B) is non-empty iff w A = w A . Let us check this equivalence. Suppose w

A = w A = a 1 • a 2 • a 3 • . . .. The accepting run of A is of the form q 0 , v 0 a 1 ,p 1 ,X 1 -----→ q 1 , v 1 a 2 ,p 2 ,X 2 -----→ q 2 , v 2 . . .
Similarly, the accepting run of A is of the form

q 0 , v 0 a 1 ,p 1 ,X 1 -----→ q 1 , v 1 a 2 ,p 2 ,X 2 -----→ q 2 , v 2 . . .
This leads to the existence of symbolic model accepted by B as described by its run below:

q 0 , q 0 φ mod ∧ V g∈X 1 ∪X 1 PLTL mod (g)∧p 1 ∧p 1 -----------------------→ q 1 , q 1 V g∈X 2 ∪X 2 PLTL mod (g)∧p 2 ∧p 2 -------------------→ q 2 , q 2 . . .
where φ mod is a conjunction of periodicity constraints satisfied by v 0 , v 0 according to the definition of B. A concrete model for this symbolic model can be exactly v

0 , v 0 , v 1 , v 1 , v 2 , v 2 , . . .. Indeed, for all a, b, c ∈ Z, a = b + c im- plies a ≡ K b + c K where c K is the unique member of {0, . . . , K -1} such that c = c K + α × K for some α ∈ Z. So l(B) is non-empty. Now suppose that l(B) is non-empty.
There is a concrete model of the form σ = u 0 , u 0 , u 1 , u 1 , u 2 , u 2 , . . . in l(B) and an accepting run of the form

q 0 , q 0 φ mod ∧ V g∈X 1 ∪X 1 PLTL mod (g)∧p 1 ∧p 1 -----------------------→ q 1 , q 1 V g∈X 2 ∪X 2 PLTL mod (g)∧p 2 ∧p 2 -------------------→ q 2 , q 2 . . . such that -σ, 0 |= φ mod ∧ g∈X 1 ∪X 1 PLTL mod (g) ∧ p 1 ∧ p 1 , -σ, 1 |= g∈X 2 ∪X 2 PLTL mod (g) ∧ p 2 ∧ p 2 , -etc.
Given tuples z, z ∈ Z n 1 +n 2 , we write z ≡ K z def ⇔ for every i ∈ {1, . . . , n 1 + n 2 }, z i ≡ K z i . We extend this definition to models in the natural way. Since K is the lcm of all the integers k occurring in constraints using ≡ k in B, by the Generalized Chinese Remainder Theorem, for every σ = t 0 , t 0 , t 1 , t 1 , t 2 , t 2 , . . . such that for every i ∈ N, we have u i , u i ≡ K t i , t i . σ ∈ l(B). Let us define a model σ 0 as follows. t 0 , t 0 def = v 0 , v 0 and therefore t 0 , t 0 ≡ K u 0 , u 0 . Suppose t i , t i is defined and let us define t i+1 , t i+1 . We update the variables according to the elements of X i+1 ∪ X i+1 . One can easily check that if t i , t i ≡ K u i , u i , then t i+1 , t i+1 ≡ K u i+1 , u i+1 . Consequently, σ 0 ∈ l(B) and

q 0 , t 0 a 1 ,p 1 ,X 1 -----→ q 1 , t 1 a 2 ,p 2 ,X 2 -----→ q 2 , t 2 . . .

is an accepting run of A for some w

A = a 1 • a 2 • a 3 • • • . Similarly, q 0 , t 0 a 1 ,p 1 ,X 1 -----→ q 1 , t 1 a 2 ,p 2 ,X 2 -----→ q 2 , t 2 . . . is an accepting run of A . Consequently, w A = w A .
The above result of pspace upper bound can be extended if in the definition of ESSA, the constraint language IPC * is extended to IPC {∃,[]} . On the model of the above proof, one can show that if σ ∈ l(B) for some LTL(IPC {∃,[]} )automaton and σ ≡ K σ , then σ ∈ l(B). By contrast, adding constraints of the form x = 0 (that are not in IPC {∃,[]} ) would lead to undecidability by reduction from the halting problem for two-counter machines.

On the other side, one can show that the equivalence problem for ESSA is pspace-hard even if -the constraints occurring in transitions are literals (conjunction and disjunction are disallowed) containing atomic constraints of the form x ≡ k c, -the update maps are restricted to either x := x -identity-or x := c (no incrementation, no decrementation), -the only k occurring in ≡ k is 2, -the alphabet Σ is binary (if Σ is unary, then the equivalence problem is trivial). Observe that time granularities are encoded with only three symbols (fill), (gap) and (separator). in [START_REF] Wijsen | A string based-model for infinite granularities[END_REF].

Lemma 13. The equivalence problem for ESSA is pspace-hard.

Proof. We reduce QBF to the equivalence problem for ESSA. Let φ be an instance of QBF of the form below:

∀ x 1 ∃ x 2 . . . ∀ x 2n-1 ∃ x 2n φ m i=1 (l i 1 ∨ l i 2 ∨ l i 3 )
where the l i j 's are literals over the propositional variables in x 1 , . . . , x 2n . We shall define, in logarithmic space in |φ|, an ESSA A such that φ is satisfiable iff w A = a ω . This will lead to the pspace-hardness of the equivalence problem for ESSA since it is easy to design an ESSA B such that w B = a ω . First, we recall in Figure 5 the standard recursive procedure EVAL(ψ, v) to solve QBF. The first argument is a QBF formula and v is an interpretation of propositional variables for a superset of the free variables in ψ.

φ is QBF satisfiable iff EVAL(φ, ∅) returns 1, see e.g. [HU79, Sect. 13.4] where ∅ denotes the empty interpretation. From the execution of EVAL(φ, ∅), we can extract a sequence of the form v 1 , A 1 , . . . , v α , A α , that corresponds to the successive calls to EVAL with the first argument being the formula φ (usually called the matrix of φ) from φ and A i is the value returns by EVAL(φ , v i ). Without any loss of generality, we can assume that each v i belongs to {0, 1} 2n . Observe that v 1 = 0 2n , A α = EVAL(φ, ∅), and v 1 , . . . , v α is a strictly increasing sequence of natural numbers encoded by 2n bits. Moreover, if A i = 0 for some i < α and

v i = b 1 • • • b 2n then v i+1 = b 1 • • • b j-1 10 2n-j
where j is the greatest element of {2, 4, . . . , 2n} such that b j = 0. Similarly, if A i = 1 for some i < α and

EVAL(ψ, v) -if ψ = p, then return v(p); -if ψ = ψ 1 ∧ ψ 2 , then, if EVAL(ψ 1 , v) = 1, then return EVAL(ψ 2 , v), otherwise return 0; -if ψ = ψ 1 ∨ ψ 2 , then, if EVAL(ψ 1 , v) = 1, then return 1, otherwise return EVAL(ψ 2 , v); -if ψ = ¬ψ 1 , then return 1 -EVAL(ψ 1 , v); -if ψ = ∃ p ψ 1 , then if EVAL(ψ 1 , v[p ← 0]) = 1, then return 1, otherwise return EVAL(ψ 1 , v[p ← 1]); -if ψ = ∀ p ψ 1 , then if EVAL(ψ 1 , v[p ← 0]) = 0, then return 0, otherwise return EVAL(ψ 1 , v[p ← 1]);
v i = b 1 • • • b 2n then v i+1 = b 1 • • • b j-1 10 2n-j
where j is the greatest element of {1, 3, . . . , 2n -1} such that b j = 0.

We build an ESSA A simulates the above-mentioned sequence of calls of the form EVAL(φ , v). Let A be the following structure Q, q 0 , v 0 , Σ, δ ; -Q is the union of the following elements:

• {LIT i 1 , LIT i 2 , LIT i 3 : 1 ≤ i ≤ m}, • {rdepth i : 1 ≤ i ≤ 2n} (rdepth i
is reached when we go to recursion depth i), • {0, 1} (i stands for "EVAL(φ, ∅) returns i").

-q 0 = LIT 1 1 and v 0 = 0 2n . -Σ = {a, b}.

-Before defining the transition table δ we need some preliminary definitions.

For every j ∈ {1, . . . , 2n + 1} we write UPD j to denote the following set of update maps:

{x k := x k : 1 ≤ k < j} ∪ {x j := 1} ∪ {x k := 0 : j < k ≤ 2n}.

The set UPD 2n+1 does not modify the values of the variables in {x 1 , . . . , x 2n } and therefore we denote it by ID. We define the map L that translates naturally literals into atomic constraints in the following way: L(x i ) = (x i ≡ 2 1) and L(¬x i ) = (x i ≡ 2 0). The encoding of the structure of φ is done via the following transitions:

• For j = 1, . . . , m, LIT j 1 a,L(l j 1 ),ID -----→ LIT j+1 1 (satisfaction of the clause C j = l j 1 ∨l j 2 ∨l j 3 thanks to the interpretation of l j 1 with the current values of the x i s) and LIT j 1 a,¬L(l j 1 ),ID ------→ LIT j 2 (otherwise, check whether C j is satisfied thanks to l j 2 ). In the case j = m, the former transition is replaced by LIT m 1 a,L(l m 1 ),ID ------→ rdepth 2n-1 (no more clauses need to be satisfied, start the process for reducing the recursion depth).

• For j = 1, . . . , m, LIT j 2 a,L(l j 2 ),ID -----→ LIT j+1 1 and LIT j 2 a,¬L(l j 2 ),ID ------→ LIT j 3 . In the case j = m, the former transition is replaced by LIT m 2 a,L(l m 2 ),ID ------→ rdepth 2n-1 .

• For j = 1, . . . , m, LIT j 3 a,L(l j 3 ),ID -----→ LIT j+1 1 (satisfaction of C j thanks to the interpretation of l j 3 ) and LIT j 3 a,¬L(l j 3 ),ID ------→ rdepth 2n (the clause C j is not satisfied by the current interpretation, start the process for reducing the recursion depth). In the case j = m, the former transition is replaced by LIT m 3 a,L(l m 3 ),ID ------→ rdepth 2n-1 . The following transitions allow to branch to the appropriate recursion depth.

• for j ∈ {3, . . . , 2n}, rdepth j a,x j ≡ 2 1,ID ------→ rdepth j-2 and rdepth j a,x j ≡ 2 0,UPD j --------→ LIT 1 1 . Moreover, for j ∈ {1, 2}, we consider the following transitions: rdepth 1 a,x 1 ≡ 2 0,UPD 1 --------→ LIT 1 1 , rdepth 1 a,x 1 ≡ 2 1,ID ------→ 1, rdepth 2 a,x 2 ≡ 2 0,UPD 2 --------→

LIT 1 1 , and rdepth 2 a,x 2 ≡ 2 1,ID ------→ 0. This part of δ mimicks the constraints between v i and v i+1 described earlier in the proof. By way of example, we present in Figure 6, the ESSA for the QBF formula ϕ below:

∀ x 1 ∃ x 2 ∀ x 3 ∃ x 4 (x 1 ∨ x 2 ∨ x 4 ) ∧ (¬x 1 ∨ x 3 ∨ ¬x 4 ).
Observe that in the ESSA associated with ϕ, only the incoming transitions of LIT 1 1 modify the values of the variables. In order to simplify the figure, for some transition with letter a and set of update maps ID, we have only labelled the transition by the guard. By the way, it is easy to check that ϕ is satisfiable, by showing for instance that the run of the automaton explores the following interpretations of x 1 , x 2 , x 3 , x 4 : 0000, 0001, 0010, 0011, 1000, 1010.

Moreover, the ESSA associated with ϕ is not flat in the sense of [START_REF] Comon | Multiple counters automata, safety analysis and Presburger arithmetic[END_REF][START_REF] Comon | Flatness is not a weakness[END_REF].

LIT 1 1 LIT 1 2 LIT 1 3 LIT 2 1 LIT 2 2 LIT 2 3 rdepth 4 rdepth 2 0 rdepth 3 rdepth 1 1 x 1 ≡ 2 0 x 1 ≡ 2 1 x 2 ≡ 2 0 x 2 ≡ 2 1 x 4 ≡ 2 1 x 4 ≡ 2 0 x 1 ≡ 2 1
x 1 ≡ 2 0

x 3 ≡ 2 0

x 3 ≡ 2 1

x 4 ≡ 2 1 x 4 ≡ 2 0 a, ID, b, ID,

x 3 ≡ 2 1
a, x 3 ≡ 2 0, UPD 3

x 1 ≡ 2 1 a, x 1 ≡ 2 0, UPD 1

x 4 ≡ 2 1 a, x 4 ≡ 2 0, UPD 4

x 2 ≡ 2 1 a, x 1 ≡ 2 0, UPD 2 Fig. 6. ESSA associated with ∀x 1 ∃x 2 ∀x 3 ∃x 4 (x 1 ∨ x ∨ x 4 ) ∧ (¬x 1 ∨ x 3 ∨ ¬x 4 )

Concluding remarks

We have introduced a first-order theory of periodicity constraints IPC ++ whose satisfiability is pspace-complete and a version of LTL with past-time operators whose atomic formulae are constraints from IPC ++ (with comparison of variables at different states). PLTL mod is a very concise logical formalism to deal with periodicity constraints for which model checking and satisfiability are pspace-complete. Furthermore, we have shown that PLTL ∃ (IPC + ) [resp. PLTL ↓ (IPC + )], the fragment PLTL(IPC + ) of PLTL mod extended with the quantifier ∃ [resp. with the freeze operator ↓] is expspace-complete. As an application, we have also proved that the equivalence problem for ESSA introduced in [LM01, Sect. 5] is pspace-complete, even if restricted to two variables.

In Table 1, we recall our main results about LTL and PLTL over periodicity constraints and we indicate how they relate to recent results. Each problem is complete for the corresponding class appearing in the table. At the intersection of a line labeled by a constraint language L and a column labeled by the logical languages L/L , we provide the decidability/complexity status of the satisfiability problem for the logics L(L) and L (L), respectively. Since there is no difference between LTL and PLTL, we provide a unique status. Table 1. Summary

All undecidability results with {xy = c, x = c} are consequences of the fact that LTL over the constraint language allowing atomic constraint of the form x = y and x = y + 1 is undecidable by simulation of two-counter machines [START_REF] Comon | Flatness is not a weakness[END_REF]. The recent results from [DLN05,DG05,LP05] answer to the questions left open in [START_REF] Demri | LTL over integer periodicity constraints (extended abstract)[END_REF] and are evidence that our results are optimal. For instance, PLTL(IPC + ) extended with the freeze operator is expspacecomplete whereas PLTL(IPC ++ ) extended with the freeze operator is already Σ 1 1 -hard. Indeed, LTL({x = y}) with the freeze operator is shown Σ 1 1 -complete in [START_REF] Demri | On the freeze quantifier in constraint LTL: decidability and complexity[END_REF][START_REF] Lisitsa | Temporal logic with predicate λ-abstraction[END_REF] The pspace-completeness of PLTL mod leaves open for which constraint system D (not necessarily fragment of Presburger arithmetic), LTL over D is decidable in pspace. Necessary conditions are provided in [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF] to guarantee the polynomial space upper bound (completion property and frame checking in pspace) and similar conditions are also introduced in [START_REF] Ph | Computational complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning[END_REF][START_REF] Lutz | A tableau algorithm for description logics with concrete domains and GCIs[END_REF]. The question is however open in full generality. In particular, fragments of Presburger arithmetic usually do not satisfy the completion property.

Fig. 1 .

 1 Fig. 1. Standard semantics for IPC ++ constraints

a 2 -

 2 → . . .. The unique ω-sequence generated from the ESSA A is denoted by w A . The equivalence problem for ESSA consists in checking whether w A = w A , given two ESSA A and A . This problem introduced in [LM01] is central to check the equivalence of time granularities when granularities are encoded by such automata. Condition 2. in the definition of the transition relation δ has been introduced in [LM01] (in a slightly different form but equivalent to ours) in order to handle priorities between transitions.

Fig. 5 .

 5 Fig. 5. Standard procedure to solve QBF in polynomial space

  i+1 , there is no configuration of the form LIT 1 1 , v . Moreover, for every i ∈ {1, . . . , α}, if A i = 1, then LIT 1 2n . One can check that if EVAL(φ, ∅) returns 1

  Dem04a, Sect. 7] (with past) [DLN05,LP05] (without past) {xy = c, x = c} Σ

  day ≡ 7 0 ∧ 2(0 ≤ day < 7)∧ 2((min = 59 ∧ sec = 59 ∧ hour = 23 ⇒ Xday ≡ 7 day + 1)∧ 2((min = 59 ∨ sec = 59 ∨ hour = 23 ⇒ Xday = day).-Similarly, one can defined day-in-month, month, and year assuming that there is some end dates. In many practical situations, the problem of in-

	finiteness (for years for instance) can be circumverted by fixing some end date far ahead. Indeed, with PLTL mod formalism this can be done concisely,
	for instance x < 2 n requires only O(n) symbols since the integers are encoded
	with a binary representation.
	-The sentence "φ holds sometime next monday" (where the time unit is the
	second) is encoded by the following conjunction (depending whether the
	current day is monday or not):
	current day is monday	current day is not monday
	p ⇒ pU((¬p ∧ (¬pU(pU(p ∧ φ)))))	∧¬p ⇒ (¬pU(pU(p ∧ φ)))
	with p = day ≡ 7 0. It is easy to see that this can be easily generalized to
	any interval of time (next year, next week, previous year, etc.).
	Calendar logic. In [Ohl94], a calendar logic is introduced and studied in which
	formulae of the form [τ ]φ are interpreted by "for every point of the interval τ ,
	the formula φ holds". The expression τ is called a time term and a peculiarity of
	such logic is to allow time terms at formula positions. The encoding of calendars in PLTL mod allows to translate [τ ]φ into 2(τ ⇒ φ) where τ is a constraint in IPC ++ encoding τ . For instance, consider the statement "if tomorrow's lunch
	time is at noon, I'll ring you" that is formalized in calendar logic [Ohl94] by
	x

day + 1 (noon(x day ) ⊆ lunchtime(x day ) ⇒ ring).

One way to encode this statement in PLTL mod using the forthcoming encoding of Gregorian calendar is the following:

(Xday ≡ 7 day)U( next tick is tomorrow Xday ≡ 7 day + 1 ∧Xφ 0 ) with φ 0 def = (day ≡ 7 XdayU lunch time at noon

  β 1 , . . . , x d ← x j d , β d ] holds true with p ∈ IPC

++

and p has free variables x 1 , . . . , x d whenever [x 1 ← σ (i, x j 1 , β 1 ), . . . , x d ← σ (i, x j d , β d )] |= p in IPC ++ .

  t k , X and σ (i+1) = t 1 , . . . , t k , X then 1. t s+1 , . . . , t k = t 1 , . . . , t k-s (shift of the values of s first variables) 2. X ∩ {s + 1, . . . , k} 2

What is called "IPC" in[START_REF] Toman | DATALOG with integer periodicity constraints[END_REF] is precisely defined by p ::= x ≡ k y + c | x ≡ k c | p ∧ p | ∃x p.

Acknowledgments: Thanks are due to the anonymous referees for their numerous useful suggestions to improve the quality of the paper.

(**) σ , i |= p[x 1 ← x f ( x j 1 ,β 1 ) , . . . , x d ← x f ( x j d ,β d ) ] holds true with p ∈ IPC ++ and p has free variables x 1 , . . . , x d whenever

is IPC ++ satisfiable where IPC ++ (.) is the map defined in Sect. 3.1.

Lemma 8. φ is satisfiable iff there is a structure σ : N → Σ sat φ satisfying (C3) such that σ , 0 |= φ where φ is obtained from φ by replacing every occurrence of X β x α by x f ( x α ,β ) .

The abstraction of PLTL mod models is now satisfactory since the domain of σ in Lemma 8 is finite and it is of exponential cardinality in |φ|.

Büchi automata

Using the approach for LTL reducing model-checking and satisfiability problems to the emptiness problem for Büchi automata [START_REF] Vardi | Reasoning about infinite computations[END_REF], we construct a Büchi automaton A φ on the alphabet Σ φ such that L(A φ ), the language recognized to A φ , is non-empty iff φ is PLTL mod satisfiable. The automaton A φ is defined as the intersection of the following automata.

The Büchi automaton

By Lemma 2, one can check in polynomial time in |φ| whether u u -→ u .

The Büchi automaton A (C3) recognizes the ω-sequences satisfying (C3).

A (C3) is defined as the structure The rest of this section is dedicated to construct A PLTL based on developments from [START_REF] Laroussinie | Temporal logic with forgettable past[END_REF] and on the abstraction introduced in Sect. 4.1. As usual, we define cl (φ), the closure of φ, as the smallest set of formulae such that 1. {φ, X -1 , } ⊆ cl (φ) and cl (φ) is closed under subformulae, 2. cl (φ) is closed under negation (we identify ¬¬ψ with ψ),

Corollary 4. The equivalence problem for ESSA is pspace-complete.

The proof of the pspace upper bound stated in Lemma 12 entails that checking whether w A = w A can be done in time

where n is the number of variables used in A, A and maxsize is the size of the greatest integer k in ≡ k -guards occurring in A, A . Hence, the greatest integer occuring in A, A has value in O(2 maxsize ). Consequently, the parameterized version of the equivalence problem for ESSA is fixed-parameter tractable (FTP) when the parameters are the number of variables and the integers, see e.g. [DF99,DFS99] for definitions and motivations about the parameterized complexity paradigm. However, the proof of Lemma 13 entails that the problem remains pspace-hard when the only integer k in ≡ k -guards occurring in A, A is 2 or when the integers are encoded with a unary representation. Similarly, the problem remains pspace-hard when only two distinct variables are used. Indeed, by following the construction of the proof of Lemma 13, the binary encoding of a first variable encodes a propositional valuation whereas the second variable is used as an auxiliary register to test the nullity of each bit of the first variable. Details are omitted here. By contrast, we are only able to prove the co-np-hardness of the problem restricted to a unique variable. Hence, it is open whether the equivalence problem for ESSA restricted to a unique variable (but without restriction on the size of integers) is pspace-hard.

Another simpler problem which arises when dealing with time granularities, is to find the nth occurrence of a given symbol in a string [START_REF] Lago | Towards compact and tractable automaton-based representations of time granularities[END_REF]Sect. 4]. Here is the definition of the occurrence problem for ESSA: input : An ESSA A, a ∈ Σ and n, m ∈ N (with a binary representation). question Is the nth occurrence of a in w A in position less than m? Theorem 8. The occurrence problem for ESSA is pspace-complete.

Proof. The proof of Lemma 13 entails the pspace-hardness when n, m are encoded with a binary representation. Indeed, φ is not QBF satisfiable iff the first occurrence of b in w A is in position less than (2 8×|φ| × 4 × |φ| 2 ) + 1. In order to establish the pspace upper bound, let us define a nondeterministic algorithm that runs in polynomial space (by Savitch's theorem, we get pspace). Compute on the fly a path starting from the initial configuration of length at most m: at each step we need to remember the current configuration q, v the next one q , v and how many a have been seen so far. Since the length of the path is less than m, encoding of q, v and q , v requires a polynomial amount of bits and the counter for the number of a requires O(log(n)) bits. In order to get a path of length at most m, a counter with O(log(m)) is sufficient. Finally, the one-step relation between q, v and q , v can be checked in polynomial space in the sum of the respective sizes of the configurations.