Nicolas Markey
email: nmarkey@ulb.ac.be

Past is for Free: on the Complexity of Verifying Linear Temporal Properties with Past

We study the complexity of satisfiability and model checking problems for fragments of linear-time temporal logic with past (pltl). We consider many fragments of pltl, obtained by restricting the set of allowed temporal modalities, the use of negations or the nesting of future formulas into past formulas. Our results strengthen the widely accepted fact that "past is for free", in the sense that allowing symmetric past-time modalities does not bring additional theoretical complexity. This result holds even for small fragments and even when nesting future formulas into past formulas.

Introduction

Temporal logics. In 1977, Pnueli introduced temporal logics as a tool for reasoning about concurrent programs [START_REF] Pnueli | The temporal logic of programs[END_REF]. Those logics provide powerful methods for specifying and verifying properties of reactive systems. We refer to [START_REF] Clarke | Model Checking[END_REF][START_REF] Emerson | Temporal and modal logic[END_REF][START_REF] Manna | The Temporal Logic of Reactive and Concurrent Systems: Specification[END_REF][START_REF] Manna | Temporal Verification of Reactive Systems: Safety[END_REF] for more motivations and background.

Linear-time propositional temporal logic (called ltl) is the most used framework in this area: An ltl formula expresses properties about the ordering of events along a run of a system. For instance, the fact that, at all times, a request will eventually be granted can be expressed with:

G (request ⇒ F grant) (S1)
Temporal logics with past. ltl is a pure-future temporal logic, i.e. a logic where modalities only refer to the future of the current state. It is possible, however, to define past-time modalities [START_REF] Kamp | Tense Logic and the Theory of Linear Order[END_REF][START_REF] Gabbay | The declarative past and imperative future: Executable temporal logic for interactive systems[END_REF][START_REF] Lichtenstein | The glory of the past[END_REF]. For example, for expressing that a grant may only occur if some request has been issued, we would write

G (grant ⇒ F -1 request) (S2)
It is well-known that past-time modalities do not increase the expressiveness of ltl [START_REF] Kamp | Tense Logic and the Theory of Linear Order[END_REF][START_REF] Gabbay | On the temporal analysis of fairness[END_REF]. In [START_REF] Gabbay | The declarative past and imperative future: Executable temporal logic for interactive systems[END_REF], Gabbay gives a method for translating ltl+Past formulas into equivalent pure-future ltl formulas. For instance, an equivalent pure-future formula for (S2) would be

¬ (¬request) U (grant ∧ ¬request) (S3)
expressing that we cannot reach a grant without encountering a request in the meantime. By concern of minimality, since they do not add expressive power, past modalities have not been widely studied, and model-checkers such as Spin or Cadence-SMV do not handle ltl+Past specifications. However, over the last few years, past has been more and more studied: Several methods have been proposed for model-checking ltl+Past [START_REF] Vardi | Reasoning about infinite computations[END_REF][START_REF] Kesten | A decision algorithm for full propositional temporal logic[END_REF][START_REF] Gastin | LTL with past and two-way very-weak alternating automata[END_REF][START_REF] Benedetti | Bounded model checking for past LTL[END_REF], and some of them are being implemented.

The benefits of the past. Allowing past-time modalities makes specifications easier and more natural [START_REF] Lichtenstein | The glory of the past[END_REF]. Furthermore, there is a sense in which past really brings more expressive power: there is a succinctness gap between ltl and ltl+Past, i.e. there exists ltl+Past formulas that only have ltl equivalents of exponential size [START_REF] Laroussinie | Temporal logic with forgettable past[END_REF][START_REF] Markey | Temporal logic with past is exponentially more succinct[END_REF]. Finally, since model checking and satisfiability are not more difficult for ltl+Past (pspace-complete in both cases [START_REF] Sistla | The complexity of propositional linear temporal logics[END_REF]), one could argue that ltl+Past should be preferred. These arguments seem to indicate that past is for free. Can this observation be made stronger and more systematic? In this paper, we investigate if this line of argument still holds for different fragments of ltl+Past, in order to characterize fragments that are more expressive but not harder to verify.

Looking for simpler fragments. Pspace-hardness occurs in the general case, but some fragments of ltl+Past have lower complexity (e.g. L + (F , X ) [START_REF] Sistla | The complexity of propositional linear temporal logics[END_REF] or L(F , F -1 ) [START_REF] Etessami | First order logic with two variables and unary temporal logic[END_REF]). Identifying such "simpler" fragments could lead to improved algorithms for special cases, and help understand where the precise boundary lies between hard and easy fragments. Several fragments have already been considered [START_REF] Sistla | The complexity of propositional linear temporal logics[END_REF][START_REF] Demri | The complexity of propositional linear temporal logics in simple cases[END_REF], but not much is known about those with past-time modalities.

Our contribution. We provide a systematic study of fragments of ltl+Past obtained by three kinds of restrictions: on the set of allowed modalities, on the use of negations, and on nesting of past and future modalities. This includes the pure-future fragments. We sum up our results in table 1, on page 8. They rely on a few basic techniques that are used throughout the paper.

Several results are somewhat surprising. The first one is that our simple techniques were sufficient to characterize the exact complexity classes for all the problems we considered: All of them are either npcomplete or pspace-complete. While many people would think that there is no room for model checking problems between np and pspace, the gap is actually quite large and is populated by a few rare model checking problems [START_REF] Laroussinie | Model checking CTL + and FCTL is hard[END_REF][START_REF] Laroussinie | On model checking durational Kripke structures (extended abstract)[END_REF][START_REF] Ph | Oracle circuits for branching-time model checking[END_REF].

We also prove that, in many cases, restrictions on the set of allowed modalities or on the use of negations decrease the theoretical complexity of verification problems. This means that there are many fragments for which specialized algorithms could be more efficient than classical ones.

Concerning past-time modalities, it should be remarked that if a given future modality is allowed, adding its symmetric past-time modality does not increase the complexity. Moreover, allowing or disallowing the nesting of future modalities in the scope of past modalities does not change the complexity of the verification problems. To sum up, past comes with no extra cost.

Last, we remark that, in some (positive) fragments, existential and universal problems may have different complexities. This had probably not been remarked by Sistla and Clarke when they erroneously claim (in [START_REF] Sistla | The complexity of propositional linear temporal logics[END_REF]) that validity of L + (F , X ) is conp-complete, when it is in fact pspace-complete.

Related work.

As regards fragments of ltl+Past, Ramakrishna et al. [START_REF] Ramakrishna | An automata-theoretic decision procedure for propositional tem-poral logic with Since and Until[END_REF] studied lusat, the fragment of ltl+Past with only U and S , and they provide an optimal (pspace) automata-theoretic algorithm for model checking with this fragment. Other fragments of ltl (with no past) are addressed in [START_REF] Demri | The complexity of propositional linear temporal logics in simple cases[END_REF], namely fragments obtained by bounding the temporal height and the number of atomic propositions of formulas. Branching-time temporal logics with past have been investigated in [START_REF] Kupferman | Once and for all[END_REF][START_REF] Laroussinie | A hierarchy of temporal logics with past[END_REF].

Outline of the paper. In the sequel, we first formally define the structures, logics and problems under study, and sum up our results. We prove np-completeness results in section 2, and pspace-completeness results in section 3. We summarize our study and conclude in section 4.

1 pltl: Linear Temporal Logic with Past Syntax of pltl. Let AP = {P 1 , P 2 , . . .} be a countable set of atomic propositions. We define the syntax of pltl as follows:

pltl ∋ φ, ψ ::= ψ ∨ φ | ¬φ | X φ | ψ U φ | X -1 φ | ψ S φ | P 1 | P 2 | . . .
where U reads "until", S reads "since", X is "next" and X -1 is "previous".

Some very useful abbreviations are commonly defined: ⊤ ≡ P 1 ∨ ¬P 1 , ⇒, ⇔... As regards temporal modalities, we will use the classical F (eventually) and G (always), as well as their past counterparts F -1 φ ≡ ⊤ S φ and G -1 φ ≡ ¬F -1 ¬φ, read "eventually in the past" and "always in the past" respectively.

Modalities S , X -1 , F -1 and G -1 are called "past modalities", while U , X , F , G are "future modalities". Subformulas, temporal height and size of a formula. Given a formula Φ ∈ pltl, the set of its subformulas, denoted by sf(Φ), is defined inductively as follows:

