Stéphane Demri

Alain Finkel

Valentin Goranko

-Govert Van Drimmelen

Ò×¹ Ñö ¸ Ò Ð Ð×úº

Òº

Ññº Øùº

Model-Checking CTL* over Flat Presburger Counter Systems ⋆

Keywords: model-checking, infinite-state transition systems, Presburger arithmetic, CTL*, counter systems

This paper studies model-checking of fragments and extensions of CTL* on infinitestate counter systems, where the states are vectors of integers and the transitions are determined by means of relations definable within Presburger arithmetic. In general, reachability properties of counter systems are undecidable, but we have identified a natural class of admissible counter systems (ACS) for which we show that the quantification over paths in CTL* can be simulated by quantification over tuples of natural numbers, eventually allowing translation of the whole Presburger-CTL* into Presburger arithmetic, thereby enabling effective model checking. We provide evidence that our results are close to optimal with respect to the class of counter systems described above.

Introduction

Background. Model-checking of infinite-state systems (for a survey see [START_REF] Burkart | Verification of infinite structures[END_REF]) is a rapidly growing area of formal verification. It has been successfully applied to real-time and hybrid systems, concurrent systems, Petri nets, asynchronous communication devices (unbounded FIFO channels), infinite and unbounded data structures (counters, queues, lists), control systems, parameterized systems (networks of arbitrary number of processes), etc. The single most important property of practical interest in infinite-state transition systems is state reachability which is often undecidable in structures with otherwise decidable first-order theories, such as automatic structures [START_REF] Khoussainov | Automatic presentations of structures[END_REF]. Therefore, intensive research has been devoted to identifying classes of finitely presentable infinite structures with decidable reachability and related properties.

Transition systems determined by relations definable in Presburger arithmetic provide a large natural class of infinite-state transition systems [START_REF] Bardin | Flat acceleration in symbolic model checking[END_REF], suitable for modeling in various applications such as the TTP Protocol (embedded systems) [START_REF] Bardin | FASTer Acceleration of Counter Automata in Practice[END_REF], broadcast protocols [START_REF] Esparza | On the verification of broadcast protocols[END_REF], and programs with pointer variables (Bardin et al., 2006a;[START_REF] Bouajjani | Programs with lists are counter automata[END_REF][START_REF] Finkel | Towards Model-Checking Programs with Lists[END_REF]. Important cases of such transition systems with computable reachability have been established in [START_REF] Ibarra | Reversal-bounded multicounter machines and their decision problems[END_REF][START_REF] Fribourg | Proving safety properties of infinite state systems by compilation into Presburger arithmetic[END_REF][START_REF] Comon | Multiple counters automata, safety analysis and Presburger analysis[END_REF][START_REF] Finkel | Decidability of reachability problems for classes of two counters automata[END_REF][START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF]. The method of acceleration for computing reachability sets has been developed in [START_REF] Boigelot | Symbolic methods for exploring infinite state spaces[END_REF][START_REF] Leroux | Algorithmique de la vérification des systèmes à compteurs. Approximation et accélération. Implémentation de l'outil FAST[END_REF] and is implemented in the verification tool FAST [START_REF] Leroux | Algorithmique de la vérification des systèmes à compteurs. Approximation et accélération. Implémentation de l'outil FAST[END_REF][START_REF] Bardin | FASTer Acceleration of Counter Automata in Practice[END_REF]Bardin et al., 2006b); see also the verification tools LASH [START_REF] Boigelot | Symbolic methods for exploring infinite state spaces[END_REF] and TReX [START_REF] Annichini | TReX: a tool for reachablity analysis of complex systems[END_REF].

Motivation. For practical model-checking, an infinite-state system must be provided with an effective finitary presentation, and in particular, must admit a symbolic representation of sets of states and transitions. Such representations can be based on:

-automata (finite, pushdown, on infinite words or trees, etc.), as in pushdown graphs [START_REF] Muller | The theory of ends, pushdown automata , and second-order logic[END_REF], prefix-recognizable graphs [START_REF] Caucal | On infinite transition graphs having a decidable monadic theory[END_REF], and automatic structures [START_REF] Blumensath | Finite Presentations of Infinite Structures: Automata and Interpretations[END_REF], -interpretations into sufficiently rich infinite structures with respective decidable theories, e.g., again, automatic structures [START_REF] Blumensath | Finite Presentations of Infinite Structures: Automata and Interpretations[END_REF] and treeinterpretable structures [START_REF] Blumensath | Axiomatising Tree-Interpretable Structures[END_REF], [START_REF] Caucal | On infinite transition graphs having a decidable monadic theory[END_REF].

-algebraic equations or operations [START_REF] Courcelle | Graph rewriting: An algebraic and logic approach[END_REF], etc.

Presburger arithmetic (PrA) is a logical formalism that is intrumental in many applications and it is a particularly appropriate platform for symbolic representation of a wide variety of infinite state systems, such as counter systems (see [START_REF] Bardin | FAST: Fast Acceleration of Symbolic Transition Systems[END_REF]) where vectors of integers are subjected to linear transformations according to a finite control graph. These strongly extend counter automata [START_REF] Minsky | Computation, Finite and Infinite Machines[END_REF] and even very simple examples of counter systems can have notoriously difficult and unpredictable behaviour, a witness being the Collatz problem (a.k.a. the Syracuse problem), see e.g. [START_REF] Lagarias | The 3x+1 problem and its generalizations[END_REF]. An important and natural class of counter systems, in which various practical cases of infinite state systems can be modelled (e.g. broadcast protocols [START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF]), are those with a flat control graph, where no control location occurs in more than one simple cycle (see [START_REF] Boigelot | Symbolic methods for exploring infinite state spaces[END_REF][START_REF] Comon | Multiple counters automata, safety analysis and Presburger analysis[END_REF][START_REF] Comon | Flatness is not a weakness[END_REF][START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF][START_REF] Bardin | FAST: Fast Acceleration of Symbolic Transition Systems[END_REF][START_REF] Leroux | Algorithmique de la vérification des systèmes à compteurs. Approximation et accélération. Implémentation de l'outil FAST[END_REF]Leroux et al., 2005;[START_REF] Bardin | Flat acceleration in symbolic model checking[END_REF][START_REF] Bozga | Flat parametric counter automata[END_REF]). Essential results on verifying safety and reachability properties on flat counter systems have been obtained in [START_REF] Comon | Multiple counters automata, safety analysis and Presburger analysis[END_REF][START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF]. However, until recently such properties had not been considered in the framework of any formal specification language, and thus a natural question arises to identify expressive logical languages in which formal specification and verification of properties of counter systems can be conducted.

On the other hand, most of the studies on CTL ⋆ -model checking so far have been restricted to (unfoldings of) finite transition systems, and few decidability results for CTL ⋆ -model checking on essentially infinite-state systems are known [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]. This is particularly surprising since CTL ⋆ is one of the most known applied non-classical logics among the temporal logics. Actually, most of these results are immediate consequences of stronger results about decidable modal mu-calculus, or even the whole monadic second-order logic (MSO) in such systems, see e.g. [START_REF] Walukiewicz | Pushdown processes: games and model-checking[END_REF]. Furthermore, these decidability results typically refer to the propositional CTL ⋆ , while model checking of first-order extensions of even much simpler temporal logics is typically undecidable. That is why, it is important to search for larger classes of effectively generated infinite state systems (without necessarily decidable MSO), but in which natural first-order extensions of CTL ⋆ have decidable model-checking problems.

Our contribution. In this paper, which is an improved and extended version of [START_REF] Demri | Towards a model-checker for counter systems[END_REF], We jointly address both problems described above, and we obtain a nearly optimal solution of them. Our main contributions are the following:

1) We introduce an extension of CTL ⋆ [START_REF] Emerson | Sometimes' and 'Not Never' revisited: on branching versus Linear time temporal logic[END_REF] over Presburger arithmetic, i.e., where atomic propositions range over Presburger-definable sets of configuration states. We interpret that extension over Presburger counter systems (abbreviated by PCS), thus proposing a very powerful specification language for such systems. Presburger counter systems are infinite-state transition systems with states being vectors of integers (counter values) and transition relations definable in Presburger arithmetic. This class of models naturally includes the counter automata (or Minsky machines). Presburger counter systems are interesting in two complementary ways: they naturally arise in the reachability analysis of counter systems, and on the other hand they can be viewed as models for symbolic representation of infinite state transition systems.

