Stéphane Demri

Amit Kumar Dhar

Arnaud Sangnier

Equivalence Between Model-Checking Flat Counter Systems and Presburger Arithmetic ?

We show that model-checking flat counter systems with the branching-time temporal logic CTL* extended with arithmetical constraints on counter values has the same worst-case complexity as the satisfiability problem for Presburger arithmetic. The lower bound already holds with strong restrictions: the logical language uses only the temporal operator EF and no arithmetical constraints, and the guards on the transitions are made of linear constraints. This work complements our understanding of model-checking flat counter systems with linear-time temporal logics, such as LTL, for which the problem is already known to be (only) NP-complete with guards restricted to the linear fragment.

Introduction

Branching-time temporal logics for counter systems. At first glance, modelchecking counter systems with temporal logics seems a hopeless enterprise since even the control-state reachability problem for Minsky machines is known to be undecidable [START_REF] Minsky | Computation, Finite and Infinite Machines[END_REF]. However, we are also aware that decidability can be regained by considering some syntactical or semantical restrictions on the systems. As a matter of fact, many subclasses of counter systems admit a decidable reachability problem and even better, sometimes the reachability sets are definable in Presburger arithmetic (PA) [START_REF] Presburger | Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt[END_REF]. This is the reason why model-checking problems with temporal logics have been considered for some of these classes like onecounter automata [START_REF] Göller | Branching-time model checking of parametric one-counter automata[END_REF][START_REF] Göller | Branching-time model checking of one-counter processes and timed automata[END_REF], Petri nets [START_REF] Habermehl | On the complexity of the linear-time mu-calculus for Petri nets[END_REF], reversal-bounded counter systems [START_REF] Bersani | The complexity of reversal-bounded model-checking[END_REF], flat counter systems [START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF]. The previous list is certainly not exhaustive and a general question is how to take advantage of the decidability of the reachability problem to conclude the decidability of model-checking problems with temporal logics. This provides a rich variety of decision problems, depending on the subclasses of counter systems and on the temporal logics at hand. If one considers the specific class of flat (a.k.a weak) counter systems (counter systems with all loops disjoint from each other), it has been shown that their reachability sets are definable in PA, see e.g. [START_REF] Boigelot | Symbolic methods for exploring infinite state spaces[END_REF][START_REF] Comon | Multiple counter automata, safety analysis and Presburger Arithmetic[END_REF][START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF][START_REF] Bozga | Safety problems are NP-complete for flat integer programs with octagonal loops[END_REF], and the model-checking of these systems with very expressive branching-time temporal logics is decidable [START_REF] Demri | Model-checking CTL ⇤ over flat Presburger counter systems[END_REF]. However in this latter work, no precise complexity analysis on the model-checking problem is performed. As an answer to that, recently in [START_REF] Demri | On the complexity of verifying regular properties on flat counter systems[END_REF] (see also [START_REF] Dhar | Algorithms for model-checking flat counter systems[END_REF]) a complete complexity analysis for model-checking flat counter systems with linear-time properties has been provided. In the present paper, we decide to focus on the modelchecking problem considering branching-time temporal logics, more specifically we consider a variant of CTL ⇤ [START_REF] Emerson | sometimes' and 'not never' revisited: on branching versus linear time temporal logic[END_REF] extended with atomic propositions which allows to describe for each position in the runs counter values.