sf(P ) = {P } for all P ∈ AP sf(¬φ) = {¬φ} ∪ sf(φ) sf(φ ∨ ψ) = {φ ∨ ψ} ∪ sf(φ) ∪ sf(ψ) sf(X φ) = {X φ} ∪ sf(φ) sf(φ U ψ) = {φ U ψ} ∪ sf(φ) ∪ sf(ψ) sf(X -1 φ) = {X -1 φ} ∪ sf(φ) sf(φ S ψ) = {φ S ψ} ∪ sf(φ) ∪ sf(ψ)
Obviously, the number of subformulas is bounded by the size (i.e. the number of symbols) of the formula. The closure of the formula Φ, written sf(Φ), is the least set containing sf(Φ) and stable under negation. It contains at most twice as many formulas as sf(Φ).

The temporal height of a formula Φ ∈ pltl, for a given set M of modalities, is defined recursively as follows:

h M (P ) = 0 h M (¬φ) = h M (φ) h M (φ ∨ ψ) = max(h M (φ), h M (ψ))
and, for any modality O of arity p,

h M (O(φ 1 , . . . , φ p )) = max(h M (φ 1 ), . . . , h M (φ p )) + 1 if O ∈ M 0 otherwise
The temporal height of a formula is its temporal height for the set of all modalities. The past temporal height is the temporal height for the set of past-time modalities. The temporal height is obviously bounded by the size of the formula.

Semantics. Formulas of pltl are interpreted over paths. A path is a pair (π, ξ) in which π is an infinite sequence of states π(0), π(1), ... and ξ is a mapping from {π(0), π(1), . . . , π(n), . . .} → 2 AP . This way, the states of π are labelled with atomic propositions.

Given a path (π, ξ), a natural i and a formula φ, we inductively define the relation1 (π, ξ), i |= φ (read "φ holds at position i along (π, ξ)") as follows:

π, i |= P iff P ∈ ξ(π(i)), π, i |= φ ∧ ψ iff π, i |= φ and π, i |= ψ, π, i |= ¬φ iff π, i |= φ, π, i |= X φ iff π, i + 1 |= φ, π, i |= ψ U φ iff there exists some j ≥ i s.t. π, j |= φ and for all i ≤ k < j, π, k |= ψ, π, i |= X -1 φ iff i > 0 and π, i -1 |= φ, π, i |= ψ S φ
iff there exists some j ≤ i s.t. π, j |= φ and for all j < k ≤ i, π, k |= ψ.

Equivalence of formulas. Two formulas are (globally) equivalent over a class Π of paths (which we denote φ ≡ Π ψ) if for any path π ∈ Π and any integer i, the equivalence π, i |= φ ⇔ π, i |= ψ holds. The formulas are initially equivalent over Π (φ ≡ Π i ψ) if for all paths π ∈ Π, π, 0 |= φ ⇔ π, 0 |= ψ is true. We omit Π when the equivalence has to hold along all paths in (2 AP ) N .

Obviously, two equivalent formulas are initially equivalent. The converse does not hold. For instance, P 1 S P 2 and P 2 are initially equivalent, but they clearly are not globally equivalent.

A formula φ is said to be initially (resp. globally) valid over Π if it is initially (resp. globally) equivalent to ⊤ over Π. It is initially (resp. globally) satisfiable over Π if its negation is not initially (resp. globally) valid over Π. This means that there exists a path π ∈ Π (resp. a path π ∈ Π and a position i along that path) such that π, 0 |= φ (resp. π, i |= φ).

These definitions formalize the results we mentioned about expressive power in the introduction: that pltl is as expressive as ltl [START_REF] Kamp | Tense Logic and the Theory of Linear Order[END_REF][START_REF] Gabbay | On the temporal analysis of fairness[END_REF][START_REF] Gabbay | The declarative past and imperative future: Executable temporal logic for interactive systems[END_REF] means that for any pltl formula, there exists an initially equivalent ltl formula. The exponential succinctness gap in [START_REF] Laroussinie | Temporal logic with forgettable past[END_REF] can be expressed as follows: there exists a sequence of pltl formulas (φ n ), s.t. |φ n | ∈ O(n), and for which any sequence of initially equivalent ltl formulas (ψ n ) verifies that |ψ n | ∈ Ω(2 n ).

Verification problems. In this paper, we are concerned with the following problems:

-Initial satisfiability and validity, as defined above; -Universal model checking, i.e. is initial validity over a given set Π of paths; -Existential model checking, i.e. initial satisfiability over a given set Π of paths.

Note that we only study "initial" problems, since these are the most interesting ones as regards verification. Moreover, in the general case, initial problems and their global counterparts are interreducible: for instance, a formula φ is globally satisfiable if, and only if, F φ is initially satisfiable, and conversely, φ is initially satisfiable if, and only if, G -1 F -1 φ is globally satisfiable.

Kripke Structures. For model checking, the set Π is often defined through a Kripke Structure (KS for short), that is, a 4-tuple K = (Q, Q 0 , l, R) in which Q is a finite set of states, Q 0 is the set of initial states, l ∈ (2 AP ) Q indicates the propositions that are true in each state of Q, and R ⊆ Q × Q is a total relation representing the set of allowed transitions. The size of K, which we denote |K|, is |Q| + |R|. A KS generates a set Π of infinite paths in the obvious way.

It should be remarked right now that, in the general case, both model checking problems are dual: indeed, there exists a path satisfying a formula φ if, and only if, it is not the case that every path satisfies the negation of φ. But this equivalence only holds for fragments allowing negation.

Loops. A path (π, ξ) is said to be ultimately periodic if there exist two integers m and p, with p > 0, such that for any integer n ≥ m, π n = π n+p . Such a path can be finitely represented by a loop, that is a deterministic KS, or, equivalently, by a couple of finite words (u, v) over the alphabet 2 AP , where |u| = m and |v| = p. The path correponding to a loop L = (u, v), which we denote by π L , is uv ω . The type of a loop (u, v) is (|u|, |v|). The size of a loop of type (m, p) is the integer m + p. The size of an ultimately periodic path π is the size of the smallest loop encoding that path2 . Subpath, subloop. Given a path (π, ξ), a subpath is a path (π ′ , ξ |π ′ ) where π ′ is a subsequence of π. We equivalently say that π ′ is a subpath of π, or that π contains π ′ . If π ′ is a subpath of π, there exists an increasing function f such that, for all i, π ′ i = π f (i) . We will write π ′ ⊑ f π when we need the function f . Otherwise, we simply write π ′ ⊑ π.

In the same way, given a loop L, a subloop is a loop L ′ whose associated path is a subpath of the path associated to L. We also write L ′ ⊑ L in that case. Note that a subloop could be bigger than its original loop. For instance, from the loop (ε, ab) (where ε is the empty word), whose size is 2, we can extract the loop (aaba, aab), whose size is 7.

Let L = (u, v) be a loop. We say that a subloop L ′ = (u ′ , v ′ ) of L is acceptable, and we write L ′ L, whenever u ′ is a subpath of u and v ′ a subpath of v. The size of an acceptable subloop is always lower than or equal to the size of the original loop.

Fragments of pltl. We consider three types of restrictions: first of all, restrictions about the allowed modalities. For denoting the fragment of ltl where only M 1 , . . . , M p are allowed, we use the classical notation L(M 1 , . . . , M p ). For instance, L(F ) is the logic where F is the only allowed temporal modality 3 . The second restriction we deal with affects negations: we write L + (F , X ), for example, for the logic where the only modalities are F and X , and where modalities can not occur in the scope of a negation. Last, a formula is said to be stratified if it has no future modality in the scope of past modalities [START_REF] Manna | Completing the temporal picture[END_REF]. Sets of stratified formulas are denoted by L s (. . .). We write L + s (F , S ) when combining restrictions about negation and stratification.

For example,

F (a ∧ G -1 (b ∨ F c)) lies in L + (F , G -1 ), but it is not stratified. It is initially equivalent to (b ∨ F c) U (a ∧ (b ∨ F c)), which is in L + ( U ). And it is globally equivalent to F (a ∧ (F c ∨ G -1 b ∨ b S c)), which belongs to L s (F , S ).
Our results. In the sequel, we get the following results:

Exist. MC Univ. MC Satisf. Validity L + (F ),L + (G ),L + (X ) np-c. conp-c. np-c. conp-c. L + (F , X ) (np-c.) pspace-c. (np-c.) pspace-c. 4 L + (G , X ) pspace-c. conp-c. pspace-c. conp-c. L + s (F , X -1 ) np-c. pspace-c. np-c. pspace-c. L + s (G , X -1 ) pspace-c. conp-c. np-c. conp-c. L + (F , X , F -1 , X -1 ) np-c. pspace-c. np-c. pspace-c. L + (G , X , G -1 , X -1 ) pspace-c. conp-c. pspace-c. conp-c. L + s (G , S , X -1 ) pspace-c. pspace-c. np-c. pspace-c. L + (G , S , X -1 ) pspace-c. pspace-c. np-c. pspace-c. L(X , S , X -1 ) np-c. conp-c. np-c. conp-c. L(F , F -1 ) np-c. conp-c. np-c. [10] conp-c. L + s (F , S ) pspace-c. pspace-c. pspace-c. conp-c. L + s (G , S ) pspace-c. pspace-c. np-c. pspace-c. L + (G , S ) pspace-c. pspace-c. np-c. pspace-c. L + ( U ) pspace-c. pspace-c. pspace-c. conp-c. L + ( U , S ) pspace-c. pspace-c. pspace-c. conp-c. pltl (pspace-c.) (pspace-c.) (pspace-c.) (pspace-c.)
Table 1: Complexity of pltl verification

