Clark Barrett

Stéphane Demri

Morgan Deters

Witness Runs for Counter Machines

In this paper, we present recent results about the verification of counter machines by using decision procedures for Presburger arithmetic. We recall several known classes of counter machines for which the reachability sets are Presburger-definable as well as temporal logics with arithmetical constraints. We discuss issues related to flat counter machines, path schema enumeration, and the use of SMT solvers.

Introduction

Infinite-state systems. Model-checking is a standard approach to verifying properties of computing systems [START_REF] Clarke | Model checking[END_REF] and it is known that dealing with infinity or unboundedness of computational structures leads easily to undecidable verification problems. Such problems include testing boundedness (checking whether a counter in a counter machine takes a finite amount of values) and those dealing with model-checking temporal formulae in which atomic formulae can state properties about unbounded values (e.g., arithmetical constraints about counter values). Roughly speaking, techniques for the verification of infinite-state systems stem from exact methods in which potentially infinite sets of configurations are finitely represented symbolically to semi-algorithms that are designed to behave well in practice. When exact methods can produce decision procedures, this is because an underlying finite structure can be identified in the verification problem. For instance, the set of reachable configurations can be effectively represented symbolically, typically by a formula in Presburger arithmetic, for which satisfiability is 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]. The use of Presburger arithmetic for formal verification has been advocated in [START_REF] Suzuki | Verification Decidability of Presburger Array Programs[END_REF]. Finiteness can also occur in a more subtle way, as in well-structured transition systems [START_REF] Finkel | Well-structured transitions systems everywhere![END_REF], for which termination is guaranteed thanks to underlying well-quasi-orderings, see e.g. [START_REF] Kosaraju | Decidability of reachability in vector addition systems[END_REF][START_REF] Ouaknine | On the Decidability of Metric Temporal Logic[END_REF].

Counter machines. Counter machines are well-known infinite-state systems that have many applications in formal verification. Their ubiquity stems from their use as operational models for several purposes, including for instance for broadcast protocols [START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF], for programs with pointer variables (see [BBH + 06]) and for logics for data words, see e.g. [START_REF] Bojańczyk | An extension of data automata that captures XPath[END_REF]. However, numerous model-checking problems for counter machines, such as reachability, are known to be undecidable. Many subclasses of counter machines admit a decidable reachability problem, such as reversal-bounded counter automata [START_REF] Ibarra | Reversal-bounded multicounter machines and their decision problems[END_REF] and flat counter automata [START_REF] Comon | Multiple counter automata, safety analysis and Presburger Arithmetic[END_REF][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]. These two classes of machines admit reachability sets effectively definable in Presburger arithmetic (assuming some additional conditions, unspecified herein). In general, computing the transitive closures of integer relations is a key step to solve verification problems on counter machines, see e.g. [BW94,CJ98,Fri00,FL02,BIK09].

Flatness. Flat counter machines are counter machines in which each control state belongs to at most one simple cycle (i.e., a cycle without any repetition of edges). Several classes of such flat operational devices have been identified and reachability sets have been shown effectively Presburger-definable for many of them, see e.g. [START_REF] Fribourg | Proving safety properties of infinite state systems by compilation into Presburger arithmetic[END_REF][START_REF] Comon | Multiple counter automata, safety analysis and Presburger Arithmetic[END_REF][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][START_REF] Bozga | Fast acceleration of ultimately periodic relations[END_REF]. This provides a decision procedure for the reachability problem, given a prover for Presburger arithmetic validity. Effective semilinearity boils down to check that the effect of a loop can be characterized by a formula in Presburger arithmetic (or in any decidable fragment of first-order arithmetic). The results for flat counter machines can be then obtained by adequately composing formulae for loops and for finite paths. However, this approach, briefly described in this paper, suffers from at least two drastic limitations. First, flatness in counter machines remains a strong restriction on the control graph, though this has been relaxed by considering flattable counter machines, see e.g. [START_REF] Bardin | Flat acceleration in symbolic model checking[END_REF][START_REF] Leroux | Flat counter systems are everywhere! In ATVA'05[END_REF][START_REF] Leroux | Presburger Vector Addition Systems[END_REF] and Section 3.5, where a machine may not itself be flat, but is known to have a flat unfolding with the same reachability set. The second limitation is due to the fact that reachability questions are not the only interesting ones and the verification of properties expressed in dedicated temporal logics is often desirable, see e.g. [START_REF] Demri | Model-checking CTL * over flat Presburger counter systems[END_REF].

In this paper, we present a selection of results about the verification of counter machines, at times assuming flatness, from reachability problems to model-checking problems with temporal logics. We follow an approach similar to [START_REF] Fribourg | Petri nets, flat languages and linear arithmetic[END_REF] to translate verification problems into Presburger arithmetic satisfiability. We focus on flattable counter machines and how to compute flat unfoldings by enumerating path schemas while invoking SMT solvers to optimize this enumeration. This part of the paper presents preliminary results, and it will be the subject of a dedicated paper. Satisfiability Modulo Theories. Deciding Presburger arithmetic fragments is essential to verify properties of programs; see e.g. [START_REF] Shostak | A practical decision procedure for arithmetic with function symbols[END_REF] and [START_REF] Suzuki | Verification Decidability of Presburger Array Programs[END_REF] for an early use of Presburger arithmetic for formal verification. Most well-known SMT solvers deal with quantifier-free linear integer formulae, also known as quantifierfree linear integer arithmetic ('QF_LIA' in the parlance of SMT-LIB [START_REF] Barrett | The SMT-LIB standard: Version 2.0[END_REF]). For instance, this includes Z3 [START_REF] De Moura | Z3: An Efficient SMT Solver[END_REF], CVC4 [BCD + 11] and Alt-Ergo [START_REF] Conchon | SMT Techniques and their Applications: from Alt-Ergo to Cubicle[END_REF], to cite a few of them. However, dealing with quantifiers is usually a difficult task for SMT solvers that are better tailored to theory reasoning. Many generalpurpose SMT solvers (including CVC3, CVC4, Z3, Yices, Alt-Ergo) do accept formulas with quantifiers and they handle them in roughly the same way, through heuristic instantiation. Z3 is unique in that it implements several quantifierelimination procedures as preprocessing steps, including a procedure for Presburger arithmetic ('LIA' in SMT-LIB). It is worth also mentioning automatabased tools dealing with satisfiability such as MONA [START_REF] Biehl | MONA: Decidable arithmetic in practice[END_REF], LASH [START_REF] Boigelot | On the use of weak automata for deciding linear arithmetic with integer and real variables[END_REF] or TAPAS [START_REF] Leroux | TaPAS: The Talence Presburger Arithmetic Suite[END_REF]. Even though Presburger arithmetic admits quantifier elimination, it is known that eliminating quantifiers can be computationally expensive (see e.g., [START_REF] Reddy | Presburger arithmetic with bounded quantifier alternation[END_REF][START_REF] Grädel | Subclasses of Presburger arithmetic and the polynomial-time hierarchy[END_REF]). Recent developments propose a promising, lazy approach for quantifier elimination [START_REF] Monniaux | Quantifier elimination by lazy model enumeration[END_REF].

Machines with Registers

In this section, we briefly present Presburger arithmetic (PA), the class of Presburger counter systems, and standard subclasses.

Presburger arithmetic in a nutshell

Presburger arithmetic (PA) has been introduced by M. Presburger 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] where it is shown decidable by quantifier elimination. This decidability result on the theory of addition is regarded today as a key result in theoretical computer science.

Let VAR = {x, y, z, . . .} be a countably infinite set of variables. Terms are expressions of the form a 1 x 1 + • • • + a n x n + k where a 1 , . . . , a n are constant coefficients in N, k is in N and the x i 's are variables. Variables and terms come with their interpretations when the variables are interpreted by natural numbers. A valuation v is a map VAR → N and it can be extended to the set of all terms as follows: v(k) = k, v(ax) = a × v(x) and v(t + t ) = v(t) + v(t ) for all terms t and t . Formulae are defined by the grammar below:

φ ::= t ≤ t | ¬φ | φ ∧ φ | ∃ x φ
where t and t are terms and x ∈ VAR. A formula φ is in the linear fragment def ⇔ φ is a Boolean combination of atomic formulae of the form t ≤ t . The semantics for formulae in (PA) is defined with the help of the satisfaction relation |= that determines the conditions for the satisfaction of a formula under a given valuation (we omit the Boolean clauses):

-v |= t ≤ t def ⇔ v(t) ≤ v(t ), -v |= ∃ x φ def ⇔ there is n ∈ N such that v[x → n] |= φ where v[x → n] is equal to v except that x is mapped to n.
Any formula φ(x 1 , . . . , x n ) whose free variables are among x 1 , . . . , x n , with n ≥ 1, defines a set of n-tuples φ(x 1 , . . . ,

x n ) def = { v(x 1 ), . . . , v(x n ) ∈ N n : v |= φ}
which contains all the tuples that make true the formula φ by ignoring the irrelevant interpretation of the bound variables and by fixing an arbitrary ordering between the variables. For instance,

x 1 < x 2 = { n, n ∈ N 2 : n < n }.
Let φ be a formula φ(x 1 , . . . , x n ) with n ≥ 1 free variables x 1 , . . . , x n . We say that φ is a Presburger set. The satisfiability problem for (PA) is a decision problem that takes as input a formula φ and asks whether there is a valuation v such that v |= φ. If such a valuation exists, we say that φ is satisfiable.

Theorem 1 (Presburger Arithmetic Decidability). [START_REF] Presburger | Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt[END_REF] The satisfiability problem for (PA) is decidable.

The satisfiability problem can be solved in triple exponential time [START_REF] Oppen | A 2 2 2pn upper bound on the complexity of Presburger arithmetic[END_REF] by analyzing the quantifier elimination procedure described in [START_REF] Cooper | Theorem proving in arithmetic without multiplication[END_REF]. It was shown 2ExpTime-hard in [START_REF] Fischer | Super-exponential complexity of Presburger arithmetic[END_REF] and to be in 2ExpSpace in [START_REF] Ferrante | The Computational Complexity of Logical Theories[END_REF]. An exact complexity characterization is provided in [START_REF] Berman | The complexity of logical theories[END_REF] (double exponential time on alternating Turing machines with linear amounts of alternations).

Presburger counter systems

The systems introduced below are finite-state automata augmented with registers, also known as counters (variables interpreted as natural numbers). Transitions are labelled by arithmetical constraints on counters defined in (PA). A Presburger counter system C = Q, n, δ is a structure (see e.g. [START_REF] Demri | Model-checking CTL * over flat Presburger counter systems[END_REF][START_REF] Leroux | Presburger counter machines[END_REF]) such that -Q is a nonempty finite set of control states, n ≥ 1 is the dimension of the system, i.e. the number of counters, we assume that the counters are represented by the variables x 1 , . . . , x n , δ is the transition relation defined as a finite set of triples of the form q, φ, q , where q, q are control states and φ is a Presburger formula whose free variables are among x 1 , . . . , x n , x 1 , . . . , x n . Prime variables are intended to be interpreted as the next values of the unprimed variables.