2) We identify a class of Presburger counter systems for which the local model checking problem for the Presburger-CTL ⋆ is decidable. These are Presburger counter systems defined over flat control graphs with arcs labelled by transition functions defined by Presburger formulae, for which counting iteration over every cycle in the control graph is Presburger definable. A well-studied case when the latter condition is satisfied is when the composition monoids generated by the transition functions over every cycle are finite (see [START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF].

3) We show that the decidability results described above persist in some strong extensions of the Presburger-CTL ⋆ , i.e. with a class of temporal operators defined by means of constrained queue-content decision diagrams (aka CQDD) (see [START_REF] Bouajjani | Symbolic Reachability Analysis of FIFO-channel systems with nonregular sets of configurations[END_REF]) in a way analogous to Wolper's Extended temporal logic [START_REF] Wolper | Temporal logic can be more expressive[END_REF].

4) We provide evidence that our results are close to optimal with respect to the class of Presburger counter systems described above, by showing that small relaxations of each of the conditions lead to undecidability. For example, by dropping either the counting iteration property or the flatness condition, undecidability is obtained.

Related work.

Analyzing the reachability problem for counter systems is paramount for the verification of infinite-state systems, see e.g. [START_REF] Ibarra | Counter Machines: Decidable Properties and Applications to Verification Problems[END_REF] (reversal-bounded systems), [START_REF] Comon | Multiple counters automata, safety analysis and Presburger analysis[END_REF] (flat systems), [START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF] (flat Presburger transition systems), [START_REF] Dang | Presburger Liveness Verification of Discrete Timed Automata[END_REF] (discrete timed automata), see also the decidability of reachability for classes of 2-counter systems [START_REF] Finkel | Decidability of reachability problems for classes of two counters automata[END_REF]. It is worth noting that, even though decidability can be obtained only at the cost of making drastic restrictions on counter systems, there is a natural class of counter systems that are sufficiently expressive for modelling different case studies and for which one may verify the safety properties by means of the effective computation of the reachability relation [START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF][START_REF] Bardin | FAST: Fast Acceleration of Symbolic Transition Systems[END_REF][START_REF] Leroux | Algorithmique de la vérification des systèmes à compteurs. Approximation et accélération. Implémentation de l'outil FAST[END_REF][START_REF] Leroux | Flat counter systems are everywhere![END_REF][START_REF] Bardin | Flat acceleration in symbolic model checking[END_REF]. For instance, the flattable systems [START_REF] Leroux | Flat counter systems are everywhere![END_REF] admit a flat finite unfolding of the control graph with the same reachability set. On the logical side, temporal logics with Presburger constraints have been defined and investigated in [START_REF] Čerans | Deciding Properties of Integral Relational Automata[END_REF][START_REF] Bouajjani | On the verification problem of nonregular properties for nonregular processes[END_REF][START_REF] Bultan | Symbolic model checking of infinite state systems using Presburger arithmetic[END_REF][START_REF] Comon | Flatness is not a weakness[END_REF][START_REF] Schuele | Global vs. Local Model Checking: A Comparison of Verification Techniques for Infinite State Systems[END_REF][START_REF] Demri | LTL over integer periodicity constraints[END_REF][START_REF] Bruyère | Durations, Parametric Model-Checking in Timed Automata with Presburger Arithmetic[END_REF], some of which have quite expressive decidable fragments. However, undecidability of the reachability problem can be proved for quite restricted counter systems, see e.g. [START_REF] Cortier | About the Decision of Reachability for Register Machines[END_REF][START_REF] Potapov | From Post Systems to the Reachability Problems for Matrix Semigroups and Multicounter Automata[END_REF] while at the same time very few classes of counter systems are decidable for CTL ⋆ (see e.g. [START_REF] Finkel | A Direct Symbolic Approach to Model Checking Pushdown Systems (Extended Abstract)[END_REF] for one-counter systems). A logical formalism closer to the one developed in this paper is presented in [START_REF] Bultan | Symbolic model checking of infinite state systems using Presburger arithmetic[END_REF] where an undecidable temporal logic with CTL-like operators and atomic formulae in Presburger arithmetic is introduced and the models are counter systems. The class of models is not restricted (hence decidability does not hold) but model-checking is performed by a symbolic analysis and an approximation algorithm. Interestingly, if we restrict ourselves to the same temporal operators, it is open whether our main decidability result can be established by giving up functionality. Model checking discrete timed automata with parametric timed CTL is also shown decidable by translation into Presburger arithmetic in [START_REF] Bruyère | Durations, Parametric Model-Checking in Timed Automata with Presburger Arithmetic[END_REF].

Structure and content of the paper.

In Section 2 we present preliminary definitions about graphs and Presburger arithmetic. In Section 3 we introduce the class of Presburger counter systems (PCS) and we present the branching-time temporal logic FOPCTL ⋆ (PrA) [n] whose models are transition systems generated from PCS. Admissible PCS are introduced in Section 4 and we recall (un)decidability results of the reachability problem for some classes of PCS. In Section 5, we show our main decid-ability result about model-checking admissible counter systems with FOPCTL ⋆ (PrA) [n]. Section 6 provides undecidability results indicating that our result in Theorem 20 is close to optimal.

In Section 7 we show the decidability of model-checking problems over admissible PCS even when CQDD-based temporal operators are added to the temporal logic. Section 8 contains concluding remarks and states open problems related to our results.

Preliminaries

Graphs, paths, cycles. A labelled graph G = Σ, Q, E is a structure such that Q is a non-empty set, Σ is a non-empty finite alphabet and E ⊆ Q × Σ × Q. Graphs with a singleton alphabet are the standard graphs. As usual, q, a, q ′ ∈ E is also denoted by q a -→ q ′ . A path in G is a sequence q 0 a0 -→ q 1 . . .

an-1

--→ q n such that for i ∈ {0, . . . , n -1}, q i ai -→ q i+1 is a transition. A cycle in a labelled graph is a closed path (where the initial and final vertices coincide) with no repeating edges. A simple cycle is a cycle in which the only repeated vertex is the initial (and final) vertex. Observe that herein we use notions about cycles a bit different from those in graph theory. Given a path λ = q 0 a0 -→ q 1 . . .

an-1

--→ q n , where each q i ∈ Q, a i ∈ Σ, we define the length of λ to be |λ| = n. A graph is flat if every cycle in it is a simple cycle; equivalently, if every vertex occurs in at most one cycle.

Presburger arithmetic. Presburger arithmetic is the first-order theory PrA of the structure N, +, ≤ , well-known to be decidable [START_REF] Presburger | Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt[END_REF]. However, all results in this paper will still hold in a more general setting, based on the structure Z, +, ≤ which is easily seen to be first-order interpretable into N, +, ≤ , and therefore has a decidable first-order theory, too. For simplicity of notation, and with a benign abuse of terminology, hereafter we will refer to the first-order theory of Z, +, ≤ as Presburger arithmetic, too, and will use the same notation, PrA, for it. Given a Presburger formula A(x 1 , . . . , x n ) with free variables in x = x 1 , . . . , x n and a = a 1 , . . . , a n ∈ Z n , the truth of A(x 1 , . . . , x n ) with respect to the assignment of values a to x is denoted by a |= PrA A(x). Elements of Z n will be usually denoted by a, b, c, . . . and vectors of variables will be denoted by x, y, z, t, . . . , possibly decorated. A set X ⊆ Z n is said to be Presburger definable iff there is a Presburger formula A(x) with free variables x = x 1 , . . . , x n such that

X = {a ∈ Z n : a |= PrA A(x)}. For n > 0, A binary relation of dimension n is a relation R ⊆ Z n ×Z n . Respectively, R is Presburger definable iff there is a Presburger formula A(x, x ′ ) with free variables x = x 1 , . . . , x n and x ′ = x ′ 1 , . . . , x ′ n such that R = { a, a ′ ∈ Z n × Z n : a, a ′ |= A(x, x ′ )}. DEFINITION 1. -Let f be a partial function from Z n to Z n with domain dom(f ).
f is a translation if there exists b ∈ Z n such that for every a ∈ dom(f ) we have f (a) = a + b.

f is affine if there exist a matrix A ∈ Z n×n and b ∈ Z n such that for every a ∈ dom(f ) we have f (a) = Aa + b.

f is Presburger definable iff the graph of f is a Presburger definable relation.

Temporal Logics on Presburger Counter Systems

In this section, we introduce Presburger counter systems and a first-order extension of the temporal logic CTL * interpreted over such systems.

Presburger Counter Systems

The Presburger transition systems defined below are infinite state transition systems that can be finitely described by formulae in Presburger arithmetic.

When infinite state transition systems arise in the modeling of computational processes, there is often a natural factoring of each system state into a control component and a memory component, where the set of control states (locations) is typically finite. We refer to the combined state of the system, containing the location, the memory state and the position of the head, as a configuration of the system.

We will be interested in systems where the memory states are n-dimensional vectors of integers. In particular, we define systems where the transition relation on such vectors may be described by relations definable in Presburger arithmetic. DEFINITION 2. -A Presburger counter system (PCS) of dimension n is a labelled graph C = Σ, Q, δ, n , where -Σ is a finite set of Presburger formulae of the form A(x, x ′ ) where x and x ′ are tuples of n variables, -Q is a finite set of locations,