The results in bold are proved in this paper, the ones in parentheses were proved in [START_REF] Sistla | The complexity of propositional linear temporal logics[END_REF], and the other ones are corollaries, deduced by inclusion or duality. For instance, existential model checking for L + s (F , X -1 ) is np-complete since it is a subcase of existential model checking for L + (F , F -1 , X , X -1 ), and since it is more general than existential model checking for L + (F ). pspace-completeness of validity for L(F , X ) comes by duality from pspace-completeness of satisfiability for L + (G , X ). It should be remarked that X is selfdual (since we consider infinite paths) but X -1 is not: for example, the argument above for validity of L(F , X ) cannot be applied to L + s (F , X -1 ).

NP-complete problems

In this section, we first prove that verifying any non-trivial fragments of pltl is at least np-hard. "Non trivial" means fragments allowing at least one future modality. For "trivial" fragments, model checking problems amount to evaluating a boolean formula, which is alogtime-complete [START_REF] Buss | Algorithms for boolean formula evaluation and for tree contraction[END_REF], and satisfiability and validity are the classical satisfiability and validity problems for boolean formulas, which are (co)np-complete.

We then provide np algorithms for several fragments of pltl, which therefore are np-complete.

np-hardness of verifying linear temporal properties

Our first result is a small extension of a result given in [START_REF] Sistla | The complexity of propositional linear temporal logics[END_REF]:

Theorem 1. For L + (F ), L + (G ) and L + (X ), the existential model checking problem is np-hard.
Proof. -We adapt Sistla and Clarke's proof [START_REF] Sistla | The complexity of propositional linear temporal logics[END_REF] of np-hardness for model checking L(F ). To a 3-sat instance i j α i,j , where the α i,j are literals on {x 1 , x 2 , . . . , x n }, we associate the following KS:

x 1 x 1 x 2 x 2
x n

x n

To one path in that structure corresponds one valuation of the variables x i : Variable x i is evaluated to true if, and only if, the path runs through state x i . Satisfiability of our 3-sat instance is equivalent to the existence of a path verifying i j F α i,j in the above KS. -in the same way, satisfiability of i j α i,j is equivalent to the existence of a path satisfying i j G ¬(α i,j ) in the same structure. -for L + (X ), our 3-sat instance i j α i,j is satisfiable if, and only if, the above KS contains a path verifying i j X 2n(α i,j )-1 α i,j , where n(

x k ) = n(x k ) = k.
By duality (since, for instance, verifying that "all paths satisfy a formula φ ∈ L + (F )" amounts to verifying that "there does not exist a path satisfying ¬φ", with ¬φ ∈ L + (G )), we get Theorem 2. Universal model checking for fragments L + (G ), L + (F ) and L + (X ) is conp-hard.

np-easy problems

What we saw in the previous section entails that any non-trivial verification problem concerning linear temporal logics is np-hard. We know from [START_REF] Sistla | The complexity of propositional linear temporal logics[END_REF] that this lower bound is optimal for L(F ) and L + (F , X ), that is, the satisfiability and (existential) model checking problems for these logics are np-complete. In this section, we prove np-easiness of satisfiability for four other fragments: L(X , X -1 , S ), L(F , F -1 ), L + (F , F -1 , X , X -1 ), and L + (G , S ). These results carry on to existential model checking, except for L + (G , S ), which we will prove is pspace-complete.

