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

Hans De Nivelle

Deciding Modal Logics through Relational Translations into GF 2

We provide a simple translation from the satisfiability problem for regular grammar logics with converse into GF 2 , which is the intersection of the guarded fragment and the 2-variable fragment of first-order logic. This translation is theoretically interesting because it translates modal logics with certain frame conditions into first-order logic, without explicitly expressing the frame conditions. Using the same method, one can show that other modal logics can be naturally translated into GF 2 , including nominal tense logics and intuitionistic propositional logic. In our view, the results in this paper provide strong evidence that the natural first-order fragment corresponding to modal logics, is GF 2 .

Introduction

Translating modal logics. Modal logics are used in many areas of Computer Science, as for example knowledge representation, model-checking, and temporal reasoning. In order to reason with knowledge bases, or to check that a certain temporal program meets a certain specification, one needs to be able to do theorem proving in modal logics. For theorem proving in modal logics, two main approaches can be distinguished. Either one develops a theorem prover directly for the logic under consideration, or one translates the logic into a general logic, usually first-order logic. Translation of modal logics into first-order logic, with the explicit goal to mechanise such logics is an approach that has been introduced in [START_REF] Morgan | Methods for automated theorem proving in non classical logics[END_REF]. Morgan distinguishes two types of translations: The semantical translation, which is nowadays known as the relational translation (see e.g., [START_REF] Van Benthem | Correspondence Theory[END_REF]) and the syntactic translation, which consists in reifing modal formulae by translating the formula, together with the axioms and inference rules from a Hilbert-style system into classical logic using an additional provability predicate. Until recent, it appeared that this method was not suitable for obtaining decision procedures, but in the recent paper [START_REF] Hustadt | A principle for incorporating axioms into the firstorder translation of modal formulae[END_REF], this method has been modified. The authors were able to translate a couple of modal logics, including KT, KD, KB, into GF 2 by proving a bound on the size of the formulas that can occur in Hilbert-style proofs. It is surprising that this method, with a philosophy which is completely different from our translation method, arrives for these logics at a very similar translation. This is a point that needs further investigation.

Here we study the semantic method for obtaining decision procedures. Our goal is to translate a modal logic into a decidable fragment of first-order logic, which preferably has the same complexity as the modal logic, and which allows theorem proving techniques that are similar to the ones allowed by the original modal logic. A survey on translation methods for modal logics can be found in [START_REF] Ohlbach | Encoding two-valued non-classical logics in classical logic[END_REF], where more references are provided.

Guarded fragments. Both the guarded fragment, introduced in [START_REF] Andreka | Modal languages and bounded fragments of predicate logic[END_REF] (see also [START_REF] Grädel | On the restraining power of guards[END_REF]) and FO 2 , the fragment of classical logic with two variables [START_REF] Gabbay | Expressive functional completeness in tense logic[END_REF][START_REF] Grädel | On the decision problem for two-variable first-order logic[END_REF], have been used for this purpose. The authors of [START_REF] Andreka | Modal languages and bounded fragments of predicate logic[END_REF] explicitly mention the goal of identifying 'the modal fragment of first-order logic' as a motivation for introducing the guarded fragment. Apart from satisfying nice logical properties [START_REF] Andreka | Modal languages and bounded fragments of predicate logic[END_REF], the guarded fragment GF has an EXPTIME-complete satisfiability problem, in case the maximal arity of the predicate symbols is fixed in advance [START_REF] Grädel | On the restraining power of guards[END_REF]. Moreover, efficient mechanisation of the guarded fragment is possible thanks to the design of resolution-based decision procedures [START_REF] De Nivelle | A resolution decision procedure for the guarded fragment[END_REF][START_REF] De Nivelle | Deciding the guarded fragments with resolution[END_REF]. In [START_REF] Hladik | Implementation and optimisation of a tableau algorithm for the guarded fragment[END_REF], a tableau procedure for the guarded fragment with equality is implemented and tested; A tableau procedure FO 2 is described in [START_REF] Marx | Tableau calculus for local cubic modal logic and its implementation[END_REF].

Unfortunately, there are some simple modal logics with the satisfiability problem in PSPACE, which can be translated neither into GF, nor into FO 2 by the relational translation. The reason for this is the fact that the frame condition that characterizes the logic cannot be expressed in GF ∪ FO 2 .

The simplest examples of such logics are K4 and S4. Transitivity cannot be expressed in GF ∪ FO 2 .

Because of the apparent insufficiency of GF to capture some of the basic modal logics, various extensions of GF have been proposed and studied. For instance, GF 2 with transitive guards is 2EXPTIME-complete [START_REF] Szwast | On the decision problem for the guarded fragment with transitivity[END_REF][START_REF] Kieronski | The two-variable guarded fragment with transitive guards is 2EXPTIME-hard[END_REF] whereas µGF, the guarded fragment of first-order logic extended with a µcalculus-style fixed point operator, is still decidable and in 2EXPTIME. This fragment does contain the simple modal logics S4, but the resulting decision procedure is much more complicated than a direct decision procedure would be. After all, there exist simple tableaux procedures for S4. In addition, µGF does not have the finite model property, although S4 has. Almost structure-preserving translations. An approach that seems better suited for theorem proving, and that does more justice to the low complexities of the simple modal logics is the approach taken in [START_REF] De Nivelle | Translation of S4 and K5 into GF and 2VAR[END_REF][START_REF] De Nivelle | Translation of S4 and K5 into GF and 2VAR[END_REF]. There, an almost structure-preserving translation from the modal logics S4, S5 and K5 into GF 2 was given. The correctness proofs there were ad hoc, and at that time it was not clear upon which principles they are based. Here we show that this translation method relies on the fact that the frame conditions for S4 and K5 are regular in some sense that will be made precise in Section 2. Some subformulas are translated into a sequence of GF 2 formulas simulating a finite-state automaton, the structure of which depends on the frame condition. The simplicity of the method leaves hope that GF 2 may be rich enough after all to naturally capture most of the usual modal logics.

The theoretical interest of the translation method lies in the fact the translation method preserves the structure of the formula almost completely. Only for subformulas of form [a]φ does the translation differ from the relational translation. On these subformulas, a sequence of formulas is generated that simulates an NDFA based on the frame condition for the modal logic. In our view, this translation also provides an explanation why some modal logics like S4, have nice tableau procedures (see e.g. [START_REF] Goré | Tableaux methods for modal and temporal logics[END_REF][START_REF] Massacci | Single steps tableaux for modal logics[END_REF]): The tableau rule for subformulas of form [a]φ can be viewed as simulating our translation for a subformula of form [a]φ, which in turn simulates an NDFA corresponding to a closure property of the underlying logic. Plan of the paper. We show that the methods of [START_REF] De Nivelle | Translation of S4 and K5 into GF and 2VAR[END_REF] can be extended to a large class of modal logics. The class of modal logics that we consider is the class of regular grammar logics with converse. The axioms of such modal logics are of form

[a 0 ]p ⇒ [a 1 ] • • • [a n ]p,
where each [a i ] is either a forward or a backward modality. Another condition called regularity is required and will be formally defined in Section 2.

With our translation, we are able to translate numerous modal logics into GF 2 despite the fact that their frame conditions are not expressible in FO 2 ∪ GF: These logics include the standard modal logics K4, S4, K5, K45, S5, description logics, nominal tense logics (if we allow constants and equality in GF 2 ), and propositional intuitionistic logic, to quote a few classes of logics. Related work. Complexity issues for regular grammar logics have been studied in [START_REF] Demri | The complexity of regularity in grammar logics and related modal logics[END_REF][START_REF] Demri | Modal logics with weak forms of recursion: PSPACE specimens[END_REF] (see also [START_REF] Baldoni | A tableau calculus for multimodal logics and some (un)decidability results[END_REF]), whereas grammar logics are introduced in [START_REF] Del Cerro | Grammar logics[END_REF]. Frame conditions involving the converse relations are not treated in [START_REF] Demri | The complexity of regularity in grammar logics and related modal logics[END_REF][START_REF] Demri | Modal logics with weak forms of recursion: PSPACE specimens[END_REF]. The current work can be viewed as a natural continuation of [START_REF] De Nivelle | Translation of S4 and K5 into GF and 2VAR[END_REF] and [START_REF] Demri | The complexity of regularity in grammar logics and related modal logics[END_REF]. The frame conditions considered in the present work can be defined by the MSO definable closure operators [START_REF] Ganzinger | The two-variable guarded fragment with transitive relations[END_REF]. However, in contrast with the method of [START_REF] Ganzinger | The two-variable guarded fragment with transitive relations[END_REF], we obtain the optimal complexity upper bound for the class of regular grammar logics with converse (EXPTIME), whereas the method of [START_REF] Ganzinger | The two-variable guarded fragment with transitive relations[END_REF] obtains a non-elementary upper bound.

As already mentiond, the recent paper [START_REF] Hustadt | A principle for incorporating axioms into the firstorder translation of modal formulae[END_REF] presents another translation of modal logics into GF 2 , by adequately encoding the modal formula and the axioms, and by showing that the set of formulas that can occur in a proof is finite. Although for logics such as S4, the method in [START_REF] Hustadt | A principle for incorporating axioms into the firstorder translation of modal formulae[END_REF] results in the same formulas as ours, it is still open how the methods are related in the general case. For instance, no regularity conditions are explicitly involved in [START_REF] Hustadt | A principle for incorporating axioms into the firstorder translation of modal formulae[END_REF] whereas this is a central point in our work. Finally, it should be noted that this paper is a short version of [START_REF] Demri | Deciding regular grammar logics with converse through first-order logic[END_REF], which contains all proofs that are omitted in this paper.

Regular Grammar Logics with Converse

Formal grammars are a convenient way of defining frame properties for modal logics. Many standard modal logics can be nicely defined by a grammar logic.

We give examples at the end of this section, in Table 1 and Example 2.9. After Example 2.9 we describe a sequence of logics which are not regular grammar logics. In order to define regular grammar logics, we recall below a few definitions from formal language theory, semi-Thue systems, and finitestate automata.

Semi-Thue Systems

An alphabet Σ is a finite set {a 1 , . . . , a m } of symbols. We write Σ * to denote the set of finite strings that can be built over elements of Σ, and we write for the empty string. We write u 1 • u 2 for the concatenation of two strings. For a string u ∈ Σ * , we write |u| to denote its length. A language over some alphabet Σ is defined as a subset of Σ * .

A semi-Thue system S over Σ is defined as a subset of Σ * × Σ * . The pairs (u 1 , u 2 ) ∈ Σ * × Σ * are called production rules. We will mostly write u 1 → u 2 instead of (u 1 , u 2 ) for production rules. The system S will be said to be context-free if S is finite and all the production rules are in Σ × Σ * . The one-step derivation relation ⇒ S is defined as follows: Put u ⇒ S v iff there exist