Our motivations. As we have seen, reachability problems and the verification of linear-time properties for flat counter systems have been well-studied (see e.g. [START_REF] Demri | On the complexity of verifying regular properties on flat counter systems[END_REF][START_REF] Bozga | Safety problems are NP-complete for flat integer programs with octagonal loops[END_REF]) and our goal is to understand the computational complexity of modelchecking these systems with branching-time temporal logics such as CTL or CTL ⇤ (see e.g. [START_REF] Emerson | sometimes' and 'not never' revisited: on branching versus linear time temporal logic[END_REF]). There exist some classes of counter systems for which considering branching-time extensions, instead of simple (repeated) reachability questions, lead to undecidability. This is the case of Petri nets for which the model-checking of CTL is undecidable (with propositional variables only) whereas the reachability problem and model-checking problems with several LTL variants are known to be decidable [START_REF] Mayr | Persistence of vector replacement systems is decidable[END_REF][START_REF] Kosaraju | Decidability of reachability in vector addition systems (preliminary version)[END_REF][START_REF] Habermehl | On the complexity of the linear-time mu-calculus for Petri nets[END_REF]. As far as flat counter systems are concerned, we already know that we are on the safe side in the sense that decidability of model-checking with CTL ⇤ formulae is established in [START_REF] Demri | Model-checking CTL ⇤ over flat Presburger counter systems[END_REF] thanks to a translation into PA. However no lower bound is provided and the translation produces a formula which is exponentially bigger than the system given in input. This is rather unsatisfactory. Our main motivation is therefore to understand the complexity of model-checking flat counter systems with branching-time logics and to design optimal algorithms. Our contribution. We prove that the model-checking problem of flat counter systems with a version of CTL ⇤ equipped with arithmetical constraints on counter values is equivalent to the satisfiability problem for PA, modulo logarithmicspace reductions.

-For the complexity lower bound, we show that the satisfiability problem for PA can be reduced to the model-checking problem but there is no need for arithmetical constraints and for temporal operators other than EF. -For the complexity upper bound, we reduce the model-checking problem to the satisfiability problem in PA by using the fact that runs in flat counter systems can be encoded by tuples of natural numbers and then the semantics for CTL ⇤ can be internalised in PA. This last fact has been already observed in [START_REF] Demri | Model-checking CTL ⇤ over flat Presburger counter systems[END_REF] but herein, we provide a logarithmic-space reduction which makes a substantial difference with [START_REF] Demri | Model-checking CTL ⇤ over flat Presburger counter systems[END_REF]. Indeed, we are also able to quantify over path schemas (symbolic representation of potential infinite sets of runs), but concisely. Once more, this witnesses that verification problems can be encoded efficiently into PA, see e.g. [START_REF] Suzuki | Verification Decidability of Presburger Array Programs[END_REF][START_REF] Fribourg | Proving safety properties of infinite state systems by compilation into Presburger arithmetic[END_REF][START_REF] Bruyère | Durations, parametric model-checking in timed automata with Presburger arithmetic[END_REF]. -As a consequence, we are able to get the equivalence with PA to known branching-time temporal logics stronger than CTL EF (such as CTL) and our proof works as well when considering past-time operators.. Moreover, we compare the translation with PA fragments to obtain a more precise complexity of subproblems of the model-checking problem. From the known complexity characterization of PA fragments [START_REF] Haase | Subclasses of Presburger arithmetic and the weak EXP hierarchy[END_REF], we also deduce a finer characterisation of the complexity of model-checking problem for fragments of CTL ⇤ over flat counter systems. As far as proofs are concerned, for the lower bound, we take advantage of the observation that a quantification in PA over a variable z can be simulated by a loop that increments a corresponding counter and there is a correspondence between the first-order quantifier 9 [resp. 8] and the temporal connective EF [resp. AG]. For the upper bound, quantification over path schemas is done directly followed by a quantification over the number of times loops are visited. However, we provide a new way to encode runs in flat counter systems, which is rewarding complexity-wise. Not only the complexity bound we get is better than the one given in [START_REF] Demri | Model-checking CTL ⇤ over flat Presburger counter systems[END_REF] but also our reduction into PA is much simpler, and therefore this leaves some hope to incorporate it in a tool which will use then some solvers for PA or fragments, see e.g. [START_REF] De Moura | Z3: An Efficient SMT Solver[END_REF][START_REF] Leroux | TaPAS: The Talence Presburger Arithmetic Suite[END_REF][START_REF] Barrett | CVC4[END_REF].

Plan of the paper. In Section 3, we provide the preliminary definitions whereas Section 4 establishes the lower-bound results thanks to a reduction of the satisfiability problem for PA into model-checking flat counter systems with CTL EF . Section 5 presents the reduction of model-checking CTL ⇤ over flat counter systems to the satisfiability problem for PA. More precisely, Section 5.1 presents a way to encode runs using a small amount of integer vectors, whereas Section 5.2 shows a way to construct a PA formula to check the validity of a run represented by such integer vectors. Section 5.3 deals with the encoding of an instance of the model-checking problem for CTL ⇤ by some Presburger arithmetic formula, which leads us to the optimal complexity upper bound. Section 6 shows that the global model-checking problem can be also solved thanks to the established translation into PA. Section 7 provides a more involved translation of modelchecking problem to PA in order to get a better comparison between fragments of CTL ⇤ and known PA fragments.

The present paper is an extended and completed version of [START_REF] Demri | Equivalence between model-checking flat counter systems and Presburger arithmetic[END_REF]. It includes all the proofs and a bit more explanations in several places. Furthermore, we have added a few more results, namely the use of past-time operators in the logic and the result about global model-checking obtained as a by-product and study of the model-checking problem for the fragments of CTL ⇤ . Moreover, the material in Section 7 is new.

Omitted proofs can be found in the technical appendix.

Related Work

In this section, we provide a more systematic presentation of related works, maybe at the price of little redundancy with the previous section.

Model-checking problems & PA:

It is well-known that many verification problems can be shown decidable by translation into decision problems on Presburger arithmetic, see e.g. [START_REF] Suzuki | Verification Decidability of Presburger Array Programs[END_REF][START_REF] Fribourg | Proving safety properties of infinite state systems by compilation into Presburger arithmetic[END_REF][START_REF] Bruyère | Durations, parametric model-checking in timed automata with Presburger arithmetic[END_REF]. A typical situation arises when the sets of reachable configurations can be defined by formulae in Presburger arithmetic, as it is done, for instance, for one-counter automata [START_REF] Haase | Reachability in succinct and parametric one-counter automata[END_REF], reversal-bounded counter systems [START_REF] Ibarra | Reversal-bounded multicounter machines and their decision problems[END_REF], flat counter systems [START_REF] Comon | Multiple counter automata, safety analysis and Presburger Arithmetic[END_REF]. These results have paved the way to further interests in model-checking of logical formulas over these subclasses.

Similar to the case of reachability sets, many different model-checking problems over the subclasses of counter systems have been studied in connection with PA. For example, in [START_REF] Lechner | Model Checking Flat Freeze LTL on One-Counter Automata[END_REF], the authors have translated the problem of modelchecking flat freeze LTL formulas over one-counter automata to PA formulas and thereby reducing the problem to the satisfiability problem of PA. Similarly, translations of model-checking problems over reversal-bounded counter systems have been performed in [START_REF] Hague | Model checking recursive programs numeric data types[END_REF][START_REF] Bersani | The complexity of reversal-bounded model-checking[END_REF].

Verification of flat counter systems: Similar to other classes of systems, PA has been used significantly for model-checking problems over flat counter systems. It was shown initially that the set of reachable configurations for flat counter systems are Presburger definable [START_REF] Comon | Multiple counter automata, safety analysis and Presburger Arithmetic[END_REF] (see also [START_REF] Bozga | Safety problems are NP-complete for flat integer programs with octagonal loops[END_REF]). In [START_REF] Demri | Model-checking CTL ⇤ over flat Presburger counter systems[END_REF], the authors considered a subclass of counter systems (which are flat but more powerful than those considered in the present paper), a more expressive logical specification than considered in this paper and showed a translation from the model-checking problem to PA formulas.

Model-checking problem with various logics over flat counter systems and their optimal complexity characterization have been studied. In [START_REF] Demri | Taming Past LTL and Flat Counter Systems[END_REF], it was shown that model-checking LTL with past over flat counter systems is NP-complete. Subsequently, in [START_REF] Demri | On the complexity of verifying regular properties on flat counter systems[END_REF], a PSpace-complete characterization was shown for regular properties. A logical step in this connection as suggested in the future work section of [START_REF] Demri | On the complexity of verifying regular properties on flat counter systems[END_REF], is to investigate the model-checking problem over flat counter systems in the context of branching-time temporal logics. In terms of the techniques used in this paper, it is more related to the work done in [START_REF] Demri | Model-checking CTL ⇤ over flat Presburger counter systems[END_REF]. Even though the translation presented in [START_REF] Demri | Model-checking CTL ⇤ over flat Presburger counter systems[END_REF] shows the decidability of the model-checking problem, the translation itself witnesses an exponential blow-up. We show that the translation was non-optimal by giving a better translation in the current paper.

3 Counter systems and branching-time temporal logics

Presburger arithmetic

Presburger arithmetic (PA) is the first-order theory of natural numbers with addition. It was introduced by M. Presburger who has shown the decidability of its satisfiability problem by quantifier elimination [START_REF] Presburger | Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt[END_REF]. We recall here the syntax and interpretation of this theory.

In the paper, we consider VAR = {z 1 , z 2 , z 3 , . . .}, a countably infinite set of variables. Terms are expressions of the form

t ::= a 2 N | a.z | t 1 + t 2 ,
where a and k are in N and, z belongs to VAR. A valuation f is a map VAR ! N and it can be extended to the set of all terms inductively as follows:

f (a) def = a f (az) def = a ⇤ f (z) f (t 1 + t 2 ) def = f (t 1 ) + f (t 2 ). Given a valuation f , a variable z and a natural n, the notation f [z 7 ! n] rep- resents the valuation f 0 such that f 0 (z 0 ) = f (z 0
) for all z 0 2 VAR \ {z} and f 0 (z) = n. Formulae of PA are defined by the grammar

::= t  t 0 | ¬ | ^ | 9 z ,
where t and t 0 are terms and z 2 VAR. We denote the class of formulae without any quantifier as the linear fragment of PA. Thus, A formula is in the linear fragment def , is a Boolean combination of atomic formulae of the form t  t 0 . The semantics for formulae in PA is defined with the satisfaction relation |= which says whether a valuation f satisfies a formula : for instance

f |= t  t 0 def , f (t)  f (t 0
) and f |= 9 z def , there is n 2 N such that f [z 7 ! n] |= . We write (z 1 , . . . , z n ) to denote a formula such that its free variables are among z 1 , . . . , z n . A formula (z 1 , . . . , z n ) with n 1, defines a set of n-tuples

J (z 1 , . . . , z n )K def = {hf (z 1 ), . . . , f(z n )i 2 N n : f |= }.
For v 2 N n , we also write v |= instead of v 2 J (z 1 , . . . , z n )K. For a given PA formula , the set of free variables of is denoted by free( ). The satisfiability problem for PA (also written SAT(PA)) is then the decision problem that takes as input a formula and asks whether there is a valuation f such that f |= . If such a valuation exists, we say that is satisfiable. Decidability of Presburger arithmetic has been shown in [START_REF] Presburger | Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt[END_REF]. An exact complexity characterization is provided in [START_REF] Berman | The complexity of logical theories[END_REF] and a precise study with respect to the quantifier alternation is done in [START_REF] Haase | Subclasses of Presburger arithmetic and the weak EXP hierarchy[END_REF]. Guards can be made quite general and any Presburger formula can be allowed. Since we provide a translation into PA, this can allow us to consider a more general model, as in Presburger counter machines [START_REF] Demri | Model-checking CTL ⇤ over flat Presburger counter systems[END_REF][START_REF] Leroux | Presburger counter machines[END_REF]. However, since we will be talking about precise characterization of problems where quantifier alternation is crucial, we restrict our guards to be from the linear fragment of Presburger arithmetic For each transition = hq, g, u, q 0 i in , we use the following notations:

Counter systems

Let C = {x 1 ,
-Q is a finite set of control states, - ✓ Q ⇥ G n ⇥ Z n ⇥ Q is a
source( ) = q, target( ) = q 0 , guard ( ) = g and update( ) = u. As usual, to a counter system S = hQ, C n , , `i, we associate a labelled transition system T(S) = hC, !i where C = Q ⇥ N n is the set of configurations and !✓ C ⇥ ⇥ C is the transition relation defined by: hhq, vi, , hq 0 , v 0 ii 2! (also written hq, vi ! hq 0

,

v 0 i) iff -q = source( ), -q 0 = target( ), -v |= guard ( ) and -v 0 = v + update( ).
We write c ! c 0 iff there exists some edge such that c ! c 0 . Given c 0 2 Q ⇥ N n , a run ⇢ starting from c 0 in S is a (possibly infinite) path in the associated transition system T(S) denoted as

⇢ := c 0 0 ! • • • m 1 ! c m m ! • • •
where c i 2 Q ⇥ N n and i 2 , for all i 2 N. Then, let trans(⇢) be the !-word 0 1 . . . made of transitions appearing in the run ⇢. For every i 0, we define

⇢[i] = c i and ⇢ i = c 0 0 ! c 1 • • • i 1 ! c i .
We write c ! ⇤ c 0 iff there exists a run ⇢ and i 2 N such that ⇢[0] = c and ⇢[i] = c 0 . Note that a run in a counter system S is either finite or infinite. A run ⇢ is maximal iff either it is infinite, or it is finite and the last configuration is a deadlock (i.e., it does not have any successor configurations). For a finite maximal run ⇢, we write |⇢| = ↵ where ⇢[↵] is the deadlock configuration. For an infinite maximal run ⇢, we have |⇢| = !.

A counter system is flat if every node in the underlying graph belongs to at most one simple cycle (a cycle being simple if no edge is repeated twice in it) [START_REF] Comon | Multiple counter automata, safety analysis and Presburger Arithmetic[END_REF][START_REF] Leroux | Flat counter automata almost everywhere! In ATVA[END_REF]. In a flat counter system, simple cycles can be organized as a DAG where two simple cycles are in the relation whenever there is a path between a node of the first cycle and a node of the second cycle. We write FlatCS to denote the class of flat counter systems.

Logical specifications

We consider a logic that extends the classical CTL ⇤ [14] by adding past-time temporal operators and arithmetical constraints on counter values. By a slight abuse of notation, the logic is also called CTL ⇤ . Since this logic will be used to describe runs of a counter machine equipped with a set of counters C n = {x 1 , . . . , x n }, we assume that the dimension n is known when giving formulae. The CTL ⇤ formulae are defined as follows:

::= p | (x 1 , . . . , x n ) | ^ | ¬ | X | U | X 1 | S | E
where p 2 AT and (x 1 , . . . , x n ) is a Presburger formula with free variables in C n . We write CTL EF to denote the fragment of CTL ⇤ in which the only (unary) temporal operator is EF (EF

def = E (> U ) and > def = (x 1 = x 1 )
). Our version of CTL ⇤ is defined as the standard version with past-time operators, see e.g. [START_REF] Emerson | sometimes' and 'not never' revisited: on branching versus linear time temporal logic[END_REF], except that the Kripke structures are replaced by transition systems from counter systems and at the atomic level, arithmetical constraints are allowed.

Let S = hQ, C n , , `i be a counter system with transition system T(S) = hC, !i. Given a maximal run ⇢ in S and a position i  |⇢|, the satisfaction relation |= for CTL ⇤ is defined as follows:

⇢, i |= p def , p 2 `(q), where ⇢[i] = hq, vi ⇢, i |= (x 1 , . . . , x n ) def , v |= (x 1 , . . . , x n ), where ⇢[i] = hq, vi ⇢, i |= X def , i + 1  |⇢| and ⇢, i + 1 |= ⇢, i |= 1 U 2 def , ⇢, j |= 2 for some i  j such that j  |⇢| and ⇢, k |= 1 for all i  k < j ⇢, i |= X 1 def , i > 0 and ⇢, i 1 |= ⇢, i |= 1 S 2 def , ⇢, j |= 2 for some j  i such that j 0 and ⇢, k |= 1 for all j < k  i ⇢, i |= E def , there is a maximal run ⇢ 0 s.t. ⇢ 0 i = ⇢ i and ⇢ 0 , i |= .
Given a CTL ⇤ formula , a counter system S and a configuration c from S, we say that S, c |= iff there exists a maximal run ⇢ in S with ⇢[0] = c such that ⇢, 0 |= . Note that the symbol |= is overloaded but this shall not cause any confusion. A flat counter system S is called non-blocking if every maximal run ⇢ in S is infinite. Otherwise it is called a blocking flat counter system. The model-checking problem for flat counter systems over CTL ⇤ is defined as follows (let us call it MC(CTL ⇤ , FlatCS)):

Input: A flat counter system S, a configuration c and a formula in CTL ⇤ Output: Do we have S, c |= ?

We know that MC(CTL ⇤ , FlatCS) is decidable [START_REF] Demri | Model-checking CTL ⇤ over flat Presburger counter systems[END_REF] but its exact complexity is not fully characterised (actually, this is the main purpose of the present paper). The restriction to LTL formulae is known to be NP-complete [START_REF] Demri | Taming Past LTL and Flat Counter Systems[END_REF] when guards are restricted to the linear fragment. In Section 4, we show that SAT(PA) can be reduced to MC(CTL ⇤ , FlatCS) restricted to CTL EF without arithmetical constraints and to flat counter systems such that the guards are simple linear constraints. By contrast, model-checking flat finite Kripke structures over CTL ⇤ is P 2 -complete [START_REF] Emerson | Modalities for model checking: Branching time logic strikes back[END_REF][START_REF] Laroussinie | Model checking CTL + and FCTL is hard[END_REF].

From blocking to non-blocking flat counter systems

We shall see now that we can restrict our attention to non-blocking flat counter systems where all the maximal runs are infinite. The idea is that we can transform using logarithmic space an instance of the model-checking problem with any flat counter systems into one where the counter system is flat and non-blocking.

Let L be either CTL ⇤ or CTL EF , S = hQ, , C n , `i a flat counter system, c a configuration and a formula in L. We will show how to build in logarithmic space a non-blocking flat counter system S 0 , a configuration c 0 and a formula 0 in L such that S, c |= iff S 0 , c 0 |= 0 . Roughly speaking, the counter system S 0 is obtained from S by adding a new state q ? that is reachable whenever a deadlock configuration is reached in S and q ? has a self-loop with no effect on counters. The formula 0 is obtained from by relativisation related to the control state q ? .

We construct S 0 = hQ 0 , 0 , C n , `0i as follows:

-Q 0 def = Q ] {q ? }.
-`0(q ? ) def = {p ? } where p ? is a new propositional variable and for all q 2 Q, `0(q) def = `(q). -0 def = [ {hq, ¬g q , 0, q ? i|q 2 Q} [ {hq ? , >, 0, q ? i} where for every state

q 2 Q, g q = W source( )=q guard ( ).
Observe that since S is flat, the counter system S 0 is flat too. We define then a formula map t(•) for formulas in CTL ⇤ such that t(•) is the identity for the atomic formulae, is homomorphic for Boolean connectives, for the temporal operators X 1 and S and for the path quantifier E and, it satisfies the following simple clauses:

-t(X ) def = X(¬p ? ^t( )). -t( U 0 ) def = t( )U(¬p ? ^t( 0 ))
). When dealing with the fragment CTL EF , these two clauses are replaced by t(EF ) = EF(¬p ? ^t( )). Then, we have the following result whose detailed proof can be found in Appendix A.

Lemma 2. S 0 is a non-blocking flat counter system, t( 0) belongs to L and S, c |= iff S 0 , c |= t( ). Thanks to Lemma 2, in the sequel only non-blocking flat counter systems are considered. Furthermore, since the reachability relation is definable in PA for flat counter systems [START_REF] Demri | Model-checking CTL ⇤ over flat Presburger counter systems[END_REF], it is even possible to decide whether all maximal runs from a given configuration are infinite. [START_REF] Boigelot | Symbolic methods for exploring infinite state spaces[END_REF] From SAT(PA) to a subproblem of MC(CTL ⇤ , FlatCS)

Atomic formulae in CTL ⇤ are arbitrary Presburger formulae with free variables in {x 1 , . . . , x n }. Consequently, it is easy to reduce (in logarithmic space) SAT(PA)

to MC(CTL ⇤ , FlatCS). Clearly, this is not interesting and the generality of the guards and the logical atomic formulae in the paper is only considered because, when establishing the complexity upper bound, we can be quite liberal. Below, we show that a very restricted fragment of MC(CTL ⇤ , FlatCS), simply called MC (CTL ⇤ , FlatCS), is already as hard as the satisfiability problem for PA and our reduction is based on a simple correspondence between quantifiers in PA and the temporal operators EF and AG in CTL ⇤ . First, we define MC (CTL ⇤ , FlatCS) as the subproblem of MC(CTL ⇤ , FlatCS) with the two following restrictions:

1. atomic formulae are restricted to propositional variables (no arithmetical constraints on counter values) and the only temporal connective is EF (and its dual AG, by closure under negation); 2. the guards on the transitions are linear constraints t  t 0 or their negations.

So, there are no Boolean connectives and no first-order quantifications.

Theorem 3. There is a logspace reduction from SAT(PA) to MC ( CTL ⇤ , FlatCS).

Proof. Let be a formula in PA. Without any loss of generality, we can assume that has the following form:

Q 1 z 1 Q 2 z 2 • • • Q n z n 0 (z 1 , z 2 , . . . , z n ) with Q 1 , Q 2 , . . . , Q n 2 {9, 8}
and 0 is a quantifier-free formula. Note that given any formula in PA, we can reduce it to an equivalent formula of this form in logarithmic space (which is then fine for our main result since logarithmic-space reductions are closed under composition [START_REF] Papadimitriou | Computational complexity[END_REF]). This is essentially based on the construction of formulae in prenex normal form in first-order logic.

Let us consider the counter system S defined below in Figure 1 where e i 2 N n is the ith unit vector. Observe that 0 (x 1 , x 2 , . . . , x n ) may contain Boolean connectives but we can get rid of them in S . In order to eliminate the Boolean connectives in the guard of the transition between q n and q n+1 , we follow two simple rules, while preserving flatness (easy to check since that transition does not belong to a loop). We explain now our technique. Without any loss of generality, we can assume that negations are only in front of linear constraints.

For each transition of the form q ,0 ! q 0 with being a formula with Boolean connectives, we disintegrate it into a flat system such that there exists a run from q to q 0 iff v |= holds for any configuration hq, vi. A transition q 1 ^ 2 ,0 ! q 0 is replaced by q 1 ,0 ! q 00 2 ,0 ! q 0 where q 00 is new. Similarly, a transition q

1 _ 2 ,0
! q 0 is replaced by q 1 ,0 ! q 0 and q 2 ,0 ! q 0 , assuming that q does not belong to a loop. It is easy to show that S can be transformed into a flat counter system S 0 by applying the two rules above as much as possible so that eventually, S 0 is a counter system matching the requirements of MC (CTL ⇤ , FlatCS). This is a standard way of decomposing and representing a positive Boolean combination of literals. For the ease of the proof, we will actually prove the properties of S as shown in Figure 1.

Below, we define in CTL EF whose atomic formulae are among q 1 , . . . , q n+1 (also abusively understood as control states) such that ( †) S , hq 0 , 0i |= iff is satisfiable in PA. Intuitively, each variable z i from is taken care of by the ith loop (that can only increment the ith counter). This is not enough, and additionally, the quantifications from are simulated in the formula by using EF or AG, depending whether the first-order quantification is either existential or universal. Below, we define formally the formulae

i with i 2 [1, n + 1] so that def = 1 : i def = 8 < : EF(q i ^ i+1 ) i  n and Q i = 9 AG(q i ) i+1 ) i  n and Q i = 8 EFq n+1 i = n + 1 Given a valuation f : VAR ! N, we write v f 2 N n to denote the vector such that v f [i] def = f (z i ) for every i 2 [1, n].
In order to establish ( †) it is sufficient to show the following property ( † †).

( † †).1 for all valuations f , we have

f |= 0 (z 1 , z 2 , . . . , z n ) iff hq n , v f i |= n+1 , ( † †).2 for all i 2 [1, n] and valuations f such that f (z i ) = • • • = f (z n ) = 0, we have f |= Q z i • • • Q n z n 0 (z 1 , z 2 , . . . , z n ) iff hq i 1 , v f i |= i .
It is easy to see that, we get the property ( †) by applying ( † †).2 with i = 1.

First, we prove ( † †).1. Recall that n+1 = EF q n+1 and the only edge between q n and q n+1 is the following:

q n 0 (x1,...,xn),0 ! q n+1
Let f be a valuation. By the definition of |=, we have

hq n , v f i |= EF q n+1 iff v f |= 0 (x 1 , . . . , x n ). By definition of v f , we get v f |= 0 (x 1 , . . . , x n ) iff f |= 0 (z 1 , z 2 , . . . , z n
). Now we prove ( † †).2 by induction. The base case i = n + 1 corresponds precisely to the satisfaction of the property ( † †).1. Suppose that ( † †).2 holds for i + 1, we show that it holds for i too. Case 1:

Q i = 9. Let f be a valuation such that f (z i ) = • • • = f (z n ) = 0. We prove that f |= 9 z i • • • Q n z n 0 (z 1 , . . . , z n ) iff hq i 1 , v f i |= EF(q i ^ i+1 ). 10 First, assume that f |= 9 z i • • • Q n z n 0 (z 1 , . . . , z n ). By assumption, there exists a 2 N such that f [z i 7 ! a] |= Q i+1 z i+1 • • • Q n z n 0 (z 1 , z 2 , . . . , z n ). By the induction hypothesis, hq i , v f 0 i |= i+1 where f 0 = f [z i 7 ! a]
. Now consider the transition system T(S ) and its configuration hq i 1 , v f i. There is a run ⇢ in T(S) starting from hq i 1 , v f i that reaches q i where the loop l i is visited exactly a times. Since the effect of the simple loop l i is to increment the counter x i each time, and v f [i] = 0, there is a finite run from

hq i 1 , v f i to hq i , v f 0 i. So, hq i 1 , v f i |= EF(q i ^ i+1 ).
On the other hand, assume that

hq i 1 , v f i |= EF(q i ^ i+1 ). By definition of |=, there exists a run ⇢ in T(S ) with ⇢[0] = hq i 1 , v f i such that for some position j  |⇢|, ⇢[j] |= q i ^ i+1 . Thus, ⇢[j] = hq i , v 0 i for some v 0 2 N n . Since q i is
reached only after taking the simple loop l i , let us assume that the loop l i is taken a 0 times. Since, the effect of the simple loop l i is to increment the counter x i each time, v 0

[i] = a and v f and v 0 differ only on the ith component.

So, v 0 = v f 0 where f 0 = f [z i 7 ! a]. Since hq i , v f 0 i |= i+1 , by the induction hypothesis f [z i 7 ! a] |= Q i+1 z i+1 • • • Q n z n 0 (z 1 , z 2 , . . . , z n ). By definition of |= in PA, we conclude that f |= 9 z i • • • Q n z n 0 (z 1 , . . . , z n ). Case 2: Q i = 8. Let f be a valuation such that f (z i ) = • • • = f (z n ) = 0. We prove that f |= 8 z i • • • Q n z n 0 (z 1 , . . . , z n ) iff hq i 1 , v f i |= AG(q i ) i+1 ). First, we assume that f |= 8 z i • • • Q n z n 0 (z 1 , . . . , z n ). By assumption, for all a 2 N we have f [z i 7 ! a] |= Q i+1 z i+1 • • • Q n z n 0 (z 1 , z 2 , . . . , z n ).
By the induction hypothesis, we have hq i , v f 0 i |= i+1 where f 0 = f [z i 7 ! a] with a 2 N. Now consider the transition system T(S ) and its configuration hq i 1 , v f i. There are two types of run ⇢ in T(S) starting from hq i 1 , v f i:

1. ⇢ reaches q i and the loop l i is visited exactly a times for some a 2 N. 2. ⇢ loops l i infinitely many times and never reaches q i . Due to the implication, q i ) i+1 we can easily ignore the runs of type 2 above. Hence, we will consider only the runs where l i is taken only finitely many times. Since the effect of the simple loop l i is to increment the counter x i each time, and v f [i] = 0, there are finite runs from hq i 1 , v f i to hq i , v f 0 i for each of the valuations