We systematically use the small witness method in order to do this, consisting in -providing a polynomial time algorithm for verifying that an ultimately periodic path may be checked in polynomial time against any pltl formula; -showing that the fragments listed above have the "polynomial witness property", i.e. if a formula is satisfiable, it is satisfiable along a polynomial size ultimately periodic path. This obviously gives an np-algorithm for satisfiability: First guess an ultimately periodic witness, and then check it. In several cases, this technique also provides a proof for np-easiness of the model checking problems: Indeed, we show that, for some fragments, we can add arbitrary states in the polynomial witness, which ensures that we can find a polynomial witness in the KS under study. In these cases, the algorithm for existential model checking is as follows: First pick the candidate witness in the Kripke structure, and check that it satisfies the formula. For a deterministic KS, the ctl model checking algorithm [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching time temporal logic[END_REF][START_REF] Clarke | Automatic verification of finitestate concurrent systems using temporal logic specifications[END_REF] can be applied to ltl formulas too, since path quantification will always refer to the only possible execution. This simple approach does not extend to the problem of checking whether a loop satisfies a pltl formula: In a loop, future is deterministic but past is not, since the first state of the periodic part has two predecessors. The following lemma gives a way to overcome that problem 5 . Lemma 4. Let φ be a pltl-formula. For any loop L of type (m, p), for all k ≥ m + h P (φ)p,

π L , k |= φ iff π L , k + p |= φ.
This lemma indicates that, after some initial fluctuations, a state of the periodic part always satisfies the same subformulas, irrespective of how many times the periodic part has been traversed.

Proof. The proof is by induction on the structure of the formula φ:

-for φ = P , φ = ¬φ 1 and φ = φ 1 ∨ φ 2 , the result is obvious;

-if φ = X φ 1 or φ = φ 1 U φ 2 ,

we can apply the induction hypothesis

to states occurring after the k-th one.

-if φ = X -1 φ 1 , then since k -1 ≥ m + (h P (φ 1 ) + 1)p -1 ≥ m + h P (φ 1 )p, by induction hypothesis, we get the equivalence π L , k -1 |= φ 1 ⇔ π L , k -1 + p |= φ 1 . Thus π L , k |= X -1 φ 1 ⇔ π L , k + p |= X -1 φ 1 ; -if φ = φ 1 S φ 2 , we have h P (φ) = max(h P (φ 1 ), h P (φ 2 ))+1. Suppose that π L , k |= φ. There exists some k ′ ≤ k s.t. π L , k ′ |= φ 2 , and for k ′ < l ≤ k, π L , l |= φ 1 .
Two cases may arise:

-if k ′ < kp, then we know that the states from π k-p to π k satisfy φ 1 . By induction hypothesis, so do the states from π k to π k+p . Thus, π L , k + p |= φ, since π L , k ′ |= φ 2 and all the states between π k ′ +1 and π k+p satisfy φ 1 ; -otherwise, k ′ ≥ kp ≥ m + h P (φ 1 )p, and the induction hypothesis directly applies to the states between π k ′ and π k . Thus π L , k |= φ ⇒ π L , k + p |= φ. The reverse implication may be proved similarly.

Corollary 5. Model-checking pltl over a loop can be done in polynomial time.

Proof. Given a loop L of type (m, p) and a pltl-formula ψ, we use dynamic programming in order to compute which subformulas of φ are true in the different states of the path π L . For this purpose, we apply the following labelling algorithm:

-First unwind the periodic part of the loop h times with h greater than h P (φ). This gives a loop of type (m + hp, p). -Then label that loop with the subformulas in sf(φ) inductively, according to the following rules:

-If φ is an atomic proposition P , label the state k with P if, and only if, P ∈ l(k), -For boolean combinations, as well as for X -and U -modalities, use the classical ctl labelling algorithm, -For a formula φ = X -1 φ 1 , whenever a state i is labelled with φ 1 , then label state i + 1 (if it exists) with φ. -For a formula φ = φ 1 S φ 2 , if a state i is labelled with φ 2 , then label it with φ. Else if state i -1 has been labelled with φ and state i has been labelled with φ 1 , then label state i with φ.

This algorithm runs in time O(|L| 2 •|φ| 2 ). It can easily been proved, using Lemma 4, that a state is labelled with the set of subformulas it satisfies.

2.2.2

Looking for ultimately periodic paths. We recall the existence of an ultimately-periodic witness for any satisfiable formula of pltl [START_REF] Sistla | The complexity of propositional linear temporal logics[END_REF]. Theorem 6. A pure-future formula φ ∈ ltl is satisfiable if, and only if, it is satisfiable in a loop. A Kripke structure K "existentially" satisfies a formula φ if, and only if, it contains an ultimately-periodic path satisfying φ. These results also hold for pltl formulas.

Proof. For L( U , X , S ), the first statement is shown in [START_REF] Sistla | The complexity of propositional linear temporal logics[END_REF]. The second one can be shown by a classical reduction from model checking to satisfiability (see [32, lemma 4.3]): Given a KS K = (Q, Q 0 , l, R) and a formula φ, we add a new atomic propositions P q for each q ∈ Q. We define the following formulas (we will use them several times in the sequel):

ψ state = q∈Q P q ∧ q∈Q (P q ⇒ ¬( q ′ =q P q ′ ) ψ label = q∈Q P q ⇒ ( p∈l(q) p ∧ p ′ / ∈l(q)
¬p)

ψ trans = q∈Q (P q ⇒ q ′ s.t. (q,q ′ )∈R X P q ′ )
The first formula ensures that exactly one "state" proposition is true at a time, the second one means that atomic propositions labelling that state are true, and the third one means that transitions are respected. Now, the formula

φ = q 0 ∈Q 0 P q 0 ∧ G ψ state ∧ G ψ label ∧ G ψ trans ∧ φ
is satisfiable if, and only if, K contains a path starting from q 0 along which φ is true. But if φ is satisfiable, it is satisfiable along an ultimately-periodic path. This path witnesses the existence of an ultimately-periodic path in K along which φ is true.

The result is extended to pltl thanks to the following Theorem:

Theorem 7 ( [START_REF] Kamp | Tense Logic and the Theory of Linear Order[END_REF][START_REF] Gabbay | The declarative past and imperative future: Executable temporal logic for interactive systems[END_REF]). For any pltl formula φ, there exists a boolean combination of pure-future and pure-past formulas which is initially equivalent to φ.

2.2.3 np-easy fragments. Lemmas 8 to 12 are four technical lemmas that directly entail the polynomial witness property for several pltl fragments. They prove np-easiness of satisfiability or validity for these fragments. Some of them also entail np-easiness of model checking.

Lemma 8. The truth of an L(X , X -1 , S )-formula φ in the initial state of a path π only depends on the first h X (φ) states of π.

This result is obvious.

Lemma 9. Let φ ∈ L(F , F -1
), and L be a loop s.t. π L , i |= φ for some integer i. Then there exists an acceptable subloop L ′ L, whose size is polynomial in |φ|, containing π i , and s.t. any acceptable subloop

L ′′ s.t. L ′ L ′′ f L satisfies π L ′′ , f -1 (i) |= φ.
This lemma means that a path satisfying an L(F , F -1 ) formula has polynomialy many "important" states, the other states being removable.

Proof. We suppose that the loop L is of type (m, p), and that, for some i, π L , i |= φ. We write h = h P (φ).

For each subformula of φ of type F -1 ξ, if there exists a position where ξ is satisfied, then we know (from Lemma 4) that there is one lower than m + hp. In this case, we write

i F -1 ξ = min{i | π L , i |= ξ}
The same holds for subformulas of type F ξ: if there exists a state satisfying ξ, we write

i F ξ = max{j ∈ 0; m + hp -1 | π L , j |= ξ}
For each F -or F -1 -subformula ψ, we define j ψ to be either equal to i ψ if i ψ ≤ m, or congruent to i ψ modulo p and between m and m + p -1 otherwise. We define L ′ to be the acceptable subloop of L built by keeping states j ψ for all F -and F -1 -subformulas ψ of φ. We also add the current state π i . The acceptable subloop L ′′ is defined from L ′ by possibly inserting some other states of L. We let f be the function s.t. π L ′′ f π L . Remark that -L ′′ has type (m ′′ , p ′′ ) with m ′′ ≤ m and p ′′ ≤ p, unwind the loop select the states you want to keep create the corresponding acceptable subloop

a b c d e f g a b c d e f g c ′ d ′ e ′ f ′ g ′ c ′′ d ′′ e ′′ f ′′ g ′′ a b c d e f g c ′ d ′ e ′ f ′ g ′ c ′′ d ′′ e ′′ f ′′ g ′′ a c e f Figure 1 Construction of L ′ -f (m ′′ ) ≤ m ≤ f (m ′′ + 1), -for all k, f (m ′′ + kp ′′ ) ≤ m + kp ≤ f (m ′′ + kp ′′ + 1).
The example shown on Figure 1 explains this construction. We now have to prove that this construction is correct. For this, we show that

∀ψ ∈ sf(φ), ∀j ∈ N, π L ′ , j |= ψ ⇔ π L , f (j) |= ψ.
We prove this by induction on the structure of ψ:

-for atomic propositions and boolean combinations, the result is straightforward; -if ψ = F ψ 1 , suppose that for some j, π L ′ , j |= F ψ 1 . Then for some state j ′ ≥ j, we have π L ′ , j ′ |= ψ 1 . By ind. hyp. and since f is increasing, we get a state f (j

′ ) ≥ f (j) s.t. π L , f (j ′ ) |= ψ 1 , and π L , f (j) |= F ψ 1 .
Conversely, if we suppose that π L , f (j) |= F ψ 1 , then there exists a state j ′ ≥ f (j) s.t. π L , j ′ |= ψ 1 . Two cases may arise:

-either j ′ ≤ m + hp -1, then we have j ′ ≤ i F ψ 1 . By ind. hyp. we get that π L ′ , f -1 (i F ψ 1 ) |= ψ 1 , and since f is increasing, we have f -1 (i F ψ 1 ) ≥ j. -or j ′ ≥ m + hp. In that case, Lemma 4 ensures that there exists a state k satisfying ψ 1 s.t. k is between m + (h -1)p and m + hp -1. Then k ≤ i F ψ 1 , and π L ′ , f -1 (i F ψ 1 ) |= ψ 1 . The remark above ensures that f -1 (i F ψ 1 ) lies between m ′ +(h-1)p ′ and m ′ + hp ′ . Since Lemma 4 also applies to L ′ , we get that for all l ≥ 0,

π L ′ , f -1 (i F ψ 1 ) + lp ′ |= ψ 1 . Thus for all m, π L ′ , m |= F ψ 1 , especially for m = j. -if ψ = F -1 ψ 1 , the proof is similar. Lemma 10. Let φ ∈ L + (F , F -1 , X , X -1
) be a satisfiable formula, and L a loop s.t. π L , i |= φ for some integer i. Then there exists an acceptable subloop L ′ of L, whose size is polynomial in |φ|, containing π i , and s.t. any loop L ′′ for which

L ′ L ′′ f L satisfies π L ′′ , f -1 (i) |= φ.
Proof. The proof is similar to the proof of Lemma 9: we first unwind the loop h P (φ) times. Then, by induction on the structure of the formula, we build a set S of "witness states". At each step, we prove that

∀j ≤ m + h P (φ) • p, ∀ψ ∈ sf(φ), (j, ψ) ∈ S ⇒ π L , j |= ψ (1)
-initially, S contains {(i, φ)}. The property ( 1) is satisfied by hypothesis; -while S contains pairs of the form (j, ψ) where ψ is not (a negation of) an atomic proposition, we remove (j, ψ) from S, put it in T and -if ψ = α ∨ β, then either π L , j |= α or π L , j |= β. We add (j, α) or (j, β) to S in order to keep (1) true; -if ψ = α ∧ β, then add (j, α) and (j, β) to S;

-if ψ = X α, then add (j + 1, α) (or (j + 1 -p, α) if j + 1 > m + h P (φ) • p) to S; -if ψ = X -1 α, then add (j -1, α) to S. We know that j ≥ 1 since π L , j |= X -1 α.
Thus (1) still holds; -if ψ = F α, we know that α is true in some state k greater than j and smaller than m + (h(φ) + 1)p. If k is greater than m + h(φ)p + 1, then we can substract p in order to remains lower than m + h(φ)p + 1 to Lemma 4). Thus we add (k, α) to S, so that (1) is still satisfied; -if ψ = F -1 α, the argument is the same. This process clearly ends, since the sum of sizes of formulas in S decreases at each step. Moreover, |S ∪ T | ≤ |φ| at the end. Now consider the acceptable subloop L ′ of L containing the states we kept in S ∪ T . We also possibly add some other states (this construction is the same as the one shown in Figure 1). We write f for the function s.t. π L ′ f π L . The remarks of the previous proof still apply. Then π L ′ , f -1 (i) |= φ.

Indeed, we prove that, for any (j, ψ) ∈ T ∪S, we have π L ′ , f -1 (j) |= ψ: clearly, for each (j, ψ) in S, we have π L ′ , f -1 (j) |= ψ since ψ is an atomic proposition. For (j, ψ) ∈ T , several cases may arise:

-if ψ = α ∨ β, then either (j, α) or (j, β) is in T ∪ S, and the result comes by ind. hyp., -if ψ = α ∧ β, then (j, α) and (j, β) are in T ∪ S, and the result also comes from the ind. hyp.,

-if ψ = X α, then (j + 1, α) (or (j + 1 -p, α)) is in T ∪ S.
In the first case, the result is immediate. In the second case, it comes from Lemma 4, -for the other modalities F ,F -1 and X -1 , the argument is the same.

This proof can easily be adapted to L + (F , X , F -1 , ¬X -1 ¬), where ¬X -1 ¬ is the dual modality of X -1 . Indeed, we simply have to handle that dual modality slightly differently, by differentiating the case when j = 0 and the other cases when building S. By duality from this remark, we get a conp algorithm for universal model checking and validity for L + (G , X , G -1 , X -1 ).

Lemma 11. Let φ ∈ L + (G , S , X -1 ), π a path and a a state. Then

-If a ω , 0 |= φ, then for all i, a ω , i |= φ; -If π, 0 |= φ, then (π 0 ) ω , 0 |= φ.
Proof. We use structural induction once again: Assume that a ω , 0 |= φ. Then:

-If φ is an atomic proposition, a conjunction or a disjunction, the result is obvious;

-If φ = G ψ, then a ω , 0 |= ψ. induction hypothesis, a ω , i |= ψ
for all i, and a ω , i |= φ for all i; -If φ = ψ 1 S ψ 2 , then a ω , 0 |= ψ 2 . By induction hypothesis, all position i satisfy ψ 2 along a ω , and a ω , i |= φ for all i;

-If φ = X -1 ψ, we cannot have a ω , 0 |= φ.
The second statement is proved in the same way: We assume that π, 0 |= φ, and prove that (π 0 ) ω , 0 |= φ:

-It is obvious for atomic propositions and positive boolean combinations; -If φ = G ψ, then π, 0 |= ψ. By induction hypothesis, (π 0 ) ω , 0 |= ψ, and the first statement of the lemma ensures that for positions i, (π 0 ) ω , i |= ψ. Hence the result; -If φ = ψ 1 S ψ 2 , the same arguments apply; -The case when φ = X -1 ψ is trivial, as previously.

Lemma 12. Let φ ∈ L + ( U , S ). For all path π and for all state s, we have -if for some i, s ω , i |= φ, then for all i, s ω , i |= φ; -if for some i, π, i |= φ, then for all j, (π i ) ω , j |= φ.

Thus a non-valid L + ( U , S )-formula has a small counterexample, and validity for that fragment is conp-complete.

Proof. We begin with the first statement, by induction:

-For atomic propositions, or (positive) boolean combinations of subformulas, the result is obvious;

-If φ = φ 1 U φ 2 , then s ω , i |= φ entails that s ω , i |= φ 2 . By induction,
for all j, s ω , j |= φ 2 , and φ cannot be satisfied along s ω ; -A similar argument may be used if φ = φ 1 S φ 2 .

We prove the second part of the lemma in the same way:

-It is obvious for atomic propositions, as well as for conjunctions or disjunctions;

-If φ = φ 1 U φ 2 , then π, i |= φ entails that π, i |= φ 2 . By induc- tion, (π i ) ω , i |= φ 2 ,
and the first part of the lemma ensures that (π i ) ω , j |= φ 2 for all j. Hence (π i ) ω , j |= φ for all j; -In the same way, when φ = φ 1 S φ 2 , then (π i ) ω , i |= φ 2 , then (π i ) ω , j |= φ 2 for all j, and (π i ) ω , j |= φ for all j.

Theorem 13. Satisfiability and existential model checking are npcomplete for L(X , S , X -1 ), L(F , F -1 ), L + (F , F -1 , X , X -1 ), and for their non-trivial fragments.

Validity is conp-complete for L + ( U , S ) and its non-trivial fragments.

Satisfiability is np-complete for L + (G , S , X -1 ) and its non-trivial fragments.

np-easiness is a direct consequence of the previous results. nphardness was proved in Section 2.1. These results are summarized in the table on page 8.

PSPACE-complete problems

In this section, we prove pspace-hardness of verification problems for several fragments of pltl.

The proofs are reductions from two tiling problems we now define: Let C be a finite set of colors. A domino-type is a 4-tuple d up , d down , d left , d right of colors of C. Given a set T ⊆ C 4 of dominotypes, and two integers m and n, tiling the m × n-grid amounts to finding a function f :

[1, m] × [1, n] → T s.t. ∀(i, j) ∈ [1, m -1] × [1, n], f (i, j) right = f (i + 1, j) left ∀(i, j) ∈ [1, m] × [1, n -1], f (i, j) up = f (i, j + 1) down
We consider the following tiling problem, which is a slightly modified version of [14, prob. B 2 ]:

Given a set T of domino-types, a natural m (in unary), and two colors c 0 and c 1 of C, does there exist a natural n s.t. the m × n-grid can be tiled, with the additional conditions that f (1, 1) down = c 0 and f (m, n) up = c 1 ?

This problem is pspace-complete. The second problem we will use is the following: Given a set T of domino-types, a natural m (in unary), and two colors c 0 and c 1 of C, do all correct tiling satisfying f (1, 1) down = c 0 eventually satisfy f (m, n) up = c 1 for some n?

This problem is also pspace-complete since it can encode the universality problem for a polynomial space Turing machine.

Let (C, T = {d 1 , . . . d p }, m, c 0 , c 1 ) be an instance of B 2 . W.l.o.g., we may assume that the domino-types whose d up -color is c 1 are numberred from 1 to q, and the other ones from q + 1 to p.

We build the Kripke structure shown on Figure 2. The set of atomic propositions is T ∪ {E} ∪ {i = k | k = 1, . . . , m}. The initial states are all the states where the d down -color is c 0 and the value of i is 1. All the transitions from a state labelled with i = k to a state labelled with i = k + 1 are enabled for k ≤ m -1. For i = m, if the d up -color is not c 1 , then it is only possible to go to states labelled with i = 1, else it is only possible to go to state E.

i=1,d 1 i=1,d 2 . . . i=1,d q i=1,d q+1 . . . i=1,d p i=2,d 1 i=2,d 2 . . . i=2,d q i=2,d q+1 . . . i=2,d p • • • • • • . . . • • • • • • . . . • • • i=m,d 1 i=m,d 2 . . . i=m,d q i=m,d q+1 . . . i=m,d p E i=1,d 2 i=m,d 2 Figure 2
The Kripke structure K associated with our tiling problem.

We now have to write formulas stating that:

-Colors are respected from left to right; -Colors are respected from top to bottom; -The initial and final conditions are fulfilled.

The fragment L + ( U )

It is well-known that model-checking and satisfiability are pspacecomplete for L( U ) [START_REF] Sistla | The complexity of propositional linear temporal logics[END_REF]. The result here is a little stronger since we cannot, for instance, encode the G modality in L + ( U ).

Theorem 14. Existential model-checking for L + ( U ) is pspace-hard.

Proof. We simply have to express the three properties stated above with L + ( U ) formulas:

-Both "initial" and "final" conditions are satisfied:

φ if def = ⊤ U E
-The sequence of colors from left to right is correct:

φ horiz def = m-1 k=1 d∈T (i = k ∧ d) ⇒ i = k U (i = k + 1 ∧ d ′ ∈T d ′left =d right d ′ ) U E
-The sequence is also correct from bottom to top:

φ vert def = m k=1 d∈T (i = k ∧ d) ⇒ i = k U ¬i = k∧ (¬i = k) U E ∨ (i = k ∧ d ′ ∈T d ′down =d up d ′ ) U E
A path in K satisfying the conjunction of those formulas eventually reaches E, after having run n times through a state where i = 1 holds. The path gives rise to a function f : [1, m] × [1, n] → T in the obvious way. This function is a tiling function since the path satisfies the φ horiz and φ vert conditions. Thus the (pspace-complete) problem B 2 is (polynomialy) reducible to model-checking L + ( U ), and model checking L + ( U ) is pspace-hard.

Corollary 15. Satisfiability for L + ( U ) is pspace-hard.

Proof. A classical method for such a proof is to reduce model checking to satisfiability. However, since we cannot use or express G in L + ( U ), we cannot encode the behaviour of a (general) Kripke structure. Thus we will reduce our tiling problem to the satisfiability problem, by encoding the Kripke structure of Figure 2 into an L + ( U ) formula. This is possible since we only have to encode its behaviour until it reaches E.

We assume that the KS of Figure 2 is (Q, Q 0 , l, R), and we keep the notations introduced in the proof of Theorem 6, page 12.

We define

φ K def = q 0 ∈Q 0 P q 0 ∧ ¬E ∧ (ψ state ∧ ψ label ∧ ψ trans ) U E
By construction, φ K ∧ φ horiz ∧ φ vert is satisfiable if, and only if, the instance of the tiling problem we considered has a solution.

Theorem 16. Universal model checking is pspace-hard for L + ( U ).

Proof. This proof requires the second tiling problem: The input is the same, but the question is whether all correct tilings having c 0 as leftmost bottom color will eventually have c 1 as rightmost top color. We will write a formula expressing that each path either does not represent a correct tiling, or eventually reaches E. Thus we write -Left-to-right tiling condition is not satisfied at some place:

φ horiz def = m-1 k=1 d∈T ⊤ U i = k ∧ d∧ i = k U (i = k + 1 ∧ d ′ ∈T d ′left =d right ¬d ′ )
-Bottom-up tiling condition is not fulfilled at some place:

φ vert def = m k=1 d∈T ⊤ U i = k ∧ d ∧ i = k U ¬i = k ∧ ¬i = k U (i = k ∧ d ′ ∈T d ′down =d up ¬d ′ )
A path satisfying those properties does not correspond to a correct tiling. Thus checking that all the paths satisfy φ horiz ∨ φ vert ∨ ⊤ U E amounts to solving our tiling problem.

pspace-hardness for

L + (F , X ), L + (G , X ), L + s (F , X -1 ) and L + s (G , X -1 )
Satisfiability and existential model checking for L + (F , X ) are npcomplete [START_REF] Sistla | The complexity of propositional linear temporal logics[END_REF]. We show here that universal model checking is harder for that fragment.

Theorem 17. The universal model checking problem for L + (F , X ) is pspace-hard.

Proof. The reduction is similar to the previous one, and formulas are even easier to write: We simply have to write the formulas expressing that a path does not correspond to a correct tiling:

-Left-to-right tiling condition is not satisfied at some place:

φ horiz def = m-1 k=1 d∈T F (i = k ∧ d ∧ d ′ ∈T d ′left =d right X ¬d ′ )
-Bottom-up tiling condition is not fulfilled at some place:

φ vert def = m k=1 d∈T F (i = k ∧ d ∧ d ′ ∈T d ′down =d up X n ¬d ′ )
By duality, we get Corollary 18. Existential model checking and satisfiability problems are pspace-hard for L + (G , X ).

Proof. For existential model checking, the result comes by duality from the previous Theorem. The reduction from existential model checking to satisfiability for L(F , X ) [START_REF] Sistla | The complexity of propositional linear temporal logics[END_REF] also applies to L + (G , X ).

It is easy to adapt the proof of Theorem 17 to L + (F , X -1 ). This entails the following Theorem: Theorem 19. The universal model checking problem for L + (F , X -1 ) is pspace-hard.

The following result also holds, but is not exactly dual with the previous one: Theorem 20. The existential model checking problem is pspace-hard for L + s (G , X -1 ).

Proof. We consider the dual problem of the one we used for the proof of Theorem 16: Given the same input, the question is whether there exists a correct tiling that never satisfies the "final" condition. For this purpose, we simply have to express that a path satisfies the tiling conditions:

-Left-to-right tiling condition is satisfied:

φ horiz def = m k=2 d∈T G (i = k ∧ d ⇒ d ′ ∈T d ′right =d left X -1 d ′ )
-Bottom-up tiling condition is satisfied:

φ vert def = m k=1 d∈T G (i = k ∧ d ⇒ (X -1 k ⊥ ∨ d ′ ∈T d ′up =d down X -1 n d ′ ))
Checking that there exists a path satisfying φ horiz ∧ φ vert ∧ G ¬E amounts to solving the initial pspace-complete problem.

Even though satisfiability for L + s (G , X -1 ) is np-complete, we prove here that validity for L + s (F , X -1 ) is pspace-complete, which emphasizes the fact that X -1 is not self-dual: Lemma 21. Validity is pspace-hard for L + s (F , X -1 ).

Proof. We reduce the same problem we used in the proof of Theorem 16: Do all correct tilings having c 0 as leftmost bottom color eventually have c 1 as rightmost top color?

We encode a slightly modified KS in order to be able to refer to the beginning of a path: The only initial state is labelled with Init, it has no incoming edge and has outgoing edges to the states where i = 1 and the d down -color is c 0 . Figure 3 illustrates this construction.

The reduction is achieved as follows: We write a formula stating that -either the path does not belong to the modified structure, -or it does not correspond to a correct tiling, -or it eventually reaches E.

For the sake of simplicity, and since it is not ambiguous, we assume that our new KS is defined by (Q, {Init}, R, l). We keep the notations introduced in the proof of Theorem 6. That a path does not belong to the modified structure can be expressed through a disjunction of four subformulas:

Init i=1,d 1 i=1,d 2 . . . i=1,d q i=1,d q+1 . . . i=1,d p i=2,d 1 i=2,d 2 . . . i=2,d q i=2,d q+1 . . . i=2,d p • • • • • • . . . • • • • • • . . . • • • i=m,d 1 i=m,d 2 . . . i=m,d q i=m,d q+1 . . . i=m,d p E i=1,d 2 i=m,d 2
φ init = ¬Init φ state = F ¬ψ state φ label = F ¬ψ label φ trans = F ¬Init ∧ (s,s ′ )∈R (¬s ′ ∨ X -1 ¬s) ∨ Init ∧ X -1 ⊤
A path satisfies the disjunction of these formulas iff it is not extracted from our Kripke structure.

Expressing that the path does not represent a correct tiling is done in the same way as before:

φ horiz = d∈T F X -1 d ∧ ¬E ∧ ¬ d ′ ∈T d ′left =d right d ′ φ vert = d∈T F (X -1 ) m d ∧ ¬E ∧ ¬ d ′ ∈T d ′down =d up d ′
Let G be an infinite correct tiling having c 0 as leftmost bottom color, and π G its associated path. Since the disjunction is valid, and since π G correspond to a correct tiling, the validity of the disjunction above entails that π G satisfies F E, i.e. that the tiling eventually has c 1 as its rightmost top color.

Conversely, if all correct tilings having c 0 as leftmost bottom color eventually have c 1 as rightmost top color. Then, if a path belongs to the Kripke structure and correspond to a correct tiling, it will eventually reach state E. Proof. We still consider the structure of Figure 3. We express that -the initial and final conditions are satisfied:

φ if def = F E
-horizontal sequences of dominoes form a correct tiling:

φ horiz def = F E ∧ m k=2 d∈T (i = k ∧ d) ⇒ i = k S (i = k -1 ∧ d ′ ∈T d ′right =d left d ′ ) S Init
-vertical tiling conditions are fulfilled:

φ vert def = F E ∧ m k=1 d∈T (i = k ∧ d) ⇒ i = k S (¬i = k∧ ((¬i = k) S (Init ∨ (i = k ∧ d ′ ∈T d ′up =d down d ′ ))) S Init
A path satisfying all these conditions eventually reaches E, and corresponds to a correct tiling. Thus, existential model checking for

L + s (F , S ) is pspace-complete. Theorem 23. Existential model checking for L + s (G , S ) is pspace- hard.
Proof. This demonstration uses the same problem as in the demonstration of theorem 20, but the reduction uses the structure of figure 3. Thus, we have to write two formulas stating that the sequence of states satisfies the horizontal and vertical tiling conditions:

-Left-to-right tiling condition is satisfied:

φ horiz def = m k=2 d∈T G i = k ∧ d ⇒ d ′ ∈T d ′right =d left (i = k S (i = k -1 ∧ d ′ )
-Bottom-up tiling condition is satisfied:

φ vert def = m k=1 d∈T G i = k ∧ d ⇒ i = k S ¬i = k∧ (¬i = k) S Init ∨ (i = k ∧ d ′ ∈T d ′up =d down d ′ )
Checking that there exists a path satisfying φ horiz ∧ φ vert ∧ G ¬E amounts to solving the initial pspace-hard problem.

Theorem 24. Satisfiability is pspace-hard for L + s (F , S ).

Proof. We simply have to encode the KS of Figure 3 into temporal logic formulas. We still use notations defined on page 12. We define the followong formulas:

φ init def = Init ∧ ψ state ∧ ψ label φ trans def = (i = 1 ∧ ¬(d down = c 0 )) ⇒ (i = 1 S i = m) ∧ (i = 1 ∧ (d down = c 0 )) ⇒ (i = 1 S (φ init ∨ i = m)) ∧ m k=2 (i = k ⇒ (i = k S (i = k -1))) S φ init φ path def = F E ∧ E S (¬E ∧ (¬E ∧ ψ state ∧ ψ label ∧ φ trans ) S φ init )
This does not ensure that a path exactly encodes a run in the Kripke structure, since we cannot avoid going back to Init in the middle of the run. But the formula ensures that the part of the path between the first occurence of an E and the latest Init before that E really encodes a run in the Kripke structure. The conjunction of this formula and formulas of the proof of theorem 22 is satisfiable if, and only if, the tiling problem has a solution. Thus satisfiability is pspace-complete for L + s (F , S ).

Theorem 25. The universal model checking problem for L + s (F , S ) is pspace-hard.

Proof. The reduction is similar to the one of Theorem 16. We have to write formulas expressing that horizontal or vertical tiling conditions are not fulfilled. In L + s (F , S ), this cas be written as follows:

-Left-to-right tiling condition is not satisfied at some position: Proof. We reduce the dual problem of our initial tiling problem: Given the same input, the question is whether there exists no correct tiling meeting both initial and final conditions. This is achieved by writing that, for all path in the Kripke structure of Figure 3, if state E is eventually reached, then the path does not correspond to a correct tiling. Thus we write: Clearly, if φ is valid, then the path corresponding to a correct tiling having c 0 as leftmost bottom color cannot reach E, i.e. the tiling never has c 1 as rightmost top color. Conversely, if no correct tiling ever meets both initial and final requirements, then any path not satisfying φ will start in state Init, reach state E, and correspond to a correct tiling, which is impossible.

ψ horiz(k,d) def = (i = k ∧ d) ∧ (i = k S (i = k -1 ∧ d ′ ∈T d ′right =d left
G E ⇒ ⊤ S (
Theorem 28. Model-checking and satisfiability for fragments L + ( U ), L + (G , X ), L + s (G , X -1 ), L + s (F , S ), and for fragments of pltl containing one of them, are pspace-complete. Model-checking is pspacecomplete for L + s (G , S ). Proof. This is a direct consequence of [START_REF] Sistla | The complexity of propositional linear temporal logics[END_REF]Theorem 4.1], and of Theorems in this section.

Concluding remarks

The results we got are sufficient to completely classify all the considered fragments of pltl w.r.t. the complexity of (existential and universal) model-checking and satisfiability problems.

This exhaustive case study led to several surprising results. We showed that existential and universal model checking might have the different complexity for positive fragments (np vs. pspace). We found only one case where existential model checking and satisfiability have different theoretical complexity. On the other hand, we observe that using the symmetric past-time modalities of the allowed future modalities does not increase the complexity of verification problems. The same remark holds for the use of future modalities in the scope of past-time modalities. This all boils down to the conclusion that past is really cheap.

After this study on the effect of adding past into fragments of ltl, it would be interesting to look into when "past is for free" for extensions of that logic, such as ctl * (as far as we know, the complexity of model checking for ctl * with linear past is still open [START_REF] Kupferman | Once and for all[END_REF]) or timed temporal logics ( [START_REF] Alur | Real-time logics: Complexity and expressiveness[END_REF] proves that, for the validity problem over timed state sequences, past can be added for free in the Metric Temporal Logic from [START_REF] Koymans | Specifying real-time properties with metric temporal logic[END_REF], but not in the Timed Propositional Temporal Logic of [START_REF] Alur | A really temporal logic[END_REF]).

2. 2 . 1

 21 Model checking a loop. We first recall the following result: Theorem 3. Given a pure-future formula φ and a loop L, one can check in time O(|L| • |φ|) whether π L , 0 |= φ.

Figure 3

 3 Figure 3 The modified Kripke structure (assuming that excatly d 2 and d q+1 have c 0 as d down -color).

3. 3 Theorem 22 .

 322 pspace-hardness for L + s (F , S ) and L + s (G , S ) Existential model checking for L + s (F , S ) is pspacehard.

FF

  ψ horiz(k,d)-Bottom-up tiling condition is not fulfilled at some position:ψ vert(k,d) def = (i = k ∧ d) ∧ (i = k S (¬i = k ∧ (¬i = k S (i = k ∧ d ′ ∈T d ′up =d down ¬d ′ )))) ψ vert(k,d) All path satisfy F E ∨ φ horiz ∨ φ vert if,and only if, all correct tiling eventually have c 1 as rightmost top color. Theorem 26. The universal model checking problem for L + s (G , S ) is pspace-hard.

Theorem 27 .=Fψ

 27 Validity for L + s (G , S ) is pspace-hard.Proof. We keep the notations of the previous proof, and write the following formula:φ def Init ⇒ G E ⇒ vert(k,d) )∨ ¬ψ state ∨ ¬ψ label ∨ ( (s,s ′ )∈R ¬s ′ ∨ s ′ S ¬s)

In the sequel, we won't mention ξ whenever it is not ambiguous.

This "smallest loop" does exist, since if two loops of type (m, p) and (m ′ , p ′ ) represent the path π, then we can build a loop of type (min(m, m ′ ), gcd(p, p ′ )) encoding π.

In this case, we see F as a modality, and not as an abbreviation of ⊤ U • .

Contrary to a claim in[START_REF] Sistla | The complexity of propositional linear temporal logics[END_REF] that it is co-np-complete.

Another algorithm, reducing to the problem of model checking a finite path against pltl, has been proposed in[START_REF] Markey | Model checking a path[END_REF].


Nicolas Markey
email: markey@lifo.univ-orleans.fr

Temporal Logic with Past is Exponentially More Succinct

We positively answer the old question whether temporal logic with past is more succinct than pure-future temporal logic. Surprisingly, the proof is quite simple and elementary, although the question has been open for twenty years.

Introduction

Temporal logics with past. Temporal logic have been defined by Arthur Prior in 1957 [START_REF] Prior | Time and Modality[END_REF] as a tool for reasoning about temporal informations in a logical framework. This logic uses temporal modalities for referencing to past or future events. It has been introduced in the field of formal verification by Amir Pnueli in 1977 [START_REF] Pnueli | The Temporal Logic of Programs[END_REF]. Leslie Lamport suggested to classify temporal logics into two general kinds: linear-time temporal logic and branching-time temporal logic [START_REF] Lamport | Sometimes" is sometimes "Not Never[END_REF]. In linear-time temporal logic (LTL), we can express for instance that any request is eventually granted:

G (request ⇒ F grant). (1)
With past-time modalities, we can express that a grant should be preceeded by a request:

G (grant ⇒ F -1 request). (2)
With or without past? In 1980, Gabbay proved that past-time modalities did not add expressive power to pure future linear-time temporal logic [START_REF] Gabbay | On the Temporal Analysis of Fairness[END_REF]. He also provided an algorithm for translating formulas with past-time modalities into equivalent pure future ones [START_REF] Gabbay | The Declarative Past and Imperative Future: Executable Temporal Logic for Interactive Systems[END_REF]. Another procedure was given in [START_REF] Moser | Completeness and Soundness of Axiomatizations for Temporal Logics without Next[END_REF] for temporal logic without next. For instance, equation (2) above can be written ¬((¬request) U (grant ∧ ¬request)).

(

) 3
This formula is more intricate than the natural formula of equation (2). Moreover, the size of the formula computed by the algorithm is assumed to be non elementary in the size of the initial one. But Gabbay's theorem has been used as an argument for dropping past-time modalities from linear-time temporal logic. What we show here is that, as regards succinctness, past-time modalities do add expressive power (this result has been published in [START_REF] Laroussinie | Temporal Logic with Forgettable Past[END_REF]).

Outline. I will first briefly recall some definitions about linear-time temporal logics with past, and the possibility to "remove" past-time modalities. I will then focus on the translation of LTL formulas into Büchi automata, and more precisely on the size of the resulting automaton. I will then use this result for proving the succinctness gap between LTL+Past and pure future LTL.

1 From PLTL to LTL LTL and PLTL. Let Prop = {p, q, . . . } be a finite set of atomic propositions. Linear-time temporal logic with past-time modalities (which we denote PLTL in the sequel 1 ) is defined with the following syntax:

PLTL ∋ φ, ψ ::= ¬φ | φ ∨ ψ | φ U ψ | X φ | φ S ψ | X -1 φ | p | q | . . .
The pure future fragment of PLTL, denoted by LTL, is defined as follows:

LTL ∋ φ, ψ ::= ¬φ | φ ∨ ψ | φ U ψ | X φ | p | q | . . .
Formulas are interpreted at some position along linear paths, i.e. along infinite sequences (ω-orders) of elements of 2 Prop . The semantics for atomic propositions and boolean operators are the classical ones. For modalities, given a path π and a position i, we have:

π, i |= φ U ψ if, and only if, ∃k ≥ i. (π, k |= ψ ∧ ∀i ≤ j < k. π, j |= φ) π, i |= X φ if, and only if, π, i + 1 |= φ π, i |= φ S ψ if, and only if, ∃k ≤ i. (π, k |= ψ ∧ ∀k < j ≤ i. π, j |= φ) π, i |= X -1 φ if, and only if, i ≥ 1 and π, i -1 |= φ
The classical abbreviations F (eventually) and G (always), and their past-time counterparts, are defined by:

F φ def = ⊤ U φ G φ def = ¬F ¬φ F -1 φ def = ⊤ S φ G -1 φ def = ¬F -1 ¬φ
1 Here, P in PLTL stands for Past.

Two formulas φ, ψ of PLTL are said to be equivalent (which we write φ ≡ ψ) if, and only if, they verify the following property: for any path π and any position i, π, i

|= φ ⇔ π, i |= ψ.
Initial equivalence is a weaker notion of equivalence: φ and ψ are initially equivalent (φ ≡ i ψ) if, and only if,

for any path π, π, 0 |= φ ⇔ π, 0 |= ψ.
Both notions of equivalence clearly coincide for LTL, but not for PLTL formulas.

Translations to pure-future temporal logic. [START_REF] Gabbay | On the Temporal Analysis of Fairness[END_REF] proves that LTL is expressive complete, thus as expressive as PLTL [START_REF] Kamp | Tense Logic and the Theory of Linear Order[END_REF]. Moreover, [START_REF] Gabbay | The Declarative Past and Imperative Future: Executable Temporal Logic for Interactive Systems[END_REF] presents a syntactic algorithm for translating a PLTL formula into an initially equivalent LTL one. For many computer scientists, this has been one reason for not considering past in temporal logics, by concern of minimality.

However, since 1980, the cost of the translation has not been precisely characterized. The algorithm provided by [START_REF] Gabbay | The Declarative Past and Imperative Future: Executable Temporal Logic for Interactive Systems[END_REF] is assumed to be non elementary.

By a detour through counter-free Büchi automata, it is possible to get a more efficient algorithm: first translate the formula φ ∈ PLTL into a Büchi automaton [START_REF] Lichtenstein | The Glory of the Past[END_REF], then translate that automaton into an equivalent deterministic Muller automaton. The resulting automaton can be assumed to be counter free, since otherwise, the language it defines would not be star free. Then [START_REF] Maler | Tight Bounds on the Complexity of Cascaded Decomposition of Automata[END_REF][START_REF] Maler | On the Cascade Decomposition of Automata, its Complexity and its Application to Logic[END_REF] provides a translation of counter free Muller automaton into LTL. All of the three steps possibly involves an exponential blowup, and the size of the final formula is at most triply exponential in the size of the initial one.

In the sequel, we prove that at least one exponential is unavoidable, i.e. there exists a family of PLTL formulas φ n with size O(n), whose equivalent formulas have size Ω(2 n ).

LTL and Büchi automata

Let's get back to the aforementioned translation of LTL formulas into Büchi automata. The important theorem is the following:

Theorem 1 ([WVS83, VW86])
Given an LTL formula φ, one can build a Büchi automaton A φ = (Σ, S, ρ, S 0 , F ) where Σ = 2 Prop and |S| = 2 O(|φ|) , such that L(A φ ) is exactly the set of paths satisfying the formula φ.

Let n be a nonnegative integer, Prop = {p 0 , p 1 , . . . , p n }. We consider the following path property, mentionned in [EVW02]:

Any two positions of the path that agree on propositions p 1 , p 2 , . . . , p n also agree on proposition p 0 .

(4)

This property can be expressed by the following LTL formula, which tests all the possible valuations for the atomic propositions:

φ n def = a i ∈{⊤,⊥} i∈[1,n] F ( n i=0 p i = a i ) ⇒ G n i=1 p i = a i ⇒ (p 0 = a 0 )
This formula has size 2 O(n) . We now prove that there is no polynomial size LTL formula expressing the same statement. The proof is adapted from [EVW02]. Assume that there exists a polynomial-size LTL formula for the property (4). From the above Theorem 1, there would exist a Büchi automaton of size single exponential whose language is exactly the set of computations verifying φ n .

We show that this is not possible: any automaton recognizing L(φ n ) = {u ∈ (2 Prop ) ω | u |= φ n } requires at least 2 2 n states. Indeed, let A be an automaton recognizing exactly L(φ n ), let a 0 , . . . , a 2 n -1 be any sequence of the 2 n subsets of {p 1 , . . . , p n }, and let K be a subset of {0, . . . , 2 n -1}. We define a sequence of letters b i ∈ Σ as follows:

b i def = a i if, and only if, i / ∈ K a i ∪ {p 0 } if,

and only if, i ∈ K

We also define the finite word w

K def = b 0 b 1 • • • b 2 n -1 .
Clearly, two different choices of K lead to two different sequences of (b i ) i=0...2 n -1 , thus to two different words w K . Therefore, there exists exactly 2 2 n such words.

Let K and K ′ be two distinct subsets of {0, . . . , 2 n -1}. Obviously, the words w ω K and w ω K ′ are accepted by the automaton A. There exist two paths π K and π K ′ in the automaton A accepting the words w ω K and w ω K ′ , respectively. Consider the 2 n -th state of each of these paths, which we name q K and q K ′ . If these states were identical, then the suffix π K starting from state q K could be appended to the prefix of π K ′ up to state q K ′ (= q K ), thus giving an accepting path (since the Büchi acceptance conditions are satisfied along π K ) for the word w K ′ • w ω K . But that word w K ′ • w ω K should not be accepted by A since it does not satisfy the formula φ n . Thus any automaton recognizing exactly L(φ n ) has at least 2 2 n states, so that

|φ n | is in Ω(2 n ).
3 PLTL is exponentially more succinct than LTL In order to prove the succinctness result, we will use a slightly modified property, namely:

Any position of the path that agrees on propositions p 1 , p 2 , . . . , p n with the initial state also agrees on proposition p 0 .

(

This property can be expressed in PLTL through the following formula:

ψ n def = G n i=1 (p i ⇔ F -1 G -1 p i ) ⇒ (p 0 ⇔ F -1 G -1 p 0 ) .
This formula clearly expresses property (5), since F -1 G -1 p means that p holds in the initial state of the path. Moreover, φ n has size O(n).

Since any PLTL formula can be translated into an initially equivalent LTL formula, we let ψ ′ n be an LTL formula initially equivalent to ψ n , and we define

φ ′ n def = G ψ ′ n .
We claim that φ n and φ ′ n are equivalent. Indeed, that some path π satisfies φ ′ n exactly means that for all i, π, i |= ψ ′ n . Since ψ ′ n ∈ LTL, this amounts to say that π i , 0 |= ψ ′ n . Since ψ ′ n ≡ i ψ n , it is equivalent to the fact that, for all i, π i , 0 |= ψ n , that is "for all position i, for all position j, if position j agrees with position i on propositions p 1 , p 2 , . . . , p n , then it also agrees with position i on proposition p 0 ", which we means that π satisfies φ n .

Bringing all the pieces together, we get the following theorem:

Theorem 2 PLTL can be exponentially more succinct than LTL.

The proof is quite simple now: consider formula ψ n , and its LTL equivalent ψ ′ n . We know that ψ n has size linear in n, and we know that G ψ ′ n has size Ω(2 n ), since it is an LTL formula expressing property (4). Thus ψ ′ n has size at least Ω(2 n ). In fact, this even proves that ψ ′ n has at least Ω(2 n ) distinct subformulas, since in the construction of A φ , the states are the subsets of the set of subformulas of φ (thus ψ ′ n cannot even be succinctly represented as a dag sharing common subformulas).

Remark that the proof requires formulas with bounded temporal height, and uses an unbounded number of atomic propositions. It can be adapted in order to use only finitely many atomic propositions, but with an unbounded temporal height (by encoding atomic propositions with only one atomic proposition [DS02]). Moreover, the proof uses neither the U nor the S modalities. The result thus carries over to L(F , F -1 ). It can be shown however that L(F , F -1 ) is strictly more expressive (as regards to the classical notion of expressivity) than L(F ).

Conclusion

This simple proof only partially answers the question on the size of the optimal translation from PLTL to LTL: we proved that the gap is at least single exponential, but the best known upper bound is triply exponential.

  Moshe Y. Vardi, and Thomas Wilke. First-Order Logic with Two Variables and Unary Temporal Logic. Infor-

	[DS02]	Stéphane Demri and Philippe Schnoebelen. The Complexity of
		Propositional Linear Temporal Logics in Simple Cases. Infor-
		mation and Computation, 174(1), pages 84-103, Academic Press,
		April 2002.
	[EVW02]	Kousha Etessami,