u 1 , u 2 ∈ Σ * , and u → v ∈ S, such that u = u 1 • u • u 2 , and v = u 1 • v • u 2 . The full derivation relation ⇒ *
S is defined as the reflexive and transitive closure of ⇒ S . Finally, for every u ∈ Σ * , we write L S (u) to denote the language {v ∈ Σ * : u ⇒ * S v}. A context-free semi-Thue system S, based on Σ is called regular if for every a ∈ Σ, the language L S (a) is regular. In that case, one can associate to each a ∈ Σ an NDFA (non-deterministic finite automaton) recognizing the language L S (a).

Grammar Logics with Converse

In grammar logics, modal frame conditions are expressed by the production rules of semi-Thue systems. For example, transitivity on the relation R a is expressed by the production rule a → a • a. Similarly, reflexivity can be expressed by a → . We also allow frame conditions that contain the converses of accessibility relations. For this reason, we will associate to every symbol a in the alphabet a unique converse symbol a. Using converses, for example symmetry on the relation R a can be represented by the production rule a → a whereas euclideanity on the relation R a can be represented by the production rule a → a • a.

Given an alphabet Σ, we define the multimodal language L Σ based on Σ. In order to do this, we assume a countably infinite set PROP = {p 0 , p 1 , . . .} of propositional variables. Then L Σ is recursively defined as follows:

φ, ψ ::= p | ⊥ | | ¬φ | φ ∧ ψ | φ ∨ ψ | [a]φ | a φ
for p ∈ PROP and a ∈ Σ. We define the negation normal form (NNF) as usual: ¬ is applied only on members of PROP. We will make use of the NNF when we translate formulas to GF 2 . Let Σ be an alphabet. A Σ-frame is a pair F = W, R , such that W is non-empty, and R is a mapping from the elements of Σ to binary relations over W. So, for each a ∈ Σ, R a ⊆ W × W. A Σ-model M = W, R, V is obtained by adding a valuation function V with signature PROP → P(W ) to the frame. The satisfaction relation |= is defined in the usual way.

• For p ∈ PROP, M, x |= p iff x ∈ V (p). • For a ∈ Σ, M, x |= [a]φ iff for all y, s.t. R a (x, y), M, y |= φ. • For a ∈ Σ, M, x |= a φ iff there is an y, s.t. R a (x, y) and M, y |= φ. • M, x |= φ ∧ ψ iff M, x |= φ and M, x |= ψ. • M, x |= φ ∨ ψ iff M, x |= φ or M, x |= ψ. • M, x |= ¬φ iff it is not the case that M, x |= φ.
A formula φ is said to be true in the Σ-model M (written M |= φ) iff for every x ∈ W , M, x |= φ. A Σ-frame maps the symbols in Σ to binary relations on W. This mapping can be extended to the full language Σ * as follows:

• R equals { x, x : x ∈ W }, • For u ∈ Σ * , a ∈ Σ, R u•a equals { x, y : ∃z ∈ W, R u (x, z) and R a (z, y)}.
Now we define how semi-Thue systems encode conditions on Σ-frames. Definition 2.1 Let u → v be a production rule over some alphabet Σ. We say that the Σ-frame F = W, R satisfies u → v if the inclusion R v ⊆ R u holds. F satisfies a semi-Thue system S if it satisfies each of its rules. We also say that S is true in F. A formula φ is said to be S-satisfiable iff there is a Σ-model M = W, R, V which satisfies S, and which has an x ∈ W such that M, x |= φ. Similarly, a formula φ is said to be S-valid iff for all Σ-models M = W, R, V that satisfy S, for all x ∈ W, we have M, x |= φ.

We assume that a logic is characterized by its set of satisfiable formulas, or equivalently, by its set of universally valid formulas. We call logics that can be characterized by a semi-Thue system using Definition 2.1 grammar logics. Those logics that can be characterized by regular semi-Thue systems are called regular grammar logics. For instance, the modal logic S4 is the regular modal logic defined by the regular semi-Thue system {a → , a → aa}. In order to be able to cope with properties such as symmetry and euclideanity, we now introduce converses: Definition 2.2 Let Σ be an alphabet. We call a function • on Σ a converse mapping if for all a ∈ Σ, we have a = a and a = a.

It is easy to prove the following: Lemma 2.3 Let Σ be an alphabet with converse mapping •. Then • is a bijection on Σ. In addition, Σ can be partitioned into two disjoint sets Σ + and Σ -, such that (1) for all a ∈ Σ + , a ∈ Σ -, (2) for all a ∈ Σ -, a ∈ Σ + .

In fact, there exist many partitions Σ = Σ -∪ Σ + . When we refer to such a partition, we assume that an arbitrary one is chosen. We will assume that the modal operators indexed by letters in Σ + are forward modalities (conditions on successor states) whereas the modal operators indexed by letters in Σ -are backward modalities (conditions on predecessor states). Definition 2.4 A converse mapping • can be extended to words over Σ * as follows:

(1) = , (2) if u ∈ Σ * and a ∈ Σ, then u • a = a • u.
Definition 2.5 Given a semi-Thue system S over some alphabet Σ with converse mapping •, we call S a semi-Thue system with converse if u → v ∈ S implies u → v ∈ S. The converse closure of a semi-Thue system S is the ⊆-smallest semi-Thue system S with converse for which S ⊆ S .

It is easily checked that the converse closure is always well-defined. Definition 2.6 Let Σ be an alphabet with converse mapping • . A Σ, •frame is a Σ-frame for which in addition, for each a ∈ Σ, R a equals { y, x : R a (x, y)}.

The following property of Σ, • -frames is easily checked: Lemma 2.7 Let Σ be an alphabet with converse mapping •. Let F = W, R be a Σ, • -frame. Then for each u ∈ Σ * , R u = { y, x : R u (x, y)}.

As a consequence, semi-Thue systems not satisfying Definition 2.5 cannot characterize more Σ, • -frames than semi-Thue systems that do satisfy Definition 2.5: Lemma 2.8 Let Σ be an alphabet with converse mapping •. Let F be a Σ, •frame. Let S be a semi-Thue system over Σ, let S be its converse closure. Then F satisfies S iff F satisfies S .

We call the logics that can be characterized by a regular semi-Thue system with converse using Definition 2.6 and Definition 2.1 regular grammar logics with converse. The models of such logics are based on Σ, • -frames which guarantees that converses are taken into account.