Figure 1 contains a Presburger counter system C such that inc(i) [resp. dec(i)] stands for the formula that increments [resp. decrements] the counter x i and keeps unchanged the other counters. Formulae zero(i) tests if counter x i is equal to zero but it has no effect on the counters.

Elements t = q, φ, q ∈ δ are called transitions and are often represented by q φ -→ q . A configuration of the Presburger counter system C = Q, n, δ is a pair q, x ∈ Q × N n . Given two configurations q, x , q , x and a transition t = q φ -→ q , we write q, x t -→ q , x whenever v |= φ (in (PA)) and for every Most verification problems on Presburger counter systems are known to be undecidable since they include Minsky machines [Min67, Chapter 11] (see also [START_REF] Minsky | Recursive unsolvability of Post's problems of 'tag' and other topics in theory of Turing machines[END_REF]Section 3]) that are Turing-complete, even if restricted to two counters [START_REF] Minsky | Computation, Finite and Infinite Machines[END_REF]Chapter 14]. The introduction of program machines with registers in [START_REF] Minsky | Computation, Finite and Infinite Machines[END_REF], nowadays best known as Minsky machines, has been motivated by proposing an alternative to Turing machines that is closely related to programs.

i ∈ [1, n], v(x i ) def = x(i) and v(x i ) def = x (i). Given a Presburger counter system C, its transition system T(C) = S, - → is a graph with S = Q × N n and - →⊆ S × S such that q, x , q , x ∈-→ def ⇔ there exists a transition t ∈ δ such that q, x t - → q , x .

Decision problems

In this section, we recall several standard decision problems about Presburger counter systems. They are mainly related to reachability questions (problems related to temporal logics are introduced in Section 4).

Reachability problem:

Input: a Presburger counter system C and configurations q 0 , x 0 and q f , x f . Question: is there a finite run from q 0 , x 0 to q f , x f ?

Control state reachability problem:

Input: a Presburger counter system C, a configuration q 0 , x 0 and a state q f . Question: is there a finite run with initial configuration q 0 , x 0 and whose final configuration has control state q f ? Other verification problems on Presburger counter systems are worth mention, though not discussed herein, including the control state repeated reachability problem and the termination problem.

Some classes of Presburger counter systems

In this section, we introduce classes of Presburger counter systems by restricting the general definition provided above. Additional requirements can be of dis-tinct nature: restriction on syntactic resources (number of counters, etc.), restriction on the control graph (e.g., flatness) and semantical restrictions (reversalboundedness, etc.).

Counter systems. A counter system C = Q, n, δ is a Presburger counter system such that for each transition t = q φ -→ q ∈ δ, φ can be written as φ g ∧φ u , where φ g (guard) is a Boolean combination of atomic formulae of the form t ≤ t built over x 1 , . . . , x n and φ u (update) is a formula of the form i∈[1,n] x i = x i + b(i) where b ∈ Z n . The transition t is also written q φg,b ---→ q . Minsky machines [START_REF] Minsky | Computation, Finite and Infinite Machines[END_REF] are counter systems such that each update can change at most one counter and the guards are restricted to and to zero-tests. The Presburger counter system in Figure 1 is indeed a counter system with the above meaning.

A vector addition system with states [KM69] (VASS for short) is a counter system such that all the transitions are of the form q ,b --→ q . So, a VASS can be represented by a tuple V = Q, n, δ where Q is the finite set of control states and δ is a finite subset of Q × Z n × Q. A famous result states that the reachability problem for VASS is decidable [START_REF] Mayr | An algorithm for the general Petri net reachability problem[END_REF][START_REF] Kosaraju | Decidability of reachability in vector addition systems[END_REF][START_REF] Leroux | The general vector addition system reachability problem by Presburger inductive invariants[END_REF]. It has been the subject of the book [START_REF] Reutenauer | The mathematics of Petri nets[END_REF] and its proof requires many non-trivial steps involving graph theory, logic and theory of well-quasi-orderings. Nevertheless, the exact complexity of the reachability problem is open: we know it is ExpSpacehard [START_REF] Lipton | The reachability problem requires exponential space[END_REF] and no primitive recursive upper bound exists. In [START_REF] Leroux | The general vector addition system reachability problem by Presburger inductive invariants[END_REF], existence of semilinear separators in case of non-reachability in VASS leads to promising developments.

A note to the reader. Counter systems are the main class of Presburger counter systems considered in this document. However, we are aware that the current term might be confusing: when we really want to mean the full class of systems, we will use the more general term 'Presburger counter system.' Reversal-bounded counter systems. In this section, we consider counter systems for which the atomic formulae in guards are of the form t ≤ k or t ≥ k with k ∈ Z and t is of the form i a i x i with the a i 's in Z. There is no real restriction with the class introduced earlier except that we require that atomic formulae occur in a certain way.

A reversal for a counter occurs in the run of some counter system when there is an alternation from nonincreasing mode to nondecreasing mode and vice-versa. Below, we propose a slight generalization from [START_REF] Bersani | The complexity of reversal-bounded modelchecking[END_REF] that captures the notion of reversal-boundedness from [START_REF] Ibarra | Reversal-bounded multicounter machines and their decision problems[END_REF]; reversal-boundedness applies to counters but also to terms occurring in guards. Let C = Q, n, δ be a counter system and T be a finite set of terms including {x 1 , . . . , x n }. From a run ρ = q 0 , x 0 , q 1 , x 1 , . . . of C, in order to describe the behavior of counters and terms varying along ρ, we define a sequence of mode vectors md 0 , md 1 , . . . (of the same length as ρ) such that each md i has profile T → { , }. Intuitively, each value in a mode vector records whether a term is currently in an increasing phase or in an decreasing phase (this includes the counters themselves as in standard reversal-boundedness). Given t = i a i x i and a counter vector x, we write x(t) to denote the integer a i x(i). We are now ready to define the sequence md 0 , md 1 , . . . By convention, md 0 is the constant map . For every j ≥ 0 and t ∈ T, we have md j+1 (t) def = md j (t) when x j (t) = x j+1 (t), md j+1 (t) def = when x j+1 (t) -x j (t) > 0 and md j+1 (t) def = when x j+1 (t) -x j (t) < 0. Let Rev t = {j ∈ [0, len(ρ)-1] : md j (t) = md j+1 (t)}; we say that ρ is r-T-reversal-bounded for some r ≥ 0 def ⇔ for all t ∈ T, card(Rev t ) ≤ r. Given a counter system C, we write T C to denote the set of terms t occurring in atomic formulae of the form t ∼ k with ∼∈ {≤, ≥} augmented with the counters in {x 1 , . . . , x n }. An initialized counter system C, q, x is reversal-bounded def ⇔ there is r ≥ 0 such that every run from q, x is r-T C -reversal-bounded. When T is reduced to {x 1 , . . . , x n }, Treversal-boundedness is equivalent to reversal-boundedness from [START_REF] Ibarra | Reversal-bounded multicounter machines and their decision problems[END_REF]. Note that the counter system in Figure 1 is {x 1 , x 2 }-reversal-bounded from any initial configuration of the form q 1 , x 0 .

Compared to the subclasses considered so far, reversal-bounded counter systems are augmented with an initial configuration so that existence of the bound r is relative to the initial configuration. Secondly, this class is not defined from the class of counter systems by imposing syntactic restrictions but rather semantically. The main property related to reversal-bounded counter systems is the result below.

Theorem 2. [Iba78,BD11] Given a counter system C, r ≥ 0 and control states q, q , one can effectively compute a Presburger formula φ q,q (x 1 , . . . , x n , y 1 , . . . , y n ) such that for all valuations v, we have v |= φ iff there is an r-T C -reversal-bounded run from q, v(x 1 ), . . . , v(x n ) to q , v(y 1 ), . . . , v(y n ) .

So, bounding the number of reversals in runs allows to characterize the reachability sets by computing Presburger formulae. This approach can be generalized to richer models, see e.g., [START_REF] Howell | An analysis of the nonemptiness problem for classes of reversal-bounded multicounter machines[END_REF][START_REF] Finkel | Reversal-bounded counter machines revisited[END_REF][START_REF] Hague | Model checking recursive programs numeric data types[END_REF].

Affine Presburger counter systems. Now, we present the class of affine Presburger counter systems that substantially extends the class of counter systems by allowing any guard that can be defined in (PA) and by giving the possibility to have affine updates. A partial function f from N n to N n is affine def ⇔ 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 def ⇔ the graph of f is a Presburger set (binary relation).

A Presburger counter system C = Q, n, δ is affine when for every transition q φ -→ q ∈ δ, φ is affine and there is a triple φ g , A, b such that φ g (guard) is a formula in (PA) with free variables among x 1 , . . . , x n and φ = { x, x ∈ N 2n : x = Ax + b and x ∈ φ g }. The formula φ g represents the guard of the transition and the pair A, b is the deterministic update function. Such a triple φ g , A, b is called an affine update and we also write φ g , A, b to denote φ . Observe that one can decide whether a Presburger formula φ satisfies that φ is affine [DFGvD10, Proposition 3]. Furthermore, counter systems are affine counter systems in which the only matrix is identity. This class of Presburger counter systems has been introduced in [START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF].

Observe that given t = q φg,A,b ----→ q , there is a Presburger formula ϕ(x, x ) such that for every v, we have

v |= ϕ iff q, v(x 1 ), . . . , v(x n ) t - → q , v(x 1 ), . . . , v(x n ) .
Here is the witness formula that encodes the one-step relation:

φ g (x) ∧ i∈[1,n] (x i = j A(i, j)x j + b(i))
Note that the composition of affine updates is still an affine update.

Presburger counter systems with octagonal constraints. A Presburger counter systems with octagonal constraints is such that for each transition q φ -→ q ∈ δ, the formula φ is a conjunction of atomic formulae of the form ±y ± z ≤ k where y, z are variables among x 1 , . . . , x n , x 1 , . . . , x n , k ∈ Z and ±y stands for either y or -y (same applies for ±z). Constraints of the form ±y ± z ≤ k are called octagons and have been considered in [START_REF] Bozga | Iterating octagons[END_REF]. Note that octagons include constraints of the form y ≤ z + k or y ≤ k considered in [START_REF] Comon | Multiple counter automata, safety analysis and Presburger Arithmetic[END_REF]. Unlike the counter systems, in Presburger counter systems with octagonal constraints the transitions do not necessarily lead to functional updates. Here is an example of formula labelling a transition:

φ = (x 1 + 1 < x 1 ) ∧ (x 2 -3 = x 2 ). In [CJ98],
Presburger counter systems with octagonal constraints with only constraints of the form y ≤ z + k or y ≤ k have been studied and a major result established in [START_REF] Comon | Multiple counter automata, safety analysis and Presburger Arithmetic[END_REF] states that the effect of any loop can be effectively defined in (PA).

Imperfect counter automata. Counter automata are defined as VASS except that we accept also zero-tests on counters as guards. Below, we briefly consider variants of counter automata in which counter values can be decremented without notification (a loss) or counter values can be incremented without notification (a gain) -but not the two possibilities in the same model. A lossy counter automaton is a counter automaton such that for all q ∈ Q and for all i ∈ [1, n], q dec(i) ---→ q (which allows us to simulate losses). The control state reachability problem for lossy counter automata is decidable and actually lossy counter automata form a subclass of lossy channel systems, see e.g. [START_REF] Ph | Verifying lossy channel systems has nonprimitive recursive complexity[END_REF] and the reachability problem for lossy channel systems is decidable [START_REF] Abdulla | Verifying programs with unreliable channels[END_REF][START_REF] Finkel | Well-structured transitions systems everywhere![END_REF]. For instance, they can be used to model lossy channel systems for which the ordering of the messages is not relevant. In that case, each counter can store how many messages of a given type are present in the channel. Lossy counter automata have been introduced in [START_REF] Mayr | Undecidable problems in unreliable computations[END_REF]. Similarly, a gainy counter automaton is a counter automaton such that for all q ∈ Q and for all i ∈ [1, n], q inc(i) --→ q ∈ δ (which allows us to simulate gains). The control state reachability problem for gainy counter automata can be shown decidable by making a correspondence with reset VASS (VASS in which it is possible to reset counter values) but the problem is nonprimitive recursive, see e.g. [START_REF] Ph | Verifying lossy channel systems has nonprimitive recursive complexity[END_REF][START_REF] Ph | Revisiting Ackermann-hardness for lossy counter machines and reset Petri nets[END_REF]. Even though Presburger counter systems with imperfect computations are not further discussed in the paper, they form an interesting class of systems related to many other verification problems.

In order to conclude this section, it is worth noting that there exist plenty of other classes of Presburger counter systems for which reachability problems can be solved by using (PA) (see e.g., subclasses of Petri nets). However, since Presburger counter systems are Turing-complete, designing new (tractable) subclasses remains an ongoing process. In the next sections, we focus on presenting proof techniques to solve reachability problems for some of the classes.

3 Loops, Path Schemas and Flatness

Computing loop effects in (PA)

Let C = Q, n, δ be a Presburger counter system. A path p of C is a finite sequence of transitions from δ corresponding to a path in its control graph. We write first(p) [resp. last(p)] to denote the first [resp. last] control state of a path. A loop l is a non-empty path p such that first(p) = last(p) and we write effect(l) to denote the effect of the loop l defined as below:

{ x, x ∈ N n × N n : first(l), x l - → last(l), x }
Similarly, we write effect <ω (l) to denote the repeated effect of the loop l:

{ x, x ∈ N n × N n : first(l), x l i - → last(l), x , i ≥ 0}
The reachability problem for loops can be then defined as follows: given a loop l from a Presburger counter system C of dimension n and two counter value vectors x 0 , x f in N n , is x 0 , x f ∈ effect <ω (l)? Repeated effect is simply called acceleration in [FL02, Section 3].

Note that even though effect(l) can be defined by a Presburger formula, this does not imply that it is the case for effect <ω (l) too. Indeed, if the binary relation R is Presburger set, then this does not imply that its reflexive and transitive closure R * is a Presburger set too. For instance, if

R = { α, 2α ∈ N 2 : α ∈ N} then R * = { α, 2 β α ∈ N 2 : α, β ∈ N} is not Presburger-definable. By contrast, if S = { α, α + 1 ∈ N 2 : α ∈ N} then S * = { α, β ∈ N 2 : α < β, α, β ∈ N} is a Presburger set.
The question of deciding whether the reflexive and transitive closure of a Presburger-definable binary relation is Presburger-definable is known to be intimately related to the fact that reachability relations from Presburger counter systems are Presburger-definable, which leads to decidability when effectiveness is guaranteed too. Indeed, consider the following loop with q 1 = q k :

q 1 φ1(x1,...,x n ) -------→ q 2 φ2(x1,...,x n ) -------→ • • • φ k-1 (x1,...,x n ) --------→ q k-1 φ k (x1,...,x n ) -------→ q k .
The effect of the loop can be represented by the Presburger formula below:

ψ(x, x ) def = ∃ ȳ1 , . . . , ȳk φ 1 (x, ȳ1 ) ∧ φ 2 ( ȳ1 , ȳ2 ) ∧ • • • ∧ φ k ( ȳk , x )
where x, x , ȳ1 , . . . , ȳk are sequences of variables of length n.

In order to decide the reachability problem on the loop, it is essential to represent symbolically effect <ω (l). The best we can hope for is that effect <ω (l) is a Presburger set. This motivates the definition below.

Definition 3. Given R ⊆ N 2n , we define the counting iteration of R as the relation R CI ⊆ N n × N × N n such that x, i, y ∈ R CI def ⇔ x, y ∈ R i (i compositions of R). R has a Presburger counting iteration if R CI is a Presburger set.
If R has a Presburger counting iteration, then there exists a Presburger formula ϕ(x, z, ȳ) such that ϕ = R CI . Consequently, the relation R * is Presburgerdefinable since ∃ z ϕ = R * . Observe that { α, α + 1 ∈ N 2 : α ∈ N} has a Presburger counter iteration witnessed by a Presburger formula of the form x = x + y.

Definition 4 (The property ( ) of Presburger counter systems). A class of Presburger counter systems is said to satisfy the property ( ) when, for every loop l, effect(l) has the Presburger counting iteration and its Presburger formula is computable.

Note in particular that this means that for every loop l, the set { x, i, x :

first(l), x l i - → last(l), x , i ≥ 0} is
effectively definable by a Presburger formula ϕ l (with 2n + 1 free variables).

Finitary path schemas

A path schema P is a regular expression built over the alphabet of transitions such that its language represents an overapproximation of the set of labels obtained from finite runs following the transitions of P (counter values are ignored). This notion has been extensively used since [START_REF] Fribourg | Proving safety properties of infinite state systems by compilation into Presburger arithmetic[END_REF][START_REF] Fribourg | Petri nets, flat languages and linear arithmetic[END_REF][START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF] and this provides a natural transition since path schemas are made of loops and paths. More precisely, a finitary path schema P is of the form p 1 l * 2 p 3 l * 4 . . . l * k-1 p k where (1) l 2 , . . . , l k-1 are loops and (2) p 1 l 2 p 3 l 4 . . . p k is a path. The length of a path schema, written len(P), is defined as the number of letter occurrences in the regular expression defining the path schema (no substructure sharing). Let Lan(P) denote the set of finite words in δ * which belong to the language defined by P. Note that some elements of Lan(P) may not correspond to any actual run because of constraints on counter values. Finally, we say that a run ρ starting in a configuration q 0 , x 0 respects a path schema P if the sequence of transitions generating ρ belongs to Lan(P).

Path schemas are used as a means to encode the structure of a potentially infinite set of runs. That is why, we will pay a special attention to avoid considering distinct path schemas P and P such that Lan(P) ⊆ Lan(P ). Containment problem for regular expressions is PSpace-complete but co-NP-complete for regular expressions defining bounded languages, see e.g. [START_REF] Hunt | On the equivalence, containment, and covering problems for the regular and context-free languages[END_REF]. Any set Lan(P) defines a bounded language.

That is why, in the following we only consider path schemas such that the loops l are not multiples of smaller loops (i.e., l = (l ) i with i ≥ 2) and no path p contains a loop as a factor (which bounds the length of such paths). Such loops are called simple loops. In the following, such path schemas are called good. It is easy to see that every finite run respects a good path schema.

Lemma 5. When ( ) holds, { x, x : q, x * -→ q , x respects P} is effectively definable by a Presburger formula ϕ P (with 2n free variables).

Effective semilinearity boils down to check that the effect of a loop can be characterized by a formula in Presburger arithmetic (or in any decidable fragment of first-order arithmetic). The above result can be then obtained by adequately composing formulae for the loops and for the finite paths.

By way of example, note that the effect of the self-loop q x =2x --→ q is not definable in Presburger arithmetic since {2 i : i ≥ 0} is not Presburger-definable. By contrast, the effect of the self-loop -----------------→ q for any Presburger formula φ(x 1 , x 2 ) is Presburger-definable since { x, i, x : q, x l i -→ q, x } can be defined with the formula below:

q x 1 =x1+2∧x 2 =x2+3∧φ(x1,x2)
ϕ(x 1 , x 2 , i, x 1 , x 2 ) def = x 1 = x 1 +2i∧x 2 = x 2 +3i∧∀ y (0 ≤ y < i) ⇒ φ(x 1 +2y, x 2 +3y)
Here are concrete classes to apply Lemma 5. Theorem 6.

(I) Presburger counter systems with octagonal constraints enjoy ( ) [START_REF] Bozga | Iterating octagons[END_REF] (see also [START_REF] Comon | Multiple counter automata, safety analysis and Presburger Arithmetic[END_REF] for a substantial result on a subclass). (II) Counter systems enjoy ( ) (folklore result, see e.g. [START_REF] Fribourg | Petri nets, flat languages and linear arithmetic[END_REF][START_REF] Demri | Taming Past LTL and Flat Counter Systems[END_REF]).

An implementation of the transitive closure of octagonal relations is done in the tool FLATA, see e.g., [START_REF] Bozga | Iterating octagons[END_REF].

Flat Presburger counter systems

A Presburger counter system C is flat def ⇔ every control state belongs to at most one simple cycle (i.e., a loop in which each transition occurs at most once). As far as we can judge, the term 'flat' in that sense has been introduced in [FO97, [START_REF] Comon | Multiple counter automata, safety analysis and Presburger Arithmetic[END_REF][START_REF] Fribourg | Petri nets, flat languages and linear arithmetic[END_REF]. The Presburger counter system in Figure 1 is flat.

Lemma 7. Every flat Presburger counter system has a finite number of good path schemas that is at most exponential in its size.

Of course, this is not the only way to get a finite amount of path schemas, for instance when from an initial configuration, termination is guaranteed but here the finite number of path schemas is structurally guaranteed.

Theorem 8. Let C be a class of Presburger counter systems that enjoys ( ). Then, for every flat Presburger counter system from C, the reachability relation Reach C is Presburger-definable. This is at the heart of the decidability results for verifying safety and reachability properties on flat Presburger counter systems from [CJ98,FL02,BIK09] whereas for the verification of temporal properties, it is much more difficult to get sharp complexity characterization, see e.g. [START_REF] Demri | Taming Past LTL and Flat Counter Systems[END_REF].

Corollary 9. Let C be a class of Presburger counter systems that enjoys ( ). The reachability problem for C is decidable.

The corollary can be obtained as follows. Consider the instance C, q 0 , x 0 and q f , x f . We have seen that we can compute the Presburger formula φ that encodes the reachability relation in C. It remains to check satisfiability of the formula

( i=n i=1 (x i = x 0 (i) ∧ x i = x f (i))
) ∧ φ assuming free variables in φ are x 1 , . . . , x n , x 1 , . . . , x n . This can be done thanks to Theorem 1.

Finite monoid property in affine Presburger counter systems

Below, we present a class of affine Presburger counter systems with Presburgerdefinable loop effects even though the class does not necessarily enjoy the property ( ). Given A ∈ Z n×n , let A * be the monoid generated from A with A * = {A i : i ∈ N}. The identity element is naturally the identity matrix A 0 = I. Given a matrix A ∈ Z n×n , checking whether the monoid generated by A is finite, is decidable [START_REF] Mandel | On finite semigroups of matrices[END_REF]. By way of example, with A = 1 0 1 1 , we have

A 2 = 1 0 1 1 1 0 1 1 = 1 0 2 1 A 3 = 1 0 3 1 . . . A m = 1 0 m 1
So A * is not finite. Finiteness of the monoid generated from A is interesting because of the lemma below.

Lemma 10. [BW98,Boi99,FL02] Let R ⊆ N n × N n be a binary relation of dimension n defined by the triple

φ g , A, b such that R = { x, x ∈ N 2n : x = Ax + b and x ∈ φ g }. If A * is finite, then R has a Presburger counting iteration.
It is worth adding that one can also effectively compute the Presburger formula encoding the relation R * . A recent work unifying [CJ98,FL02,BGI09,BIL09] by considering all the families of formulae labelling transitions from these works can be found in [START_REF] Bozga | Fast acceleration of ultimately periodic relations[END_REF].

A loop in an affine counter system has the finite monoid property def ⇔ its corresponding affine update φ g , A, b , possibly obtained by composition of several affine updates, satisfies that A * is finite. Let us introduce below the class of admissible counter systems.

Definition 11. An affine Presburger counter system C is admissible iff 1. there is at most one transition between two control states (always possible as soon as disjunction is allowed in guards), 2. its control graph is flat, 3. each simple loop has the finite monoid property.

The restriction to admissible counter systems mainly takes advantage of Lemma 10 as shown below.

Theorem 12. [START_REF] Finkel | How to compose Presburger accelerations: Applications to broadcast protocols[END_REF] Let C be an admissible Presburger counter system and q, q ∈ Q. One can effectively compute a Presburger formula φ such that for every valuation v, we have v |= φ iff q, v(x 1 ), . . . , v(x n ) * -→ q , v(x 1 ), . . . , v(x n ) .

Flattable Presburger counter systems

As observed in [CJ98,FL02,Ler03,BIL09], flatness is very often essential to get effective semilinear reachability sets (but of course this is not a necessary condition, see e.g. [START_REF] Hopcroft | On the reachability problem for 5-dimensional vector addition systems[END_REF]). However, flat Presburger counter systems are seldom natural in real-life applications. That is why, a relaxed version of flatness has been considered in [FO97,Fri00,LS05,DFGvD10] so that an initialized Presburger counter system C, q 0 , x 0 is flattable whenever there is a partial unfolding of C, q 0 , x 0 that is flat and has the same reachability set as C, q 0 , x 0 . In that way, reachability questions on C, q 0 , x 0 can still be decided even in the absence of flatness. C, q 0 , x 0 is initially flattable [START_REF] Leroux | Flat counter systems are everywhere! In ATVA'05[END_REF] iff there is a a finite set of path schemas such that the configurations reachable from q 0 , x 0 are those reachable by firing the sequences of transitions from one of those path schemas (not every such sequence leads to a run). For instance, reversal-bounded initialized counter systems are initially flattable [START_REF] Leroux | Flat counter systems are everywhere! In ATVA'05[END_REF]. The fact that C, q 0 , x 0 is flattable means that as far as reachability is concerned, a finite set of path schemas captures the full reachability relation. Note that flat counter systems are (structurally) flattable but in general it is non-trivial to compute such a finite set of path schemas, see also Section 5. This problem is also known as the problem of finite good accelerations [FL02, Section 5].

Verifying Temporal Properties

Reachability problems asks for the existence of runs reaching some configuration or control state in some specific way. Often, it is desirable to check how events are temporally organized along a run and to specify such properties temporal logics have been advocated since [START_REF] Pnueli | The temporal logic of programs[END_REF]. Furthermore, we wish to include in the logical language the possibility to express directly constraints between variables of the program, whence giving up the standard abstraction made with propositional variables. When the variables are typed, they may be interpreted in some specific domain like integers, real numbers, strings and so on; reasoning in such theories can be performed thanks to satisfiability modulo theories proof techniques, see e.g., [START_REF] Barrett | Satisfiability Modulo Theories[END_REF] and [START_REF] Ghilardi | Combination methods for satisfiability and model-checking of infinite-state systems[END_REF] in which SMT solvers are used for model-checking infinite-state systems. Hence, a proposition like "x is greater than the next value of y" can be encoded in such extended temporal logics by x > Xy but this time the models are sequences of configurations. This means that each position comes with a control state and a valuation for variables. Hence, the basic idea behind the design of the logic Presburger LTL is to refine the language of atomic formulae and to allow the possibility to compare counter values at successive positions of the run of the counter systems. Similar motivations can be found in the introduction of concrete domains in description logics, that are logic-based formalisms for knowledge representation, see e.g. [START_REF] Lutz | NEXPTIME-complete description logics with concrete domains[END_REF].

Presburger LTL

We define below a version of linear-time temporal logic LTL dedicated to Presburger counter systems in which the atomic formulae are Presburger formulae about counter values, the temporal operators are those of LTL and first-order quantification over natural numbers is allowed, although we shall use it in a restricted way. Similarly, in [START_REF] Manna | Temporal verification of reative systems: safety[END_REF], a mixture of first-order logic and LTL is shown sufficient to precisely state verification problems for the class of reactive systems. We introduce a countable set of integer variables, say VAR p = {y 1 , y 2 , . . .}, for quantification over natural numbers. Elements of VAR p are distinct from the counter variables in VAR = {x 1 , x 2 , . . .} that are free variables, only interpreted by the counter values on configurations. We also consider a countably infinite set Q = {q 1 , q 2 , . . .} of control state symbols. The Presburger LTL formulae are defined as follows:

φ ::= ψ | q | φ ∧ φ | ¬φ | Xφ | φUφ | ∃ y φ,
where ψ is a Presburger formula with free variables in VAR p ∪ VAR from the linear fragment of (PA) and q ∈ Q. The symbols X and U are respectively the classical operators next-time and until from LTL.

The models of Presburger LTL formulae are infinite runs from Presburger counter systems whose set of control states is included in the countable set Q. A model ρ of dimension n for Presburger LTL is an element of (Q × N n ) ω for some finite subset Q ⊆ Q. An environment E is a partial map VAR p → N. The empty environment is denoted by ∅. The satisfiability relation |= is defined as follows between a model ρ of dimension n, a position i ≥ 0, an environment E and a formula in which the free variables are among VAR p ∪ {x 1 , . . . , x n }.

The relation |= E is defined on runs ρ = q 0 , x 0 , . . . , q k , x k , . . . such that:

ρ, i |= E q def ⇔ q = q i , -When ψ is a Presburger formula from the linear fragment with free variables included in VAR p ∪{x 1 , . . . ,

x n }, we have ρ, i |= E ψ def ⇔ v i |= ψ in Presburger arithmetic where v i is a conservative extension of E such that for every j ∈ [1, n], v i (x j ) = x i (j), -ρ, i |= E ¬φ def ⇔ ρ, i |= E φ, -ρ, i |= E φ 1 ∧ φ 2 def ⇔ ρ, i |= E φ 1 and ρ, i |= E φ 2 , -ρ, i |= E Xφ def ⇔ ρ, i + 1 |= E φ, -ρ, i |= E φ 1 Uφ 2 def ⇔ there is j ≥ i such that ρ, j |= E φ 2 and ρ, k |= E φ 1 for all i ≤ k < j. -ρ, i |= E ∃ y φ iff there is a natural number m ∈ N such that ρ, i |= E[y →m] φ.
As usual, we pose Fφ def = Uφ and Gφ def = ¬F¬φ. Semantics with finite runs instead of infinite runs can be defined similarly. A semi-closed formula is an Presburger LTL formula such that no integer variable from VAR p is free. By construction, the counter variables x 1 , . . . , x n are always free and are interpreted as the current counter values. In the decision problems defined below, we only consider semi-closed formulae and therefore there is no need to specify an environment in the statements.

For instance, one can express that the first counter strictly increases at every step: G ∃ y (y = x 1 ∧ X(x 1 > y)). Similarly, the first counter takes a finite number of values along the run can be expressed by ∃ y G(x 1 ≤ y).

Let us start by presenting the satisfiability problem for Presburger LTL:

Input: A Presburger LTL semi-closed formula φ with free counter variables x 1 , . . . , x n . Question: Is there a model ρ

∈ (Q × N n ) of dimension n such that ρ, 0 |= ∅ φ?
Observe that for satisfiability checking, it is not necessary that the model is derived from a Presburger counter system. Let us turn to existential modelchecking problem for Presburger LTL:

Input: A Presburger counter system C = Q, n, δ , an initial configuration q 0 , x 0 and a semi-closed formula φ in Presburger LTL. Question: Is there an infinite run ρ starting at q 0 , x 0 such that ρ, 0 |= ∅ φ?

Temporal logics with Presburger constraints has been developed, for instance, in [BEH95,CC00,BDR03]. Some of them have quite expressive decidable fragments. Undecidability of the existential model-checking problem for Presburger LTL can be shown using the undecidability of the halting problem for Minsky machines, see e.g., [START_REF] H Comon | Flatness is not a weakness[END_REF]. Still, using SMT solvers can be done for checking bounded reachability problems, see e.g., [BFM + 10].

In the rest of this section, we present fragments of Presburger LTL obtained by restricting first-order quantification over natural numbers. First, let us observe that if we restrict ourselves to formulae in which temporal operators are not in the scope of first-order quantification, then we get a fragment of Presburger LTL that is very similar to plain LTL. Indeed, atomic formulae are arithmetical constraints between counter values and they can be understood as high-level propositional variables; whence the automata-based approach for LTL can be easily adapted to this fragment. In that fragment, the arithmetical constraints are only local and in the construction of Büchi automata, the existence of transitions between states depends on the satisfiability status of Presburger formulae. Below, we provide restrictions in which the temporal operators may occur in the scope of first-order quantification.

Comparing successive counter values. Given a Presburger formula ψ(z 1 , . . . , z k ), we shall write ψ(X i1 x j1 , . . . , X i k x j k ) to denote the formula below

(∃ y 1 , . . . , y k X i1 (y 1 = x j1 ) ∧ • • • ∧ X i k (y k = x j k ) ∧ ψ(y 1 , . . . , y k ),
where y 1 , . . . , y k are new variables distinct from the free variables that are present in ψ(z 1 , . . . , z k ). It is easy to see that ψ(X i1 x j1 , . . . , X i k x j k ) is interpreted as the formula ψ(z 1 , . . . , z k ) in which each variable z a takes the value of x ja at the i a th next configuration. For instance, x 1 = Xx 2 specifies that the next value of x 2 is equal to the current value of x 1 . Similarly, G(x 1 = Xx 1 ) states that counter 1 has a constant value along the model. In Section 4.2, we present a simple fragment of Presburger LTL by allowing first-order quantification only for formulae of the form ψ(X i1 x j1 , . . . , X i k x j k ) and Presburger formulae (at the atomic level) are quantifier-free too. It is worth observing that we use 'X' as the next-time temporal operator whereas 'Xx' refers to the value of x at the next position.

Freeze operator. In order to verify properties on Presburger counter systems, we want also to be able to compare counter values. For that, it is possible to define the so-called 'freeze operator' with formulae of the form ↓ j r φ interpreted as ∃ y r (y r = x j ∧ φ) that store counter values. There are counterpart formulae of the form ↑ j r interpreted as y r = x j that perform equality tests. Intuitively, the modality ↓ j r is used to store the value of the counter j into the register r; the atomic formula ↑ j r holds true if the value stored in the register r is equal to the current value of the counter j. The formula G(↓ 1 1 XG¬ ↑ 1 1 ) states that the first counter has distinct values at distinct positions. Freeze operator has been introduced in numerous works, sometimes with different motivations, see e.g. [START_REF] Th | Half-order modal logic: how to prove real-time properties[END_REF][START_REF] Goranko | Temporal logic with reference pointers[END_REF][START_REF] Fitting | Modal logic between propositional and first-order[END_REF][START_REF] Lisitsa | Temporal logic with predicate λ-abstraction[END_REF]. It is also sometimes used implicitly as for the temporal semantics for imperative programs that may use first-order temporal logics, see e.g. [START_REF] Manna | The Temporal Logic of Reactive and Concurrent Systems: Specification[END_REF]. For instance, the statement that the program variable x never decreases below its initial value can be expressed by the formula below that uses a form of freeze operator: ∃y (x = y) ∧ G(x ≥ y). Recent results on satisfiability and model-checking problems can be found in [START_REF] Figueira | Future-looking logics on data words and trees[END_REF][START_REF] Demri | Model checking memoryful lineartime logics over one-counter automata[END_REF].

The logic CLTL with finite window

As mentioned earlier, we shall define the logic CLTL as a strict fragment of Presburger LTL such that first-order quantification at the level of temporal formulae is restricted to macro formulae of the form ψ(X i1 x j1 , . . . , X i k x j k ). Consequently, there is no more quantification over integer variables from VAR p and no variable in VAR p occurs in CLTL formulae. The logic CLTL has atomic formulae from the linear fragment of (PA) except that variables are replaced by expressions of the form X i x where x ∈ VAR is a variable and X i is understood as a sequence of i consecutive symbols X. The expression X i x is interpreted as the value of x at the ith next state. Given a CLTL formula φ, we define its X-length len(φ) X as the maximal number i such that an expression of the form X i x occurs in φ. Intuitively, the X-length defines the size of a frame/window of consecutive states that can be compared. The models of CLTL are pairs of sequences σ = σ 1 , σ 2 such that σ 1 : N → (VAR → N), σ 2 : N → Q for a finite subset Q ⊆ Q. The satisfaction relation is defined as for LTL except at the atomic level:

-σ, i |= q iff σ 2 (i) = q, -σ, i |= ψ(X l1 x 1 , . . . , X ln x n ) iff σ 1 (i + l 1 )(x 1 ), . . . , σ 1 (i + l n )(x n ) ∈ ψ . -σ, i |= Xφ iff σ, i + 1 |= φ, -σ, i |= φUφ iff
there is j ≥ i such that σ, j |= φ and for every i ≤ l < j, we have σ, l |= φ.

As usual, a formula φ ∈ CLTL is satisfiable whenever there exists a model σ such that σ, 0 |= φ. We write CLTL l n to denote the restriction of CLTL to formulae with at most n variables and X-length less or equal to l (below the value ω is used for some syntactic resource when there is no restriction). CLTL 0 denote the fragment in which the arithmetical constraints deal only with current counter values. Note that there is a logspace reduction from the satisfiability problem for CLTL to the satisfiability problem for CLTL ω restricted to formulae of Xlength at most 1 (CLTL 1 ω ), see e.g. [START_REF] Demri | On the freeze quantifier in constraint LTL: decidability and complexity[END_REF]. The proof is done by renaming terms and requires an unbounded amount of variables in CLTL 1

. For instance, the expressions x 1 , . . . , X 3 x 1 are encoded by G(x = Xx ∧ x = Xx ∧ x = Xx 1 ) (assuming that x, x and x are new variables) and each occurrence of Xx 1 [resp. X 2 x 1 , X 3 x 1 ] is replaced by x [resp. x , x ]. For reductions between satisfiability problems, the introduction of new variables is harmless.

The halting problem for Minsky machines can be easily reduced to the satisfiability problem for CLTL or to the existential model-checking problem for CLTL, leading to simple undecidability proofs. In the sequel, we show how to restrict the class of counter systems or the logical language in order to regain decidability.

Given a fragment F of (PA) (not necessarily restricted to the linear fragment as for CLTL), we write CLTL(F) to denote the variant of CLTL in which atomic formulae built over the quantifier-free linear fragment of (PA) are replaced by formulae from F (the definition of the satisfaction relation is update accordingly without significant changes). Similarly, we write CLTL l n (F) (n ≥ 1, l ≥ 0) to denote the restriction of CLTL(F) to formulae such that the variables are among {x 1 , . . . , x n } and the X-length is bounded by l.

Fragment F 0 is defined as follows:

F 0 φ ::= x i < x j | x i = x j | x i ≤ k
where k ∈ N. Fragment F 1 is defined as follows: 1 (F 1 ) or for CLTL 1 2 (F 1 ) is undecidable [START_REF] Demri | The effects of bounding syntactic resources on Presburger LTL[END_REF], see also [START_REF] H Comon | Flatness is not a weakness[END_REF].

F 1 φ ::= x i ∼ x j + d | x i ∼ d where d ∈ Z and ∼∈ {<, >, ≤, ≥, =}. For instance, x 1 = X 8 x 2 + 1 ∈ CLTL 8 2 (F 1 ) and XXX(Xx 1 ≥ 27) ∈ CLTL 1 1 (F 0 ). The logic CLTL defined in [CC00] is precisely CLTL 1 ω (F 1 )

Model-checking linear-time properties

Flat counter systems. Below, we state several recent results about model-checking problems for subclasses of counter systems for which the complexity is relatively low. We recall that guards in counter systems belong to the linear fragment and the updates are in Z n . Theorem 14. [START_REF] Demri | Taming Past LTL and Flat Counter Systems[END_REF] Model-checking flat counter systems with CLTL 0 is NPcomplete (also holds with past-time temporal operators).

The NP upper bound is obtained as follows given a flat counter system with initial configuration q 0 , x 0 and a formula φ in CLTL 0 :

-Guess a good infinitary path schema P from q 0 , x 0 . Infinitary path schemas are of the form

p 1 l * 2 p 3 l * 4 . . . l * k-1 p k l ω k .
-Guess an unfolded path schema P from P by eliminating disjunctions in guards and counter values (but at the cost of adding new atomic propositions). Unfolding a path schema amounts to copying loops a (polynomial) number of times while adding atomic propositions or constraints in guards to guarantee that each visit in a new loop satisfies the same guards. -Build an existential Presburger formula that encodes all the runs respecting P from q 0 , x 0 (all the quantified variables are loop counters). -Guess a run respecting P and check whether it satisfies φ symbolically. Each loop may be visited an exponential number of times, but a stuttering theorem allows the symbolic model-checking algorithm to perform efficiently.

Efficient solvers for quantifier-free (PA) are required to make feasible the above algorithm. By contrast, we get a little higher complexity with linear µ-calculus or first-order logic (FOL).

Theorem 15.

[DDS13] Model-checking flat counter systems with linear µ-calculus or with FOL both with arithmetical constraints is PSpace-complete.

It is unclear what are the counterpart results for flat Presburger counter systems with octagonal constraints.

LTL on VASS.

Structural restrictions seem more efficient to reduce the computational complexity of temporal model-checking. By way of comparison, modelchecking vector addition systems with states with linear µ-linear calculus (without arithmetical constraints) is already ExpSpace-complete [START_REF] Habermehl | On the complexity of the linear-time mu-calculus for Petri nets[END_REF].

Let us present a fragment of Presburger LTL introduced in [Jan90] such that the atomic formulae are either control states or atomic formulae of the form x i ≥ k or ¬(x i ≥ k) with k ∈ N. The temporal logic with fairness TLF is defined as a logic on VASS for which formulae are defined by the grammar

q | x i ≥ k | ¬(x i ≥ k) | φ ∨ φ | φ ∧ φ | GFφ, where q ∈ Q and k ∈ N.
Observe that TLF formulae are not closed under negations and the temporal properties are intersection or union of fairness conditions. Decidability of (existential) model-checking problem for TLF restricted to VASS is established in [START_REF] Jančar | Decidability of a temporal logic problem for Petri nets[END_REF] by reduction into the reachability problem for VASS. Fairness conditions on VASS can be also found in [START_REF] German | Reasoning about systems with many processes[END_REF]. Moreover, it is worth noting that the operator F cannot be expressed in TLF, otherwise undecidability would hold. Indeed, in [START_REF] Howell | Problems concerning fairness and temporal logic for conflict-free petri nets[END_REF] a linear-time temporal logic (on Petri nets) is shown undecidable with the temporal operator F, Boolean connectives and atomic formulae of the form x i ≥ k and "transition t is the next one in the run." Finally, other logical formalisms interpreted on VASS runs can be found in [START_REF] Esparza | On the decidability of model checking for several µ-calculi and Petri nets[END_REF][START_REF] Atig | On Yen's path logic for Petri nets[END_REF][START_REF] Blockelet | Model-checking coverability graphs of vector addition systems[END_REF] where complexity/decidability results are established.

Bounding the number of reversals. Results about model-checking reversal-bounded counter systems with LTL equipped with arithmetical constraints can be found in [START_REF] Bersani | The complexity of reversal-bounded modelchecking[END_REF][START_REF] Hague | Model checking recursive programs numeric data types[END_REF]. Below, we recall the definition for the reversal-bounded model-checking problem (RBMC). Its peculiarity is that the input initialized counter systems are not necessarily reversal-bounded but the input contains an explicit bound r about the maximal number of reversals within a run. Moreover, given a formula φ in CLTL, we write T φ to denote the terms of the form t ∼ k occurring in it. The problem RBMC is defined as follows:

Input: a counter system C, an initial configuration q 0 , x 0 , a formula CLTL φ (with atomic formulae of the form t ∼ k), a bound r ∈ N (in binary), Question: Is there an infinite run ρ from q, x such that ρ, 0 |= φ and ρ is r-T-reversal-bounded with T = T C ∪ T φ ?

The computational complexity for RBMC can be precisely characterized; the upper bound can be obtained by a refined analysis on runs, see e.g. [START_REF] Gurari | The complexity of decision problems for finiteturn multicounter machines[END_REF][START_REF] Bersani | The complexity of reversal-bounded modelchecking[END_REF].

Theorem 16. [BD11,HL11] RBMC is NExpTime-complete.
Actually, one can also establish that global model-checking is possible for RBMC [START_REF] Bersani | The complexity of reversal-bounded modelchecking[END_REF], i.e., the set of initial configurations for which there is a run satisfying a given temporal formula from CLTL is effectively Presburger-definable.

A quick look at a branching-time extension

The logic Presburger LTL is interpreted on linear runs but it is possible to extend it to its CTL version by interpreting the formulae on the underlying transition systems of the Presburger counter systems and by adding quantifications over paths, see e.g. [START_REF] Bozzelli | Branching-time temporal logic extended with Presburger constraints[END_REF][START_REF] Demri | Model-checking CTL * over flat Presburger counter systems[END_REF]. The formulae for Presburger CTL are defined as follows:

φ ::= ψ | q | φ ∧ φ | ¬φ | Xφ | φUφ | A φ | ∃ y φ
where ψ is a Presburger formula with free variables included in VAR p ∪ VAR from the linear fragment and q ∈ Q. Semantics for Presburger CTL is provided via models that are transition systems obtained from Presburger counter systems. Again, the satisfaction relation |= is parameterized by an environment E. Given a Presburger counter system C = Q, n, δ with transition system T(C) = S, -→ , the satisfaction relation |= E is defined at position i of the run as for Presburger LTL except for quantifications over paths: ρ, i |= E A φ def ⇔ for all infinite runs ρ starting at configuration ρ(i), we have ρ , 0 |= E φ. First-order quantification over counter values allows us to state many interesting properties in Presburger CTL such as determinism (for all the configurations reachable from the initial configuration, there is at most one successor configuration):

A G( i∈[1,n] ¬∃y(E X(x i = y) ∧ E X(x i = y))) ∧ ( q∈Q ¬(E Xq ∧ E X¬q)).
Similarly, boundedness (the set of configurations reachable from the initial configuration is finite) can be stated with ∃y,

y A G i∈[1,n] y ≤ x i ≤ y .
Model-checking problem for Presburger CTL is defined as follows: given a Presburger counter system C with transition system T(C) = S, -→ , an initial configuration q 0 , x 0 , and a semi-closed formula φ from Presburger CTL , determine whether for every run ρ from q 0 , x 0 , we have ρ, 0 |= φ.

Theorem 17. [START_REF] Demri | Model-checking CTL * over flat Presburger counter systems[END_REF] Model-checking admissible Presburger counter systems with Presburger CTL is decidable.

The proof provides a reduction into satisfiability in (PA) by encoding the runs by tuples of natural numbers. Indeed, every admissible Presburger counter system is flat and therefore it has a finite amount of good path schemas. Runs respecting a path schema can be encoded as tuples of natural numbers by counting how many times the loops are visited. Temporal formulae are then encoded by internalizing the semantics into (PA) itself. Other decidability and complexity results can be found in [START_REF] Bozzelli | Verification of gap-order constraint abstractions of counter systems[END_REF][START_REF] Carapelle | Satisfiability of CTL * with constraints[END_REF]. Nevertheless, it remains open whether modal µ-calculus (with atomic arithmetical constraints on counter values) can be shown decidable on admissible Presburger counter systems.

Path Schema Enumeration

In this section, we explain the interest of designing algorithms for the enumeration of finitary path schemas and how to prune the search space by subsumption. We present a preliminary version of an algorithm for enumerating path schemas. More details and developments will be provided in a forthcoming paper. Only finitary path schemas are discussed in this section but infinitary ones could be generated in a similar way. Moreover, we assume that we are dealing with a class of Presburger counter systems satisfying the property ( ), recalling Definition 4 on page 10, such as the class of counter systems where the guards are Boolean combinations of linear constraints and the updates in Z n are those from VASS.

Why path schema enumeration?

As is well-known, Presburger counter systems are Turing-complete and it is undecidable to check the existence of a run satisfying a given property (even for very basic ones). However, approximating the Presburger counter systems by looking at a subclass of runs provides a means to produce answers in some cases. For example, a finite set of path schemas is a simple way to represent a (potentially) infinite set of runs. Being able to generate path schemas in a structured and controlled fashion while using structural properties of the control graph as well as arithmetical constraints of counter values will be helpful to test the existence of runs satisfying some property.

A wish list for generating path schemas. Even though it is not difficult to generate path schemas in a fair and complete way by tracing the transitions, the details of the enumeration are quite important but often underestimated, see e.g.. [START_REF] Bardin | Flat acceleration in symbolic model checking[END_REF][START_REF] Demri | Model-checking CTL * over flat Presburger counter systems[END_REF] (see some exception in [START_REF] Leroux | Algorithmique de la vérification des systèmes à compteurs. Approximation et accélération. Implémentation de l[END_REF]). First, we want an enumeration strategy that is efficient in practice. Previous work has left open the question of efficient enumeration of path schemas, as the results have been of a theoretical nature, and path schemas didn't have to be enumerated explicitly. Second, we want an enumeration strategy that will find a finite set of path schemas that fully captures the behavior of a Presburger counter system, if possible. As noted earlier, some classes of Presburger counter systems are known to have a finite number of good path schemas. For flat Presburger counter systems, the number of good path schemas is exponential in the size of the control graph whereas for flattable initialized Presburger counter systems, the number of path schemas is finite but with no specific bound on this number. Finally, we want an enumeration strategy in which we have a clear way of detecting whether we have enumerated sufficiently many path schemas to capture the behavior of the Presburger counter system.

Enumerating path schemas can also be viewed as a way to underapproximate the set of runs; this is similar to a standard approach to consider subclasses of runs by bounding some features and to search for 'bounded runs' that may satisfy a desirable or undesirable property. Examples include reversal-bounded counter machines (which have a bound on the number of reversals) [HR87,BD11,HL11], context-bounded model-checking (where there is a bound on the number of context switches) [START_REF] Qaader | Context-bounded model checking of concurrent software[END_REF], and of course bounded model-checking (BMC) (where there is a bound on the distance of the reached positions), see e.g. [BCC + 03].

Pruning the search space: path schema subsumption

Let C = Q, n, δ be a Presburger counter system and P 1 , . . . , P N , P be finitary path schemas such that first(P 1 ) = • • • = first(P N ) = first(P) and last(P 1 ) = • • • = last(P N ) = last(P), i.e., all the path schemas start and end by the same control states. One can think of P 1 , . . . , P N as the path schemas already in our database whereas P is a new path schema for which we have to decide whether we keep it or not. Such a path schema P must be consistent, i.e., there exists a finite run that respects it. The path schema P is consistent w.r.t. the initial condition φ init (y 1 , . . . , y n ) iff the formula ∃ x 1 , . . . , x n ∃ x 1 , . . . , x n φ init (x 1 , . . . , x n ) ∧ ϕ P (x 1 , . . . , x n , x 1 , . . . , x n ) is valid. Then, comes subsumption. The set {P 1 , . . . , P N } subsumes P w.r.t. the initial condition φ init (y 1 , . . . , y n ) (and with respect to reachability) def ⇔ the formula below is valid:

∀ x 1 , . . . , x n ∀ x 1 , . . . , x n (φ init (x 1 , . . . , x n ) ∧ ϕ P (x 1 , . . . , x n , x 1 , . . . , x n )) ⇒ i∈[1,N ] ∃ z 1 , . . . , z n φ init (z 1 , . . . , z n ) ∧ ϕ Pi (z 1 , . . . , z n , x 1 , . . . , x n )
For the class of counter systems, the consistency problem is NP-complete, and the subsumption problem can be expressed in the fragment of (PA) with at most one quantifier alternation. The above subsumption notion can be also formulated as follows. A path schema P enriched with φ init (y 1 , . . . , y n ) defines a set of finite runs such that the initial counter values satisfy φ init (y 1 , . . . , y n ) and the run respects P. Moreover, such a pair defines a set of counter values-those that have been reached at the end of the runs, say [P] φinit def = {x f : q 0 , x 0 * -→ q f , x f respects P and φ init (x 0 )}. Counter values are therefore extracted from runs. Now, subsumption can be formulated as follows:

[P] φinit ⊆ [P 1 ] φinit ∪ • • • ∪ [P N ] φinit .
There exist other means to extract witness counter values from runs. A pattern φ pat is a formula from Presburger LTL without first-order quantification (see Section 4) and with free occurrences of the integer variables y 1 , . . . . y α that are therefore interpreted rigidly. By way of example, we consider the version of Presburger LTL on finite runs. Let us define the set of tuples [P] φpat,φinit obtained by extracting the parameter values from runs respecting P and whose initial configuration satisfies φ init (see the semantics in Section 4):

[P] φpat,φinit def = {E : ρ = q 0 , x 0 * - → q f , x f respects P, φ init (x 0 ) & ρ, 0 |= E φ pat } Note that [P] φinit above corresponds to [P] φpat,φinit with φ pat def = F(x 1 = y 1 ∧ • • • ∧ x n = y n ∧ ¬X )
Let us define the generalized path schema subsumption problem: {P 1 , . . . , P N } subsumes P with respect to the initial condition φ init (y 1 , . . . , y n ) and the property/pattern φ pat

def ⇔ [P] φpat,φinit ⊆ [P 1 ] φpat,φinit ∪ • • • ∪ [P N ] φpat,
φinit (of course, a Presburger counter system is also part of the instance).

Lemma 18. For any class of Presburger counter systems satisfying ( ), there is a reduction from the generalized path schema subsumption problem to the validity problem for (PA).

The proof consists in encoding the runs satisfying a path schema by tuples and then to use the standard translation from LTL to first-order logic. The initial condition φ init and atomic formulae in PLTL formulae are already Presburger formulae, so do not require special treatment in the translation process.

How to deal with quantifiers

Note that Presburger formulae built to perform subsumption tests contain quantifiers. Most well-known Satisfiability Modulo Theories (SMT) solvers can deal with quantifier-free formulae, also known as linear arithmetic (LIA). For instance, this includes Z3 [START_REF] De Moura | Z3: An Efficient SMT Solver[END_REF], CVC4 [BCD + 11], and Alt-Ergo [START_REF] Conchon | SMT Techniques and their Applications: from Alt-Ergo to Cubicle[END_REF], to cite a few of them; see also Pugh's Omega test [START_REF] Pugh | A practical algorithm for exact array dependence analysis[END_REF]. However, as observed earlier, dealing with quantifiers is usually a difficult task for SMT solvers. Fortunately, quantifiers can be eliminated but this may be expensive computationally. Cooper's elimination procedure [START_REF] Cooper | Theorem proving in arithmetic without multiplication[END_REF], when considering ∃ x ψ with quantifier-free ψ, does not assume that ψ is in disjunctive normal form (a disjunction of conjuncts, with conjuncts made of literals). This is a remarkable difference with the original algorithm presented 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]. Indeed, transforming a propositional formula into an equivalent formula in disjunctive normal form may cause an exponential blow-up. A more advanced improvement of Cooper's procedure can be found in [START_REF] Reddy | Presburger arithmetic with bounded quantifier alternation[END_REF]; recent developments propose a lazy approach to quantifier elimination [START_REF] Monniaux | Quantifier elimination by lazy model enumeration[END_REF].

An algorithm that builds cycle schemas and path schemas

In this section, we present an algorithm to generate path schemas from a Presburger counter system. It proceeds by building path schemas of larger and larger sizes. An outer loop ensures that all path schemas of some constant size k -1 have been built before the generation of path schemas of size k is attempted. The algorithm is inherently iterative, and its first k iterations enumerate all path schemas of size less than or equal to k.

Path schemas are generated by building upon smaller path schemas. Given a path schema of size k -1, the algorithm extends it by adding a transition; the result is a new path schema of size k. Path schemas may also be extended by cycles, and for this, the algorithm detects and maintains cycle schemas (see below). These cycle schemas are detected by using smaller path schemas.

Preliminary definitions: cycle schemas and suffixes. A cycle schema L is a path schema starting and ending by the same control state. The set of cycles generated by a cycle schema L is precisely Lan(L). We write Lan (L) to denote the smallest set of paths such that Lan(L) ⊆ Lan (L) and if

t 1 • • • t α ∈ Lan (L), then t 2 • • • t α t 1 ∈ Lan (L).
The set Lan (L) can be also obtained from Lan(L) by considering all possible rotations of loops.

Path schemas can be concatenated assuming that constraints on control states are respected. Let P = P 1 • P 2 be a path schema obtained by concatenating two path schemas such that (1) P 2 starts by q and is of length at least one, (2) P 2 ends by q, (3) there is a transition t = q φ -→ q . Obviously, P 2 • t is a cycle schema. P 2 is called a suffix of P. Similarly, let P = P 1 • (l) * • P 2 be a path schema with l = p 1 • p 2 , such that (1) p 2 starts by q , (2) P 2 ends by q, (3) there is a transition t = q φ -→ q . Obviously, p 2 • (l) * • P 2 • t is another cycle schema. p 2 • (l) * • P 2 is called an augmented suffix of P. By definition, an augmented suffix is any suffix obtained in one of the two above-mentioned ways. A simple suffix is a suffix without a loop, i.e., a non-empty sequence of transitions being the suffix of a path schema. ps-complexity. A path p ∈ δ * has ps-complexity k def ⇔ there is a path schema P of length k such that p ∈ Lan(P) and no path schema P of strictly smaller size verifies p ∈ Lan(P ). In a sense, the ps-complexity of a path measures how concisely the path can be represented with the help of path schemas generated from the Presburger counter system. Similarly, a run ρ has ps-complexity k def ⇔ there is a path schema P of length k such that ρ respects P and for no path schema P of strictly smaller size, ρ respects P . The relative length of a loop l with respect to control state q 0 is equal to the length of l plus the minimal distance between the initial control state q 0 and a control state occurring in l (can be infinite, can be equal to the length of l if q 0 occurs in l). Again, no constraints about counter values are involved at this stage. Subsumption test. Our algorithm is parameterized by a subsumption test. When a path schema is subsumed by the set of path schemas previously discovered, it is not itself enumerated. This leads to less redundant results, and to less work being done by the algorithm at larger k. It also leads to an easy termination test: during a level k, if no new path schemas are enumerated, then the algorithm has already enumerated a finite set of path schemas that "capture" the behavior of the system (w.r.t. the subsumption test). The input is a Presburger counter system C, with initial state q 0 and initial condition φ init (x 1 , . . . , x n ). The input contains a path schema eligibility test (called test) so that PS (k) test ←-P is a shorthand for: if test(φ init , P, PS + (k)) then PS (k) ←-PS (k) ∪ {P}. When the test returns true, a new path schema is included in PS (k) (typically by performing a subsumption check). The output of the algorithm is PS + (k).

1. PS (0) is initialized to the empty path schema starting at control state q 0 2. k ←-1 3. while PS + (k -1) = ∅ do (a) for each P ∈ PS + (k -1) and t ∈ δ s. Properties of the algorithm. The algorithm has several nice properties such as being parameterized by an eligibility test and it produces only good path schemas (see line 3(a)(i)). It is natural to wonder about the purpose of the eligibility test. Whenever a new path schema is built by the algorithm, we do not systematically insert it in the working set of path schemas (represented by PS (k) or PS + (k)). Indeed, it may happen that there is no run that respects it when starting by the initial control state q 0 and when satisfying the initial constraint on counter values. In that case, there is no point to include it in the working set of path schemas. When path schemas are generated with the purpose to abstract a potentially infinite set of runs, only consistent path schemas are inserted. Similarly, a new path schema may be subsumed by the working set of path schemas and if the property to be checked on runs can be safely pruned, such a new path schema can be discarded. The eligibility test allows to parameterize the algorithm by any kind of Boolean function to test whether a new path schema can be inserted or not. On the other hand, it might be useful to enumerate path schemas regardless the arithmetical constraints on counter values, which corresponds to consider the algorithm when the test always returns true. Consequently, the eligibility test provides a means to eliminate new path schemas depending on the purpose of the path schema generation.

Theorem 19 below states that the algorithm generates all the cycle schemas and path schemas when constraints on counter values are ignored. A nice way to ignore such values is to assume that the test returns always true, which amounts also to view the counter system as a standard labelled transition system.

Theorem 19 (Completeness). Consider the algorithm in which the main test returns true. After completing the kth step of the main while loop:

( †) For every loop l of relative length at most k, there is a cycle schema L ∈ CS + (k) such that l ∈ Lan (L). ( † †) For every path p starting at control state q 0 of ps-complexity at most k, there is a path schema P ∈ PS + (k) such that p ∈ Lan(P).

With subsumption on counter values, a complete version of the algorithm can be obtained if cycles are generated independently of cycle schemas. At the time of writing this paper, we have designed such an algorithm, based on the one presented above. If cycle schemas are used to generate cycles during the course of the algorithm, then the enumeration procedure is known to be incomplete in the sense of case ( † †) in Theorem 19; that is, some path schemas may be missed at step k that are necessary to describe a path of ps-complexity k. However, this does not prevent us from using this algorithm for certain applications where completeness is less important, as useful path schemas might still be generated. Implementation and tests will be part of future work. desirable property to provide decision procedures on such machines, it is not sufficient if model-checking temporal properties are required; indeed, we may need to specify how intermediate configurations occur (see e.g. [START_REF] Demri | Taming Past LTL and Flat Counter Systems[END_REF]). For instance, the exact complexity of model-checking temporal properties for flat admissible Presburger counter systems is still open.

We have recalled several results from the literature and we emphasize that the generation of path schemas is a key problem for formal verification of Presburger counter systems. This is not really new (see e.g. [FO97,Boi99,Ler03,LS05]) but it is becoming an important issue, at least as important as the design of optimal decision procedures as far as worst-case complexity is concerned. The paper has been designed to put some light on this problem. However, an efficient generation of path schemas means that redundant path schemas should be eliminated as early as possible in the enumeration process. A comparison with the algorithm for acceleration technique in FAST [START_REF] Leroux | Algorithmique de la vérification des systèmes à compteurs. Approximation et accélération. Implémentation de l[END_REF] or LASH [START_REF] Boigelot | Symbolic methods for exploring infinite state spaces[END_REF] will be in order.

We have introduced the notion of subsumption to take care of redundancy and again subsumption can be checked by testing the satisfiability of a quantified Presburger formula. This is a real challenge to deal with such quantified formulae in the framework of path schemas enumeration since most SMT solvers do not behave so nicely with quantified formulae, see e.g. [dMB08,BCD + 11]. Part of our future work is dedicated to design a path schema generation algorithm that invokes SMT solvers for quantified Presburger formulae.

Fig. 1 .

 1 Fig. 1. A Presburger counter system

.

  By way of example, let us quote a few interesting results. Theorem 13. (I) Satisfiability problem for CLTL(F 0 ) is PSpace-complete, see e.g. [DD07,DG08,ST11]. (II) Satisfiability problem for CLTL 1 1 (F 1 ) is PSpacecomplete [DG09]. (III) Satisfiability problem for CLTL 2

  The algorithm. Below, we present the algorithm in which PS (k) is the set of path schemas of size k discovered. CS (k) is the set of cycle schemas discovered with relative length k. We write PS + (k)def = k ≤k PS (k ) and CS + (k) def = k ≤k CS (k ).

  t. first(t) = last(P) do { look for path schemas ending with a transition } i. if there exists no simple suffix S of P • t s.t. first(S) = last(S) then PS (k) P • t { add path schema P • t to level k } ii. for each augmented suffix S of P s.t. first(S • t) = last(S • t) do { add cycle schema S • t to level len(S • t) } CS (len(S • t)) ←-CS (len(S • t)) ∪ {S • t} (b) { add path schemas ending with a cycle } for each L ∈ CS + (k) and prime cycle l ∈ Lan (L) s.t. len(l) ≤ k do for each P ∈ PS (k -len(l)) s.t. last(P) = first(l) do PS (k) P • l { add P • l to level k } (c) k ←-k + 1; endwhile 4. return PS + (k)

test ←test ←-

ConclusionIn this paper, we have recalled several classes of Presburger counter systems for which reachability sets are computable Presburger sets. Though this is a

Acknowledgements: The second author thanks the colleagues involved in fruitful collaborations about Presburger counter systems along the years; including members of the ANR Project REACHARD, R. Lazić (Warwick University), A. Dhar and A. Sangnier (LIAFA), and members of the ACSys group at NYU.

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


Patrice Salzenstein
email: patrice.salzenstein@femto-st.fr

Nathalie Cholley

Mikhail Zarubin

Ekaterina Pavlyuchenko

Abdelhamid Hmima

Yanne K Chembo

Laurent Larger

Optoelectronic phase noise system designed for microwaves photonics sources measurements in metrology application

Keywords: Optoelectronic, phase noise, metrology, X-band, microwaves, photonic delay line, Calibration Metrology capabilities

The performance advances in communication systems like Radar system, precision navigation, space application and time and frequency metrology require more stable frequency and low phase noise system. Here is presented a configuration of phase noise measurement system operating in X-band using a photonic delay line as a frequency discriminator. This system doesn't need any excellent frequency reference and works for any frequency between 8.2 and 12.4 GHz. Using cross correlation on 500 averages, noise floor of the instrument is respectively -150 and -170 dBc/Hz at 10 1 and 10 4 Hz from the 10 GHz carrier (-90 and -170 dBc/Hz including 2 km delay lines). This instrument is developed in the context of association with the national french metrology institute (laboratoire national de métrologie et d'essais, LNE). This calibration system is to be integrated in measurements means of the accredited laboratory to improve the Calibration Metrology Capabilities (CMC) of the LNE.

INTRODUCTION

Radio frequency [START_REF] Salzenstein | Significant step in ultra high stability quartz crystal oscillators[END_REF][START_REF] Salzenstein | Frequency stability measurements of ultra-stable BVA resonators and oscillators[END_REF][START_REF] Kuna | Lowest Flicker-Frequency Floor Measured on BVA Oscillators[END_REF] or microwaves oscillators or optoelectronic oscillators with fiber delay line [START_REF] Yao | High frequency optical subcarrier generator[END_REF][START_REF] Ilchenko | High-Q microsphere cavity for laser stabilization and optoelectronic microwave oscillator[END_REF] and their further development with optical resonators [START_REF] Volyanskiy | Compact Optoelectronic Microwave Oscillators using Ultra-High Q Whispering Gallery Mode Disk-Resonators and Phase Modulation[END_REF][START_REF] Tavernier | Magnesium Fluoride Whispering Gallery Mode Disk-Resonators for Microwave Photonics Applications[END_REF][START_REF] Salzenstein | Optical mini-disk resonator integrated into a compact optoelectronic oscillator[END_REF][START_REF] Schliesser | Cavity Optomechanics with Whispering-Gallery Mode Optical Micro-Resonators[END_REF], and cryogenic sapphire oscillators [START_REF] Benmessai | Amplification process in a high-Q cryogenic whispering gallery mode sapphire Fe3+ maser[END_REF] can all present interesting performances with ultra-stable signals in short term domain characterized by a low phase noise. A convenient method is to lock the oscillator to be measured on a reference standard [START_REF] Walls | Suppressed carrier based PM and AM noise measurement techniques[END_REF][START_REF]A Phase Noise Measurement System Application[END_REF][START_REF] Salzenstein | Realization of a Phase Noise Measurement Bench Using Cross Correlation and Double Optical Delay Line[END_REF]]. However it is only possible to determine the phase noise for oscillators compared to another one with the same frequency if noise is expected to be better than a synthesizer. That's why there is a need to develop methods based on the use of two delay lines and cross correlation to be able to characterize an oscillator without referring to another one with the same delivered frequency. In this short paper is presented the development made on an instrument dedicated to such measurement for metrology applications.