f 0 = f [z i 7 ! a] with a 2 N. So, hq i 1 , v f i |= AG(q i ) i+1 ). Now, assume that hq i 1 , v f i |= AG(q i ) i+1 )
. By definition of |=, there exists a set of runs X, in T(S ) such that for all ⇢ 2 X we have ⇢[0] = hq i 1 , v f i and for all positions j < |⇢|, if ⇢[j] |= q i then ⇢[j] |= i+1 . Thus, for every run ⇢ 2 X, ⇢[j] = hq i , v 0 i for some v 0 2 N n . Since q i is reached only after taking the simple loop l i a finite number of times in any run, let us assume that for each value of a 0, there exists a run ⇢ a 2 X where the loop l i is taken a times. Since the effect of the simple loop l i is to increment the counter x i each time, we have v 0

[i] = a and v f and v 0 differ only on the ith component in any run ⇢ a in X.

So, v 0 = v f 0 where f 0 = f [z i 7 ! a]. Since hq i , v f 0 i |= i+1 for all such valuations v f 0 , by the induction hypothesis f [z i 7 ! a] |= Q i+1 z i+1 • • • Q n z n 0 (z 1 , z 2 , . . . , z n ) for all a 2 N. By definition of |= in PA, we conclude that f |= 8 z i • • • Q n z n 0 (z 1 , . . . , z n ). u t
Thus, there is a logarithmic-space reduction from SAT(PA) into MC (CTL ⇤ , FlatCS). This gives one side of the complexity equivalence we are currently establishing.

5 From MC(CTL ⇤ , FlatCS) to SAT(PA)