Originally, grammar logics were defined with formal grammars in [START_REF] Del Cerro | Grammar logics[END_REF] (as in [START_REF] Baldoni | A tableau calculus for multimodal logics and some (un)decidability results[END_REF][START_REF] Demri | The complexity of regularity in grammar logics and related modal logics[END_REF][START_REF] Demri | Modal logics with weak forms of recursion: PSPACE specimens[END_REF] conditions expressible in Π 1 when S is context-free. In fact, numerous logics are (fragments of) regular grammar logics with converse, or logics that can be reduced to such logics.

Example 2.9 The standard modal logics K, T, B, S4, K5, K45, and S5 can be defined as regular grammar logics over the singleton alphabet Σ = {a}. In Table 1, we specify the semi-Thue systems through regular expressions for the languages L S (a).

We list some of other logics for specific application domains, which can also be seen as regular grammar logics with converse.

• description logics (with role hierarchy, transitive roles), see e.g. [START_REF] Horrocks | A description logic with transitive and inverse roles and role hierarchies[END_REF];

• knowledge logics, see e.g. S5 m (DE) in [START_REF] Fagin | Reasoning about Knowledge[END_REF];

• bimodal logics for intuitionistic modal logics of the form IntK 2 + Γ [37];

• fragments of logics designed for the access control in distributed systems [START_REF] Abadi | A calculus for access control in distributed systems[END_REF][START_REF] Massacci | Tableaux methods for access control in distributed systems[END_REF].

• extensions with the universal modality [START_REF] Goranko | Using the universal modality: gains and questions[END_REF]. Indeed, for every regular grammar logic with converse, its extension with a universal modal operator is also a regular grammar logic with converse by using simple arguments from [START_REF] Goranko | Using the universal modality: gains and questions[END_REF] (add an S5 modal connective stronger than any other modal connective). Hence, satisfiability, global satisfiability and logical consequence can be handled uniformly with no increase of worst-case complexity;

• information logics, see e.g. [START_REF] Vakarelov | Abstract characterization of some knowledge representation systems and the logic NIL of nondeterministic information[END_REF]. For instance, the Nondeterministic Information Logic NIL introduced in [START_REF] Vakarelov | Abstract characterization of some knowledge representation systems and the logic NIL of nondeterministic information[END_REF] (see also [START_REF] Demri | The nondeterministic information logic NIL is PSPACE-complete[END_REF]) can be shown to be a fragment of a regular grammar logic with converse with Σ + = {f in, sim} and the converse closure of the production rules below:

• f in → f in • f in; f in → ; • sim → sim; sim → ; • sim → f in • sim • f in. For instance L S (sim) = {f in} * • {sim, sim, } • {f in} * .
A frame condition outside our current framework.

The euclideanity condition can be slightly generalized by considering frame conditions of the form (R -1 a ) n ; R a ⊆ R a for some n ≥ 1. The context-free semi-Thue system with converse corresponding to this inclusion is S n = {a → a n a, a → aa n }. The case n = 1 corresponds to euclideanity. Although we have seen that for n = 1, the language L S 1 (a) is regular, one can establish that in general, for n > 1, the language L Sn (a) is not regular. This is particularly interesting since S n -satisfiability restricted to formulae with only the modal operator [a] is decidable, see e.g. [START_REF] Gabbay | Decidability results in non-classical logics[END_REF][START_REF] Hustadt | A principle for incorporating axioms into the firstorder translation of modal formulae[END_REF]. To see why the systems L Sn (a) are not regular, consider strings of the following form:

σ n (i 1 , i 2 ) = (aa n-1 ) i 1 a (a n-1 a) i 2 . σ n (i 1 , i 2 ) = (aa n-1 ) i 1 a (a n-1 a) i 2 .
We show that ( a

⇒ * Sn σ n (i 1 , i 2 ) and a ⇒ * Sn σ n (i 1 , i 2 + 1) ) iff i 1 = i 2 .
In order to check that the equivalence holds from right to left, observe that a = σ n (0, 0), and σ n (0, 0) ⇒ Sn σ n (0, 1)

⇒ Sn σ n (1, 1) ⇒ Sn • • • ⇒ Sn σ n (i, i) ⇒ Sn σ n (i, i + 1) ⇒ Sn σ n (i + 1, i + 1) ⇒ Sn • • •
We now prove the equivalence from left to right. Let us say that u is an ancestor of v if u ⇒ Sn v. Then it is sufficient to observe the following: (i) A string of form σ n (0, j) has no ancestor.

(ii) A string of form σ n (i + 1, j) has only one ancestor, namely σ n (i, j).

(iii) A string of form σ n (i, 0) has no ancestor.

(iv) A string of form σ n (i, j + 1) has only one ancestor, namely σ n (i, j).

To have an ancestor, a string must have a sequence of at least n consecutive a's or a's. The strings of form 1 or 3 have no such sequence. The strings of form 2 or 4 have exactly one such sequence. Since the regular languages are closed under intersection, the languages {σ n (i, j) : i ≥ 0, j ≥ 0} are regular, while the languages {σ n (i, i) : i ≥ 0} are clearly not regular when n > 1, the languages L Sn (a) cannot be regular when n > 1. Hence, this will leave open the extension of our translation method to the case of context-free semi-Thue systems with converse when decidability holds (see e.g. decidable extensions of PDL with certain context-free programs in [START_REF] Harel | Dynamic Logic[END_REF]).

The Translation into GF 2

We consider our translation almost structure preserving. This is because the transformation is defined by a simple recursion, which preserves the structure of the formula for all cases, except for the case where the subformula has form [a]φ. In case the subformula does have form [a]φ, the translation constructs a sequence of formulas that simulates the regular automaton recognizing L S (a). Some specific features of our translation are the following:

• The translation introduces new predicate symbols, which it needs for simulating automata. Because of this, the translated formula is not logically equivalent to the original formula. The transformation is only satisfiability preserving. Our translation is a reduction, as understood in complexity theory, from the satisfiability problem for regular grammar logics with converse into the satisfiability problem for GF 2 . • Although our transformation is a reduction in the complexity theoretic sense, it is a relatively mild one. It does not make use of encodings of Turing machines, or another computation mechanism. It uses only a mutual recursion between the encoding of the frame conditions and the translation of logical operators.

The Transformation

We assume that S is a regular semi-Thue system with converse over alphabet Σ with converse mapping • (and partition {Σ + , Σ -}). For every a ∈ Σ, the automaton A a is an NDFA (with -transitions) recognizing the language L S (a). We write A a = (Q a , s a , F a , δ a ). Here Q a is the finite set of states, s a is the starting state, F a ⊆ Q a are the accepting states, and δ a is the transition function, which is possibly non-deterministic. When all rules in S are either right-linear or left-linear, then each automaton A a can be effectively built in logarithmic space in |S|, the size of S with some reasonably succinct encoding.

Definition 3.1 Assume that for each letter a ∈ Σ + , a unique binary predicate symbol R a is given. We define a translation function t a , mapping letters in Σ to binary predicates (α and β are variables).

• For each letter a ∈ Σ + , we define t a (α, β) = R a (α, β),

• For each letter a ∈ Σ -, we define t a (α, β) = R a (β, α).

We now define the part of the translation that takes into account the frame conditions. It takes two parameters, a one-place formula and an NDFA. The result of the translation is a first-order formula (one-place again) that has the following meaning:

In every point that is reachable by a sequence of transitions that are accepted by the automaton, the original one-place formula holds. Definition 3.2 Let A = (Q, s, F, δ) be an NDFA. Let ϕ(α) be a first-order formula with one free variable α. Assume that for each state q ∈ Q, a fresh unary predicate symbol q is given. We define t A (α, ϕ) as the conjunction of the following formulas (the purpose of the first argument is to remember that α is the free variable of ϕ):

• For the initial state s, the formula s(α) is included in the conjunction.

• For each q ∈ Q, for each a ∈ Σ, for each r ∈ δ(q, a), the formula ∀αβ [ t a (α, β) → q(α) → r(β) ] is included in the conjunction.

• For each q ∈ Q, for each r ∈ δ(q, ), the formula ∀α [ q(α) → r(α) ] is included in the conjunction.

• For each q ∈ F, the formula ∀α [ q(α) → ϕ(α) ] is included in the conjunction.

It is assumed that in each application of t Aa distinct predicate symbols are used. One can introduce the new predicate symbols of the form q for q ∈ Q either occurrence-wise, or subformula-wise. In the sequel, we adopt a subformula-wise approach and we fix that in Definition 3.2, the fresh unary predicate symbol for q ∈ Q will be always q ϕ , where ϕ is the formula being translated. As a consequence, two applications of t A (α, ϕ) reuse the same predicate symbols associated to the states of Q.

If the automaton A has more than one accepting state, then ϕ(α) occurs more than once in the translation t A (α, ϕ). This may cause an exponential blow-up in the translation but this problem can be easily solved by adding a new accepting state to the automaton, and adding -translations from the old accepting states into the new accepting state.

Using Definition 3.2, we can now give the translation itself. It is a standard relational translation on all subformulas, except for those of the form [a]ψ, on which t Aa will be used. In order to easily recognize the 2-subformulas, we require the formula φ to be in negation normal form. One could define the translation without NNF, but it would be more complicated, because we would have to add cases for ←, ↔, and we would have to take the polaraties into account while translating. Definition 3.3 Let φ ∈ L Σ be a modal formula in NNF. Let S be a regular semi-Thue system with converse over alphabet Σ with converse mapping •. Assume that for each a ∈ Σ an automaton A a recognizing L S (a) is given. We define the translation T S (φ) as t(φ, α, β) from the following function t(ψ, α, β), which is defined by recursion on the subformulas ψ of φ :

• For a propositional symbol p, the translation t(p, α, β) equals p(α), where p is a unary predicate symbol uniquely associated to the propositional variable p. The translation t(¬p, α, β) of ¬p equals ¬p(α),

• t(ψ ∧ ψ , α, β) equals t(ψ, α, β) ∧ t(ψ , α, β), • t(ψ ∨ ψ , α, β) equals t(ψ, α, β) ∨ t(ψ , α, β), • for a ∈ Σ, t( a ψ, α, β) equals ∃β [ t a (α, β) ∧ t(ψ, β, α) ],
• for a ∈ Σ, t( [a]ψ, α, β) equals t Aa (α, t(ψ, α, β) ).

When translating a subformula of form [a]ψ, the translation function t Aa of Definition 3.2 is used. The only difference with the standard relational translation is the translation of [a]-formulae. When S is formed of production rules of a formal grammar that is either right-linear or left-linear, then m is in O(|S|). For a given semi-Thue system S, the number m is fixed. Moreover, T S (φ) has size linear in |φ| when the logic is fixed.

Because we do the introduction of new symbols subformula-wise, it is possible to put the translation of the automaton outside of the translation of the modal formula. At the position where t Aa (α, t(ψ, α, β)) is translated, only q 0,ψ (α) needs to be inserted (where q 0 is the initial state of A a ). The rest of the (translation of the) automaton can be put elsewhere.

Here is the main theorem about satisfiability preservation.

Theorem 3.5 Let Σ be an alphabet with converse mapping •, let S be a regular semi-Thue system with converse over Σ, and let φ ∈ L Σ be a modal formula. Then, φ is S-satisfiable iff T S (φ) is satisfiable in first-order logic.

The proof relies on the regularity of the languages L S (a) and on the existence of a closure operator on frames. For details of the proof, we refer to [START_REF] Demri | Deciding regular grammar logics with converse through first-order logic[END_REF] or [START_REF] Demri | Deciding regular grammar logics with converse through first-order logic[END_REF]. The uniformity of the translation allows us to establish the forthcoming Theorem 3.6. The general satisfiability problem for regular grammar logic with converse, denoted by GSP(REG c ), is defined as follows:

input: a semi-Thue system with converse S represented either as a right-linear grammar or as a left-linear grammar, and an L Σ -formula φ; question: is φ S-satisfiable? Theorem 3.6 The S-satisfiability problem is in EXPTIME for every regular semi-Thue system with converse and GSP(REG c ) is EXPTIME-complete.

If we would allow arbitrary semi-Thue systems in the definition of GSP(REG c ), then Theorem 3.6 would not hold, because it is in general undecidable to determine whether a context-free semi-Thue system is regular.

Concluding Remarks

We have defined almost-structure preserving logspace transformations from a large class of modal logics into GF 2 . We think that this provides evidence that the first-order fragment corresponding to the class of regular grammar logics with converse is simply GF 2 , in particular no fixed point operators or transitive gaurds are needed. In addition, we characterized the complexity of the satisfiability problem for regular grammar logics and our method can be extended to other non-classical logics including nominal tense logics and intuitionistic logic (see details in [START_REF] Demri | Deciding regular grammar logics with converse through first-order logic[END_REF]). The translation for intuitionistic propositional logic can be obtained by combining our translation, applied on modal logic S4, with Gödel's translation from intuitionistic logic into S4. (See [START_REF] Troelstra | Basic Proof Theory[END_REF] for the Gödel translation)

The encoding we used is reminiscent to the propagation of formulas in tableaux calculi (see e.g. [START_REF] Goré | Tableaux methods for modal and temporal logics[END_REF][START_REF] Massacci | Single steps tableaux for modal logics[END_REF][START_REF] Castilho | Modal tableaux with propagation rules and structural rules[END_REF]) and the study of this relationship may be worth being pursued. We also plan to implement our method, in order to obtain insight into the practical usefulness of our translation method.

Lemma 3 . 4 T

 34 S (φ) belongs to GF 2 and T S (φ) can be computed in logspace in |φ| + m with m = max{ |A a | | a ∈ Σ }.

  ), and they form a subclass of Sahlqvist modal logics with frame

	logic	L S (a)	frame condition
	K	{a}	(none)
	KT	{a, }	reflexivity
	KB	{a, a}	symmetry
	KTB	{a, a, }	refl. and sym.
	K4	{a} • {a} *	transitivity
	KT4 = S4	{a} *	refl. and trans.
	KB4	{a, a} • {a, a} *	sym. and trans.
	K5	({a} • {a, a} * • {a}) ∪ {a}	euclideanity
	KT5 = S5	{a, a} *	equivalence rel.
	K45	({a} Table 1
	Regular languages for standard modal logics

* • {a}) * trans. and eucl.


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

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

The Effects of Bounding Syntactic Resources on Presburger LTL (Extended Abstract) *

We study decidability and complexity issues for fragments of LTL with Presburger constraints by restricting the syntactic resources of the formulae (the class of constraints, the number of variables and the distance between two states for which counters can be compared) while preserving the strength of the logical operators. We provide a complete picture refining known results from the literature, in some cases pushing forward the known decidability limits. By way of example, we show that model-checking formulae from LTL with quantifier-free Presburger arithmetic over one-counter automata is only PSPACE-complete. In order to establish the PSPACE upper bound, we show that the nonemptiness problem for Büchi one-counter automata taking values in Z and allowing zero tests and sign tests, is only NLOGSPACE-complete.

Introduction