BASIC CONCEPTS

A quasi-perfect RF-microwave sinusoidal signal can be written as :

υ(t) = V0 [1 + α(t)] cos (2πν 0 t + φ(t)) (1)
where V 0 is the amplitude, ν 0 is the frequency, α(t) is the fractional amplitude fluctuation, and φ(t) is the phase fluctuation. Equation (1) defines α(t) and φ(t) in low noise conditions: |α(t))| <<1 and |φ(t)| <<1.

Short-term instabilities of signal are usually characterized in terms of the single sideband noise spectral density PSD S(f). S is typically expressed in units of decibels below the carrier per hertz (dBc/Hz) and is defined as the ratio between the one-side-band noise power in 1 Hz bandwidth and the carrier power:

£(f) = ½ S φ (f) (2)
This definition includes the effect of both amplitude and phase fluctuations. However, the amplitude and phase noise have to be known separately because they act differently in the circuit. For example, the effect of amplitude noise can be reduced by amplitude limiting mechanism and mainly suppressed by using a saturated amplifier. Phase noise of microwave oscillators can usually be characterized by heterodyne measurement. Whereas, for such a system, we need a reference oscillator operating exactly at the frequency of the device under test (DUT) with lower phase noise. Any reference is required for homodyne measurement with delay line discriminator [START_REF] Salzenstein | Realization of a Phase Noise Measurement Bench Using Cross Correlation and Double Optical Delay Line[END_REF][START_REF] Volyanskiy | Applications of the optical fiber to the generation and to the measurement of low-phase-noise microwave signals[END_REF][START_REF] Gum | Guide to the Expression of Uncertainty in Measurement, fundamental reference document[END_REF]. At microwave frequencies electrical delay is not suitable because of its high losses. However photonic delay line offers high delay and low attenuation equal to 0.2 dB/km at λ=1.55 μm.