In this section, we present a logarithmic-space reduction from MC(CTL ⇤ , FlatCS) to the satisfiability problem for PA. In [START_REF] Demri | Model-checking CTL ⇤ over flat Presburger counter systems[END_REF], a reduction is already presented to get decidability of MC(CTL ⇤ , FlatCS). Unfortunately, it requires exponential space and it is quite difficult to parse. Following a similar idea, we propose here a simpler reduction that has the great advantage to be optimal complexity-wise. The idea of this reduction is based on the two following points:

1. encoding the runs in flat counter systems by tuples of natural numbers thanks to a symbolic representation for potential infinite sets of runs, see path schemas in [START_REF] Demri | Taming Past LTL and Flat Counter Systems[END_REF]; 2. internalising CTL ⇤ semantics into (PA) by using the encoding of runs.

Below, we consider a fixed non-blocking flat counter system S = hQ, C n , , `i. Without any loss of generality we can assume that Q = {1, . . . , ↵} for some ↵ 1 and = { 1 , . . . , } for some 1. Since Q ✓ N, configurations of S can be seen as vectors in N n+1 where the first component represents the control state and range within the interval [1, ↵] and the rest represents counter values of the configuration.

Minimal path schemas

In [START_REF] Demri | Taming Past LTL and Flat Counter Systems[END_REF], following an idea from [START_REF] Leroux | On flatness for 2-dimensional vector addition systems with states[END_REF], minimal path schemas are introduced as a means to symbolically represent all runs in flat counter systems. Path schemas can be defined as finite sequences made of transitions or simple loops (conditions apply). Formal definition is recalled below. A simple loop l of S is a nonempty finite sequence of transitions 1 , . . . , m such that source( 1 ) = target( m ), source( j ) = target( j+1 ) for all j 2 [1, m 1], and, for all j, k 2 [1, m], if j 6 = k then j 6 = k (no repetition). The length of l, written length(l), is the number m and we denote by source(l) = target(l) the control state source( 1). The number of simple loops is necessarily finite and we assume that the set of loops of S is L = {l 1 , l 2 , . . . , l }. Since S is flat, we have  ↵. Note that since there is no restriction on path schema, there can be redundant loops and edges. To restrict this, we define a minimal path schema with no redundancy, as follows. A minimal path schema P is a non-empty sequence u 1 , . . . , u N such that each u i 2 [ L and the following conditions are satisfied.

1. u N is a loop, 2. i 6 = j implies u i 6 = u j , 3. for all i 2 [1, N 1], we have target(u i ) = source(u i+1 ).

The second condition guarantees that there are no redundancies whereas the third condition ensures that P respects the control graph of S. The size of P , denoted by size(P ), is equal to N . For all j 2 [1, N], we write P [j] for u j . Here is an obvious result.

Lemma 4. The size of a minimal path schema is bounded by +  + ↵.

In order to obtain concrete paths from a path schema P , we augment P with a vector specifying how many times each internal loop is visited. By definition, a loop in P is internal if it is not the last one. An iterated path schema is a pair hP, mi where P is a minimal path schema and m 2 N size(P ) such that m[1] = size(P ) and for all i 2 [1, size(P

) 1], m[i + 1] > 0 and if P [i] 2 , then m[i + 1] = 1.
From hP, mi, we define the !-word trans(P, m)

def = P [1] m[2] . . . P [j] m[j+1]
. . . P [size(P ) 1] m[size(P )] P [size(P )] ! Note that, by definition of minimal path schema, P [size(P )] is a loop. Lemma 5 below states that iterated path schemas encode all the runs in flat counter systems thanks to flatness. Lemma 5. [START_REF] Demri | Taming Past LTL and Flat Counter Systems[END_REF] Given an infinite run ⇢ in a (non-blocking) flat counter system S, there exists an iterated path schema hP, mi such that trans(⇢) = trans(P, m). Encoding iterated path schemas. Thanks to Lemma 4, we can encode path schemas by vectors in N K with K = 1 + + . Intuitively, we encode a path schema P by two vectors v p and v t in N K where the first element of each vector is equal to size(P ) (by convention) and for all i 2 [2, size(P ) + 1], we have v t [i] = 1 if P [i] is a loop and v t [i] = 0 otherwise. So, v t encodes the type of each element (transition vs. loop) in the sequence defining P . Similarly, v p [i] represents the number of the associated transition or loop; for instance, v p [i] = 2 and v t [i] = 1 encodes that P [i] is the second loop, say l 2 . Then, we encode the vector m by a vector v it 2 N K . Let us formalize this. First, we define the function

⌧ : (({0} ⇥ [1, ]) [ ({1} ⇥ [1, ])) ! [ L such that ⌧ (0, i) def = i and ⌧ (1, i) def = l i .
Now, we provide a set of conditions C on the vectors v t , v p , v it 2 N K so that we can build from these three vectors an iterated path schema.

C.1 v p [1] = v t [1] = v it [1] with v p [1] 2 [1, K 1]; for all i 2 [v it [1] + 2, K], v p [i] = v t [i] = v it [i] = 0, C.2 v t [i] 2 {0, 1} for all i 2 [2, K], C.3 if v t [i] = 0 then v p [i] 2 [1, ], for all i 2 [2, v p [1] + 1], C.4 if v t [i] = 1 then v p [i] 2 [1, ], for all i 2 [2, v p [1] + 1], C.5 v t [v p [1] + 1] = 1, C.6 there are no i, j 2 [2, v p [1] + 1] such that i 6 = j, v t [i] = v t [j] and v p [i] = v p [j], C.7 target(⌧ (v t [i], v p [i])) = source(⌧ (v t [i + 1], v p [i + 1])) for all i 2 [2, v p [1]], C.8 for all i 2 [2, v p [1]], v it [i] > 0 and if v t [i] = 0 then v it [i] = 1.
The first four conditions ensure that the vectorial representation is coherent. The three next conditions guarantee that the encoding respects the structure of a minimal path schema, i.e. that the last element is a loop (C.5), that there are no two identical transitions or loops in the schema (C.6) and that the succession of elements effectively represents a path in the counter system (C.7). The last condition ensures that v it matches the definition of the vector in an iterated path schema. It follows that given vectors v p , v t and v it in N K that satisfy all the conditions (C.i), we can build a minimal path schema P vt,vp equal to

⌧ (v t [2], v p [2]) • • • ⌧ (v t [v p [1] + 1], v p [v p [1] + 1]).
From the vector v it , we can define the vector m vit 2 N vit [1] such that for all

i 2 [1, v it [1]], m vit [i] def = v it [i + 1].
Let us explain the encoding of iterated path schemas with vectors on a simple example. We consider the following flat counter system. There are 10 transitions and 3 simple loops. The enumeration of edges and loops is done as shown above. Let hP, mi be such that

P = 3 • 6 • l 2 • 8 • l 3
and m = (5, 1, 1, 146, 1). So, we get the resulting !-word as

3 • 6 •(l 2 ) 146 • 8 •(l 3 ) ! .
From the previous encoding, the !-word is encoded by the following vectors v p = (5, 3, 6, 2, 8, 3, 0, 0, 0, 0, 0, 0, 0, 0), v t = (5, 0, 0, 1, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0) and v it = (5, 1, 1, 146, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0).

Lemma 6 below, whose proof can be found in Appendix B, states that there exists a Presburger formula Schema(Z t , Z p , Z it ) over the sets of variables Z p = {z 1 p , . . . , z K p }, Z t = {z 1 t , . . . , z K t } and Z it = {z 1 it , . . . , z K it } which expresses the conjunctions of the conditions (C.i) i2 [START_REF] Barrett | CVC4[END_REF][START_REF] De Moura | Z3: An Efficient SMT Solver[END_REF] . For three vectors v

t , v p , v it 2 N K , we say that v t , v p , v it |= Schema(Z t , Z p , Z it ) iff for some valuation function f , we have f |= Schema(Z t , Z p , Z it ), where f (z i t ) = v t [i], f(z i p ) = v p [i] and f (z i it ) = v it [i] for all i 2 [1, K]. Lemma 6.
1. Let P be in ( [ L) + of length N  + and m 2 N N . Then, hP, mi is an iterated path schema iff there are v t , v p and v it in N K respecting C such that P = P vt,vp and m = m vit . 2. One can build a quantifier-free PA formula Schema(Z t , Z p , Z it ) of polynomial size in the size of the counter system S such that for all v t , v p , v it 2 N K , we have v t , v p , v it |= Schema(Z t , Z p , Z it ) iff v t , v p and v it satisfy C.

Encoding runs using vectors

So, we are able to characterise the minimal path schemas of a flat counter system S using a Presburger arithmetic formula. Let us show how to describe the runs respecting any path schema P of S. Lemma 5 states that any infinite run can be encoded by an iterated path schema. However, not every iterated path schema corresponds to a run in due form because counter values should be non-negative and transitions can be fired only if the guards are really satisfied. We will see now how to check that an iterated path schema indeed represents a run starting from a given configuration c. First, we need to introduce a notion of pseudorun in which only the updates are precise and where the configurations can take their values in the integers (instead of in the set of natural numbers). Given c 2 Q ⇥ Z n , a pseudo-run ⇢ starting from c in S is an infinite sequence

⇢ := c 0 1 • • • m 1 c m m • • • where c 0 = c, c i = hq i , v i i 2
Q⇥Z n for all i 0 and for all transitions 2 we have hq, vi hq 0 , v 0 i def , q = source( ), q 0 = target( )

and v 0 = v + update( ). So, a pseudo-run ⇢ = hq 0 , v 0 i 1 • • • m 1 hq m , v m i • • • is a run iff for all i 2 N, v i |= guard ( i ) and v i 2 N n .
Note also that for all configurations hq, vi, if hP, mi is an iterated path schema such that source(P [1]) = q then there exists a pseudo-run ⇢ starting from c such that trans(⇢) = trans(P, m) (where the function trans(.) is defined for infinite pseudo-run the same way it is done for infinite runs, see Section 3.2). As with runs, we denote ⇢[i] the (i + 1)-th configuration of a pseudo-run ⇢. From these observations, we conclude that an iterated path schema hP, mi augmented with c 0 = hq 0 , v 0 i satisfying source(P [1]) = q 0 , defines a unique pseudo-run that is denoted by ⇢(P, m, c 0 ). Given a configuration c 0 = hq 0 , v 0 i, we say that ⇢(P, m, c 0 ) is well-defined if source(P [1]) = q 0 . We introduce a sequence of positions in a pseudo-run as p 0 , . . . , p size(P ) 1 . By convention p 0 = 0 and for every i 2 [1, size(P ) 1] let p i def = P i j=1 m[j + 1] ⇤ length(P [j]). The value p i is called the position of the ith witness configuration ⇢(P, m, c 0 )[p i ]. Intuitively, we reach the ith witness configuration after going through the iterations of first i elements of the path schema P in ⇢(P, m, c 0 ). We say that ⇢(P, m, c 0 ) is positive if for all the witness configurations hq, vi, we have v 2 N n . Note that since for all path schemas P , we have size(P )  + , the number of witness configurations for such a pseudo-run is bounded by + too. Now, we show how to build a PA formula whose set of solutions corresponds to the witness configurations of a pseudo-run associated to an iterated path schema equipped with an initial configuration. Before defining the formula, we explain some further notions. In the sequel, we use the following sets of variables [START_REF] Barrett | CVC4[END_REF] to represent pseudoconfigurations (we recall that Q ✓ N, hence (pseudo)-configurations are seen as tuples in N n+1 ) and, the variables d 0 , . . . , d + 1 and y to represent positions in (pseudo)-runs. Furthermore, given sets of variables X, W representing (pseudo)-configurations, a variable x and a vector u 2 N n , we use the shortcut X = W + x.u for the following formula:

-X 0 = {x 1 0 , . . . , x n+1 0 } and X = {x 1 , . . . , x n+1 } to represent configurations, -W i = {w 1 i , . . . , w n+1 i } for every i 2 [0, +
n+1 î=2 x i = w i + x.u[i 1].
Now, we introduce the formula Witness which allows us to check whether a given set of configurations and natural numbers represent the witness configurations and their respective positions in a pseudo-run associated to an iterated path schema. The main idea of the formula is to verify at each step whether the control states of the witness configurations match with the states of the taken transitions or loops in the path schema and then to compute the effect of the corresponding element of the iterated path schema taking into account the number of iterations.

Witness(W0, . . . ,

W + 1 , d0, . . . , d + 1 , Zt, Zp, Zit, X0) def = (d0 = 0 ^X0 = W0 ^1 W s=0 max( , ) W j=1 z 2 p = j ^z2 t = s ^x1 0 = source(⌧ (s, j)))^ + 1 V i=1 (i < z 1 t ) 1 W s=0 max( , ) W j=1 (z i+1 p = j ^zi+1 t = s ^di = di 1 + z i+1 it ⇤ length(⌧ (s, j))ŵ 1 i = target(⌧ (s, j)) ^Wi = Wi 1 + z i+1 it ⇤ update(⌧ (s, i)))
We are aware that the above formula is not particularly pretty at first glance, but it only states simple properties. We need to go through this process of writing down such formulae for the sake of checking the correctness of our enterprise and for paving the way to a future implementation of the translation that requires sufficiently details. More formulae will follow for the same reasons but we shall try to explain as much as possible every bit, while trying to avoid the boredom of repetitive arguments.

Lemma 7 below characterizes the property respected by formula Witness by construction (a detailed proof can be found in Appendix C).

Lemma 7. Let w 0 , . . . , w + 1 , c 0 2 N n+1 , p 0 , . . . , p + 1 2 N and v t , v p , v it in N K such that v t , v p , v it |= Schema(Z t , Z p , Z it ). We have w 0 , . . . , w + 1 , p 0 , . . . , p + 1 , v t , v p , v it , c 0 |= Witness iff ⇢(P vt,vp , m vit , c
0 ) is well-defined and positive and for all j 2 [0, + 1], if j < size(P vt,vp ), then w j represents the jth witness configuration of ⇢(P vt,vp , m vit , c 0 ) and p j its position.

Hence, the formula Witness gives us a way to characterise the witness positions and the configuration at those positions of a pseudo-run represented by an iterated path schema. Identifying witness positions and the configurations is essential to check whether a pseudo-run is a run or not. In fact, using Witness, one can build in logarithmic space a formula Conf (Z t , Z p , Z it , X 0 , y, X) such that if v t , v p , v it , c 0 , i, c |= Conf then the vector c is the ith configuration hq i , v i i of a pseudo-run ⇢(P vt,vp , m vit , c 0 ) with the property that v i |= guard (trans(hP vt,vp , m vit i)[i + 1]) and v i 2 N n (here i is the number of transitions to reach that configuration). This offers us the ability to construct then a formula Run(Z t , Z p , Z it , X 0 ) to check whether a pseudo-run is a run, since, as observed earlier, it is enough to check whether at each step the ith configuration satisfies the guard of the (i + 1)th transition.

First, we explain how to build the formula Conf (Z t , Z p , Z it , X 0 , y, X). The formula uses Schema(Z t , Z p , Z it ) in order to check whether the variables correspond to an iterated path schema. Then, thanks to existential quantifications, the formula guesses the positions and the values of the witness configurations using the formula Witness(W 0 , . . . ,

W + 1 , d 0 , . . . , d + 1 , Z t , Z p , Z it , X 0
) and Lemma 7. We recall that the variables in X represent the configuration at the position y in the corresponding pseudo-run. To do so, in the formula Conf , a case analysis is performed depending where y lays with respect to the positions of the witness configurations. Here are the cases.

1. The value stored in y corresponds to a witness position from which the next step in the path schema is an edge . It is then easy to find the value of the associated configuration which corresponds to a witness configuration and also thanks to the encoding of the path schema provided by the variables in Z t ,Z p and in Z it to check that the guards of is satisfied.

2. The value stored in y corresponds to a position between two consecutive witness positions and lays inside a loop. One has to check how many times the corresponding loop has been taken and thanks to this information, the formula can compute the value of the reached configuration and find the corresponding guard to be checked for satisfiability.

3. The value stored in y lies in the last loop of the path schema, then the treatment is the same as for the second case.

Before defining the formula Conf , we introduce some useful notations. Periodicity constraints can be defined in Presburger arithmetic and we write t ⌘ c t 0 (c 2 N and t, t 0 are terms) to denote the formula 9x (t = c.x + t 0 ) _ (t 0 = c.x + t). Then for a simple loop l of the form 1 , . . . , m , for all i 2 [1, m], we will use the notation l[i] to represent the transitions i . Furthermore, we write update(l k ) to denote the tuple update(

1 ) + • • • + update( m )
. Now, we are ready to define the formula Conf :

Conf (Z t , Z p , Z it , X 0 , y, X) def = Schema(Z t , Z p , Z it ) 9W 0 . . . 9W + 1 9d 0 . . . 9d + 1 Witness(W 0 , . . . , W + 1 , d 0 , . . . , d + 1 , Z t , Z p , Z it , X 0 )^ + 1 W j=0 [(j  z 1 p ^y = d j ^zj+2 t = 0 ^X = W j ^ W k=1 (z j+2 p = k ^guard ( k )(x 2 , • • • , x n+1 )))_ (j  z 1 p ^dj  y < d j+1 ^zj+2 t = 1^ W k=1 (z j+2 p = k ^ConfLoop l k (W j , y d j , X)))_ (j = z 1 p ^dj  y ^ W k=1 (z j+2 p = k ^ConfLoop l k (W j , y d j , X)))]
where for all loop l k with k 2 [1, ], the formula ConfLoop l k (W, y, X) is used to find the configurations corresponding to X obtained when taking the loop l k from the configuration W and taking y transitions in the loop.

ConfLoop l k (W, y, X) def = length(l k ) 1 W j=0 [y ⌘ length(l k ) j ^x1 = source(l k [j + 1])ĝ uard (l k [j + 1])(x 2 , • • • , x n+1 ) 9h.(h ⇤ length(l k )  y < h ⇤ length(l k ) + 1 X = W + h ⇤ update(l k ) + r=j P r=1 update(l k [r]))].
In the definition of the formula Conf , the fourth and fifth lines correspond to the first case we have stated above, the fifth and sixth lines to the second case and the last line to the last and third cases.

Furthermore, as we have already stated, a pseudo-run

⇢ = hq 0 , v 0 i 1 • • • m 1 hq m , v m i • • • is a run iff for all i 2 N, v i |= guard ( i ) and v i 2 N n .
Consequently to construct the formula Run(Z t , Z p , Z it , X 0 ), we only have to check that the values contained in the set of variables Z t , Z p ,Z it and X 0 correspond to a pseudo-run for which at each step the vector value of the configuration is in N n and it satisfies the guard of the next transition. According to the properties satisfied by the formula Conf , we build the formula Run as follows:

Run(Z t , Z p , Z it , X 0 ) def = 8 y 9 X Conf (Z t , Z p , Z it , X 0 , y, X)
. By construction we can then deduce the following Lemma (whose proof can be found in Appendix D) concerning the properties of the formulae Conf and Run Lemma 8. For all c 0 , c 2 N n+1 , for all i 2 N and for all v t , v p , v it 2 N K , we have:

1. v t , v p , v it , c 0 , i, c |= Conf iff v t , v p , v it |= Schema, ⇢(P vt,vp , m vit , c 0 ) is well- defined, c = ⇢(P vt,vp , m vit , c 0 )[i] and c[2], • • • , c[n + 1] |= guard (trans(P vt,vp , m vit )[i + 1]). 2. v t , v p , v it , c 0 |= Run iff v t , v p , v it |= Schema and ⇢(P vt,vp , m vit , c 0
) is welldefined and is a run.

All the formulae involved in the construction use generalised conjunctions/disjunctions of length linear in the sum of the following values: number of states ↵, number of transitions , number of simple loops , number of counters n. So, it is easy to check that we only need logarithmic space to build the formulae.

Consequently, we can construct a Presburger formula in logarithmic space that characterises the vectors that can be used to represent runs in a flat counter system. This allows us to quantify over all the runs of a flat counter system starting from a distinguished configuration. The ability to do this lends a useful hand in encoding the model-checking problem in PA without exponential blowup.

Encoding CTL ⇤ formulae using (PA)

We have seen that path schemas and runs can be encoded by tuples of natural numbers whose constraints can be expressed in Presburger arithmetic. Our next aim is to encode a given CTL ⇤ formula using a formula in PA. The forthcoming encoding internalises CTL ⇤ semantics and a similar idea has been already used in [START_REF] Demri | Model-checking CTL ⇤ over flat Presburger counter systems[END_REF] but with much less concise formulae. For each CTL ⇤ formula , we build a PA formula Check (Z t , Z p , Z it , X 0 , y) where the variables Z t , Z p , Z it and X 0 encode a run as in the formula Run and, y encodes a position such that the formula checks whether the CTL ⇤ formula is satisfied at the current position. The formula Check is defined recursively (Boolean clauses are omitted) as follows:

Check p def = 9 X (Conf (Z t , Z p , Z it , X 0 , y, X) ^W {j | p 2 `(j)} x 1 = j) Check (x1,...,xn) def = 9 X (Conf (Z t , Z p , Z it , X 0 , y, X) ^ (x 2 , . . . , x n+1 )) Check X def = 9 y 0 (y 0 = y + 1 ^Check (Z t , Z p , Z it , X 0 , y 0 )) Check U 0 def = 9 y 00 (y  y 00 ^Check 0 (Z t , Z p , Z it , X 0 , y 00 )8 y 0 (y  y 0 < y 00 ) Check (Z t , Z p , Z it , X 0 , y 0 ))) Check X 1 def = y > 0 ^9 y 0 (y = y 0 + 1 ^Check (Z t , Z p , Z it , X 0 , y 0 )) Check S 0 def = 9 y 00 (y 00  y ^Check 0 (Z t , Z p , Z it , X 0 , y 00 )8 y 0 (y 00 < y 0  y ) Check (Z t , Z p , Z it , X 0 , y 0 ))) Check E def = 9 Z 0 t 9 Z 0 p 9 Z 0 it (Run(Z 0 t , Z 0 p , Z 0 it , X 0 ) ^8y 0 (0  y 0  y ) 8X 0 (Conf (Z t , Z p , Z it , X 0 , y 0 , X 0 ) ) Conf (Z 0 t , Z 0 p , Z 0 it , X 0 , y 0 , X 0 )))Ĉ heck (Z 0 t , Z 0 p , Z 0 it , X 0 , y)
). Now, we can state the main property concerning the formulae Check based on Lemmas 5, 6 and 8.