LTL with Presburger constraints. Ubiquity of counter automata in computer science stems from their use as operational models of numerous infinite-state systems, including for instance broadcast protocols [START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF] and programs with pointer variables [START_REF] Bardin | From pointer systems to counter systems using shape analysis[END_REF][START_REF] Bouajjani | Programs with lists are counter automata[END_REF]. Even the restriction to one counter has found applications in the verification of cryptographic protocols [START_REF] Lafourcade | Intruder deduction for AC-like equational theories with homomorphisms[END_REF] and the validation of XML streams [START_REF] Chitic | On validation of XML streams using finite state machines[END_REF]. However, numerous model-checking problems for counter automata, like reachability questions, are known to be undecidable. This does not end the story since many subclasses admit a decidable reachability problem such as reversal-bounded counter machines [START_REF] Ibarra | Counter machines: Decidable properties and applications to verification problems[END_REF] or flat counter systems [START_REF] Boigelot | Symbolic methods for exploring infinite state spaces[END_REF][START_REF] Leroux | Flat counter systems are everywhere![END_REF].

Extending the linear-time temporal logic LTL with Presburger constraints allows to specify quantitative properties about counter systems even though undecidability cannot be avoided (see in [START_REF] Bouajjani | On the verification problem of nonregular properties for nonregular processes[END_REF][START_REF] Comon | Flatness is not a weakness[END_REF] decidable fragments by re-stricting the use of the temporal operators). In this paper, we are interested in the decidability and complexity status of fragments of Presburger LTL restricting the following syntactic resources of the formulae: the class of constraints, the number of counters and the maximal distance between two states for which these counters can be compared. However, we preserve the full strength of the logical operators. Our investigation is based on the standard assumption that restricting the number of variables is a means to define decidable fragments of undecidable logics or to design counter/clock automata with decidable reachability problems, see e.g. [START_REF] Ibarra | Counter machines: Decidable properties and applications to verification problems[END_REF][START_REF] Finkel | Decidability of reachability problems for classes of two counters automata[END_REF][START_REF] Ouaknine | On the decidability of metric temporal logic[END_REF][START_REF] Lasota | Alternating timed automata[END_REF]. Furthermore this helps to understand the complexity gaps of decidable problems [START_REF] Demri | The complexity of propositional linear temporal logics in simple cases[END_REF][START_REF] Laroussinie | Model checking timed automata with one or two clocks[END_REF]. Our goal is therefore to identify decidable and undecidable fragments of Presburger LTL (both for model-checking and satisfiability problems) refining existing results from [START_REF] Bouajjani | Reachability analysis of pushdown automata: Application to model checking[END_REF][START_REF] Comon | Flatness is not a weakness[END_REF][START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF][START_REF] Demri | Verification of qualitative Zconstraints[END_REF].

Our contribution. We define CLTL(DL) as a fragment of Presburger LTL where atomic formulae are difference constraints. The underlying fragment of Presburger arithmetic in CLTL(DL) is identical to the one in the logic L p from [START_REF] Comon | Flatness is not a weakness[END_REF]. However, it is possible in CLTL(DL) to state constraints between counters at two non-consecutive states. For instance, "XXx = y" means that the value of y at the current state is equal to the value of x two states further. We call X-length the maximal number of X operators prefixing a counter. As far as undecidability is concerned, we show that satisfiability and model-checking over counter automata for CLTL(DL) either restricted to formulae of X-length two with at most one counter or to formulae of X-length one with at most two counters are Σ 1 1 -complete, improving results from [START_REF] Comon | Flatness is not a weakness[END_REF][START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF]. On the positive side, we prove that model-checking and satisfiability for CLTL(DL) are PSPACE-complete when restricted to X-length one and to one counter. Hence, we offer a complete and precise taxonomy of CLTL(DL) fragments with respect to decidability issue. We follow a standard automata-based approach [START_REF] Vardi | Reasoning about infinite computations[END_REF][START_REF] Kupferman | An automatatheoretic approach to branching-time model checking[END_REF] but we introduce an original symbolic representation of models that can be recognized by a fine-tuned class of one-counter automata (instead of standard Büchi automata). A nice property of this method is that it can be generalized to various LTL extensions that define ω-regular classes of models. Among the most technical parts of this work, we show that the nonemptiness problem for this class of counter automata where

• the counter is interpreted in Z,

• there are zero tests and sign tests,

• the accepted language is made of ω-sequences with Büchi acceptance condition,

• the updates of the counter correspond to add one of the values -1, 0, 1

is NLOGSPACE-complete.
This extends what is known about Büchi automata and variants of one-counter automata [START_REF] Lafourcade | Intruder deduction for AC-like equational theories with homomorphisms[END_REF][START_REF] Vardi | Reasoning about infinite computations[END_REF]. As far as we know, this is a new result obtained by analyzing runs. The details of the full proof are in [START_REF] Demri | The effects of bounding syntactic resources on Presburger LTL[END_REF]Sect. 6]. In addition, we show that model-checking LTL with quantifier-free Presburger constraints over onecounter automata is also PSPACE-complete.

Related work. Decidability and complexity issues for

LTL variants with Presburger constraints can be found in [START_REF] Bouajjani | On the verification problem of nonregular properties for nonregular processes[END_REF][START_REF] Comon | Flatness is not a weakness[END_REF][START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF][START_REF] Demri | Verification of qualitative Zconstraints[END_REF] (see also description logics with concrete domains in [START_REF] Lutz | NEXPTIME-complete description logics with concrete domains[END_REF] and logics of space and time in [START_REF] Balbiani | Computational complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning[END_REF]). Unlike these works, we are studying systematically the effects of bounding the number of variables and the X-length of formulae while preserving the logical operators. This contrasts with fragments shown to be decidable in [START_REF] Bouajjani | On the verification problem of nonregular properties for nonregular processes[END_REF][START_REF] Comon | Flatness is not a weakness[END_REF] (not closed under negation). Model-checking one-counter automata against modal µcalculus is in PSPACE [START_REF] Serre | Parity games played on transition graphs of onecounter processes[END_REF] and more generally modelchecking pushdown systems against modal µ-calculus is EXPTIME-complete [START_REF] Walukiewicz | Pushdown processes: games and modelchecking[END_REF] as well as linear µ-calculus [START_REF] Bouajjani | Reachability analysis of pushdown automata: Application to model checking[END_REF][START_REF] Finkel | A direct symbolic approach to model checking pushdown systems (extended abstract)[END_REF]. Herein we show that model-checking linear µ-calculus with quantifier-free Presburger constraints over one-counter automata is PSPACE-complete, refining the above-mentioned works. Satisfiability for this fragment is undecidable as a consequence of [START_REF] Minsky | Computation, Finite and Infinite Machines[END_REF]Sect. 14.2]. Furthermore, it is worth recalling that even though LTL can be expressed in the modal µ-calculus, these two formalisms have not the same conciseness on common fragment and therefore complexity results cannot always be transferred immediately. Because of lack of space, the omitted proofs can be found in the preliminary report [START_REF] Demri | The effects of bounding syntactic resources on Presburger LTL[END_REF].

Temporal logics, automata and Presburger constraints 2.1 From constraint languages to linear-time temporal logics

Constraint languages. Let VAR = {x 0 , x 1 , . . .} be a countably infinite set of variables. We consider several fragments of Presburger arithmetic (PA). The difference logic DL is defined by constraints of the form

E ::= x ∼ y + d | x ∼ d |E ∧ E | ¬E
where x, y ∈ VAR, d ∈ Z and ∼∈ {<, >, ≤, ≥, =}. We denote by DL + the extension of DL with periodicity constraints of the form either

x ≡ k c or x ≡ k y + c (k, c ∈ N).
Finally, QFP is the quantifier-free fragment of PA, defined by:

E ::= i∈I a i x i ∼ d | i∈I a i x i ≡ k c | E ∧ E | ¬E
where a i ∈ Z and I is a finite set of indices. Obviously, DL ⊆ DL + ⊆ QFP. Given a valuation v : VAR → Z, the satisfaction relation v |= E is defined in the obvious way. For instance, n ≡ k n iff there is z ∈ Z such that n = n + kz. All integers are encoded in binary.

Linear-time temporal logics. Given a constraint language L (typically DL, DL + or QFP), we define the logic CLTL(L) as the extension of LTL where the propositional variables are refined to atomic constraints from L over expressions representing different states of the variables. The formulae of CLTL(L) are defined by the grammar:

φ ::= E[x 1 ← X l 1 x j 1 , . . . , x n ← X l n x j n ] | φ ∧ φ | ¬φ | Xφ | φUφ where E[x 1 ← X l 1 x j 1 , . . . , x n ← X l n x j n ]
is a constraint of L with free variables x 1 , . . . , x n replaced by terms. A term is a variable x i prefixed by a certain number l of X symbols and is denoted by X l x i (its encoding requires O(l + log i) bits). The symbols X and U are respectively the classical operators "next" and "until" of LTL. We use the notations Fφ and Gφ as the abbreviations for Uφ and ¬F¬φ. A one-step constraint is an atomic formula of the form E

[x 1 ← X l 1 x j 1 , . . . , x n ← X l n x j n ] such that l 1 , . . . , l n ≤ 1.
Given a CLTL(L) formula φ we define its X-length |φ| X as the maximal number l such that a term of the form X l x occurs in φ. Intuitively, the X-length defines the size of a frame of consecutive states that can be compared. The models of CLTL(L) are ω-sequences of valuations σ : N → (VAR → Z) and the satisfaction relation is defined as for LTL except at the atomic level:

• σ, i |= E[x 1 ← X l 1 x j 1 ,..., x n ← X l n x j n ] iff (σ(i + l 1 )(x j 1 ),..., σ(i + l n )(x j n )) |= E in PA, • σ, i |= φ ∧ φ iff σ, i |= φ and σ, i |= φ , • σ, i |= ¬φ iff σ, i |= φ, • σ, i |= Xφ iff σ, i + 1 |= φ,
• σ, i |= φUφ iff there is j ≥ i such that σ, j |= φ and for every i ≤ k < j, we have σ, k |= φ.

The symbol |=, used at the level of the constraint language, is overloaded but this will not lead to any confusion. As usual, a formula φ ∈ CLTL(L) is satisfiable whenever there exists a model σ such that σ, 0 |= φ. We write CLTL l k (L) to denote the restriction of CLTL(L) to formulae with at most k variables and X-length less or equal to l. The satisfiability problem for CLTL(QFP) can be placed easily in the class Σ 1 1 from the analytical hierarchy.