-δ ⊆ Q × Σ × Q is the transition relation.
By convention, prime variables in x ′ are intended to be interpreted as the next-state values of the unprimed variables in x.

Given two locations q and q ′ , we write A q,q ′ (x, x ′ ) to denote the disjunction of all the formulae B(x, x ′ ) such that q, B(x, x ′ ), q ′ ∈ δ. Thus, without any loss of generality, we can assume that there is a unique transition between every two control states. When there is no transition between a pair of states in the counter system, we introduce one labelled by falsum ⊥.

Thus, a PCS can be regarded as a labelled graph with alphabet made of specific Presburger formulae.

Figure 1 contains a simple Presburger counter system, augmented with an initial location and final location.

s 0 s 0 x ′ = x + 1 s 1 (∃y(x = 2y) ∧ 2x ′ = x) ∨ (¬∃y(x = 2y) ∧ x ′ = 3x + 1)

Figure 1. A simple Presburger system

Every PCS C = Σ, Q, δ of dimension n naturally induces a Presburger transition system (of dimension n): S C = S, → where S = Q × Z n is a set of configurations and q, a → q ′ , a ′ iff a, a ′ |= PrA A q,q ′ (x, x ′ ). As usual, → * denotes the reflexive and transitive closure of the relation →. Whenever, q, a → * q ′ , a ′ , we say that q ′ , a ′ is reachable from q, a . Without any loss of generality, we can assume that Q ⊆ N, hence S ⊆ Z n+1 . Depending on the context, the configurations of S C will be written as a = q, a 1 , . . . , a n (location encoded in the first element of a) or simply as q, a ∈ Q × Z n . A configuration path in C is an infinite path in S C .

We say that:

-C is functional, if for all q, q ′ , the formula A q,q ′ (x, x ′ ) defines a partial function.

-a functional PCS C is a counter automaton, if for all q, q ′ , A q,q ′ (x, x ′ ) defines a translation.

-a functional PCS C is affine if for all q, q ′ , A q,q ′ (x, x ′ ) defines an affine function.

PROPOSITION 3. -Each of the following properties of Presburger counter system: being functional, translation (i.e., a counter automaton), or affine, is definable in PrA, and therefore decidable.

PROOF 4. -Let A(x, x ′ ) be a Presburger formula over the free variables x = x 1 , . . . , x n and

x ′ = x ′ 1 , . . . , x ′ n . It is immediate to check that: -A(x, x ′ ) is functional iff |= PrA ∀x∀y∀y ′ ((A(x, y) ∧ A(x, y ′ )) ⇒ (y = y ′ )). -A(x, x ′ ) is a translation iff |= PrA n i=1 ∃z∀x∀y(A(x, y) ⇒ y i = x i + z).
To check whether A(x, x ′ ) is affine requires a bit more work. We want to check the existence of a matrix A ∈ Z n×n and a vector b ∈ Z n such that for every a ∈ dom(f ) we have f (a) = Aa + b, where, f (a) is the unique a ′ such that a, a ′ |= A(x, y).

The solution below is a bit more complex than the straightforward approach. Indeed, f (0) = b, which allows to define b. A similar reasoning would allow to compute each column of A by applying f to unit elements. However, this is not sufficient since f is partial and for instance f (0) may be undefined. A less straighforward approach is described below. Here is how this can be done.

-First, note that dom(f ) is Presburger definable by the formula ∃yA(x, y).

-Therefore, dom(f ) can be defined as a finite union of sets of the form

S i = {b i + λ 1 p i,1 + • • • + λ ni p i,ni : λ 1 , . . . , λ ni ∈ N}
where b i , p i,1 , . . . , p i,ni ∈ Z n (the basis and the periods). All these integers can be effectively computed [START_REF] Ginsburg | Semigroups, Presburger formulas and languages[END_REF].

Suppose the union has K sets. If f is affine, then f (a) = Âa + b for some  and b. Then for every 1 ≤ i ≤ K and 1 ≤ j ≤ n i , there is a unique integer vector c ij (= Âp j,nj ) such that for every z ∈ S i we have that

f (z + p j,nj ) -f (z) = c ij .
( * )

(Indeed: f (z + p j,nj ) -f (z) = Â(z + p j,nj ) + b -( Âz + b) = Âz + Âp j,nj + b -Âz -b = Âp j,nj = c ij .)
The existence of such unique vector can be easily expressed by a Presburger formula and then verified. If false, then f is not affine. If true, then  and b must, in particular, satisfy the equations:

Âp j,nj = f (b i + p j,nj ) -f (b i ) for every 1 ≤ i ≤ K and 1 ≤ j ≤ n i . ( * * ) Âb i + b = f (b i ) for every 1 ≤ i ≤ K. ( * * * )
This is a system of linear equations with integer coefficients for the n 2 + n integer entries of the matrix  and the vector b. To find an integer solution of that system, or to show that there is none, one can use e.g., the method from [START_REF] Papadimitriou | On the Complexity of Integer Programming[END_REF] or [START_REF] Borosh | Bounds on positive integral solutions of linear diophantine equations[END_REF]. If there is no integer solution, then such matrix and vector do not exist, so f is not affine. If there is an integer solution, take any one; it determines a matrix A and a vector b.

We can now check that f (a) = Aa + b for any a ∈ dom(f ). Indeed, using the equations (*), (**), and (***) we have that f

(a) = f (b i + Σ j λ j p i,j ) = f (b i ) + Σ j λ j Ap i,j = Ab i + b + Σ j λ j Ap i,j = A(b i + Σ j λ j p i,j ) + b = Aa + b.

The Temporal Logic FOPCTL ⋆ (PrA)

We now define a version FOPCTL ⋆ (PrA) of first-order and past-time extension of CTL ⋆ that is appropriate for reasoning about Presburger transition systems. The name 'FOPCTL ⋆ (PrA)' indicates that FOPCTL ⋆ (PrA) contains past-time operators, first-order quantification over integers and its underlying temporal logic is CTL ⋆ . The logic FOPCTL ⋆ (PrA) differs from standard CTL ⋆ with past mainly in the definition of atomic formulae. Whereas propositional variables are used in the propositional CTL ⋆ , we will use as atomic formulae in FOPCTL ⋆ (PrA) Presburger definable predicates, interpreted on the set of configurations.

We introduce a countable set of individual variables, say VAR = {y 0 , y 1 , y 2 . . .}, for quantification over counter values. Elements of VAR are distinct from the distinguished ones in {x 0 , x 1 , . . . , x n } that are free variables, only interpreted by the values of counters on configurations (the control location being encoded by the interpretation of x 0 ). In order to match the dimension of the models where such formulae will be interpreted, the Presburger definable predicates must have a matching number of free variables, thus giving a family of logics FOPCTL ⋆ (PrA)[n] parameterized by the dimension n ≥ 1. When the dimension n is clear from the context, we just refer to FOPCTL ⋆ (PrA).

Atomic formulae of FOPCTL ⋆ (PrA)[n] are Presburger formulae of the form θ(x, y) where x = x 0 , x 1 , . . . , x n and y is a vector of variables from VAR, regarded as parameters.

Formulae of FOPCTL ⋆ (PrA)[n] are defined as follows:

ϕ def = θ(x, y) | ¬ϕ | ϕ ∧ ϕ | Xϕ | ϕUϕ | X -1 ϕ | ϕSϕ | A ϕ | ∃ y ϕ,
where y ∈ VAR and y is a sequence of variables. We shall freely use standard abbreviations for the implication ⇒, the existential path quantifier E , the always operator G, and the sometimes operator F.

The LTL fragment of FOPCTL ⋆ (PrA), denoted by FOLTL(Pr), consists of formulae of the form either E φ ′ or A φ ′ where φ ′ has no path quantifiers and no pasttime operators. We define the strict EF fragment of FOPCTL ⋆ (PrA) as the set of FOPCTL ⋆ (PrA) formulae containing only the temporal operator E F and no nested occurrences of E F. Hence, this fragment has no past-time operators either.

We will give semantics of FOPCTL ⋆ (PrA) over Presburger transition systems. The satisfaction relation |= is parameterized by an environment ρ that is a map VAR → Z, in order to interpret the free variables from VAR that occur in formulae (the map ρ will be omitted when not immediately relevant). For a PCS C = Σ, Q, δ, n with Presburger transition system S C = S, → , the satisfaction relation |= ρ is defined at position i of configuration path π as follows, where π ≤i denotes the initial part of π up to and including position i; the environment ρ will be omitted wherever it is not essential.

π, i |= ρ θ(x, y) iff π(i), ρ |= θ(x, y) in PrA, where π(i) provides the interpretation of the variables x 0 , . . . , x n and ρ the interpretation for the variables in y, y←m] ϕ where ρ[y ← m] is the environment obtained from ρ by forcing y to be interpreted by m.