Input: A flat counter system S with n counters, a control state q, a CTL ⇤ formula .

Output: A Presburger formula (z 1 , . . . , z n ) such that J K = {v 2 N n | S, hq, vi |= }.
It is actually quite easy to construct the Presburger formula for the global modelchecking problem with CTL ⇤ as the model-checking problem itself is encoded by a Presburger formula. In the previous section, we saw that given a flat counter system S, a configuration c 0 and a formula in CTL ⇤ , we construct the following Presburger arithmetic formula as described below.

= 9Z t 9Z p 9Z it 9X 0 (X 0 = c 0 ^Run(Z t , Z p , Z it , X 0 ) ^Check (Z t , Z p , Z it , X 0 , 0)).
For the global model-checking problem if we suppose that the control states of the counter systems are encoded as natural numbers, given a flat counter system S, a control state q and a formula in CTL ⇤ , we construct the Presburger formula (z 1 , . . . , z n ) as

(z 1 , . . . , z n ) = 9Z t 9Z p 9Z it 9X 0 (x 1 0 = q ^n V i=1 x i 0 = z i ^Run(Z t , Z p , Z it , X 0 ) ^Check (Z t , Z p , Z it , X 0 , 0)).
As a consequence of Lemma 10 and other previous results, we get the following characterisation.