Constraint automata. A k-variable L-automaton A is a structure Q, δ, I, F such that Q is a finite set of states, I ⊆ Q is the set of initial states, F ⊆ Q is the set of fi- nal states and δ ⊆ Q × A × Q where A is a finite subset of 1SC k (L)
, the set of Boolean combinations of one-step constraints from L built over the variables {x 1 , . . . , x k }. We use the notation q E -→ q as an abbreviation for q, E, q ∈ δ. A configuration of A is a tuple q, c ∈ Q × Z k and we denote by c(i) the i th value of c. The one-step transition relation -→ is defined as follows: q, c -→ q , c def ⇔ there exists q, E, q ∈ δ such that if each x i takes the value c(i) and each Xx i takes the value c (i), then E holds true. We write q, c E -→ q , c whenever we need to consider the constraint E on the transition. A finite (resp. infinite) path w is a sequence of the form {0, . . . , n} → (Q × Z k ) (resp. N → (Q × Z k )) such that for every i ∈ {0, . . . , n -1} (resp. for every i ∈ N) we have w(i) -→ w(i + 1). We note q, c -→ * q , c if there is a finite path from q, c to q , c . An accepting run for A is an infinite path w such that w(0) ∈ I × Z k and the set {i ∈ N : w(i) ∈ F × Z k } is infinite (standard Büchi acceptance condition). We write L symb (A) to denote the set of ω-words accepted by A viewed as an automaton over the alphabet A. A CLTL(L) model σ realizes an ω-word

E 0 E 1 • • • over A iff for every i ≥ 0, we have σ, i |= E i .

Model-checking.

The model-checking problem for CLTL(L) takes as inputs a CLTL(L) formula φ and an L-automaton A and checks whether there is a CLTL(L) model σ that realizes some word of L symb (A) and such that σ, 0 |= φ (we write A |= φ). For the restriction to CLTL l k (L), φ is in CLTL l k (L) and A is a k-variable Lautomaton. We present the existential version of the problem to simplify forthcoming developments since we also deal with satisfiability but results about the universal version can be withdrawn from those presented herein.

In the rest of the paper, we mainly consider DL +automata or subclasses that can simulate non-deterministic Minsky machines. We introduce below subclasses of DL-automata on which we will restrict in some places the model-checking problem.

Counter automata. A k-Z-counter automaton is a restricted DL-automaton such that each transition is of the form q E -→ q where E is a conjunction i∈{1...k}

E test i ∧ i∈{1...k} E update i with • E test i ∈ { } ∪ {x i ∼ 0 | ∼∈ {<, >, =, =}}, • E update i ∈ {Xx i = x i + u | u ∈ Z}
for every i. Moreover, we require that the initial values of the counters are equal to zero (with a zero test on every transition from an initial state). For ease of presentation, the elements of { } ∪ {x i ∼ 0 | ∼∈ {<, >, =, =}} are encoded by { , <, >, =, =}, the elements of {Xx i = x i +u | u ∈ Z} by Z and we order the constraints according to an arbitrary ordering of the variables. For instance, the transition

q ∧x 2 =0∧Xx 1 =x 1 ∧Xx 2 =x 2 -1 ------------------→ q is encoded by q ,=,0,-1 -----→ q .
A k-N-counter automaton is defined similarly except that we only consider non negative values for the counters. Obviously, one-Z-counter automata with updates in Z form a proper subclass of one-variable DL-automata that admit also constraints of the form Xx > x or Xx < x + d.

In Sect. 3, we define an automata-based approach which differs from [START_REF] Vardi | Reasoning about infinite computations[END_REF] by the use of one-Z-counter automata where the updates are restricted to {-1, 0, 1}, instead of classical Büchi automata. Such automata are called simple. Hence, counter automata are used as operational models (inputs of the model-checking problem) and also as language acceptors for adapting the automata-based approach from [START_REF] Vardi | Reasoning about infinite computations[END_REF]. Proving the existence of accepting runs for simple one-Z-counter automata is not immediate since we are dealing with Büchi acceptance condition, the counter is interpreted in Z and zero/sign tests are allowed.

Improving undecidability boundaries

Satisfiability for CLTL(DL) is undecidable since we can easily encode the executions of a Minsky machine with a CLTL(DL) formula. The proof of [START_REF] Comon | Flatness is not a weakness[END_REF] provides that CLTL 1 3 (DL) satisfiability is already Σ 1 1 -hard. We considerably refine this result by showing that one variable and X-length two or two variables and X-length one is enough for high undecidability.

Theorem 1 Satisfiability for CLTL 2 1 (DL) and CLTL 1 2 (DL) are Σ 1 1 -complete.
We refer to [14, Section 3.2] for the full proof that contains a reduction from the recurrence problem for nondeterministic Minsky machines, known to be Σ 1 1 -complete [1, Lemma 8]. Theorem 1 also refines the undecidability of CLTL ω 2 (DL) shown in [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF]. We present below the proof for the Σ 1 1 -hardness of CLTL 2 1 (DL) satisfiability. The proof for CLTL 1 2 (DL) is obtained by a reduction from CLTL 2 1 (DL) satisfiability (see [START_REF] Demri | The effects of bounding syntactic resources on Presburger LTL[END_REF]). Proof. (satisfiability for CLTL 2 1 (DL) is Σ 1 1 -hard) We show that the existence of an accepting run for two-Ncounter automata can be reduced to a satisfiability question in CLTL 2 1 (DL). First we show that for every two-N-counter automaton A, there is an equivalent two-N-counter automaton A computable in logarithmic space in |A| such that each transition of A changes at least the value of one counter.

Given a two-N-counter automaton

A = Q, δ, I, F , A = Q , δ , I , F is defined by: • Q def = Q ∪ {q t : t ∈ δ and t = q test 1 ,test 2 ,=,= ---------→ q }, I def = I and F def = F , • δ is defined from δ by replacing each transition t = q test 1 ,test 2 ,=,= ---------→ q ∈ δ by q test 1 ,test 2 ,+1,=
---------→ q t and q t , ,-1,= -----→ q .

One can verify that A has an accepting run iff A has an accepting run.

Now let A = Q, δ, I, F be a two-N-counter automaton such that at each transition at least one counter changes its value. We pose Q = {q 1 , . . . , q n }, I = {q α 1 , . . . , q α m } and

F = {q β 1 , . . . , q β m }. A configuration of q i , c 1 , c 2 is en- coded by a sequence of 2i states c 1 , c 1 +c 2 +1, . . . , c 1 , c 1 + c 2 + 1 by repeating i times the pair c 1 , c 1 + c 2 + 1. We re- call that a CLTL 2 1 (DL) model is simply an ω-sequence of integers. A new configuration is detected when four consec- utive values c, d, c , d are such that either c = c or d = d .
• Let φ ch be the formula stating a change of configuration:

φ ch = x < Xx ∧ (x = X 2 x ∨ X(x = X 2 x)).
• Before i states that we are just before the configuration with control state q i : Before

i def = φ ch ∧ X 2 ( 0≤j<i-1 X 2j (x = X 2 x ∧ X(x = X 2 x)) ∧ X 2(i-1) φ ch .
• Initial configuration:

φ init def = x 1 = 0 ∧ x 2 = 1 ∧ 1≤i≤m ( 0≤j<α i -1 X 2j (x = X 2 x ∧ X(x = X 2 x))∧ q α i ,φ,q j ∈δ X 2(α i -1) (φ ∧ Before j )). φ is defined below. • Recurring elements of F : φ rec def = 1≤i≤m GFBefore β i .
• Simulation of the run:

φ run def = G 1≤i≤n (Before i ⇒ q i ,φ,q j ∈δ X 2i (φ ∧ Before j ))
where φ is obtained from φ by replacing

-x 1 = 0 by x = 0, -x 2 = 0 by Xx = x + 1, -Xx 1 = x 1 + d 1 by X 2 x = x + d 1 for every d 1 ∈ {-1, 0, 1} and, -Xx 2 = x 2 + d 2 by d 1 ∈{-1,0,1} (X 2 x = x + d 1 ) ⇒ X(X 2 x = x + (d 1 + d 2 )) for every d 2 ∈ {-1, 0, 1}.
The automaton A has an accepting run iff φ init ∧φ run ∧φ rec is satisfiable. 2 Moreover, the satisfiability problem can be reduced to the model-checking problem since φ ∈ CLTL(DL) is satisfiable iff A |= φ where A is the DL-automaton that accepts all the executions (DL-automata are more liberal than counter automata).

Corollary 1

The model-checking problems for CLTL 1 2 (DL) and CLTL 2 1 (DL) are Σ 1 1 -complete.

The Σ 1 1 upper bound is obtained by reducing modelchecking to satisfiability for CLTL(DL) along the lines of [START_REF] Sistla | The complexity of propositional linear temporal logic[END_REF]. In order to simulate a proposition p, we use a constraint of the form x = 0 assuming that x is not used already for other purposes. By close inspection of the proof of Theorem 1, one can also show that satisfiability and modelchecking for CLTL 1 2 (DL) and CLTL 2 1 (DL) but restricted to the sometime operator F (instead of until) are also Σ 1 1hard.

results not only complete our classification but also many problems on one-counter automata/nets can be encoded in CLTL(DL + , PROP). These problems come from several applications: verification of cryptographic protocols [START_REF] Lafourcade | Intruder deduction for AC-like equational theories with homomorphisms[END_REF], validation of XML streams (string representations of XML documents) [START_REF] Chitic | On validation of XML streams using finite state machines[END_REF], or resolution of the identification problem [START_REF] Wakatsuki | Polynomial time identification of strict deterministic restricted onecounter automata in some class from positive data[END_REF]. By way of example, the class of one-variable DLautomata properly contains the one-counter automata that are used to validate XML streams against a recursive DTD in [START_REF] Chitic | On validation of XML streams using finite state machines[END_REF]Sect.5]. Below is the one-counter automaton recognizing the language {(ac) n a(ε|cc)a(ca) n b m b m : n, m ≥ 1} (we omit the tests related to zero):

c 1 a 0 a 2 c 3 a 5 c 4 c 6 a 7 b 9 b 8 a a c, x ++ a c a c a c c, x -- a b, x ++ b, x -- b, x -- b, x ++
where x is a counter and the alphabet is partitioned into a set of opening tags {a, b, c} and a set of corresponding closing tags {a, b, c}. The problem of checking whether a given word belongs to this language, a key problem in [9, Sect.5], can be expressed in our formalism. CLTL 1 1 (DL) can also express concisely richer standard properties, for instance non-trivial safety properties of the form G(x < 2 m ) or liveness properties such that G(x ≡ 2 n 0 ⇒ F(x ≡ 3 m 1)).

We dedicate the remaining of this section to prove decidability of the satisfiability problem for CLTL 1 1 (DL + , PROP), which is partially based on the abstraction of models. Without any loss of generality, we can assume that all the atomic formulae involving both x and Xx are of the form Xx ∼ x + d and Xx ≡ k x + c (d ∈ Z and k, c ∈ N).

Symbolic models

Let PROP = {p 1 , p 2 , . . .} be a countably infinite set of propositional variables. We define the logic CLTL(DL + , PROP) as the extension of CLTL(DL + ) by adding propositional variables at the atomic level. The main reason for introducing propositional variables stems from the fact that then satisfiability subsumes model-checking. Models of CLTL(DL + , PROP) are pairs σ 1 , σ 2 such that σ 1 : N → 2 PROP is a standard LTL model and σ 2 : N → (VAR → Z) is a CLTL(DL + ) model. The satisfaction relation is defined as for CLTL(DL) except at the atomic level:

σ 1 , σ 2 , i |= p def ⇔ p ∈ σ 1 (i) and given an atomic formula E based on DL + , σ 1 , σ 2 , i |= E def ⇔ σ 2 , i |= E in CLTL(DL + ).
There is no restriction on propositional variables in each fragment CLTL l k (DL + , PROP). In order to build an automaton that recognizes the symbolic models of a CLTL 1 1 (DL + ) formula, we introduce below a symbolic representation of valuations. Let X be a finite set of one-step constraints from DL + built over the variable x. We consider the following syntactic resources of X.

• CONS x = {d min , . . . , d -1 , d 0 , d 1 , . . . , d max } is the set of constants occurring in X in constraints of the form either x ∼ d or Xx ∼ d. We suppose that

d min < • • • < d -1 < d 0 < d 1 < • • • < d max .
• CONS step = {e min , . . . , e -1 , e 0 , e 1 , . . . , e max } is the set of constants occurring in X in constraints of the form Xx ∼ x + e. We suppose that e min < • • • < e -1 < e 0 < e 1 < • • • < e max .

• K is the least common multiple of the integers k such that ≡ k occurs in X.

Wlog, we can assume that d 0 = e 0 = 0, d max ≥ 0, e max ≥ 0, d min ≤ 0 and e min ≤ 0.

We define an abstraction of valuations like regions for timed automata and we shall prove that this abstraction fits exactly our goal. A map {x, Xx} → Z (also viewed as a pair

z 1 , z 2 ∈ Z 2 ) is represented by a tuple sv = E x , E m , E x , E m , E s ∈ C x × Mod x × C Xx × Mod Xx × C step (depending on X) such that for each term t ∈ {x, Xx}, • C t is composed of constraints of the form below -(d i < t) ∧ (t < d i+1 ) for i ∈ {min, .., max -1}, -t = d i for i ∈ {min, . . . , max}, -t < d min and d max < t, • Mod t is composed of the constraints t ≡ K c for c ∈ {0, . . . , K -1},
• C step is composed of constraints of the form x + e i < Xx ∧ Xx < x + e i+1 for i ∈ {min , . . . , max -1}, -Xx = x + e i for i ∈ {min , . . . , max }, -Xx < x + e min and x + e max < Xx.

We call such a tuple a symbolic valuation and we write SV(X) to denote the set of symbolic valuations w.r.t. X. Given a CLTL 1 1 (DL + , PROP) formula φ, SV(φ) is the set of symbolic valuations w.r.t. the set of atomic constraints occurring in φ. The size of SV(φ) is exponential in the size of φ and each element sv of SV(φ) can be encoded in polynomial space in the size of φ. By definition, we write v |= sv if the valuation v satisfies all the constraints in the symbolic valuation sv .

Lemma 1 Let X be a finite set of one-step constraints from CLTL 1 1 (DL + ) built over the variable x. (I) For every map v : {x, Xx} → Z there is a unique symbolic valuation in SV (X) denoted by sv (v) such that

v |= sv (v). (II) For all the maps v, v : {x, Xx} → Z such that sv (v) = sv (v ) and for every E ∈ X, v |= E iff v |= E. Proof. (I) Given sv ∈ SV(X), let V sv be the set of pairs z 1 , z 2 ∈ Z 2 such that z 1 , z 2 |= sv. It is easy to show that {V sv : sv ∈ SV(X), V sv = ∅} is a partition of Z 2 . (II) Let v and v be two valuations such that sv (v) = sv (v ) = E x , E x , E m , E m , E s and suppose that v |= E.
We proceed by induction on the structure of E.

• If E is of the form x = d then E x must be equal to E because d ∈ CONS x (and v |= E x ). Since v also satisfies E x , we have v |= E. • If E is of the form x < d then, (since v |= E x ), E x must be equal either to x = d with d < d or to d < x ∧ x < d with d ≤ d. Since v |= E x , we have v |= E.
• When E is of the form Xx ∼ d (resp. Xx ∼ x + d), the proof is similar, using the constraint E x (resp. E s ).

• Let E be of the form x ≡ k c. We consider the constraint E m of the form x ≡ K c . By definition, k divides K and so E m implies x ≡ k c r where c r is the remainder of the division of c by k. As c and c r belong to {0, . . . , k -1} and v satisfies both E and E m , c must be equal to c r . Since v |= E m and E m implies E, we have v |= E.

• When E is of the form Xx ≡ k c (resp. Xx ≡ k x + c) the proof is similar by using the constraint E m (resp. E m ∧ E m ).

• Now suppose that E and E are satisfied by v iff they are satisfied by v .

- 2 Given an atomic formula E from CLTL 1 1 (DL + ), we note sv |= symb E iff for every valuation v such that sv (v) = sv we have v |= E. A sequence of symbolic valuations w.r.t. φ is a word ρ : N → SV(φ) and ρ is satisfiable iff there is a model σ : N → Z for CLTL 1 1 (DL + ) such that for all i ∈ N, we have σ, i |= ρ(i) (we write σ |= ρ). A symbolic model w.r.t. φ is a pair σ 1 , ρ such that σ 1 : N → 2 PROP and ρ : N → SV(φ). The symbolic satisfaction relation |= symb is extended to symbolic models. The definition is identical to the satisfaction relation of CLTL(DL + , PROP) except for atomic constraints: σ, ρ , i

|= symb E def ⇔ ρ(i) |= symb E.

Automata-based approach

We show in the following that given a formula φ in CLTL 1 1 (DL + , PROP) we can build an automaton A φ recognizing symbolic representations of the models satisfying φ. In order to define A φ , we slightly extend the transitions of simple one-Z-counter automata (with updates in {-1, 0, 1}) by decorating them with elements from Σ ∪ {ε} where Σ is a finite alphabet and with the identical conditions about the constraints authorized in one-Z-counter automata. Since adding an alphabet is motivated by the need to consider the automata as language acceptors we define L (A) = {σ : N → (Σ ∪ {ε}) | there is an accepting run w such that ∀i w(i)

σ(i),E
---→ w(i + 1)} and L(A) = {σ \ε | σ ∈ L (A), elements of Σ occur infinitely often in σ} where σ \ε is obtained from σ by erasing all ε. L(A) is the language accepted by A. The construction of A φ relies on the following observation.

Lemma 2 A CLTL 1 1 (DL + , PROP) formula φ is satisfi- able iff there exist a symbolic model σ 1 , ρ such that σ 1 , ρ |= symb φ and a CLTL 1 1 (DL + ) model σ 2 such that σ 2 |= ρ.
Thus, A φ is defined as the intersection of two automata A symb and A sat such that L(A symb ) is the set of symbolic models that symbolically satisfies φ and L(A sat ) is the set of symbolic models σ 1 , ρ such that ρ is satisfiable. Both automata are simple one-Z-counter automata over the alphabet Σ = (2 PROP × SV(φ)) and A symb is essentially a finite-state automaton without counters. The automaton A symb is built as in [START_REF] Vardi | Reasoning about infinite computations[END_REF] for LTL except at the atomic level. We define cl (φ) the closure of φ with a slight modification to consider both atomic constraints and propositional variables and an atom of φ is a maximally consistent subset of cl (φ). Let A symb be the generalized Büchi automaton defined by the structure Q, δ, I, F such that:

• Q is the set of atoms of φ,

• I = {X ∈ Q : φ ∈ X}, • X P,sv , ,0 ------→ Y iff (atomic) P = X ∩ PROP and for every atomic E in X, sv |= symb E, (1-step) for every Xψ ∈ cl (φ), Xψ ∈ X iff ψ ∈ Y , • Let {ψ 1 Uφ 1 , . . . , ψ n Uφ n } be the set of until formulae in cl (φ). We pose F = {F 1 , . . . , F n } where F i = {X ∈ Q : ψ i Uφ i ∈ X or φ i ∈ X} for every i ∈ {1, . . . , n}.
The automaton A symb is the (non generalized) Büchi automaton equivalent to A symb which can be built in logarithmic space in the size of A symb . The automaton A φ is obtained by synchronizing A symb and A sat . Let us pose A symb = Q sy , δ sy , I sy , F sy and A sat = Q sa , δ sa , I sa , F sa . The automaton A φ = Q, δ, I, F is defined by:

• Q = Q sy × Q sa , I = I sy × I sa , F = F sy × Q sa (we will have Q sa = F sa ), • q 1 , q 2 ε,t,u --→ q 1 , q 2 ∈ δ def ⇔ q 1 = q 1 and q 2 ε,t,u --→ q 2 ∈ δ sa , • q 1 , q 2 P,sv ,t,u -----→ q 1 , q 2 ∈ δ def ⇔ q 1 P,sv , ,0
------→ q 1 ∈ δ sy and q 2 P,sv ,t,u -----→ q 2 ∈ δ sa .

Lemma 3 Given a formula φ, one can build a simple one-Z-counter automaton A sat with alphabet Σ = 2 PROP × SV(φ) such that L(A sat ) is the set of satisfiable symbolic models w.r.t φ. Moreover, A φ can be effectively built from φ in polynomial space thanks to the way A sat is defined.

Proof. We describe the construction of the automaton A sat recognizing exactly the set of symbolic models σ 1 , ρ such that ρ is satisfiable. We recall that the set CONS x is such that d 0 = 0, d max ≥ 0 and d min ≤ 0. The alphabet of A sat is 2 PROP × SV(φ) but since the set of propositional variables is not constrained in A sat , we omit them in the technical developments below. The construction of A sat is done in a modular fashion. A sat is made of a network of components/gadgets and it is of exponential size in the size of φ. A component is defined as a simple one-Z-counter automaton Σ, Q, δ, I, F such that

• I and F are singletons, • δ is a subset of (Q \ F ) × {ε} × { , =, =, >, <} × {-1, 0, 1} × (Q \ I).
The unique state in I (resp. F ) is called the input (resp. output) state of the component. Components are connected in the network by defining transitions between input states and output states. Each component in A sat has the function either to check a property of the counter from constraints in C x or to update the counter according to constraints in Mod x or Mod Xx × C step . We define below the components A E,sv for some

E ∈ C x ∪ Mod x ∪ (Mod Xx × C step )
and sv ∈ SV(φ). We write q E,sv in (resp. q E,sv out ) to denote the input (resp. output) state of A E,sv (when the context is clear we shortly write q in and q out , respectively). Each component A E,sv enforces that the next symbolic valuation that is guessed is precisely sv . For every sv = E x , E m , E x , E m , E s ∈ SV(φ), we define the following components:

• A E x ,sv is such that for every c ∈ Z, q E x ,sv in , c -→ * q E x ,sv out , c iff c = c and [x ← c] |= E x .
This component checks that c satisfies E x . Fig. 1 contains some graphical representation of components A x=d i ,sv and (a) A d i <x<d i+1 ,sv when d i ≥ 0. Components with d i ≤ 0 can be defined analogously.

q in q out 0 1 2 d i ε, >, -1 ε, >, -1 ε, , +1 ε, , +1 ε, =, 0 (b) q in q out 0 d j d i +1 d i+1 -1 ε, >, -1 ε, , +1 ε, =, 0 ε, =, 0
• A E m ,E s ,sv is such that for every c ∈ Z, [x ← c] |= E m and q E m ,E s ,sv in , c -→ * q E m ,E s ,sv out , c iff [x ← c, Xx ← c ] |= E m ∧ E s .
This component updates the counter according to E m , E s . Fig. 2 contains a graphical representation of the component

A E m ,E s ,sv with E m = x ≡ 2 1 (from sv ), E m = Xx ≡ 2 0 and E s = x < Xx < x + 7.
To build A E m ,E s ,sv , we determine on the fly (using E m , E m and E s ) that Xx = x + i for some i ∈ {1, 3, 5}.

q in q out ε, , +1 ε, , +1 ε, , +1 ε, , +1 ε, , +1 ε, , +1 ε, , +1 ε, , +1 Figure 2. A E m ,E s ,sv • A E m ,sv is such that for every c ∈ Z, q E m ,sv in , 0 -→ * q E m ,sv out , c iff [x ← c] |= E m .
This component updates the counter from 0 to a value satisfying E m (only used at the beginning of the run). Fig. 3 contains a graphical representation of some component

A x≡ K c,sv . q in q out 0 1 c +1 +(K -1) -1 -(K -1) ε, , +1 ε, , +1 ε, , -1 ε, , +1 ε, , -1 Figure 3. A x≡ K c,sv
The automaton A sat = Σ, Q, δ, I, F is defined as the "disjoint union" of the above-mentioned components with an additional initial state s 0 , F = Q and with the following additional transitions.

• For every sv = E x , E m , E x , E m , E s ∈ SV(φ), s 0 ε, ,0 --→ q E m
,sv in ∈ δ. This corresponds to decide which constraint E m the first value of the counter satisfies. The only way for the run to continue is to enter further in A E m ,sv .

• For every sv

= E x , E m , E x , E m , E s ∈ SV(φ), q E m ,sv out ε, ,0 --→ q E x ,sv in ∈ δ. When the control state is q E m ,sv
out , the counter satisfies E m . Now we want to check E x . So, the only way to continue the run is to enter in A E x ,sv .

• For every sv = E x , E m , E x , E m , E s ∈ SV(φ), q E x ,sv out ε, ,0 --→ q E m ,E s ,sv in ∈ δ. When the control state is q E x ,sv
out , this means that the counter satisfies E x and it is now time to update it according to E m , E s . The only way for the run to continue is to enter further in

A E m ,E s ,sv . • For all sv 1 = (E x ) 1 , (E m ) 1 , (E x ) 1 , (E m ) 1 , (E s ) 1 ∈ SV(φ) and sv 2 = (E x ) 2 , (E m ) 2 , (E x ) 2 , (E m ) 2 , (E s ) 2 ∈ SV(φ) s.t. (E x ) 1 [Xx ← x] = (E x ) 2
and

(E m ) 1 [Xx ← x] = (E m ) 2 , q (E m ) 1 ,(E s ) 1 ,sv 1 out sv 1 , ,0 ----→ q (E x ) 2 ,sv 2 in
∈ δ. The letter sv 1 can be read since all the verifications have been successful. The only way for the run to continue is to enter further in A (E x ) 2 ,sv 2 . A new symbolic valuation sv 2 is guessed but sv 2 has to agree with sv 1 on some constraints.

For all symbolic valuations sv

1 = (E x ) 1 , (E m ) 1 , (E x ) 1 , (E m ) 1 , (E s ) 1 ∈ SV(φ) and sv 2 = (E x ) 2 , (E m ) 2 , (E x ) 2 , (E m ) 2 , (E s ) 2 ∈ SV(φ)
, for all c, c ∈ Z, the propositions below are equivalent (by construction of the components):

(I) [x ← c] |= (E m ) 1 and q (E x ) 1 ,sv 1 in , c ε -→ * q (E m ) 1 ,(E s ) 1 ,sv 1 in , c ε -→ * q (E m ) 1 ,(E s ) 1 ,sv 1 out , c sv 1 -→ q (E x ) 2 ,sv 2 in , c ε -→ * q (E x ) 2 ,sv 2 out , c , (II) [x ← c, Xx ← c ] |= sv 1 .
We can now state the main property: the set of satisfiable symbolic models (with respect to a formula φ) is recognized by the simple one-Z-counter automaton A sat .

Let σ, ρ be a satisfiable symbolic model and for all i ∈ N,

ρ(i) = (E x ) i , (E m ) i , (E x ) i , (E m ) i , (E s ) i . So there is a CLTL 1 1 (DL) model σ : N → Z such that σ |= ρ.
We can show that σ, ρ ∈ L(A sat ) since there is an accepting run of the form

r 0 ε -→ q (E m ) 0 ,ρ(0) in , σ (0) ε -→ * q (E x ) 0 ,ρ(0) in , σ (0) ε -→ * q (E m ) 0 ,(E s ) 0 ,ρ(0) in , σ (0) ε -→ * q (E m ) 0 ,(E s ) 0 ,ρ(0) out , σ (1) ρ(0) -→ q (E x ) 1 ,ρ(1) in , σ (1) ε -→ * q (E m ) 1 ,(E s ) 1 ,ρ(1) in , σ (1) ε -→ * q (E m ) 1 ,(E s ) 1 ,ρ(1) out , σ (2) ρ(1)
-→ q

(E x ) 2 ,ρ(2) in , σ (2)
. . . Now suppose that σ, ρ ∈ L(A sat ). By construction of the network of components in A sat , there is an accepting run necessarily of the form

r 0 ε -→ q (E m ) 0 ,sv 0 in , c 0 ε -→ * q (E x ) 0 ,sv 0 in , c 0 ε -→ * q (E m ) 0 ,(E s ) 0 ,sv 0 in , c 0 ε -→ * q (E m ) 0 ,(E s ) 0 ,sv 0 out , c 1 ρ(0) -→ q (E x ) 1 ,sv 1 in , c 1 ε -→ * q (E m ) 1 ,(E s ) 1 ,sv 1 in , c 1 ε -→ * q (E m ) 1 ,(E s ) 1 ,sv 1 out , c 2 ρ(1) -→ q (E x ) 2 ,
i ∈ N, [x ← c i , Xx ← c i+1 ] |= (E x ) i ∧ (E m ) i ∧ (E x ) i ∧ (E m ) i ∧ (E s ) i . So the model σ : N → Z s.t. σ (i) = c i satisfies ρ, i.e. σ |= ρ.
This means precisely that σ, ρ is a satisfiable symbolic model.

2 In order to evaluate the complexity of the nonemptiness test for A φ , we also need the following result.

Theorem 2

The nonemptiness problem for simple one-Zcounter automata with alphabet is NLOGSPACE-complete.

The tedious proof of Theorem 2 (see [START_REF] Demri | The effects of bounding syntactic resources on Presburger LTL[END_REF]Sect. 6]) is based on the two following results. First, checking whether L(A) is non-empty for simple one-Z-counter automata A with alphabet can be reduced in logarithmic space to the existence of an accepting run in simple one-N-counter automata with no test x = 0 and no alphabet (easy). Second, checking the nonemptiness of automata from the latter class amounts to check the existence of paths of polynomial lengths satisfying specific properties. This second part requires careful and lengthy developments. We are now ready to state the main complexity result and its main corollary.

Theorem 3 Satisfiability for CLTL

1 1 (DL + , PROP) is PSPACE-complete.
The presence of propositional variables in CLTL(DL + , PROP) allows to reduce the model-checking problem for CLTL(DL + ) to the satisfiability problem for CLTL(DL + , PROP) (following [START_REF] Sistla | The complexity of propositional linear temporal logic[END_REF]). By inspection of the proof (see [START_REF] Demri | The effects of bounding syntactic resources on Presburger LTL[END_REF]Sect. 4.2]) we obtain a logspace reduction from the model-checking problem for CLTL 1 1 (DL + ) to the satisfiability problem for CLTL 1 1 (DL + , PROP).

Corollary 2 Satisfiability for CLTL 1 1 (DL + ) and modelchecking CLTL 1 1 (DL + ) formulae over 1-variable DL +automata are PSPACE-complete. PSPACE-hardness follows from PSPACE-hardness of satisfiability and model-checking for LTL restricted to one variable [START_REF] Demri | The complexity of propositional linear temporal logics in simple cases[END_REF]. As additional corollaries, we deduce that the one-variable fragment of the counter logic L p [START_REF] Comon | Flatness is not a weakness[END_REF] has a PSPACE-complete satisfiability problem and model-checking one-clock discrete timed automata with CLTL 1 1 (DL + ) can be done in PSPACE which contrasts with the undecidability results from [START_REF] Dang | Presburger liveness verification of discrete timed automata[END_REF]Section 6]. Corollary 2 can be extended by allowing propositional variables in the automata and formulae. More importantly, a quite remarkable separation feature of our technique is that we can adapt it to any extension LTL + of LTL for which formulae can be translated into Büchi automata in polynomial space. This includes extensions with past-time operators, with automata-based operators [START_REF] Wolper | Temporal logic can be more expressive[END_REF], or with fixpoint operator, see e.g. [START_REF] Vardi | A temporal fixpoint calculus[END_REF].

Theorem 4 (LTL + ) 1 1 (DL + ) model-checking and satisfiability are also in PSPACE.

It suffices to adapt the definition of A symb from plain LTL to LTL + , the automaton A sat from Lemma 3 being unchanged. As a corollary, model-checking linear µ-calculus with difference logic DL over one-variable DL-automata is PSPACE-complete, refining a result from [START_REF] Bouajjani | Reachability analysis of pushdown automata: Application to model checking[END_REF].

We conclude this section by a more prospective remark. Bounded model-checking [START_REF] Biere | Bounded model checking[END_REF] consists in searching for a counterexample in executions whose length is bounded by some integer m (encoded in binary). By adding to a finitestate system a counter that increments after each transition, one can concisely encode in our formalism the problem of finding a witness execution of length m. Of course, one needs to relativize the formulae: for instance pUq would become (x < m ⇒ p)U(x < m ∧ q).

Model-checking one-Z-counter automata

A natural question is whether Corollary 2 is optimal w.r.t. the Presburger fragment we have considered. Lemma 4 below states that we do not preserve decidability when extending the constraint language to QFP. Lemma 4 Satisfiability for CLTL 1 1 (QFP) and modelchecking CLTL 1 1 (QFP) formulae over 1-variable QFPautomata are Σ 1 1 -complete.