-π, i |= ¬ϕ iff π, i |= ϕ, -π, i |= ϕ ∧ ϕ ′ iff π, i |= ϕ and π, i |= ϕ ′ , -π, i |= Xϕ iff π, i + 1 |= ϕ, -π, i |= ϕUϕ ′ iff there is some j ≥ i such that π, j |= ϕ ′ and for each k, if i ≤ k < j then π, k |= ϕ, -π, i |= X -1 ϕ iff i > 0 and π, i -1 |= ϕ, -π, i |= ϕSϕ ′ iff there is some j ≤ i such that π, j |= ϕ ′ and for each k, if j < k ≤ i then π, k |= ϕ, -π, i |= A ϕ iff for every infinite configuration path π ′ such that π ′ ≤i = π ≤i we have π ′ , i |= ϕ, -π, i |= ρ ∃yϕ iff there is an integer m ∈ Z such that π, i |= ρ[
Past-time operators are known to simplify the expressions of specifications, see e.g. [START_REF] Laroussinie | Specification in CTL + Past for Verification in CTL[END_REF]. Here is an example of formula with a past-time operator:

A G (x 1 = x 2 ⇒ F -1 x 3 = x 4 )
The forthcoming translation will treat future-time and past-time temporal operators uniformly.

First-order quantification over counter values allows us to state many interesting properties in FOPCTL ⋆ (PrA):

Determinism: For all the configurations reachable from the initial configuration, there is at most one successor configuration:

A G 0≤i≤n ¬∃y(E X(x i = y) ∧ E X(x i = y)).

Boundedness:

The set of configurations reachable from the initial configuration is finite:

∃y, y ′ A G 1≤i≤n y ≤ x i ≤ y ′ .
Increasing chain: On some path the first counter strictly increases at every step:

E G∃y (y = x 1 ∧ X(x 1 > y)).

Model checking problems for FOPCTL

⋆ (PrA)[n]
In the definition of model-checking problems below, the formulae in FOPCTL ⋆ (PrA)[n] satisfy that none of the variables in VAR occur out of the scope of a quantification. Of course, variables related to counter values and locations (those in x) occur freely, In that way, we can sometimes omit the environments when interpreting formulae with all variables in VAR bounded. We will call such formulae semi-closed. In that way, we do not need to specify an environment in the statement below. 1) LOCAL MODEL CHECKING: Given a PCS C with Presburger transition system S C = S, → , a configuration q, a ∈ S, and a semi-closed formula ϕ from FOPCTL ⋆ (PrA)[n], determine whether C, q, a |= ϕ, meaning that for every path π such that π(0) = q, a , we have π, 0 |= ϕ. The dual version of this problem with the existential quantification over paths can be defined in a similar fashion. In the rest of the paper, we only deal with the universal version but a similar treatment is possible for the existential version, too.

2) GLOBAL MODEL CHECKING: Given a PCS C with Presburger transition system S C = S, → , and a FOPCTL ⋆ (PrA)[n] formula ϕ, compute (as a Presburger formula) the set of configurations S such that for every path π with π(0) ∈ S, we have π, 0 |= ϕ.

3) VALIDITY CHECKING WITH AN INITIAL CONDITION: Given a PCS C with Presburger transition system S C = S, → , a Presburger formula A 0 (x) and a semiclosed FOPCTL ⋆ (PrA)[n] formula ϕ, check whether for every configuration q, a satisfying A 0 (x), for every configuration q ′ , a ′ reachable from q, a , we have

C, q ′ , a ′ |= ϕ.
Variants of these problems can be defined by considering subclasses of PCS or other specification languages.

Admissible Presburger Counter Systems

As we will show later, local model checking of FOPCTL ⋆ (PrA) over the whole class of PCSs is highly undecidable (by reduction from the recurring problem for nondeterministic Minsky machines [START_REF] Minsky | Computation, Finite and Infinite Machines[END_REF][START_REF] Alur | A really temporal logic[END_REF]) even though reachability can be decided for many classes of counter systems, see e.g. [START_REF] Ibarra | Counter Machines: Decidable Properties and Applications to Verification Problems[END_REF][START_REF] Comon | Multiple counters automata, safety analysis and Presburger analysis[END_REF][START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF][START_REF] Dang | Presburger Liveness Verification of Discrete Timed Automata[END_REF]. In this section we introduce a subclass of admissible PCS in which model checking FOPCTL ⋆ (PrA) will be proved to be decidable in the next section.

DEFINITION 5. -Given a relation R ⊆ Z n × Z n we define the counting iteration of R as the relation R CI ⊆ Z n × N × Z n such that a, i, b ∈ R CI iff a, b ∈ R i . R has a Presburger counting iteration if its counting iteration is Presburger definable.
The cycle relation R λ of a cycle λ in a PCS is obtained by composing the transition relations on the cycle. According to Section 2, a cycle λ can be viewed as a sequence t 1 , . . . , t α of transitions of the form

t i = q i Ai -→ q ′ i such that for 1 ≤ i ≤ α -1, q i+1 = q ′
i and q 1 = q ′ α . We define the relation R ti as the set of pairs

{ q i , a , q ′ i , a ′ : a, a ′ |= PrA A i (x, x ′ )}. The relation R λ is then the composition R t1 • • • • • R tα . A
, x ′ , i (A(x, i, x ′ ) ⇒ i ≥ 0) ∧ (A(x, 0, x ′ ) ⇔ (x = x ′ ))∧ (A(x, i + 1, x ′ ) ⇔ (∃x ′′ A(x, i, x ′′ ) ∧ A ′ (x ′′ , x ′ )))
is valid, where A ′ (x, y) is the effect of a given cycle. This is an instance of a more general result from [START_REF] Leroux | Regular acceleration for number decision diagrams[END_REF]. Indeed, given a Presburger-definable binary relation R ⊆ Z n × Z n , it is undecidable to determine whether the transitive and reflexive closure R * is Presburger-definable too [START_REF] Leroux | Regular acceleration for number decision diagrams[END_REF]. We also know that there exist Presburger counter systems of dimension 1 that do not have the Presburger counting iteration property (for instance, consider the update x ′ 1 = 2x 1 ). In general, we expect that determining whether a counter system has a Presburger counting iteration is an undecidable problem by extending similar results from [START_REF] Leroux | Regular acceleration for number decision diagrams[END_REF]. By contrast, given a total affine function f (x) = Ax + b, by [START_REF] Boigelot | Symbolic methods for exploring infinite state spaces[END_REF] [START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF],

, { x, Ax + b : x ∈ Z n } * is Presburger-definable iff {A n : n ∈ N} is finite. Fol- lowing
{A n : n ∈ N} is finite iff { x, Ax + b : x ∈ Z n }
has the Presburger counting iteration. Finiteness of the monoid generated from A has been also considered in [START_REF] Emerson | On Model Checking for Non-Deterministic Infinite-State Systems[END_REF]. Indeed, the broadcast protocols introduced in [START_REF] Emerson | On Model Checking for Non-Deterministic Infinite-State Systems[END_REF] use monotone affine transition functions of the form f (x) = Ax + b where {A n : n ∈ N} is also finite. In [START_REF] Emerson | On Model Checking for Non-Deterministic Infinite-State Systems[END_REF], it is shown how to compute the least upper bound of f n (x) in order to construct coverability graphs. Nevertheless, this fact is not used in order to compute the exact value of the acceleration.

As pointed out in [START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF], flatness of the control graph is a key property enabling the symbolic computation of the reachability relation. That property ensures that there is only a finite number of 'schemes' of configuration paths (see details later on) in the PCS, and since one can effectively compute Presburger formulae associated with cycle relations, we obtain the following. PROPOSITION 7. - [START_REF] Comon | Multiple counters automata, safety analysis and Presburger analysis[END_REF][START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF] For every flat PCS satisfying the Presburger counting iteration property, one can effectively compute the reachability relation → * for the transition system S C = S, → by means of a formula in Presburger arithmetic. This proof of this folklore result is quite straightforward. Now, we will provide a sufficient condition for the Presburger counting iteration property. First, we need to recall a few definitions. The transitions in an affine PCS are of the form s

x ′ =Ax+b -----→ t where A ∈ Z n×n and b ∈ Z n .
A cycle λ has the finite monoid property if the multiplicative monoid of A λ is finite where Let us remark that our definition of a PCS having the finite monoid property is weaker than the one in [START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF] in which a PCS has the finite monoid property if the multiplicative monoid generated from all the matrices occurring in the PCS is finite. Our weaker condition is sufficient to obtain the following result: PROPOSITION 9. - [START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF][START_REF] Boigelot | On iterating linear transformations over recognizable set of integers[END_REF] Every flat and affine PCS with the finite monoid property has the Presburger counting iteration property.