Lemma 12. For all v 2 N n , we have v |= (z 1 , . . . , z n ) iff there exists a run ⇢ in S starting from hq, vi such that ⇢, 0 |= . As a conclusion, our method provides also a means to synthetize Presburger formulae for solving the global model-checking problem.

MC(CTL ⇤

, FlatCS) subproblems and PA fragments

The construction and translation presented in the previous sections entail that the model-checking problem for CTL ⇤ over flat counter systems and the satisfiability problem for PA are inter-reducible . Though this provides a nice complexity characterization of the model-checking problem for full CTL ⇤ logic over flat counter systems, our translation allows us to provide some tighter bounds for CTL ⇤ fragments. In [START_REF] Haase | Subclasses of Presburger arithmetic and the weak EXP hierarchy[END_REF], the author characterizes the precise complexity of PA fragments and shows equivalences with classes from the weak-Exp hierarchy. In this section, we establish a comparison between PA fragments as those considered in [START_REF] Haase | Subclasses of Presburger arithmetic and the weak EXP hierarchy[END_REF] and the model-checking problem for fragments of CTL ⇤ over flat counter systems.

For subclasses of PA, we borrow the notations used in [START_REF] Haase | Subclasses of Presburger arithmetic and the weak EXP hierarchy[END_REF] and denote by PA(i), the ⌃ i -fragment of Presburger arithmetic restricted to i quantifier alternations beginning with an existential quantifier. Let ⌃ Exp i be the ith level of the By construction Conf belongs to the existential fragment of PA and hence Run belongs to PA(3) (by definition PA(i) starts with an existential quantifier).

Let us now recall how the Check (Z t , Z p , Z it , X 0 , 0) is inductively defined :

Check p def = 9 X (Conf (Z t , Z p , Z it , X 0 , y, X) ^W {j | p 2 `(j)} x 1 = j) Check (x1,...,xn) def = 9 X (Conf (Z t , Z p , Z it , X 0 , y, X) ^ (x 2 , . . . , x n+1 )) Check X def = 9 y 0 (y 0 = y + 1 ^Check (Z t , Z p , Z it , X 0 , y 0 )) Check U 0 def = 9 y 00 (y  y 00 ^Check 0 (Z t , Z p , Z it , X 0 , y 00 )8 y 0 (y  y 0 < y 00 ) Check (Z t , Z p , Z it , X 0 , y 0 ))) Check X 1 def = y > 0 ^9 y 0 (y = y 0 + 1 ^Check (Z t , Z p , Z it , X 0 , y 0 )) Check S 0 def = 9 y 00 (y 00  y ^Check 0 (Z t , Z p , Z it , X 0 , y 00 )8 y 0 (y 00 < y 0  y ) Check (Z t , Z p , Z it , X 0 , y 0 ))) Check E def = 9 Z 0 t 9 Z 0 p 9 Z 0 it (Run(Z 0 t , Z 0 p , Z 0 it , X 0 ) ^8y 0 (0  y 0  y ) 8X 0 (Conf (Z t , Z p , Z it , X 0 , y 0 , X 0 ) ) Conf (Z 0 t , Z 0 p , Z 0 it , X 0 , y 0 , X 0 )))Ĉ heck (Z 0 t , Z 0 p , Z 0 it , X 0 , y)).
In order to complete our analysis we need as well to provide the translation for the negation of atomic propositions and for the newly introduced operators A, R and R 1 :

Check ¬p def = 9 X (Conf (Z t , Z p , Z it , X 0 , y, X) ^W {j | p 6 2 `(j)} x 1 = j) Check ¬ (x1,...,xn) def = 9 X (Conf (Z t , Z p , Z it , X 0 , y, X) ^¬ (x 2 , . . . , x n+1 )) Check R 0 def = (9 y 00 (y  y 00 ^Check (Z t , Z p , Z it , X 0 , y 00 )8 y 0 (y  y 0  y 00 ) Check 0 (Z t , Z p , Z it , X 0 , y 0 ))))_ 8 y 0 (y  y 0 ) Check 0 (Z t , Z p , Z it , X 0 , y 0 )) Check R 1 0 def = (9 y 00 (y 00  y ^Check 0 (Z t , Z p , Z it , X 0 , y 00 )8 y 0 (y 00  y  y ) Check 0 (Z t , Z p , Z it , X 0 , y 0 ))))_ 8 y 0 (y 0  y ) Check 0 (Z t , Z p , Z it , X 0 , y 0 )) Check A def = 8 Z 0 t 8 Z 0 p 8 Z 0 it (Run(Z 0 t , Z 0 p , Z 0 it , X 0 ) ^8y 0 (0  y 0  y ) 8X 0 (Conf (Z t , Z p , Z it , X 0 , y 0 , X 0 ) ) Conf (Z 0 t , Z 0 p , Z 0 it , X 0 , y 0 , X 0 ))) ) Check (Z 0 t , Z 0 p , Z 0 it , X 0 , y)).
The proof for the correctness of the extended translation is similar to the one for Lemma 9. Now, we can perform a case analysis to determine the number of quantifier alternations in the formula Check expressed in terms of qtd ( ) and we obtain the following upper bound. For the induction step, we assume that Check and Check 0 belong respectively to PA(2qtd ( ) + 3) and PA(2qtd ( 0 ) + 3). Then Check X and Check X 1 belongs as well to PA(2qtd ( ) + 3). Furthermore, we have Check U 0 belongs to PA(max(2qtd ( ) + 3, (2qtd ( 0) + 3) + 2) and since qtd ( U 0 ) = 1 + max(qtd ( ), qtd ( 0)), we have that Check U 0 belongs to PA(2qtd ( U 0 ) + 3). The exact same reasoning holds for S, R and R 1 . Finally we have that Check E belongs to PA(max(3, (2qtd ( ) + 3) + 2) which is in PA(2(qtd (E ) + 3)). Similarly, Check A belongs to PA(max(3, 2(qtd ( ) + 3) + 2) which is in PA(2qtd (A ) + 3).

If, for k 2 N, we denote by CTL ⇤ LIA (k) the set of formulas of CTL ⇤ LIA such that qtd ( )  k, the previous lemma together with the previous observations and Theorem 13 allow us to state the result below. Theorem 15. MC(CTL ⇤ LIA (k), FlatCS)) is reducible to the satisfiability problem for P A(2k + 3) and is in ⌃ Exp 2k+2 Note that by analyzing the formula built in the proof of Theorem 3 which shows that the satisfiability of PA can be reduced to the model-checking of CTL ⇤ LIA over flat counter systems, we are able to obtain a lower bound. In fact we observe that the CTL ⇤ LIA formula built from a formula of PA(k) for k 2 N is such that qtd ( ) = 2.k + 2. The following result can then be deduced.

Theorem 16. For k 4, MC(CTL ⇤ LIA (k), FlatCS)is ⌃ Exp bk/2c 2 -hard.

Conclusion

We have been able to characterise the computational complexity for MC(CTL ⇤ , FlatCS) by showing that the problem is equivalent to SAT(PA) (modulo logarithmic-space reductions). The lower bound is obtained by considering a quite strong restriction (no arithmetical constraints in formulae, the only temporal operator is EF, guards on transitions are simple linear constraints). By contrast, the restriction of the problem to LTL formulae is known to be NP-complete [START_REF] Demri | Taming Past LTL and Flat Counter Systems[END_REF][START_REF] Dhar | Algorithms for model-checking flat counter systems[END_REF] when guards are in the linear fragment and the restriction of the problem to formulae in CTL EF is also equivalent to SAT(PA). We have proposed a new way for encoding runs in flat counter systems using Presburger arithmetic formulae, but without any exponential blow up, which allows us to get a precise complexity characterisation. It remains open to determine which extensions of CTL ⇤ on flat counter systems preserve decidability, if not an efficient translation into PA (typically for logics between CTL ⇤ and the modal mu-calculus).

otherwise, we have:

maximize(⇢) def = ⇢ ↵+1 ! hq ? , v ↵ i ? ! hq ? , v ↵ i ? ! • • • where • |⇢| = ↵, • ⇢[↵] = hq ↵ , v ↵ i,
• ? = hq ? , >, 0, q ? i and • ↵+1 = hq ↵ , ¬(_ source( )=q↵ guard ( )), 0, q ? i. Since hq ↵ , v ↵ i is a deadlock configuration, we have v ↵ 2 guard ( ) for every such that source( ) = q ↵ . We conclude that v ↵ |= ¬(_ source( )=q↵ guard ( )) and hence the only possible configuration after hq, vi is hq ? , vi. So, for all such finite runs this is the only way to get an infinite maximal run extending ⇢.

In other words, if we assume that ⇢ ? = hq ? , v ↵ i ?

! hq ? , v ↵ i ? ! • • • . We can define the function maximize(•) for any run ⇢ of S as following

maximize(⇢) def = ( ⇢ if ⇢ is infinite ⇢ ↵+1 ! ⇢ ? |⇢| = ↵, for some ↵ 2 N
So, clearly, for any run ⇢ in S there exists an unique run ⇢ 0 in S 0 such that ⇢ 0 = maximize(⇢). Hence, there is a bijection between the set of maximal runs in S and the set of maximal runs in S 0 that start by a state in Q. Every maximal run in S 0 is infinite. Below, we also use the inverse map maximize 1 (•) that returns a maximal run in S.

By structural induction, we show that for all ⇢ in S and i  |⇢|, we have ⇢, i |= iff maximize(⇢), i |= t( ). As a consequence, for all configurations c in S and for all formulae in CTL ⇤ [resp. in CTL EF ], we have S, c |= iff S 0 , c |= t( ). By construction, S 0 is non-blocking and, S 0 and 0 can be built in logarithmic space in the size of S and .

-Base case: Let ⇢ be a run in S and i  |⇢|. v p [i] = v t [i] = 0 for all i 2 [size(P ) + 2, K]. Note that the above construction follows exactly the reverse steps of the construction of P vt,vp . In other words, given an iterated path schema hP, mi, the above construction gives us the vectors v t and v p such that P = P vt,vp . Moreover, we can construct v it from m 2 N size(P ) as :

v it [i] = m[i] for all i 2 [1, size(P )], v it [i] = 0 for all i 2 [size(P ) + 1, K]. Clearly by the construction of v t , v p and the fact that size(P ) > 0 we can conclude that C.1 is satisfied. Similarly, by construction, and the fact that P is a sequence of edges and loops, C.2 to C.5 are satisfied. Due to the fact that P is a minimal path schema, C.6 and C.7 are also satisfied. Since, hP, mi is an iterated path schema, C.8 is satisfied. 2. To construct the formula Schema(Z t , Z p , Z it ), we start by defining a formula i for each condition C.i. (z i t  1)

3 def = K î=2 i  z 1 p + 1 ) (z i t = 0 ) z i p  ^zi p 1) 4 def = K î=2 i  z 1 p + 1 ) (z i t = 1 ) z i p  ^zi p 1
)