Optoelectronic phase noise measurement system [START_REF] Salzenstein | Realization of a Phase Noise Measurement Bench Using Cross Correlation and Double Optical Delay Line[END_REF][START_REF] Volyanskiy | Applications of the optical fiber to the generation and to the measurement of low-phase-noise microwave signals[END_REF][START_REF] Gum | Guide to the Expression of Uncertainty in Measurement, fundamental reference document[END_REF] is schematically represented on The oscillator frequency fluctuation is converted to phase frequency fluctuation through the delay line. If the mixer voltage gain coefficient is K φ (volts/radian), then mixer output rms voltage can be expressed as [START_REF] Volyanskiy | Applications of the optical fiber to the generation and to the measurement of low-phase-noise microwave signals[END_REF] :

V² out (f) = K² φ .│H φ (jf)│².S φ (f) (3)
Where │H φ (jf)│² = 4 sin²(πfτ ) is the transfer function of optical delay line, and f is the offset frequency from the microwave carrier. The Eq. ( 3) shows that the sensitivity of the bench depends directly on K² φ and │H φ (jf)│. The first is related to the mixer and the second essentially depends on the delay τ . The maximum measurement bandwidth is practically set to 0.95/τ [START_REF] Volyanskiy | Applications of the optical fiber to the generation and to the measurement of low-phase-noise microwave signals[END_REF] , so the choice of an appropriate delay is so important. Several measurements [START_REF] Volyanskiy | Applications of the optical fiber to the generation and to the measurement of low-phase-noise microwave signals[END_REF] shows that τ = 10μs give a good agreement between bandwidth and sensitivity.