A λ = A 1 • • • A N and
As a corollary of Propositions 7 and 9, the Presburger formula defining the reachability relation in every flat and affine PCS with the finite monoid property is effectively computable. By contrast, observe that in [START_REF] Comon | Multiple counters automata, safety analysis and Presburger analysis[END_REF], even though flatness is also assumed, the transition relations are not necessarily functional. Hence, the abovementioned consequence appear to be incomparable with the main result from [START_REF] Comon | Multiple counters automata, safety analysis and Presburger analysis[END_REF]. Furthermore, the systems defined in Definition 10 below are more general than the ones in [START_REF] Comon | Multiple counters automata, safety analysis and Presburger analysis[END_REF][START_REF] Bozga | Flat parametric counter automata[END_REF] since we allow a richer language on transitions.

Finally, we require functionality of the transition relation, in order to ensure effective enumeration within Presburger arithmetic of all configuration paths in the PCS. That condition is not always necessary and can be relaxed in various ways, but that will not be discussed in the paper. Let us mention that decidability still holds true if the transitions that do not belong to cycles are non-functional. DEFINITION 10. -An admissible Presburger counter system (ACS) is a flat, functional PCS, that has the Presburger counting iteration property.

In particular, due to Proposition 9, every flat and affine PCS with the finite monoid property is admissible. As we will see further, relaxing any of the conditions for admissibility leads to undecidability, even of the simple reachability problem.

In order to conclude this section, it is worth recalling that acceleration of a loop is understood as the computation of the effect of the infinite iteration and to symbolically represent this effect with a regular language, e.g., with a finite-state automaton. The first reference to acceleration of loops in counter systems and its representation by formula appeared in the seminal paper [START_REF] Boigelot | Symbolic Verification with Periodic Sets[END_REF]. The authors accelerate loops of counter systems labelled by an affine function f (x) = Ax + b where A is a diagonal matrix in {0, 1} n×n , b ∈ Z n and the domain is given by a set of linear inequalities. In [START_REF] Boigelot | Symbolic Verification with Periodic Sets[END_REF], acceleration is represented by periodic sets that can be expressed by Presburger formulae. Since A 2 = A, the infinite iteration can be indeed represented by periodic sets. In [START_REF] Boigelot | Symbolic methods for exploring infinite state spaces[END_REF][START_REF] Boigelot | On iterating linear transformations over recognizable set of integers[END_REF], this result is extended to loops labelled by affine functions f (x) = Ax + b such that {A n : n ∈ N} is finite . A rather more complex but equivalent version is given whose domain is given by a set of linear inequalities (i.e., a domain defined by a Presburger formula without quantifiers and modulo). In [START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF], this is extended to Presburger-definable domains.

Model-Checking of FOPCTL ⋆ (PrA)[n] on Admissible Counter Systems

Herein, we show decidability of model checking FOPCTL ⋆ (PrA) over admissible Presburger counter systems. The main idea behind our decidability result is the following: in an ACS there are only finitely many 'path schemas', and although each of these generates a possibly infinite set of configuration paths, the configuration paths for each path schema can be uniformly encoded within Presburger arithmetic by finite vectors of integer parameters. Thus, the quantification over paths in FOPCTL ⋆ (PrA)[n] can be simulated by quantification over tuples of natural numbers, eventually allowing translation of FOPCTL ⋆ (PrA)[n] into PrA.

Throughout this section, let C = Σ, Q, δ be an ACS of dimension n. Recall that we also assume that there is at most one transition between any two locations, by taking the disjunction of all formulae labelling the transitions between every pair of locations.

Control paths and configuration paths

DEFINITION 11. -A control path in C is any infinite path in the graph of C. A path segment in C is a single transition t ∈ δ or a simple cycle in C, that we represent as a finite sequence of locations. A path schema in C is a sequence σ 0 , . . . , σ k of path segments in C such that: 1) for every 0 ≤ i ≤ k -1, the last location of σ i is the first location of σ i+1 , 2) no single transition σ i occurs in a cycle σ j for j > i, 3) the final path segment σ k is a cycle. 4) for i = j, we have σ i = σ j .

Cycles in a path schema that are not the final segment are called interior cycles of the schema.

The idea behind the definition above is that it allows for a unique description of every control path in the graph of C. Condition (4.) allows to get a concise description.

From now on we fix an enumeration λ 1 , . . . , λ M of all the cycles in C and assume that M > 0.

In Figure 2, we present an example of an ACS (the transitions on the figure that are not labelled are assigned arbitrary functional Presburger formulae). We give below examples of control paths, path segments and path schemata in the ACS with the following convention: a simple transition is encoded by a pair of the form q, q ′ and a cycle is encoded by a sequence q, . . . , q ′ such that q = q ′ . simple cycles: λ 1 = q 1 , q 3 , q 6 , q 1 (see dotted arrows in Figure 2), λ 2 = q 4 , q 5 , q 4 , λ 3 = q 7 , q 7 q 0 q 2 q 1 q 4 q 5 q 3 q 6 q 7

x ′ = 2x

x ′ = x + 1 x ′ = 2x x ′ = x -1 x ′ = x Figure 2
. A flat counter system control path: q 0 q 2 q 4 q ω 7 (see the bold arrows in Figure 2).

path segments: q 0 , q 1 , q 1 , q 3 , q 6 , q 1 , q 4 , q 5 , q 4 , q 5 , q 4 , q 5 , q 1 , q 3 . valid path schema: q 0 , q 1 , q 1 , q 3 , q 6 , q 1 , q 1 , q 3 , q 3 , q 7 , q 7 , q 7 . invalid path schema: q 0 , q 1 , q 1 , q 3 , q 3 , q 6 , q 1 , q 3 , q 3 , q 7 , q 7 , q 7 (Condition (2) in Definition 11 is violated).

Note that the last two path schemas above describe the same control path, but the latter violates condition 2 of the definition: the single transition q 1 , q 3 also occurs in a cycle that follows after it: q 3 , q 6 , q 1 , q 3 . Since an ACS is flat and has a finite number of locations, the following holds: PROPOSITION 12. -In every ACS C with at most one transition between two locations, the number of path schemata is bounded by (N ) N where N = |Q| + |δ|.

PROOF 13. -The number of path segments is bounded by |Q| (bound on the number of simple cycles) +|δ| (bound on the number of simple transitions). Hence, the number of path schemata is bounded by N N .

Hereafter, we suppose that there are P ≥ 1 path schemas in C. A path schema with at least one interior cycle corresponds to infinitely many different control paths, since any interior cycle in the schema may be repeated an arbitrary number of times on the control path. The number of repetitions of a given cycle in a control path is called the cycle count of that cycle. Thus, every control path is completely characterized by its underlying path schema and the cycle counts for its interior cycles. The next definition formalizes this idea. DEFINITION 14. -Let the ACS C have M > 0 cycles and P path schemas. A cycle count vector c is a tuple c 1 , . . . , c M ∈ N M , where c r represents the cycle count for the cycle λ r . A control path description α is a pair α = p, c where p ∈ {1, . . . , P } denotes the path schema, c is the cycle count vector for the control path being described, c i > 0 for every interior cycle λ i and c i = 0 for any cycle λ i in C which is not interior in the path schema p. Hereafter a control path description, may be written as p, c 1 , . . . , c M . We write α 0 for the path schema associated with control path description α.

Note that in the definition above p is simply the identifier of the control path α 0 .

The following is immediate from the flatness condition on ACS.

PROPOSITION 15. -For every control path in an ACS C, there is a unique control path description.

So, we can encode control paths by tuples of positive integers. Without risk of confusion, we identify every control path with its description. For example, in the system on Figure 2, the description of the control path q 0 q 1 q 3 (q 6 q 1 q 3 ) 3 q ω 7 with underlying path schema q 0 , q 1 , q 1 , q 3 , q 6 , q 1 , q 1 , q 3 , q 3 , q 7 , q 7 , q 7 , labelled by 1, is 1, 3, 0, 0 . Every configuration path in an ACS is uniquely described by the pair α, q, a where α is its control path and q, a is the initial configuration. Conversely, due to the functionality of C, every such pair α, q, a with location of a corresponding to the first location of the path schema α 0 , describes a unique path in the configuration graph starting at q, a , and progressing according to the transitions of the control path α. Note, however, that such a path may terminate and therefore not be considered as a configuration path.

In the example on Figure 2, from the control path q 0 q 2 q 4 q ω 7 and the initial configuration with x = 3, we obtain the configuration path q 0 , 3 q 2 , 4 q 4 , 8 q 7 , 7 ω .

Encoding the configurations along a path by a Presburger formula

In this section we construct a Presburger formula that exactly describes the configuration path associated with a control path and initial configuration. As a corollary of Theorem 16 below, we obtain Proposition 7.