5 def = K î=2 i = z 1 p + 1 ) z i t = 1 6 def = K V i=2 (i  z 1 p + 1 ) ( K V
j=2,j6 =i j  z 1 p + 1 ) (z i p 6 = z j p _ z i t 6 = z j t ))) We construct the formula Schema(Z t , Z p , Z it ) as

( 1 ^• • • ^ 8 )
. For all i 2 [1, 8], v t , v p , v it satisfies C.i iff v t , v p , v it |= i . For example, consider C.6, which expresses the minimality constraint for the minimal path schemas, stating that for any two distinct positions either the values are different or they are of different types. More formally, for all i, j 2 [1, v p [1] + 1],

i 6 = j ) (v p [i] 6 = v t [j] _ v t [i] 6 = v t [j]
). Note that 6 has a nested conjunction allowing to compare every possible pair of positions hi, ji. Moreover, for every possible pair, we check exactly the condition stated in C. [START_REF] Bruyère | Durations, parametric model-checking in timed automata with Presburger arithmetic[END_REF] ensures that q 0 = source(P vt,vp [START_REF] Barrett | CVC4[END_REF]); in fact it states that c 0 [START_REF] Barrett | CVC4[END_REF] = source(⌧ (v t [START_REF] Berman | The complexity of logical theories[END_REF], v p [START_REF] Berman | The complexity of logical theories[END_REF])). Consequently, we can define the pseudo-run ⇢(P vt,vp , m vit , c 0 ). -Let N = size(P vt,vp ). We recall that N = v t [START_REF] Barrett | CVC4[END_REF]. We will now show that w j is the jth witness configuration of ⇢(P vt,vp , m vit , c 0 ) and p j is its position for all j < N.

• First thanks to the part of formula saying d 0 = 0 ^X0 = W 0 , we know that p 0 = 0 and that w 0 = c 0 , whence w 0 is effectively the witness configuration at position 0. Now thanks to the part of the formula saying that

0 Fig. 1 .

 01 Fig. 1. Flat counter system S

Lemma 14 .

 14 Check belongs to PA(2.qtd ( ) + 3). Proof. The proof is by structural induction. For the base case, it is clear that Check p , Check ¬p , Check (x1,...,xn) and Check ¬ (x1,...,xn) are in PA(3).

i  z 1 p + 1 )

 11 ,b,a 0 ,b 0 )|target(⌧ (a,b))=source(⌧ (a 0 .b 0 (z i it > 0 ^(z i t = 0 ) z i it = 1))

=

  s ^di = d i 1 + z i+1 it ⇤

  x 2 , . . .} be a countably infinite set of counters and we write C n to denote the subset {x 1 , . . . , x n }. Let AT = {p Definition 1. A counter system is a tuple hQ, C n , , `i where

	1 , p	2 , . . .} be a countably infinite set
	of propositional variables.

  finite set of transitions, labelled by guards and updates where G n is a set of linear Presburger formulae with free( ) ✓ {x 1 , . . . ,x n }. -`: Q ! 2 AT is a labeling function,

  , • • • , x n ), we conclude that ⇢, i |= p [resp. ⇢, i |= (x 1 , • • • , x n )] iff ⇢ 0 , i |= t(p) [resp. ⇢ 0 , i |= t( (x 1 , • • • , x n ))].-Induction step: We assume that for all formulae of size at most k 1, for all runs ⇢ and for all i  |⇢|, we have ⇢, i |= iff maximize(⇢), i |= t( ). Now, we prove this property for formulae of size k. We consider hence a run ⇢ of S and i  |⇢|. • Case X : First, suppose that ⇢, i |= X . By definition of |=, i < |⇢| and ⇢, i+1 |= . By the induction hypothesis, maximize(⇢), i+1 |= t( ). Since i < |⇢|, maximize(⇢)[i+1] = ⇢[i+1] and since maximize(⇢)[i+1] |= ¬p ? , we get that maximize(⇢), i |= X(¬p ? ^t( )). Assume maximize(⇢), i |= X(¬p ? ^t( )). So, maximize(⇢), i + 1 |= t( ) and maximize(⇢), i + 1 |= ¬p ? . By construction, for all the positions j in maximize(⇢) such that the construction of P vt,vp . By definition of P vt,vp and C.1 through C.4 ensure that P vt,vp is a sequence of loops and edges from S. C.5 ensures that P vt,vp ends with a loop. C.6 and C.7 ensure that P vt,vp is a minimal path schema where none of the edges or loops are repeated. By construction v p[START_REF] Barrett | CVC4[END_REF] is exactly equal to size(P vt,vp ). Thus, m vit is defined to be in N size(Pv t ,vp ) . C.8 on v it allows us to conclude that hP vt,vp , m vit i is an iterated path schema.For the other side, given an iterated path schema hP, mi, we construct v t and v p as:v t [1] = v p [1] = size(P ). v p [i] = j and v t [i] = 0 if P [i 1]= j for some j, for all i 2 [2, size(P )+1].v p [i] = j and v t [i] = 1 if P [i 1] = l j for some j, for all i 2 [2, size(P )+1].