In practice, an FFT analyzer is needed to measure the spectral density of noise amplitude V² out (f)/B, where B is the bandwidth used to calculate V out (f)/B. The phase noise of the DUT is finally defined by Eq. ( 4) and taking into count the gain of DC amplifier G DC as :

( 4 )

RESULTS AND INTERPRETATION

The measured phase noise includes the DUT noise and the instrument background. The cross correlation method allows to decrease the cross spectrum terms of uncommon phase noise as √(1/m), where m is the average number. Thereby uncorrelated noise is removed [START_REF] Salzenstein | Realization of a Phase Noise Measurement Bench Using Cross Correlation and Double Optical Delay Line[END_REF][START_REF] Volyanskiy | Applications of the optical fiber to the generation and to the measurement of low-phase-noise microwave signals[END_REF] and sensitivity of measure is improved.

To validate the measure of our phase noise bench, we need to compare datasheet of the commercial frequency synthesizer Anritsu/Wiltron 69000B with the phase noise we measure using our system. The Fig. 3 shows the result of this measure. We can see that our bandwidth is limited to 100 kHz (τ = 10 μs) and the measured phase noise corresponds to the datasheet on Fig. 2. Fig. 4 represents the background phase noise of the bench after performing 500 averaged with cross-correlation method, when removing the 2 km optical delay line. In this case, phase noise of the 10 GHz synthesizer is rejected. The solide curve shows noise floor (without optical transfer function) respectively better than -150 and -170 dBc/Hz at 101 and 104 Hz from the 10 GHz carrier. Dotted curve is the noise floor when optical fiber is introduced.