THEOREM 16. -Given an ACS C of dimension n with M > 0 cycles, one can compute a Presburger formula PathConfig

C (v, x, i, y) such that for all α ∈ N M+1 , a ∈ Z n+1 , m ∈ N and b ∈ Z n+1 : α, a, m, b |= PathConfig C (v, x, i, y)
iff α is a valid control path description and the m th configuration of the configuration path α, a is b (v, x and y are variable sequences and i is a variable).

PROOF 17. -Sketch: First, when a cycle λ has the Presburger counting iteration property, we write ϕ λ (x, y, x ′ ) to denote the Presburger formula encoding its counting iteration relation. In that case, there is also a Presburger formula A λ (x, k, x ′ ) that expresses that x ′ is obtained from x by following k transitions along the cycle λ. Now, we will construct a formula PathConfig C in accordance with the requirements of the theorem.

First, let P be the number of path schemas in C. We consider each path schema p individually, constructing a formula SchemaConfig p (v, x, i, y) such that for all α ∈ N M+1 , a ∈ Z n+1 (encoding a configuration), m ∈ N and b ∈ Z n+1 it is the case that α, a, m, b |= SchemaConfig p (v, x, i, y) iff α is a control path description, the path schema of the control path α is p, and the m th configuration of the configuration path α, a is b. Then our desired formula PathConfig C will be the disjunction over all SchemaConfig p where p is a path schema in the system.

To define SchemaConfig p for a fixed path schema p, we proceed as follows. Suppose σ 0 , . . . , σ k is the sequence of segments in p, and α is a control path with path schema p. Along the unique (if it exists) configuration path induced by α starting with configuration a, we will identify some landmark positions and landmark configurations: for each segment σ j (where 0 ≤ j < k) we would like to identify the position t j ∈ N and the configuration w j ∈ Z n+1 immediately before the segment σ j is traversed (or entered for the first time, if the segment is a cycle).

The landmarks associated with segment σ 0 are the initial position t 0 = 0 and the initial configuration w 0 = a.

We define κ j to be the number of positions in the configuration path that are covered by segment σ j . If segment σ j is a single transition then the number of positions covered by that segment is 1. Otherwise, the segment σ j is some interior cycle λ r with |λ r | transitions in the cycle. Recall that the number of times the cycle λ r is traversed in the control path described by v is given by the cycle count v r . Then, the total number of positions in the configuration path covered by the segment σ j is v r |λ r |. Formally:

-if σ j is a transition q, A(x, x ′ ), q ′ then κ j def = 1, -if σ j is a cycle λ r then κ j def = v r |λ r |.
Having defined κ j , we can now state that our landmark positions t i will thus satisfy the following constraints: t 0 = 0 and t j+1 = t j + κ j for 0 ≤ j < k.

Next, we consider the landmark configuration that corresponds to each landmark position. We would like to describe in a uniform way those configurations that appear while a specific segment is traversed. So, for the segment σ j , we define a Presburger formula SegmentConfig j (x, i, y) such that for all a ∈ Z n+1 , m ∈ N, and b ∈ Z n+1 , it is the case that a, m, b |= SegmentConfig j (x, i, y) iff the location of the configuration a appears as one of the locations in σ j , and the configuration b is reached from configuration a after m transitions, according to the transition(s) of σ j .

When segment σ j is just a single transition, we define SegmentConfig j using the transition relation. Otherwise, if the segment is a simple cycle, we use the corresponding counting iteration relation.

Formally, we define SegmentConfig j as follows:

-if σ j is a transition t = q, A(x, x ′ ), q ′ then SegmentConfig j (x, i, y)

def = x 0 = q ∧ ((i = 0 ∧ x = y) ∨ (i = 1 ∧ A(x, y))), -if σ j is a simple cycle λ then SegmentConfig j (x, i, y) def = A λ (x, i, y).
We define the string of quantifiers ExistLandmarks def = ∃t 0 , . . . , ∃t k , ∃w 0 , . . . , ∃w k and define the formula

LandmarkConstraints def = (t 0 = 0 ∧ w 0 = x) k-1 j=0 [(t j+1 = t j + κ j ) ∧ SegmentConfig j (w j , κ j , w j+1 )].
If the configuration path is infinite, we are assured that such landmarks exist, hence the formula that claims their existence will be true. Conversely, to ensure that the path in the Presburger transition system will be infinite, we will extend the formula to confirm the existence of configurations in all positions after the last landmark:

CheckInfinite def = ∀t(t k < t → ∃z SegmentConfig k (x, t -t k , z)).
The final part of our construction of SchemaConfig p is to include a subformula that checks for the occurrence of a given configuration at a given position of the configuration path. We have to take some care to check whether position i occurs in a segment before the final cycle segment is entered, or inside the final cycle.

CheckConfig def = k-1 j=0 [(t j ≤ i ∧ i < t j+1 ) → SegmentConfig j (w j , i -t j , y)] ∧ [(t k ≤ i) → SegmentConfig k (w k , i -t k , y)].
The above formulae are now combined to give the configuration checking formula for path schema p

SchemaConfig p (v, x, i, y) def = (ξ 0 = p)∧ ExistLandmarks[LandmarkConstraints ∧ CheckInfinite ∧ CheckConfig ].
Finally we have:

PathConfig C (v, x, i, y) def = M p=1
PathConfig p (v, x, i, y).

We define two auxiliary formulae that will be used in the following proof. Firstly, we can check that a pair (v, x) denotes a valid configuration path, by checking that the initial configuration of the path is correct and that the path is infinite:

ValidPath (v, x) def = PathConfig C (v, x, 0, x) ∧ ∀i ≥ 0∃zPathConfig C (v, x, i, z)
Secondly, for two configuration paths denoted by (v, x) and (v ′ , y) we would like to express that the paths agree on all configurations up to and including position i. To this end, we construct the formula

CommonPathPrefix (v, x, v ′ , y, i) def = ∀j ≥ 0[j ≤ i ⇒ ∀z(PathConfig C (v, x, j, z) ⇔ PathConfig(v ′ , y, j, z))],
This formula will be used when quantifying over paths with identical finite past.

A decision procedure to verify an admissible counter system

We are now ready to show that model-checking FOPCTL ⋆ (PrA)[n] can be reduced to satisfiability in Presburger arithmetic. THEOREM 18. -Given an ACS C of dimension n with Presburger transition system

S C = S, → , for every semi-closed FOPCTL ⋆ (PrA)[n] formula ϕ, one can compute a Presburger formula A ϕ (x) such that for every q, a ∈ S C , q, a |= A ϕ (x) iff C, q, a |= ϕ (no need for environment since ϕ is semi-closed).
PROOF 19. -We show that, given an ACS C, for every FOPCTL ⋆ (PrA)[n] formula ϕ, one can define a Presburger formula T ( v, x, i ; ϕ) with free variables v, x, i such that α, a, m |= T ( v, x, i ; ϕ) iff for the configuration path π with control path α and initial configuration a, we have that π, m |= ϕ, if such configuration path exists.

We define T recursively on ϕ as follows:

T ( v, x, i ; θ(x, y)) def = ∀z[PathConfig C (v, x, i, z) ⇒ θ(z, y)]; T ( v, x, i ; ¬ϕ) def = ¬T ( v, x, i ; ϕ); T ( v, x, i ; ϕ ∧ ϕ ′ ) def = T ( v, x, i ; ϕ) ∧ T ( v, x, i ; ϕ ′ ); T ( v, x, i ; Xϕ) def = ∃j[(j = i + 1) ∧ T ( v, x, j ; ϕ)]; T ( v, x, i ; ϕUϕ ′ ) def = ∃j((j ≥ i ∧ [T ( v, x, j , ϕ ′ ) ∧ ∀k(i ≤ k < j ⇒ T ( v, x, k , ϕ)])); T ( v, x, i ; X -1 ϕ) def = i > 0 ∧ ∃j[(i = j + 1) ∧ T (v, x, j, ϕ)]; T ( v, x, i ; ϕSϕ ′ ) def = ∃j((j ≤ i ∧ [T ( v, y, j ; ϕ ′ ) ∧ ∀k(j < k ≤ i ⇒ T ( v, x, k ; ϕ)])); T ( v, x, i ; A ϕ) def = ∀v ′ , y[CommonPathPrefix(v, x, v ′ , y, i) ⇒ T ( v ′ , y, i ; ϕ)]; T ( v, x, i ; ∃ y ϕ) def = ∃ y T ( v, x, i ; ϕ).
The formula A ϕ (x) is defined as follows:

A ϕ (x) def = ∀ v(ValidPath (v, x) ⇒ T ( v, x, 0 ; ϕ)).
Note that, for a fixed ACS, the size of A ϕ (x) is linear in the size of ϕ. However, when the ACS is not fixed, presently we have no way to measure the size of A ϕ (x) in function of the size of the ACS. Indeed, we have no measure on the size of the Presburger formulae witnessing the Presburger counting iteration property. PROOF 21. -Indeed, in order to decide the local model checking problem, it is sufficient to check whether q, a |= A(x) holds true where the Presburger formula A(x) is computed from the proof of Theorem 18. Global model checking can be solved by computing precisely the formula A(x) and testing Presburger validity. Finally, by Proposition 7, there is a Presburger formula A ′ (x, x ′ ) computing the reachability relation in the configuration graph of some ACS. In order to solve validity checking by an initial condition A 0 (x), it is sufficient to check Presburger validity of the formula

∀ x, x ′ (A 0 (x) ∧ A ′ (x, x ′ ) ⇒ A(x ′ )).
Theorem 20 can be extended to systems and temporal logics such that PrA is replaced by any decidable extension PrA + of PrA, closed under first-order quantification and Boolean operators, obtained by adding new predicates. The notion of Presburger counter system is extended by allowing transitions labelled by elements of PrA + . Similarly, FOPCTL ⋆ (PrA + ) is obtained from FOPCTL ⋆ (PrA) by allowing atomic formulae from PrA + . The model-checking problems for FOPCTL ⋆ (PrA + ) are defined as for FOPCTL ⋆ (PrA). Finally, the notions of counting iteration property and admissible counter systems are defined with PrA + instead of PrA.

THEOREM 22. -The following problems for FOPCTL ⋆ (PrA + ) restricted to ACSs are decidable: local model checking, global model checking, validity checking with an initial configuration.

Testing the boundaries of decidable model checking in Presburger counter systems

Here we give some results and examples indicating that our result in Theorem 20 is close to optimal. Before that, call a PCS piecewise-affine whenever each transition is labelled by a disjunction of expressions of the form θ(x) ∧ x ′ = Ax + b.

PROPOSITION 23. -The reachability problem is not decidable in any of the following classes:

1) all flat affine PCSs; 2) all affine PCSs with the finite monoid property (even counter automata); 3) all flat piecewise-affine PCSs with a single location.

PROOF 24. -(1) Follows from results in [START_REF] Cortier | About the Decision of Reachability for Register Machines[END_REF] about very basic control graphs but having cycles without the Presburger counting iteration property.

(2) Follows from undecidability of the halting problem for Minsky machines [START_REF] Minsky | Computation, Finite and Infinite Machines[END_REF].

(3) Follows from [START_REF] Minsky | Computation, Finite and Infinite Machines[END_REF], too. As a matter of fact, any counter automaton can be encoded as a flat piecewise-affine PCS with a single location q 0 . Indeed, suppose that q

x:=x+1 ----→ q ′ is a transition in the counter automaton with the integer n [resp. n ′ ] attached to q [resp. q ′ ], then the unique transition in the piecewise-affine PCS is of the form q 0 (x0=n∧x ′ 0 =n ′ ∧x ′ =x+1)∨...

-----------------→ q 0 . There is an obvious correspondence between the transitions in the original counter automaton and the number of disjuncts in the Presburger formula labelling the unique transition.

To show how close to optimal our class of ACSs is, we give below an undecidability result for a fixed PCS C u that is almost an ACS, but not flat. It is obtained from an ACS by only adding a reset transition while preserving the Presburger counting iteration property and functionality (see Figure 3). C u is of dimension 4, with counters x 1 , x 2 and x 3 , x 0 is the additional counter representing the location, and "id" denotes the identity function on the counters x 1 , x 2 and x 3 . q 0 q 1 q 2 id id PROOF 26. -The proof is by reducing the recurrence problem for nondeterministic 2-counter machines that is shown Σ 1 1 -hard in [START_REF] Alur | A really temporal logic[END_REF]. A nondeterministic 2-counter machine M consists of two counters C 1 and C 2 , and a sequence of n ≥ 1 instructions. The k-th instruction is written as one of the following:

x ′ 1 = x ′ 2 = x ′ 3 = 0 x ′ 1 = x 1 + 1 x ′ 2 = x 2 + 1 x ′ 3 = x 3 + 1
k : C i := C i + 1; goto k 1 or goto k 2 . k : if C i = 0 then goto k 0 else C i := C i -1; goto k 1 or goto k 2 .
We represent the configurations of M by triples c 1 , c 2 , l where 1 ≤ l ≤ n, c 1 ≥ 0 and c 2 ≥ 0. A computation of M is a finite sequence of related configurations, starting with the initial configuration 0, 0, 1 (location encoded as last element). The recurrence problem can be stated as the existence of an infinite execution that passes through the instruction 1 infinitely often. We shall build a formula ϕ of FOLTL(Pr) [3] such that M visits 1 infinitely often iff q 2 , 0, 0, 1 |= ϕ. The formula ϕ is of the form

E (GF(x 3 = 1 ∧ X(x 0 = 0)) ∧ 1≤k≤n Gϕ ′ k ),
where ϕ ′ k encodes the k-th instruction. For instance, the k-th instruction "C 1 :=

C 1 + 1; goto k 1 or goto k 2 " is encoded by ∀y, z (x 1 = y ∧ x 2 = z ∧ x 3 = k ∧ X(x 0 = 0)) ⇒ X(¬(X(x 0 = 0)) U (X(x 0 = 0) ∧ increase C1 x 1 = y + 1 ∧ x 2 = z ∧ (x 3 = k 1 ∨ x 3 = k 2 ))).
Other instructions can be encoded similarly.

It is worth mentioning that C u can be simulated by an ACS ('flattened') in a sense preserving the reachability sets, and therefore the strict EF fragment of FOLTL(Pr) [3] has a decidable local model-checking problem for C u . Furthermore, by using the idea in the proof of Theorem 25 one can show that FOLTL(PrA) [3] has an undecidable local model-checking problem for the PCS described in Figure 4 (that is flat, has the Presburger counting iteration but is not functional) with variables x 1 , x 2 , x 3 , and x 0 representing the location, where ⊤ denotes the truth constant.

q 0 ⊤ This PCS has a unique transition that accepts any update of the counters x 1 , x 2 and x 3 . Hence, any sequence N → {q 0 } × Z 3 is an infinite configuration path of this PCS. By way of example, as done above, the k-th instruction "C

1 := C 1 + 1; goto k 1 or goto k 2 " is encoded by ∀ y, z (x 1 = y ∧ x 2 = z ∧ x 3 = k) ⇒ X(x 1 = y + 1 ∧ x 2 = z ∧ (x 3 = k 1 ∨ x 3 = k 2 )).

Decidable Extension of FOPCTL ⋆ (PrA)[n] with CQDD Patterns

We present below an extension of FOPCTL ⋆ (PrA) [n] for which model-checking over ACS can still be encoded into Presburger satisfiability.

In [START_REF] Wolper | Temporal logic can be more expressive[END_REF] Wolper extends linear-time temporal logic LTL to an extended temporal logic that has the same expressive power as Büchi automata. In this section, we similarly extend the set of path formulae from FOPCTL ⋆ (PrA)[n] by allowing temporal operators defined by another class of language acceptors, namely the CQDD (constrained queue-content decision diagrams) [START_REF] Bouajjani | Symbolic Reachability Analysis of FIFO-channel systems with nonregular sets of configurations[END_REF]. This formalism has been introduced for symbolically representing infinite sets of configurations in FIFO automata -our use of CQDD is different. Non-regular languages can be defined with CQDD; moreover, the model-checking problem for LTL augmented with operators defined from CQDD is undecidable [START_REF] Demri | Modern Applications of Automata Theory, IIsc Research Monographs, World Scientific, chapter Specification and Verification using Temporal Logics[END_REF], unlike the extension with regular languages [START_REF] Wolper | Temporal logic can be more expressive[END_REF]. The proof of that result is inspired from the undecidability proof of propositional dynamic logic (PDL) augmented with programs over the context-free language {a n 1 • a 2 • a n 1 : n ≥ 0} (see (Harel et al., 2000, Chapter 9)). This context-free language can be easily recognized by a CQDD. By contrast, we show that the model-checking problem for FOPCTL ⋆ (PrA)[n] extended with CQDD-based operators is decidable over ACS. Decidability is regained due to the flatness restriction in CQDD. Hence, in this section we show evidence that we can take advantage of flatness both in models and in formulae.

Before introducing the formal definition for CQDDs, let us mention that CQDD are finite-state automata attached to Presburger formulae that provide constraints on the number of times transitions are taken. Moreover, the underlying graphs of CQDDs is flat by definition.

A CQDD is a structure A = Σ, S, S 0 , E, l, A(y 1 , . . . , y m ), F such that:

-Σ is a finite set of symbols (the alphabet), -S is a finite set of states, -S 0 ⊆ S is the set of initial states, -E ⊆ S × Σ × S is a set of transitions of cardinality m and S, Σ, E is flat, -F ⊆ S is a set of final (or accepting) states, -l is a bijection from E to {1, . . . , m}, -A(y 1 , . . . , y m ) is a Presburger formula.