Since we have i  |⇢| we deduce that ⇢[i] = maximize(⇢)[i]. As t(•) is the identity for atomic formulae p and (x 1

  . Clearly, v t , v p , v it satisfies C.6 iff v t , v p , v it |= 6 .Finally, the formula Schema states that all formulae i hold for the vectorsv t , v p , v it . Hence it is easy to see that, v t , v p , v it |= Schema(Z t , Z p , Z it ) iff v t , v p , v it satisfies C. N and v t , v p , v it in N K such that v t , v p , v it |= Schema(Z t , Z p , Z it ). By Lemma 6, we know that v t , v p and v it respect the conditions in C and consequently that hP vt,vp , m vit i is an iterated path schema.First we suppose that w 0 , . . . , w

			u t
	C Proof of Lemma 7
	-The subformula
	1 _	max( , ) _
	s=0	j=1	z 2 p = j ^z2

Proof. Let w 0 , . . . , w + 1 , c 0 2 N n+1 and p 0 , . . . p

+ 1 2 + 1 , p 0 , . . . , p + 1 , v t , v p , v it , c 0 |= Witness. t = s ^x1 0 = source(⌧ (s, j))

Acknowledgments: We would like to thank the anonymous referees for their remarks and suggestions that help us to improve the quality of the paper.

? Work partially supported by the EU Seventh Framework Programme under grant agreement No. PIOF-GA-2011-301166 (DATAVERIF).

Lemma 9. Let c 0 2 N n+1 , i 2 N and v t , v p , v it 2 N K be such that we have v t , v p , v it , c 0 |= Run. Then, the conditions below are equivalent: -⇢(P vt,vp , m vit , c 0 ), i |= , v t , v p , v it , c 0 , i |= Check (Z t , Z p , Z it , X 0 , y). Proof. The proof is by structural induction. Let c 0 2 N n+1 and i 2 N and v t , v p , v it 2 N K be such that v t , v p , v it , c 0 |= Run. Thus, from Lemma 8, we can conclude that ⇢(P vt,vp , m vit , c 0 ) is a run in S. We will show that for any i, ⇢(P vt,vp , m vit , c 0 ), i |= iff v t , v p , v it , c 0 , i |= Check (Z t , Z p , Z it , X 0 , y). -Base case 1:

= p. By definition, we have Check p (Z t , Z p , Z it , X 0 , y) = 9X Conf (Z t , Z p , Z it , X 0 , y, X) ^_{j|p2`(j)} x 1 = j. Assume that for some i, ⇢(P vt,vp , m vit , c 0 ), i |= p. Then p 2 `(c i [START_REF] Barrett | CVC4[END_REF]) with c i = ⇢(P vt,vp , m vit , c 0 )[i]. From Lemma 8, we know that v t , v p , v it , c , i, c i |= Conf and c i [START_REF] Barrett | CVC4[END_REF] 2 {j | p 2 `(j)}. Thus, v t , v p , v it , c 0 , i |= Check p . Now, assume v t , v p , v it , c 0 , i |= Check p for some i. Thus, there exists a configuration c i such that v t , v p , v it , c 0 , i, c i |= Conf and c i [START_REF] Barrett | CVC4[END_REF] 2 {j | p 2 `(j)}. In that case by Lemma 8, c i = ⇢(P vt,vp , m vit , c 0 )[i] and p 2 `(c i [START_REF] Barrett | CVC4[END_REF]). Hence, ⇢(P vt,vp , m vit , c 0 ), i |= p. -Base case 2: = (x 1 , . . . , x n ). By definition, we have Check (x1,...,xn) (Z t , Z p , Z it , X 0 , y) = 9X Conf (Z t , Z p , Z it , X 0 , y, X) ^ (x 2 , . . . , x n+1

). Assume that for some i, ⇢(P vt,vp , m vit , c 0 ), i |= (x 1 , . . . ,

Recall that c i [START_REF] Barrett | CVC4[END_REF] is a value encoding a control state. From Lemma 8 we know that v t , v p , v it , c 0 , i, c i |= Conf and (c i [START_REF] Berman | The complexity of logical theories[END_REF]

0 , y). We will prove the same for the case when

. By the induction hypothesis, ⇢(P vt,vp , m vit , c 0 ), i 1 |= . By definition of |=, we get ⇢(P vt,vp , m vit , c 0 ), i |= X 1 . • U 0 : First we assume that ⇢(P vt,vp , m vit , c 0 ), i |= U 0 for some i. By definition of |=, there exists j i such that ⇢(P vt,vp , m vit , c 0 ), j |= 0 and for all i  l < j, ⇢(P vt,vp , m vit , c 0 ), l |= . By the induction hypothesis, we get v t , v p , v it , c 0 , j |= Check 0 (Z t , Z p , Z it , X 0 , y) and for all i  l < j,

for some i. By definition of Check U 0 , we have that there exists i  j such that

. By the induction hypothesis, we obtain ⇢(P vt,vp , m vit , c 0 ), j |= 0 and for all i  l < j, ⇢(P vt,vp , m vit , c 0 ), l |= . By definition of |=, we get that, ⇢(P vt,vp , m vit , c 0 ), i |= U 0 . • S 0 : First we assume that ⇢(P vt,vp , m vit , c 0 ), i |= S 0 for some i. By satisfaction relation, there exists j  i such that ⇢(P vt,vp , m vit , c 0 ), j |= 0 and for all j < l  i, ⇢(P vt,vp , m vit , c 0 ), l |= . By induction hypothesis, we get

for some i. By definition of Check S 0 , we have that there exists

By the induction hypothesis, we obtain ⇢(P vt,vp , m vit , c 0 ), j |= 0 and for all j < l  i, ⇢(P vt,vp , m vit , c 0 ), l |= . By definition of |=, we get that, ⇢(P vt,vp , m vit , c 0 ), i |= S 0 . • E : Let us assume that ⇢(P vt,vp , m vit , c 0 ), i |= E for some i. By definition of the satisfaction relation, there exists a run ⇢ 0 such that ⇢ 0 i = ⇢(P vt,vp , m vit , c 0 ) i and ⇢ 0 , i |= . By Lemma 5, we know that there exists an iterated path schema hP, mi such that trans(⇢ 0 ) = trans(P, m). From Lemma 6, we get that there exist vectors

Hence, using the result of Lemma 8 concerning the formula Conf , we conclude that

Thus, by definition of Check E and using Lemma 8, we obtain that there ex-

Furthermore, the formula Check E allows us as well to state that for all j 2 [0, i], we have

21

By the induction hypothesis, In view of the previous results, we are in a position to construct a Presburger formula pertaining to our original aim of encoding the model-checking problem MC(CTL ⇤ , FlatCS). Given a flat counter system S, a configuration c 0 and a formula in CTL ⇤ , we construct the following Presburger arithmetic formula as

Then, Lemmas 8 and 9 allow us to get the following property. This allows us to conclude the main result of this section.

Theorem 11. There is a logarithmic-space reduction from MC( CTL ⇤ , FlatCS) to SAT(PA).

Equipped with Theorem 11 and Theorem 3 and the fact that CTL EF is a subclass of CTL ⇤ , we can conclude that the model-checking problem of flat counter systems with CTL ⇤ is equivalent to SAT(PA), modulo logarithmic-space reductions.

Global Model-Checking

The method we have used so far is robust enough to draw more conclusions. As shown below, it is also possible to construct a formula in PA that captures the set of (initial) counter values from which there is an infinite run satisfying a given CTL ⇤ formula. The global model-checking problem over flat counter systems with CTL ⇤ (written GMC(CTL ⇤ , FlatCS)) is the following: weak-Exp hierarchy which is analogous to the polynomial-time hierarchy but built with the help of ExpTime (see e.g. [START_REF] Hemachandra | The strong exponential hierarchy collapses[END_REF]). The following result, established in [START_REF] Haase | Subclasses of Presburger arithmetic and the weak EXP hierarchy[END_REF], is stated below.

Theorem 13. For any fixed i > 0, the PA(i + 1) fragment of Presburger arithmetic is ⌃ Exp i -complete.

In order to analyze the complexity of our model-checking problem and to use this latter result on PA, we need to focus on a restriction of CTL ⇤ where the atomic propositions (x 1 , . . . , x n ) that describe the counter values belong to the linear fragment of PA (i.e., is quantifier-free). We denote by CTL ⇤ LIA this fragment of CTL ⇤ . Now, we aim at analyzing the PA formulae generated by the translation of a specific instance of the model-checking problem as presented in Section 5. Since we are interested in the quantifier alternation of the produced formulae, negation may increase the number of quantifier alternations. In order to simplify the analysis, without any of loss of generality, we can assume that the negations are pushed until the atomic propositions and we consequently need to extend the syntax of CTL ⇤ with the disjunction operator, the universal path quantifiers, A def = ¬E¬ , the release operator R 0 def = ¬(¬ U¬ ) and the past release operator R 1 0 def = ¬(¬ S¬ ). Thanks to these dual operators, we can restrict ourselves to CTL ⇤ LIA formulae in negation normal form (negation can only occur in front of atomic propositions).

We consider now a flat counter system S, a configuration c and a formula in negation normal form belonging to CTL ⇤ LIA . We will compute an integer K such that the translation of the instance of MC(CTL ⇤ , FlatCS), provided in the previous section, yields a PA formula in the fragment PA(K). In fact, we will see that K depends on the joint quantifier and temporal depth of the CTL ⇤ LIA formula , denoted by qtd ( ) and defined inductively as follows :

Now, let us analyse the formula produced in Section 5. We recall that it has the following shape:

The fragment in which this formula belongs to depends on the shape of the formulas Run(Z t , Z p , Z it , X 0 ) and Check (Z t , Z p , Z it , X 0 , 0). We begin our analysis with the easier formula Run(Z t , Z p , Z it , X 0 ). By definition,

A Proof of Lemma 2

Proof. First, we show that every maximal run in S 0 is infinite. For every maximal run ⇢ in S, we write maximize(⇢) to denote the maximal run in S 0 defined as follows:

such that ⇢, j |= 0 and for all k 2 [i, j 1], we have ⇢, k |= . Since maximize(⇢)[j] = ⇢[j], we get that maximize(⇢), j |= ¬p ? . Using furthermore the induction hypothesis, we deduce maximize(⇢), i |= t( )U(¬p ? ^t( 0)). Now suppose that maximize(⇢), i |= t( U 0

). By definition of t(•), there is i  j 0 such that maximize(⇢), j 0 |= t( 0) and maximize(⇢), j 0 |= ¬p ? and for all k 0 2 [i, j 0 1], we have maximize(⇢), k 0 |= t( ). Since maximize(⇢), j 0 |= ¬p ? , we know that j 0  |⇢| and

. By the induction hypothesis, ⇢, j 0 |= 0 and for all

By definition of |=, 0 < i and ⇢, i 1 |= . Since i  |⇢|, by the induction hypothesis, maximize(⇢), i 1 |= t( ) and consequently we get that maximize(⇢), i |= X 1 t( ). Assume maximize(⇢), i |= X 1 t( ). By a similar reasoning, we can prove that ⇢, i |= X 1 .

• Case S 0 : First suppose that ⇢, i |= S 0 . There is 0  j  i such that ⇢, j |= 0 and for all k 2 [j + 1, i], we have ⇢, k |= . Using the induction hypothesis, since i  |⇢| and hence j  |⇢|, we obtain directly that maximize(⇢), i |= t( ) S t( 0). Similarly if we assume maximize(⇢), i |= t( S 0

), using the fact that i  |⇢| and the induction hypothesis we deduce that ⇢, i |= S 0 .

• Case E : First, suppose that ⇢, i |= E . By definition of |=, there is a maximal run ⇢ 0 such that ⇢ 0 i = ⇢ i and ⇢ 0 , i |= . By the induction hypothesis, maximize(⇢ 0

), i |= t( ). Since by construction we have maximize(⇢ 0

) i = ⇢ 0 i = ⇢ i = maximize(⇢) i , we deduce maximize(⇢), i |= E t( ). Assume that maximize(⇢), i |= E t( ). So, there is a run ⇢ 0 such that ⇢ 0 i = maximize(⇢) i and ⇢ 0 , i |= t( ). By the induction hypothesis, maximize 1 (⇢ 0 ), i |= . By construction we have maximize 1

The proof is the same as the one for the case U 0 . u t

B Proof of Lemma 6

Proof.

1. By definition, an iterated path schema is a pair hP, mi such that P is a minimal path schema and m 2 N size(P ) . Now assume that we have vectors v t , v p , v it 2 N K such that v t , v p , v it satisfy all the conditions C. We perform length(⌧ (s, j)))), we have that for all 1 < j < N,

and this allows us to deduce that p j is the position of the jth witness configuration (using the definition of witness configuration).

• Similarly, the part of the formula saying

and consequently w j corresponds effectively to the jth witness configuration. Furthermore since for all j < N, w j belongs to N n+1 , then we deduce that the pseudo-run ⇢(P vt,vp , m vit , c 0 ) is positive. We now assume that ⇢(P vt,vp , m vit , c 0 ) is well-defined and positive and for all j 2 [0, + 1], if j < size(P vt,vp ), then w j is the jth witness configuration of ⇢(P vt,vp , m vit , c 0 ) and p j its position. Let N = size(P vt,vp ). We recall that N = v t [START_REF] Barrett | CVC4[END_REF] by definition of P vt,vp . By definition of the witness configurations, the following assertions hold:

p 0 = 0 and w 0 = c 0 and c 0 [START_REF] Barrett | CVC4[END_REF] = source(P vt,vp [START_REF] Barrett | CVC4[END_REF]), whence w 0 [START_REF] Barrett | CVC4[END_REF] = source(P vt,vp [START_REF] Barrett | CVC4[END_REF]); -For all 1 < j < N,

-For all 1 < j < N,

-For all 1 < j < N, for all i 2 [2, n + 1],

These assertions allow us to conclude that w 0 , . . . , w

D Proof of Lemma 8

Proof. Proof of (1.). We assume that there exist c 0 , c 2 N n+1 and i 2 N and v t , v p , v it 2 N K such that v t , v p , v it , c 0 , i, c |= Conf . Thanks to the conjunct Schema(Z t , Z p , Z it ), we have that v t , v p , v it |= Schema and using Lemma 6 we know that hP vt,vp , m vit i is an iterated path schema. Furthermore we know that there exist w 0 , . . . , w ) is well-defined and positive and for all j 2 [0, + 1], if j < size(P vt,vp ), then w j represents the jth witness configuration of ⇢(P vt,vp , m vit , c 0 ) and p j its position. Now, we proceed on a case analysis on the value of i:

-First assume that there exists j  v p [START_REF] Barrett | CVC4[END_REF] = size(P vt,vp ) such that i = p j and v t [j + 2] = 0. We know from the formula that c = w j and hence since w j = ⇢(P vt,vp , m vit , c 0 )[p j ] (by definition of witness configuration), we deduce that c = ⇢(P vt,vp , m vit , c 0 )[i]. Furthermore we have that v t [j + 2] = 0, hence P vt,vp [j + 1] 2 and we also have that c

Using the definition of iterated path schema we have that -Now assume that there exists j  v p [START_REF] Barrett | CVC4[END_REF] = size(P vt,vp ) such that p j  j < p j+1 and v t [j + 2] = 1 (hence P vt,vp [j + 1] is a loop). Then, we have w j , i

Then let u 2 [0, length(l k ) 1] and v 2 N such that i p j = v ⇤length(l k )+u. Note that since p j  i < p j+1 , we know that the pseudo-run ⇢(P vt,vp , m vit , c 0 ) at position i lies exactly in the loop l k and that it has taken this loop v times exactly and the u first transitions. Moreover, the next transition will still be one of the loops (otherwise we would have i p j+1 ). The formula enforces that c

-The case where there exist j = v p [START_REF] Barrett | CVC4[END_REF] = size(P vt,vp ) and p j  j is similar to the previous one, the only difference being that this time the position of the run is in the last loop of the minimal path schema P vt,vp .

The All the formulae involved in the construction use generalised conjunctions/disjunctions of length linear in the sum of the following values: number of states ↵, number of transitions , number of simple loops , number of counters n. So, it is easy to check that we only need logarithmic-space to build the formulae.