Constraints of the form ax + by = 0 where a, b ∈ Z allow to encode a configuration q i , c 1 , c 2 of a Minsky machine (q i is the ith control state) by the value 2 c 1 3 c 2 5 i and zero tests can be done using modulo relations. This follows directly from [26, Sect. 14.2] about one counter machines with multiplication and division by constants. In this section, the strategy to regain decidability consists in restricting the class of models to one-Z-counter automata. Modelchecking becomes decidable (even in PSPACE) for LTL with full quantifier-free Presburger constraints restricted to one variable but with no restriction on the X-length.

Let A = Q A , δ A , I A , F A be a one-Z-counter automaton (not necessarily simple) whose set of updates is of the form Xx = x + u with u ∈ {u min , u min + 1, . . . , u max }. Without any loss of generality, we can assume that u min = -u max . Given a CLTL ω 1 (QFP) formula φ such that |φ| X = l, we consider the following syntactic resources:

• K is the lcm of the integers k such that ≡ k occurs in φ,

• CONS is the set of constants d such that a i X i x ∼ d occurs in φ,

• COEF is the set of constants a i such that a i X i x ∼ d occurs in φ.

Without any loss of generality, we can assume that a min = -a max where a min and a max are respectively the minimal and the maximal element of COEF. For technical reasons (see details in [14, Sect. 5]), we pose

CONS(A, φ) = {d min , . . . , d max } such that d max = -d min = l(l+1)
2 a max u max . We define a symbolic valuation wrt A and φ as an element of the set

SV (A, φ) = C x × Mod x × C 1 step × • • • × C l step such that • C x is the set composed of the constraints x < d min , d max < x, and x = d for d ∈ CONS(A, φ).
• Mod x is the set composed of the constraints x ≡ K c for c ∈ {0, . . . , K -1}.

• C i step is composed of constraints X i x = X i-1 x + u for u ∈ {u min , . . . , u max }.
A result similar to Lemma 1 can be established. We define a symbolic satisfaction relation as in Sect. 3: sv |= symb E iff for every valuation v : {x, Xx, . . . , X l x} → Z such that sv (v) = sv we have v |= E. We can naturally extend this relation to symbolic valuation sequences.

Lemma 5 Let φ be a CLTL ω 1 (QFP) formula and A be a one-Z-counter automaton. A |= φ iff there are a symbolic model ρ ∈ SV (A, φ) such that ρ |= symb φ and an accepting run q 0 , c 0 , q 1 , c 1 , q 2 , c 3 , . . . of A such that c 0 , c 1 , c 2 . . . |= ρ.

We build the automaton A φ as the intersection A symb ∩ A sat such that A symb recognizes the set of symbolic models satisfying φ and A sat recognizes the set of symbolic models generated from accepting runs. The definition of A symb and the synchronization between A symb and A sat are similar to Sect. 3 considering the alphabet Σ = SV(A, φ) (with ε-transitions) and the corresponding relation |= symb . Lemma 6 below is a pivot result for proving Theorem 5 and its proof is a variant of the proof of Lemma 3.

Lemma 6 Given a formula φ and a one-Z-counter automaton A, one can build a simple one-Z-counter automaton

A sat with alphabet Σ = 2 PROP × SV(A, φ) such that L(A sat ) is the set of satisfiable symbolic models w.r.t φ and A. Moreover, A φ can be effectively built from φ and A in polynomial space thanks to the way A sat is defined.

Proof. Let A = Q A , I A , F A , δ A be a one Z-counter automaton and φ be a CLTL ω 1 (QFP) formula such that |φ| X = l. The automaton A sat is defined over the alphabet Σ = SV (A, φ). As in the proof of Lemma 3, the construction is modular. We denote Q A × Q the set of states of A sat where Q is a set of auxiliary states used in the construction of components similar to components in the proof of Lemma 3. For every sv = E x , E m , E 1 s , . . . , E l s and q a ∈ Q A , we define components:

• A q a E m ,sv such that for every c ∈ Z, q a , q E m ,sv in , 0 -→ * q a , q E m ,sv out , c iff [x ← c] |= E m .

• A q a E x ,sv such that for every c ∈ Z, q a , q E x ,sv in , c -→ * q a , q E x ,sv out , c iff c = c and [x ← c] |= E x . • We also need to define another kind of components that update the counter. For every d ∈ CONS(A, φ), A q a E 1 s ,sv is such that for every c ∈ Z, q a , q

E 1 s ,sv in , c -→ * q a , q E 1 s ,sv out , c iff [x ← c, Xx ← c ] |= E 1 s .
The different components are connected as follows:

• The set of initial states is composed of the states of the form q 0 , q E m ,sv in for every sv = E x , E m , E 1 s , . . . , E l s ∈ SV(φ, A) and q 0 ∈ I A . • For every sv = E x , E m , E 1 s , .., E l s ∈ SV(φ, A) and q 0 ∈ I A , q 0 , q E m ,sv out ε, ,0 --→ q 0 , q E x ,sv in ∈ δ.

• For all sv = E x , E m , E 1 s , . . . , E l s ∈ SV(φ, A), q a , q E x ,sv out ε, ,0

--→ q a , q E 1 s ,sv in ∈ δ.

• For all sv 1 = (E x ) 1 , (E m ) 1 , (E 1 s ) 1 , .., (E l s ) 1 ∈ SV(φ, A), sv 2 = (E x ) 2 , (E m ) 2 , (E 1 s ) 2 ,.., (E l s ) 2 ∈ SV(φ, A) and q a , q a ∈ Q A such that -(E 1 s ) 1 equals Xx = x + d and q a ∼,d -→ q a ∈ δ A for some ∼∈ { , <, >, =, =},

-(E 1 s ) 1 ∧ (E 1 m ) 1 ⇒ (E 1 m ) 2 is valid in PA (check- able in polynomial time), -for every 1 ≤ i ≤ l -1, (E i s ) 2 = (E i+1 s ) 1 [X i+1 x ← X i x, X i x ← X i-1 x],
we have q a , q E 1 s ,sv 1 out sv 1 ,∼,0 ----→ q a , q (E x ) 2 ,sv 2 in ∈ δ.

• The set of final states is { q f , q E x ,sv out | q f ∈ F A }.

By construction, for all paths • • • q i , q

(E x ) i ,sv i in , c i -→ • • • sv i -→ q i+1 , q (E x ) i+1 ,sv i+1 in , c i+1 • • • sv i+1 --→ • • • sv i+l-1 ----→ q i+l , q (E x ) i+l ,sv i+l in , c i+l • • • in A sat ,
we have c i , . . . , c i+l |= sv i .

2 Now we can conclude about the complexity of the model-checking problem.

Theorem 5 Model-checking CLTL ω 1 (QFP) formulae over one-Z-counter automata is PSPACE-complete. PSPACE-hardness is a consequence of [START_REF] Demri | The complexity of propositional linear temporal logics in simple cases[END_REF], see also a direct proof in [START_REF] Demri | The effects of bounding syntactic resources on Presburger LTL[END_REF]Sect. 5]. As for Theorem 4, model-checking linear µ-calculus with QFP constraints over one-Z-counter automata is in PSPACE, refining [START_REF] Bouajjani | Reachability analysis of pushdown automata: Application to model checking[END_REF]. By contrast, satisfiability for CLTL 1 1 (QFP) is undecidable.

Conclusion

Figure 4 summarizes the complexity of satisfiability, model-checking over DL-automata and model-checking over k-Z-counter automata for most LTL-like specification languages considered herein.

Apart from the completion of our classification, the more positive results concern one-counter automata/nets, see applications in [START_REF] Chitic | On validation of XML streams using finite state machines[END_REF][START_REF] Wakatsuki | Polynomial time identification of strict deterministic restricted onecounter automata in some class from positive data[END_REF][START_REF] Lafourcade | Intruder deduction for AC-like equational theories with homomorphisms[END_REF]. The PSPACE upper bound for model-checking one-Z-counter automata over CLTL ω 1 (QFP) or even over its linear µ-calculus extension refines results from [START_REF] Finkel | A direct symbolic approach to model checking pushdown systems (extended abstract)[END_REF][START_REF] Bouajjani | Reachability analysis of pushdown automata: Application to model checking[END_REF][START_REF] Walukiewicz | Pushdown processes: games and modelchecking[END_REF][START_REF] Serre | Parity games played on transition graphs of onecounter processes[END_REF] that concern more general systems and languages.

MC (DL)

SAT MC (CA) CLTL 1 3 (DL) undec. [START_REF] Comon | Flatness is not a weakness[END_REF] undec. [START_REF] Comon | Flatness is not a weakness[END_REF] undec.

[10] CLTL ω 2 (DL) undec. [START_REF] Minsky | Computation, Finite and Infinite Machines[END_REF] undec. [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF] undec. [

-

  If v |= E ∧ E then v |= E and v |= E . By the induction hypothesis v |= E and v |= E whence v |= E ∧ E . If v |= ¬E then v |= E. Using the induction hypothesis, we have v |= E and we conclude that v |= ¬E.

Figure 1 .

 1 Figure 1. (a) A x=d i ,sv and (b) A d i <x<d i+1 ,sv

  sv 1 in , c 2 . . . By construction of each component and by equivalence between (I) and (II) above, [x ← c 0 ] |= (E m ) 0 and for every

Figure 4 .

 4 Figure 4. Summary

  (DL or DL + ) PSPACE-c., Cor. 2 PSPACE-c., Cor. 2 PSPACE-c, Theo. 5 + [15] CLTL 1 1 (QFP) undec., Lem. 4 undec., Lem. 4 PSPACE-c, Theo. 5 + [15] CLTL ω 1 (QFP) undec., Lem. 4 undec., Lem. 4 PSPACE-c., Theo. 5 + [15]

				26]
	CLTL 2 1 (DL)	undec., Cor. 1	undec., Theo. 1	PSPACE-c, Theo. 5 + [15]
	CLTL 1 2 (DL)	undec. [26]	undec., Theo. 1	undec. [26]
	CLTL 1 1

PSPACE-completeness of CLTL 1 1 (DL + ) with propositional variablesTo complete the results of Section 2, we show that satisfiability for CLTL[START_REF] Alur | A really temporal logic[END_REF] 1 (DL) and model-checking CLTL 1 1 (DL) formulae over 1-variable DL-automata are PSPACEcomplete. To do so, we establish a PSPACE upper bound for satisfiability of the richer logic CLTL 1 1 (DL + , PROP), including periodicity constraints of the form x ≡ k y + c, x ≡ k c (k, c ∈ N) and propositional variables that can be viewed as specific variables with a strict discipline on their constraints. As a matter of fact, the above-mentioned

* Partially supported by project AVERISS (ANR) and bilateral CNRS/NRF project No19812.