An accepting run for the word σ = a 0 a 1 a 2 . . . a k-1 is a sequence q 0

a0 -→ q 1 a1 -→ q 2 . . . a k -1
--→ q k such that q 0 ∈ S 0 , q k ∈ F (the standard acceptance conditions for finite-state automata), -for every i ∈ {0, . . . , k -1}, q i , a i , q i+1 ∈ E, -n 1 , . . . , n m |= A(y 1 , . . . , y m ) in Presburger arithmetic, where each n i is the number of occurrences of the transition l -1 (i) in the sequence (alternatively, (n 1 , . . . , n m ) is the Parikh image of σ).

The word σ is also said to be accepted by the automaton A. We write L(A) to denote the set of words accepted by A.

Figure 4 presents a CQDD with its constraint on the number of occurrences (each transition is related to a unique letter and to a unique variable in the constraint). π, i |= A(φ 1 , . . . , φ n ) iff either ǫ ∈ L(A), or there is a finite word a i1 a i2 . . . a in ∈ L(A) such that for every 1 ≤ j ≤ n, π, i + (j -1) |= φ ij . Thus, π, i |= A(φ 1 , . . . , φ n ) holds when a finite pattern induced from L(A) satisfies the respective arguments on the suffix path starting from position i. Note the correspondence between the letters a 1 , . . . , a k and the arguments φ 1 , . . . , φ n . These automata-based operators are defined like those in [START_REF] Wolper | Temporal logic can be more expressive[END_REF] except that the languages of finite words we consider are not exactly the regular languages. Of the regular languages only the bounded ones are allowed, and some context-free languages can be obviously defined.

For instance, in EFOPCTL ⋆ (Pr) [n] we can state that there is a path and some m = 0 such that φ 1 holds true at the m first positions, then φ 2 holds true at the m next positions and then neither φ 1 nor φ 2 holds true forever. It is known that ETL is more expressive that LTL [START_REF] Wolper | Temporal logic can be more expressive[END_REF] and this result could be lifted between FOPCTL ⋆ (PrA)[n] and EFOPCTL ⋆ (Pr) [n]. However, at the present moment, we do not have a formal proof of this. Theorem 18 can be extended by allowing CQDD-based operators.

THEOREM 27. -Given an ACS C of dimension n with Presburger transition system S C = S, → , for every EFOPCTL ⋆ (Pr) [n] formula ϕ, one can compute a Presburger formula A ϕ (x) such that for every q, a ∈ S C , q, a |= A ϕ (x) iff C, q, a |= ϕ.

PROOF 28. -First, one can show that any language recognized by a CQDD A can be recognized by an ACS augmented with an alphabet. In such enriched ACS, the transitions between control states are of the form q A(x,x ′ ),a -----→ q ′ where a is a letter from a finite alphabet. Any transition t = q a -→ q ′ in the CQDD is translated in the enriched ACS by a transition of the form q xt:=xt+1,a ------→ q ′ where x t is a variable attached to the transition t. To any final state q of the CQDD, we associate the transition q A(xt 1 ,...,xt m ),ǫ ---------→ q new the CQDD having m distinct transitions and q new being a new control state. There is a natural correspondence between the accepting runs of the CQDD and paths in the enriched ACS from initial states and q new . In that way, the final constraint A(y 1 , . . . , y m ) on the m transitions can be simulated in some ACS by increasing the ith counter whenever the ith transition is visited in the accepting run and checking the final constraint amounts to adding a final transition with identity function and domain precisely the values of the counters satisfying A(y 1 , . . . , y m ). Hence, the proof technique from Theorem 16 can be used again. Typically, the following formulae can be defined in Presburger Arithmetic:

-By replacing valid control paths with accepting runs, there is a formula P athConf ig A (v, i, j) stating that the ith transition of the accepting run v is a j .

-The formula Length(v, l) states that the accepting run v has l transitions.

-The formula AcceptingRun(v) states that v encodes an accepting run. Typically, we also use a path schema (starting from an initial state) and a cycle count vector which is possible because of the flat structure of A.

Once these formulae are defined, it remains to define T ( v, x, i ; A(φ 1 , . . . , φ k )) as follows (we omit the obvious case when ε ∈ L(A)): ∃ v ′ , l, AcceptingRun(v ′ ) ∧ Length(v ′ , l)∧ ((l = 0)∨∀ 1 ≤ i ′ ≤ l, c∈{1,...,k} P athConf ig A (v ′ , i ′ , c) ⇒ T ( v, x, i+i ′ -1 ; φ c )).

Then, the formula A ϕ (x) can be defined as in the proof of Theorem 18.

As a corollary, local model-checking problem for EFOPCTL ⋆ (Pr)[n] over ACS is decidable.

COROLLARY 29. -The following problems for EFOPCTL ⋆ (Pr) [n] are decidable: local model checking, global model checking, validity checking with an initial configuration.

Concluding Remarks

In this paper we have established decidability of various model-checking problems for FOPCTL ⋆ (PrA) and related CTL ⋆ -like languages over Presburger arithmetic on a class of counter systems, by translation into Presburger arithmetic. Indeed, encoding quantification over paths can be performed by quantification over tuples of natural numbers. Hence, we have improved the decidability boundary for model-checking ACS with CTL ⋆ -like languages. The decidability of model-checking is currently open on extensions with fixed-point operators (e.g., Presburger µ-calculus) or monadic second-order quantification over ACS.

Another direction for further work is to analyze and extend further the class of ACS. For instance, giving up the functionality assumption on transitions that do not belong to a cycle preserves decidability, while it is open whether giving up the full functionality assumption still preserves decidability in the absence of first-order quantification. Similarly, the complexity of local model checking ACS with quantifier-free Presburger transition formulae over FOPCTL ⋆ (PrA) is not fully characterized.

There are several related questions that have at least theoretical interest, which we have no addressed in the paper. For instance, how are the configuration graphs of ACSs placed relative to Caucal's hierarchy [START_REF] Caucal | On infinite transition graphs having a decidable monadic theory[END_REF]? It is not difficult to construct examples of ACS, like the one shown in Figure 5, with configuration graphs which are not pushdown graphs [START_REF] Muller | The theory of ends, pushdown automata , and second-order logic[END_REF]. In the ACS displayed in Figure 5 the transitions from q 2 to q 3 and q 4 are only enabled when x = 0. It is easy to see that the configuration graph generated from the initial state (0, 0, 0, 0) has infinitely many non-isomorphic ends, and therefore, by Muller-Schupp's theorem [START_REF] Muller | The theory of ends, pushdown automata , and second-order logic[END_REF] it is not a pushdown graph.

We currently do not know whether all ACS generate prefix-recognizable configuration graphs, or any graphs from higher levels of Caucal's hierarchy. Of course, decidability of MSO in a configuration graph does not imply decidability of FOPCTL ⋆ (PrA), but it could suggest further strengthening of the results in the current paper.

Finally, the results in this paper can be extended to non-admissible counter systems, which are behaviorally equivalent in a suitable sense to ACSs. Typically, such q 1 q 2 q 3 q 4 z ′ 1 := z 1 + 1 z ′ 2 := z 2 + 1

x ′ := x + 1

x ′ := x -1, y ′ := y + 1

z ′ 1 := z 1 + 1 z ′ 2 := z 2 + 1

  the cycle λ is labelled by the sequence of matrices A 1 • • • A N . DEFINITION 8. -A PCS C has the finite monoid property if every cycle in the control graph of C has that property.

  THEOREM 20. -The following problems for FOPCTL ⋆ (PrA) restricted to ACSs are decidable: local model checking, global model checking, validity checking with an initial configuration.

Figure 3 .

 3 Figure 3. Almost an admissible counter system

  Figure 4. A CQDDLet A = Σ, S, S 0 , E, l, A(y 1 , . . . , y m ), F be a CQDD with the letters from Σ linearly ordered: a 1 < . . . < a k . The extension EFOPCTL ⋆ (Pr)[n] of the logic FOPCTL ⋆ (PrA)[n] consists in considering formulae of the form A(φ 1 , . . . , φ n ) defined as follows:

Figure 5 .

 5 Figure 5. A simple ACS with a non-pushdown graph and non-terminating paths

  cycle has the Presburger counting iteration property if its cycle relation has a Presburger counting iteration. DEFINITION 6. -A PCS C has the Presburger counting iteration property if every cycle in the control graph of C has that property. Observe that if a PCS C has the Presburger counting iteration property, we can effectively identify the Presburger formula associated with each cycle. It is sufficient to enumerate Presburger formulae A(x, i, y) and test whether

	∀x

, ANR projects AVERISS and VERIDYC.