EVALUATION OF THE UNCERTAINTY

There are two categories of uncertainties terms [START_REF] Gum | Guide to the Expression of Uncertainty in Measurement, fundamental reference document[END_REF] : the first category is called "type A", statistic contribution such as reproducibility, repeatability, special consideration about Fast Fourier Transform analysis, and the experimental standard deviation. Second family of uncertainties contributions is "type B" and due to various components and temperature control, but also to the asymmetry of the instrument. Experience with or general knowledge of the behavior and properties of relevant materials and instruments, manufacturer's specifications, data provided in calibration and other certificates, uncertainties assigned to reference data taken from handbooks. By the way, uncertainty on £(f) strongly depends on propagation of uncertainties through the transfer function as deduced from equation ( 4). Global uncertainty is strongly related to repeatability of the measurements. Repeatability is the variation in measurements obtained by one person on the same item and under the same conditions. Repeatability conditions include: the same measurement procedure, the same observer, the same measuring instrument, used under the same conditions, repetition over a short period of time, the same location. We switch on all the components of the instrument and perform a measurement keeping the data of the curve. Then we need to switch them off and switch them on again to obtain another curve. We must repeat this action several times until we have ten curves. Elementary term of uncertainty for repeatability is found to be equal to 0.68 dB. Other elementary terms still have lower contributions. For instance, temperature effects, resolution of instruments or uncertainty on the determination of the coefficient K φ are lower. Its leads to a global uncertainty of 1.58 dB [START_REF] Pavlyuchenko | Uncertainty budget on optoelectronic phase noise measurement bench[END_REF].

CONCLUSION

Performances and first consideration about estimation of the uncertainty was a bit detailed in this paper to show the main advantage of the instrument developed for metrology applications. With high performance better than -150 dBc/Hz at 10 Hz from the 10 GHz carrier, integration in the mean of the accredited laboratory is expected and the new field of capabilities in terms of calibration of single source in X-band will be soon achieved in order to extend the CMC of the LNE.

Fig. 1 .

 1 It consists on two equal and fully independent channels. The phase noise of the oscillator is determined by comparing phase of the transmitted signal to a delayed replica through optical delay using a mixer. It converts the phase fluctuations into voltage fluctuations. An elecro-optic modulator allows modulation of the optical carrier at microwave frequency. The lenght of the short branch where microwave signal is propagating is negligible compared to the optical delay line. Mixers are used as phase detectors with both saturate inputs in order to reduce the amplitude noise contribution. The low pass filters are used to eliminate high frequency contribution of the mixer output signal. DC amplifiers are low flicker noise.

Figure 1 .

 1 Figure 1. Phase noise bench.

Figure 2 .

 2 Figure 2. Datasheet of 10 GHz phase noise of commercial Anritsu 69000B series synthesizer.

Figure 3 .

 3 Figure 3. Phase noise of the commercial synthesizer measured with our bench with K φ = 425 mV/rad and G DC = 40 dB.

Figure 4 .

 4 Figure 4. Phase noise floor of the bench measured with Anritsu synthesizer (500 averages).

ACKNOWLEDGEMENTS

This work was partly supported by the Laboratoire National de Métrologie et d'Essais (LNE) under contract number LNE/DRST 10 7 002.