Olivier Raimond

Bruno Schapira
email: bruno.schapira@math.u-psud.fr

INTERNAL DLA GENERATED BY COOKIE RANDOM WALKS ON Z

We prove a law of large numbers for the right boundary in the model of internal DLA generated by cookie random walks in dimension one. The proof is based on stochastic algorithms techniques.

Introduction

The model of Internal DLA (internal diffusion limited aggregation) on Z d is a basic example of cluster growth model, which has the Euclidean ball as limiting shape, and for which we have now very good control (presumably sharp) on the size of the fluctuations around this limiting shape.

It was introduced, on a mathematical level at least, by Diaconis and Fulton [START_REF] Diaconis | A growth model, a game, an algebra, Lagrange inversion, and characteristic classes[END_REF] in dimension one. In this case the cluster at any time is an interval, and the analysis of its extremities can be transposed in terms of Polya's urn, for which we know that the law of large numbers and the central limit theorem hold. In particular fluctuations around the mean value are diffusive.

In dimension larger than or equal to 2 it has been first studied by Bramson, Griffeath and Lawler [START_REF] Bramson | Internal diffusion limited aggregation[END_REF] who proved that the limiting shape is the Euclidean ball and that fluctuations are sublinear. Two years later Lawler [START_REF] Lawler | Subdiffusive fluctuations for internal diffusion limited aggregation[END_REF] showed that fluctuations are subdiffusive (with an upper bound in n 1/3 ). Finally very recently Jerison, Levine and Sheffield [START_REF] Jerison | Logarithmic fluctuations for internal DLA[END_REF][START_REF] Jerison | Internal DLA in higher dimensions[END_REF][START_REF] Jerison | Internal DLA and the Gaussian free field[END_REF], and independently Asselah and Gaudillière [START_REF] Asselah | From logarithmic to subdiffusive polynomial fluctuations for internal DLA and related growth models[END_REF][START_REF] Asselah | Sub-logarithmic fluctuations for internal DLA[END_REF] have obtained a bound in ln n in dimension 2 and in √ ln n in dimension larger than or equal to 3, which agrees with computer simulations.

In its simplest form the model is defined as follows. First at time 0, the cluster A(0) is empty. Next if the cluster at time n is some subset A(n) of Z d , run a simple random walk and stop it when it first exit A(n). Then A(n + 1) is the union of A(n) and the site where this random walk stopped. A lot of relevant variations on this model can be imagined. For instance Levine and Peres [START_REF] Levine | Scaling limits for internal aggregation models with multiple sources[END_REF] assume that random walks can start from different sources (not only the origin). Another natural modification is to change the underlying graph. For instance Blachère and Brofferio [START_REF] Blachère | Internal diffusion limited aggregation on discrete groups having exponential growth[END_REF] consider graphs with exponential growth and Shellef [START_REF] Shellef | IDLA on the supercritical percolation cluster[END_REF] looked at the case of a random graph, namely a supercritical cluster of percolation.

In another direction it is also interesting to see how the analysis can be transposed when we change the simple random walk by some other random process. For instance Enriquez, Lucas and Simenhaus [START_REF] Enriquez | The Arcsine law as the limit of the internal DLA cluster generated by Sinai's walk[END_REF] study the case of random walks in random environment in dimension one and the purpose of this paper is to study the case of cookies random walks (also called multi-excited random walks) in dimension one as well. These last processes are simple examples of self-interacting random walks, which have been first introduced and studied by Benjamini and Wilson [START_REF] Benjamini | Excited random walk[END_REF] and Zerner [START_REF] Zerner | Multi-excited random walks on integers[END_REF]. Actually our purpose is to introduce some new technique for the study of Internal DLA in dimension one and then look at a specific example. The case of excited random walks seemed interesting to us, because it contains many different situations when we let the parameters of the model vary. But most of our analysis carry out for rather general processes, and in particular when the random walk is recurrent and satisfies a central limit theorem (see Theorem 2.1 and Proposition 2.2 below). For cookies random walks, this has been obtained by Dolgopyat [START_REF] Dolgopyat | Central limit theorem for excited random walk in the recurrent regime[END_REF] for some values of the parameters.

Our tools are stochastic algorithms techniques which extend those used by Diaconis and Fulton in their original paper. Our main result is a law of large numbers for the extremities of the cluster. We first present a general result in Subsection 2.1 and then we consider in more details the case of cookies random walks in Subsection 2.2. The proofs are postponed to the remaining sections.

Model and results

2.1.

A general law of large numbers. The internal DLA process is a sequence of growing clusters (intervals in dimension one) which are constructed via a collection (X (n) k , k ≥ 0) n≥1 , of independent random processes on Z. We assume here that these processes start from 0 and only jump to the nearest neighbor, which means that for all n, X (n) 0 = 0, and for all k, X

(n) k+1 -X (n) k = ±1.
We then define the right boundaries (d n , n ≥ 0) of the intervals as follows. First d 0 = 0, and for all n ≥ 0,

d n+1 = d n + 1, if X (n+1) hits the site d n + 1 before the site d n -n -1. Otherwise d n+1 = d n .
(We also implicitly assume that our processes visit a.s. an infinite number of sites, which assures that d n is well defined for all n ≥ 0.) Now for n ≥ 0, set

x n := d n + 1 n + 2 ,
and for x ∈ Z, set

T (n) x = inf{k ≥ 0 : X (n) k = x}.
Define also the function

h n : [0, 1] → [0, 1], by h n (x) = P T (n) [(n+2)x] < T (n) [(n+2)(x-1)]
, where for any u ∈ R, [u] denotes the integer with the smallest absolute value, at distance strictly less than 1 from u. Note that for all n ≥ 0, h n is nonincreasing, h n (0) = 1 and h n (1) = 0. The next result is a general law of large numbers for d n .

Theorem 2.1. Assume that there exists a function h, such that for any

x ∈ [0, 1], h n (x) converges to h(x), as n → ∞. Then there exists p ∈ [0, 1], such that x n → p, as n → ∞,

almost surely. Moreover p is characterized by the fact that h(p-) ≥ p ≥ h(p+).

A typical situation when this theorem applies is when the

X (n) are i.i.d. and transient. Indeed in this case, it is immediate that h n (x) → p := P[X (n) → +∞],
for all x ∈ (0, 1). Another typical situation when the theorem applies well, in the recurrent regime, is when there is an invariance principle: for instance if for some c > 0, the process defined for t ≥ 0 by

Y (n) t := X (n) [n c t] n ,
converges in law in the Skorokhod space to some process (Y t , t ≥ 0), as n → ∞. In this case, for x ∈ R, set

T x := inf{t ≥ 0 : Y t ≥ x} if x ≥ 0 inf{t ≥ 0 : Y t ≤ x} if x < 0,
A basic observation is the following:

Proposition 2.2. Assume that there exists c > 0, such that (Y

(n) t
, t ≥ 0) converges in law to some process (Y t , t ≥ 0). Assume that T 1 and T -1 are a.s. finite. Assume also that h defined for all x ∈ [0, 1], by h(x)

:= P[T x < T x-1 ], is continuous. Then, for any x ∈ [0, 1], h n (x) → h(x), as n → ∞.
Note that if Y is a continuous semimartingale, with a nonzero martingale part, then the function h defined in the proposition is automatically continuous.

2.2. Excited random walks. We look now more precisely at the case of excited (also called multi-excited or cookie) random walks, which is a typical nontrivial example to which our general result apply, at least in most situations. However we stress that for some values of a parameter, Theorem 2.1 does not apply and this leads to interesting unsolved questions.

We start by recalling the definition of excited random walks and we will then review some known results which are relevant here.

We define an environment as the set of two sequences (p i,+ , i ≥ 1) and (p i,-, i ≥ 1) of positive reals in (0, 1). Then the law of an excited random walk (X n , n ≥ 0) in this environment is defined as follows. First X 0 = 0. Then, if (F n , n ≥ 0) is the natural filtration of X, we have

P(X n+1 = X n + 1 | F n ) =    1/2 if X n = 0 p i,+ if X n > 0 and L n (X n ) = i p i,-if X n < 0 and L n (X n ) = i,
where for all x and n ≥ 1, L n (x) = #{k ≤ n : X k = x} is the local time of the walk in x at time n. Moreover X always jumps to a nearest neighbor, so for all n, P(

X n+1 = X n + 1 | F n ) = 1 -P(X n+1 = X n -1 | F n ).
This definition slightly differs from usual ones, where p i,+ = p i,-and where 0 does not play a special role, but technically this does not change anything. The reason why we use this definition is that it gives rise to slightly richer situations. For instance the process can be transient only to the right. Now we need some assumption on the environment. We say that a sequence of reals (x i , i ≥ 1) is nonnegative, resp. nonpositive, if x i ≥ 0, resp. x i ≤ 0, for all i ≥ 1. We will use the following hypothesis: Consider also the process Y (n) defined for each n ≥ 1 and for all t ≥ 0 by

Y (n) t := X [nt] √ n . (1)
It was proved by Zerner [START_REF] Zerner | Multi-excited random walks on integers[END_REF] that under Hypothesis 2.3, X is recurrent if, and only if, α ≤ 1 and β ≤ 1. Note that a recurrence criterion has also been proved without assuming Hypothesis 2.3, but with the other hypothesis that p i,± = 1/2 for i large enough (see [START_REF] Kosygina | Positively and negatively excited random walks on integers, with branching processes[END_REF]). Later on Dolgopyat proved the following central limit theorem: 1 Theorem 2.4 (Dolgopyat [START_REF] Dolgopyat | Central limit theorem for excited random walk in the recurrent regime[END_REF]). Assume Hypothesis 2.3 holds. Assume also that α < 1 and β < 1. Then the process (Y (n) t , t ≥ 0) converges in the Skorokhod space toward the (α, β)-perturbed Brownian motion (Y t , t ≥ 0) defined by the equation:

Y t = B t + α sup s≤t Y s + β inf s≤t Y s , ( 2
)
where B is a Brownian motion.

Perturbed Brownian motions are continuous processes which were introduced by Le Gall and Yor [START_REF] Gall | Excursions browniennes et carrs de processus de Bessel, (French) [Brownian excursions and squares of Bessel processes[END_REF]. Uniqueness in law for the equation ( 2) was later proved by Perman and Werner [START_REF] Perman | Perturbed Brownian motions[END_REF] for any α < 1 and β < 1, and pathwise uniqueness has been proved by Chaumont and Doney [START_REF] Chaumont | Pathwise uniqueness for perturbed versions of Brownian motion and reflected Brownian motion[END_REF].

We note also that both Zerner's recurrence criterion and Theorem 2.4 were proved in the more general case when the p i,± may be random. Here we will only consider deterministic environments.

If α < 1 and β < 1, denote by Q (α,β) the law of the (α, β)-perturbed Brownian motion starting from 0 and by h (α,β) the function defined for x ∈ [0, 1] by

h (α,β) (x) = Q (α,β) [T x < T x-1 ] ,
where for any x, T x denotes the hitting time of x. Observe that h (α,β) is continuous and decreasing, thus has a unique fixed point p(α, β). Since h (α,β) (1) = 0 = 1h (α,β) (0), we have p(α, β) ∈ (0, 1). Actually h (α,β) (x) = P (Z(1 -α, 1 -β) ≤ 1 -x), where Z(1 -α, 1 -β) denotes a Beta random variable with parameters 1 -α and 1 -β (see Proposition 4 (iii) in [START_REF] Perman | Perturbed Brownian motions[END_REF]). So another formula for h (α,β) is given by

h (α,β) (x) = 1-x 0 t -α (1 -t) -β B(1 -α, 1 -β) dt, (3)
with B(•, •) the Beta function. Note that h (α,β) (x) = 1-h (β,α) (1-x), which implies that p(α, β) = 1 -p(β, α). Formula (3) shows that p(α, β) is a continuous function of (α, β) ∈ (-∞, 1) 2 , and that p(α, β) → 1, if α → 1 and β < 1 remains fixed (resp. p(α, β) → 0, if β → 1 and α < 1 remains fixed). Moreover p is monotone in (α, β), in the sense that if α ≤ α ′ and β ≥ β ′ , then p(α, β) ≤ p(α ′ , β ′ ). Now we consider the model of internal DLA when (X (n) , n ≥ 0) is sequence of i.i.d. excited random walks with the same law as X above. The next result gives then a law of large numbers for d n in different situations: Theorem 2.5. Assume that Hypothesis 2.3 holds. If (α, β) = (1, 1), then there exists p ∈ [0, 1], such that x n → p almost surely.

• If moreover α < 1 or β < 1, then p only depends on α and β and is a continuous function of (α, β) in this domain.

1 Actually Zerner and Dolgopyat assumed that p i,+ = p i,-for all i, but their proofs extend immediately to the present setting.

• If α < 1 and β < 1, then p = p(α, β) is the unique fixed point of h (α,β) , in particular p ∈ (0, 1). • If α > 1 or β > 1, then p = P(X n → +∞).

• If α = 1 and β < 1, then p = 1 (resp. if α < 1 and β = 1, then p = 0).

On the other hand, if p i,+ = -p i,-, for all i ≥ 1, and α = β = 1, then x n → 1/2 almost surely.

Note that the picture is almost complete. But we do not know whether x n converges in general when α = β = 1 and whether p = P(X n → +∞) only depends on α and β when α > 1 and β > 1.

Proof of Theorem 2.1

The proof is based on the observation that the sequence (x n , n ≥ 1) is solution of a stochastic algorithm. First, since h n is nonincreasing for all n ≥ 0, h is also nonincreasing. In particular it has left and right limits in all points, and there is a unique p ∈ [0, 1], such that h(p-) ≥ p ≥ h(p+). Next, by definition

d n+1 = d n + 1(T (n+1) dn+1 < T (n+1)
gn-1 ), for all n ≥ 1. Therefore

x n+1 = x n + p -x n n + 3 + ǫ n+1 n + 3 + r n+1 n + 3 for all n ≥ 1,
where

ǫ n+1 := 1(T (n+1) dn+1 < T (n+1) dn-n-1 ) -h n (x n ), (4)
is the increment of a martingale, and r n+1 := h n (x n ) -p. Set now y n := x n -p. Then

y 2 n+1 = y 2 n - 2y 2 n n + 3 + ǫ ′ n+1 n + 3 + s n+1 n + 3 + t n+1 for all n ≥ 1,
where ǫ ′ n+1 = 2ǫ n+1 y n , s n+1 = 2r n+1 y n and t n = O(n -2 ). In particular the ǫ ′ n are still the increments of a martingale. We claim now that lim sup

n→∞ s n+1 ≤ 0. (5) Indeed, let ǫ > 0 be fixed. First if |x n -p| ≤ ǫ, then |s n+1 | ≤ 2ǫ, since |h n | ≤ 1. Now if x n ≥ p + ǫ, since h n is nonincreasing, h n (x n ) -p ≤ h n (p + ǫ) -p. But h n (p + ǫ) → h(p + ǫ) ≤ p,
by hypothesis. This proves that h n (x n ) -p ≤ ǫ, for n large enough. The case x n ≤ p -ǫ is similar. This proves [START_REF] Blachère | Internal diffusion limited aggregation on discrete groups having exponential growth[END_REF]. We deduce that s ′ n := max(s n , 0) converges to 0, as n → ∞. Define next (z n , n ≥ 1) by z 1 = y 2 1 and

z n+1 = z n - 2z n n + 3 + ǫ ′ n+1 n + 3 + s ′ n+1 n + 3 + t n+1 for all n ≥ 1.
Since |ǫ ′ n | ≤ 2, it is a well known fact that z n → 0 almost surely (see [START_REF] Benaïm | Dynamics of stochastic approximation algorithms[END_REF] or [Du, Theorem 3.III.9 p.105]). But on the other hand it is immediate by induction on n, that 0 ≤ y 2 n ≤ z n , for all n ≥ 1. Thus y n → 0 almost surely, which concludes the proof of Theorem 2.1.

Proof of Proposition 2.2

Note that Y 0 = 0 a.s., so h(0) = 1 and h(1) = 0. Now fix some x ∈ (0, 1). For y ∈ R, set T (n, y) := T (n) [(n+2)y] /n c . Let ǫ > 0 be such that x + ǫ < 1 and x -ǫ > 0. Since by hypothesis T 1 and T -1 are a.s. finite, there exists T > 0, such that P[T 1 ≥ T ] ≤ ǫ, and P[T -1 ≥ T ] ≤ ǫ. Since Y (n) converges in law to Y , by using Skorokhod's representation theorem, we can assume that Y (n) converges a.s. uniformly to Y on [0, T ]. In other words, if

Ω n,ǫ := sup t≤T |Y (n) t -Y t | < ǫ ,
then we can assume that P(Ω n,ǫ ) → 1, as n → ∞. In particular P(Ω n,ǫ ) ≤ ǫ, for n large enough. Now, since x + ǫ < 1, we have

P[Ω n,ǫ , T (n, x) ≥ T ] ≤ ǫ,
and similarly with x -1 instead of x. Moreover,

Ω n,ǫ ∩ {T (n, x) < T (n, x -1) ≤ T } ⊂ {T x-ǫ < T x-1-ǫ } . h n (x) = P[T (n, x) < T (n, x -1)] ≤ 3ǫ + P[Ω N,ǫ , T (n, x) < T (n, x -1) ≤ T ] ≤ 3ǫ + P[T x-ǫ < T x-1-ǫ ] = 3ǫ + h(x -ǫ),
for n large enough. We can prove similarly that h n (x) ≥ h(x + ǫ) -3ǫ, for n large enough. Since ǫ can be taken arbitrarily small, and since h is assumed to be continuous, this concludes the proof of the proposition.

Proof of Theorem 2.5

• First when α < 1 and β < 1, the result follows from Theorem 2.1, Proposition 2.2 and Theorem 2.4.

• If now α > 1 or β > 1, then Zerner's result [START_REF] Zerner | Multi-excited random walks on integers[END_REF] implies that the cookie random walk is transient. We then immediately get that for any x ∈ (0, 1), h n (x) → p := P[X n → ∞]. Thus we can apply Theorem 2.1 with h the function equal to p on (0, 1), and such that h(0) = 1 and h(1) = 0.

Note that if we are in the case α > 1 and β > then by Lemma 8 in [START_REF] Zerner | Multi-excited random walks on integers[END_REF] we have P[X n > 0 for all n > 0] > 0 and P[X n < 0 for all n > 0] > 0. Thus p ∈ (0, 1). On the other hand if α > 1 and β ≤ 1, then p = 1 (resp. if α ≤ 1 and β > 1, then p = 0).

• We consider next the case α = 1 and β < 1 (the case α < 1 and β = 1 is entirely similar), which belongs to the recurrent regime. We have to prove that x n → 1 almost surely. For this we use the following monotonicity result due to Zerner: Lemma 5.1 ([20] Lemma 15). Let P be the law of a cookie random walk evolving in an environment (p i,± , i ≥ 1) and P ′ the law of a cookie random walk evolving in another environment (q i,± , i ≥ 1). Assume that p i,+ ≥ q i,+ and p i,-≥ q i,-, for all i ≥ 1. Then P[T y < T x ] ≥ P ′ [T y < T x ], for all x < 0 < y.

Two cases may appear now. Either there exists M such that M-1 i=1 p i,+ < 1 ≤ M i=1 p i,+ , or for all ǫ > 0, there exists M = M (ǫ) such that 1 -ǫ ≤ M i=1 p i,+ < 1.

In any case, set q i,-= p i,-, for all i ≥ 1, and q i,+ = 1/2, for i > M . In addition, in the first case, set q i,+ = p i,+ , for i ≤ M -1 and q + M = p + M -ǫ, with ǫ < p + M . In the second case, set q i,+ = p i,+ , for i ≤ M . The above lemma implies that in both cases, the process (d n , n ≥ 0) associated to (p i,± , i ≥ 1) stochastically dominates the process (d ′ n , n ≥ 0) associated to (q i,± , i ≥ 1). Thus lim inf x n ≥ p(α ǫ , β), for all ǫ > 0, where α ǫ = M i=1 q i,+ . But α ǫ → 1, when ǫ → 0. Moreover we already saw in the discussion above Theorem 2.5 that p(α, β) → 1, when α → 1. This proves that x n converges a.s. to 1.

• It remains to consider the case when p i,+ = -p i,-, for all i ≥ 1, and α = β = 1. In this case the processes X and -X have the same law. Thus h n (1/2) = 1/2 for all n ≥ 1, and as an immediate consequence (h n (x) -1/2)(x -1/2) ≤ 0, for all x ∈ [0, 1]. In particular, we can follow the proof of Theorem 2.1, and we find that s n+1 ≤ 0, for all n ≥ 1. Since it was all we needed in this proof, we conclude as well that x n → 1/2 almost surely. This finishes the proof of Theorem 2.5.

Hypothesis 2 . 3 .

 23 Each of the sequences(p i,+ -1/2, i ≥ 1) and (p i,--1/2, i ≥ 1)is either nonnegative or nonpositive.


Jérôme Leroux
email: leroux@labri.fr

Vector Addition System Reachability Problem: A Short Self-Contained Proof

The reachability problem for Vector Addition Systems (VASs) is a central problem of net theory. The general problem is known to be decidable by algorithms exclusively based on the classical Kosaraju-Lambert-Mayr-Sacerdote-Tenney decomposition (KLMTS decomposition). Recently from this decomposition, we deduced that a final configuration is not reachable from an initial one if and only if there exists a Presburger inductive invariant that contains the initial configuration but not the final one. Since we can decide if a Preburger formula denotes an inductive invariant, we deduce from this result that there exist checkable certificates of non-reachability in the Presburger arithmetic. In particular, there exists a simple algorithm for deciding the general VAS reachability problem based on two semi-algorithms. A first one that tries to prove the reachability by enumerating finite sequences of actions and a second one that tries to prove the non-reachability by enumerating Presburger formulas. In this paper we provide the first proof of the VAS reachability problem that is not based on the KLMST decomposition. The proof is based on the notion of production relations, inspired from Hauschildt, that directly proves the existence of Presburger inductive invariants. * -→ m is definable. Hence * -→ m is an asymptotically definable periodic relation.

Almost Semilinear Reachability Relations

In this section we prove the following Theorem 9.1. All the other results or definitions introduced in this section are not used in the sequel. Theorem 9.1. The reachability relation of a Vector Addition System is an almost semilinear relation. * -→ m .

Introduction

Vector Addition Systems (VASs) or equivalently Petri Nets are one of the most popular formal methods for the representation and the analysis of parallel processes [START_REF] Esparza | Decidability issues for petri nets -a survey[END_REF]. Their reachability problem is central since many computational problems (even outside the realm of parallel processes) reduce to the reachability problem. Sacerdote and Tenney provided in [START_REF] Sacerdote | The decidability of the reachability problem for vector addition systems (preliminary version)[END_REF] a partial proof of decidability of this problem. The proof was completed in 1981 by Mayr [START_REF] Mayr | An algorithm for the general petri net reachability problem[END_REF] and simplified by Kosaraju [START_REF] Kosaraju | Decidability of reachability in vector addition systems (preliminary version)[END_REF] from [START_REF] Sacerdote | The decidability of the reachability problem for vector addition systems (preliminary version)[END_REF][START_REF] Mayr | An algorithm for the general petri net reachability problem[END_REF]. Ten years later [START_REF] Lambert | A structure to decide reachability in petri nets[END_REF], Lambert provided a further simplified version based on [START_REF] Kosaraju | Decidability of reachability in vector addition systems (preliminary version)[END_REF]. This last proof still remains difficult and the upper-bound complexity of the corresponding algorithm is just known to be non-primitive recursive. Nowadays, the exact complexity of the reachability problem for VASs is still an open-problem. Even the existence of an elementary upper-bound complexity is open. In fact, the known general reachability algorithms are exclusively based on the Kosaraju-Lambert-Mayr-Sacerdote-Tenney (KLMST) decomposition.

Recently [START_REF] Leroux | The general vector addition system reachability problem by Presburger inductive invariants[END_REF] we proved thanks to the KLMST decomposition that Parikh images of languages accepted by VASs are semi-pseudo-linear, a class that extends the Presburger sets. An application of this result was provided; we proved that a final configuration is not reachable from an initial one if and only if there exists a forward inductive invariant definable in the Presburger arithmetic that contains the initial configuration but not the final one. Since we can decide if a Presburger formula denotes a forward inductive invariant, we deduce that there exist checkable certificates of non-reachability in the Presburger arithmetic. In particular, there exists a simple algorithm for deciding the general VAS reachability problem based on two semi-algorithms. A first one that tries to prove the reachability by enumerating finite sequences of actions and a second one that tries to prove the non-reachability by enumerating Presburger formulas.

In this paper we provide a new proof of the reachability problem that is not based on the KLMST decomposition. The proof is based on the production relations inspired by Hauschildt [START_REF] Hauschildt | Semilinearity of the Reachability Set is Decidable for Petri Nets[END_REF] and it proves directly that reachability sets are almost semilinear, a class of sets introduced in this paper that extend the class of Presburger sets and contained in the class of semi-pseudo-linear sets. In particular this paper provides a more precise characterization of the reachability sets of VASs.

Outline of the paper: Section 2 provides notations and classical definitions. Section 3 and Section 4 introduce classes of sets used in the sequel : definable conic sets and vector spaces in the first one and asymptotically definable periodic sets, Presburger sets, and almost semilinear sets in the second one. Section 5 and Section 6 show that is sufficient to prove that the reachability relation of a Vector Addition system is an almost semilinear relation in order to deduce the existence of forward inductive invariants definable in the Presburger arithmetic proving the non-reachability. In Section 7 we introduce the class of Vector Addition Systems and the central notion of production relations. We show in the next Section 8 that these relations are asymptotically definable periodic. In Section 9 we prove that the reachability relation of a Vector Addition System is an almost semilinear relation. Finally in Section 10 we combine all the previous results to deduce the decidability of the Vector Addition System reachability problem based on Presburger inductive invariants.

Notations

We introduce in this section notations and classical definitions used in this paper.

We denote by N, N >0 , Z, Q, Q ≥0 , Q >0 the set of natural numbers, positive integers, integers, rational numbers, non negative rational numbers, and positive rational numbers. Vectors and sets of vectors are denoted in bold face. The ith component of a vector v ∈ Q d is denoted by v(i). We introduce ||v|| ∞ = max 1≤i≤d |v(i)| where |v(i)| is the absolute value of v(i). The total order ≤ over Q is extended componentwise into an order ≤ over the set of vectors Q d . The addition function + is also extended component-wise over

Q d . Given two sets V 1 , V 2 ⊆ Q d we denote by V 1 + V 2 the set {v 1 + v 2 | (v 1 , v 2 ) ∈ V 1 × V 2 }, and we denote by V 1 -V 2 the set {v 1 -v 2 | (v 1 , v 2 ) ∈ V 1 × V 2 }.
In the same way given T ⊆ Q and V ⊆ Q d we let T V = {tv | (t, v) ∈ T × V}. We also denote by v 1 + V 2 and V 1 + v 2 the sets {v 1 } + V 2 and V 1 + {v 2 }, and we denote by tV and T v the sets {t}V and T {v}. In the sequel, an empty sum of sets included in Q d denotes the set reduced to the zero vector {0}.

A (binary) relation R over Q d is a subset R ⊆ Q d × Q d .
The composition of two relations R and S is the relation denoted by R • S and defined as usual by the following equality:

R • S = y∈Q d (x, z) ∈ Q d × Q d | (x, y) ∈ R ∧ (y, z) ∈ S
The reflexive and transitive closure of a relation R is denoted by R * . In this paper, notions introduced over the sets are transposed over the relations by identifying

Q d ×Q d with Q 2d .
An order over a set S is said to be well if for every sequence (s n ) n∈N of elements s n ∈ S we can extract a sub-sequence that is non-decreasing for , i.e. there exists a strictly increasing sequence (n k ) k∈N of natural numbers in (N, ≤) such that (s n k ) k∈N is non decreasing for . A minimal element of an ordered set (S, ) is an element s ∈ S such that for every t ∈ T the relation t s implies s = t. Given a set Y ⊆ S we denote by min (Y ) the set of minimal elements of the ordered set (Y, ). Let us recall that if (S, ) is well ordered then X = min (Y ) is finite and for every y ∈ Y there exists x ∈ X such that x y.

Let us consider an order over a set S. We introduce the component-wise extension of over the set of vectors S d defined by s t if s(i) t(i) for every i ∈ {1, . . . , d}.

Lemma 2.1 (Dickson's Lemma). The ordered set (S d , ) is well for every well ordered set (S, ).

Example 2.2. The set (N, ≤) is well ordered. Hence (N d , ≤) is also well ordered. The set (Z, ≤) is not well ordered.

Definable Conic Sets

A conic set is a set C ⊆ Q d such that 0 ∈ C, C + C ⊆ C and such that Q ≥0 C ⊆ C. A conic set C is said to be finitely generated if there exists a finite sequence c 1 , . . . , c k of vectors c j ∈ C such that C = Q ≥0 c 1 + • • • + Q ≥0 c k . Definition 3.1. A conic set C is said to be definable if it is definable in FO (Q, +, ≤, 0).
In this section definable conic sets are geometrically characterized thanks to the vector spaces and the topological closure. Example 3.2. Fig. 1 depicts examples of finitely generated conic sets and (non finitely generated) definable conic sets. The conic set

C = {(c 1 , c 2 ) ∈ Q 2 ≥0 | √ 2c 2 ≤ c 1 } is not definable. Fig. 1. The finitely generated conic set Q ≥0 (1, 1) + Q ≥0 (1, 0) and the definable conic set {(0, 0)} ∪ {(c1, c2) ∈ Q 2 >0 | c2 ≤ c1} A vector space is a set V ⊆ Q d such that 0 ∈ V, V + V ⊆ V and such that QV ⊆ V. Let X ⊆ Q d .
The following set is a vector space called the vector space generated by X.

V =    k j=1 λ j x j | k ∈ N and (λ j , x j ) ∈ Q × X   
This vector space is the minimal for inclusion among the vector space that contains X. Note that the vector space V generated by a conic set C satisfies the equality V = C -C. Let us recall that every vector space V is generated by a finite set X with at most d vectors. The rank rank(V) of a vector space V is the minimal natural number r ∈ {0, . . . , d} such that there exists a finite set X with r vectors that generates V. Note that rank(V) ≤ rank(W) for every pair of vector spaces V ⊆ W. Moreover, if V is strictly included in W then rank(V) < rank(W).

Example 3.3. Vector spaces V included in Q 2 satisfy rank(V) ∈ {0, 1, 2}. Moreover these vectors spaces can be classified as follows : rank(V) = 0 if and only if

V = {0}, rank(V) = 1 if and only if V = Qv with v ∈ Q 2 \{0}, and rank(V) = 2 if and only if V = Q 2 . The (topological) closure of a set X ⊆ Q d is the set X of vectors r ∈ Q d such that for every ∈ Q >0 there exists x ∈ X satisfying ||r -x|| ∞ < . A set X is said to be closed if X = X.
Note that X is closed and this set is the minimal for inclusion among the closed sets that contain X. Let us recall that a vector space V is closed and the closure of a conic set is a conic set. Since the classical topological interior of a conic set C is empty when the vector space generated by C is not equal to Q d (the conic set is degenerated), we introduce the notion of interior of C relatively to the vector space

V = C -C. More precisely, a vector c ∈ C is said to be in the interior of C if there exists ∈ Q >0 such that c + v ∈ C for every v ∈ C -C satisfying ||v|| ∞ < .
We denote by int(C) the set of interior vectors of C. Let us recall that int(C) is non empty for every conic set C, and

C 1 = C 2 if and only if int(C 1 ) = int(C 2 ) for every conic sets C 1 , C 2 . Example 3.4. Let X = (1, 5) × (1, 5). Then X = [1, 5] × [1, 5] (see Fig. 2). Fig. 2. Sets X = (1, 5) × (1, 5) and X = [1, 5] × [1, 5]
The following lemma characterizes the finitely generated cones. Lemma 3.5 (Duality). Let V ⊆ Q d be a vector space. A conic set C ⊆ V is finitely generated if and only if there exists a sequence (h j ) 1≤j≤k of vectors h j ∈ V\{0} such that:

C = k j=1 v ∈ V | d i=1 h j (i)v(i) ≥ 0
Moreover in this case the following equality holds if and only if V is the vector space generated by C:

int(C) = k j=1 v ∈ V | d i=1 h j (i)v(i) > 0
Proof. This is a classical result of duality [START_REF] Schrijver | Theory of Linear and Integer Programming[END_REF]. Example 3.6. Let us introduce the whole vector space V = Q 2 and the finitely generated conic set

C = Q ≥0 (1, 1) + Q ≥0 (1, 0). Fig. 3 shows that C = j∈{1,2} {v ∈ V | d i=1 h j (i)v(i) ≥ 0} where h 1 = (0, 2) and h 2 = (2, -2).
Lemma 3.7. The topological closure of a set definable in FO (Q, +, ≤, 0) is a finite union of finitely generated conic sets.

Proof. Let X ⊆ Q d be a set definable in FO (Q, +, ≤, 0). Since this logic admits quantification elimination we deduce that there exists a quantifier free formula in this logic that denotes X. Hence there exists a finite sequence (A j ) 1≤j≤k of finite sets A j ⊆ Q d × {>, ≥} such that X = k j=1 X j where:

X j = (h,#)∈Aj x ∈ Q d | d i=1 h(i)x(i)#0
We can assume without loss of generality that X j is non empty. Moreover if k = 0 the proof is immediate since X = ∅. So we can assume that k ≥ 1. Let us introduce the following set R j :

R j = (h,#)∈Aj x ∈ Q d | d i=1 h(i)x(i) ≥ 0 Lemma 3.5
shows that R j is finitely generated. Thanks to Lemma 3.5, we deduce that R = k j=1 R j is closed. We are going to prove that X = R. Since X j ⊆ R j we get X ⊆ R. As R is closed we deduce that X ⊆ R. Let us prove the converse inclusion. Let r ∈ R. There exists j ∈ {1, . . . , k} such that r ∈ R j . Since X j is non empty, there exists x j ∈ X j . As r j ∈ R j and x j ∈ X j we deduce that r j + Q >0 x j ⊆ X j . Hence r j ∈ X j and we have proved the other inclusion R ⊆ X. Therefore X is a finite union of finitely generated conic sets since it is equal to R. Theorem 3.8. A conic set C ⊆ Q d is definable if and only if the conic set C ∩ V is finitely generated for every vector space V ⊆ Q d .

Proof. Let us first consider a definable conic set C ⊆ Q d , let V be a vector space, and let us prove that X is finitely generated where X = C ∩ V. Since X is definable in FO (Q, +, ≤, 0), Lemma 3.7 shows that X = k j=1 C j where C j is a finitely generated conic sets. Moreover, as X is non empty we deduce that k ≥ 1. As X is a conic set we deduce that k j=1 C j ⊆ X. Moreover, as 0 ∈ C j for every j, we deduce that C j ⊆ k j=1 C j for every j. Thus X = k j=1 C j and we have proved that X is finitely generated.

Conversely, we prove by induction over r that the conic sets C ⊆ Q d such that rank(C -C) ≤ r and such that the conic set C ∩ V is finitely generated for every vector space V ⊆ Q d are definable. The case r = 0 is immediate since in this case C = {0}. Let us assume the induction proved for an integer r ∈ N and let us consider a conic set C ⊆ Q d such that rank(C -C) ≤ r + 1 and such that the conic set C ∩ V is finitely generated for every vector space V ⊆ Q d . We introduce the vector space

W = C -C. Since C = C ∩ V with V = Q d ,
we deduce that C is finitely generated. Lemma 3.5 shows that there exists a finite sequence (h j ) 1≤j≤k of vectors h j ∈ W\{0} such that the following equality holds:

C = k j=1 x ∈ W | d i=1 h j (i)x(i) ≥ 0
Since int(C) = int(C) we get the following equality:

int(C) = k j=1 x ∈ W | d i=1 h j (i)x(i) > 0
In particular int(C) is definable in FO (Q, +, ≤, 0, 1). As int(C) ⊆ C ⊆ C we deduce the following decomposition where

W j = {w ∈ W | d i=1 h j (i)w(i) = 0}: C = int(C) ∪ k j=1 (C ∩ W j )
Observe that h j ∈ W\W j and in particular W j is strictly included in W. Thus rank(W j ) < rank(W) ≤ r + 1. Note that C j = C ∩ W j is a conic set such that rank(C j -C j ) ≤ rank(W j ) ≤ r and such that C j ∩ V is a finitely generated conic set for every vector space V. Thus by induction C j is definable in FO (Q, +, ≤, 0, 1). We deduce that C is definable. We have proved the induction.

Example 3.9. Observe that the conic set

C = {(c 1 , c 2 ) ∈ Q 2 ≥0 | √ 2c 2 ≤ c 1 } is not finitely generated. Let us consider V = Q 2 and
observe that C ∩ V = C and since C = C we deduce that C ∩ V is not finitely generated. Theorem 3.8 shows that C is not definable.

Presburger Sets And Almost Semilinear Sets

In this section we introduce the Presburger sets and the almost semilinear sets.

A periodic set is a subset P ⊆ Z d such that 0 ∈ P and such that P + P ⊆ P. A periodic set P is said to be finitely generated if there exists a finite sequence p 1 , . . . , p k of vectors p j ∈ P such that P = Np 1 + • • • + Np k (see Fig. 4). A subset S ⊆ Z d is called a Presburger set if it can be denoted by a formula in the Presburger arithmetic FO (Z, +, ≤, 0, 1). Let us recall [START_REF] Ginsburg | Semigroups, Presburger formulas and languages[END_REF] that a subset S ⊆ Z d is Presburger if and only if it is semilinear, i.e. a finite union of sets b + P where b ∈ Z d and P ⊆ Z d is a finitely generated periodic set. The class of almost semilinear sets is obtained by weakening the finiteness property of the periodic sets P. Definition 4.1. A periodic set P is said to be asymptotically definable if the conic set Q ≥0 P is definable. Remark 4.2. Every finitely generated periodic set P is asymptotically definable since in this case Q ≥0 P is a finitely generated conic set and in particular a definable conic set.

Example 4.3. The periodic set

P = {(p 1 , p 2 ) ∈ N 2 | √ 2p 2 ≤ p 1 } is not asymptot- ically definable since Q ≥0 P = {(c 1 , c 2 ) ∈ N 2 | √ 2c 2 ≤ c 1 } is not definable (see example 3.9). p(2) p(1)
Fig. 4. The finitely generated periodic set

P = N(1, 1) + N(2, 0) p(2) p(1) p(1) + 1 ≤ 2 p(2) p(2) ≤ p(1)
= {p ∈ N 2 | p(2) ≤ p(1) ≤ 2 p(2) -1} is rep- resented in Figure 5. Observe that Q ≥0 P = {0} ∪ {c ∈ Q 2 >0 | p(2) ≤ p(1)
} is a definable conic set. Thus P is an asymptotically definable periodic set.

The following lemma shows that the class of asymptotically definable periodic sets is stable by finite intersections. Lemma 4.5. We have

(Q ≥0 P 1 ) ∩ (Q ≥0 P 2 ) = Q ≥0 (P 1 ∩ P 2 ) for every periodic sets P 1 , P 2 ⊆ Z d . Proof. Observe that P 1 ⊆ Q ≥0 P 1 and P 2 ⊆ Q ≥0 P 2 . Hence P 1 ∩ P 2 ⊆ C where C = (Q ≥0 P 1 ) ∩ (Q ≥0 P 2 ). As C is a conic set we deduce that Q ≥0 (P 1 ∩ P 2 ) ⊆ C. For the converse inclusion. Let c ∈ C. Since c ∈ Q ≥0 P 1 , there exists λ 1 ∈ Q ≥0 such that c ∈ λ 1 P 1 . Symmetrically there exists λ 2 ∈ Q ≥0 such that c ∈ λ 2 P 2 . Let n 1 , n 2 ∈ N >0 such that n 1 λ 1 ∈ N and n 2 λ 2 ∈ N. Let n = n 1 n 2 and observe that nc ∈ n 2 (n 1 λ 1 )P 1 ⊆ P 1 since P 1 is a periodic set. Symmetrically nc ∈ P 2 . We have proved that nc ∈ P 1 ∩P 2 . Thus c ∈ Q ≥0 (P 1 ∩P 2 )
and we get the other inclusion. The class of almost semilinear sets is included in the class of Presburger sets. The strict inclusion will be proved strict as a direct consequence of a stronger result proved in this paper. In fact the reachability relation of a Vector Addition System is proved to be almost semilinear and we know that in general such a relation is not Presburger.

= {(0, 0)} ∪ {(2 n , 1) | n ∈ N} ∪ ((1, 2) + N 2 ) depicted in Fig.6. Observe that Q ≥0 P is the definable conic set {(0, 0)} ∪ Q ≥0 × Q >0 . Note that P is not almost semilinear since P ∩ (N × {1}) = {(2 n , 1) | n ∈ N} can not

Linearizations

The linearization of a periodic set P ⊆ Z d is the periodic set lin(P) defined by the following equality: lin(P) = (P -P) ∩ Q ≥0 P Lemma 5.1. The linearization of an asymptotically definable periodic set is finitely generated.

Proof. Let V be the vector space generated by P and let us introduce the conic set

C = Q ≥0 P. Note that Q ≥0 P ⊆ V and since V is closed we get C ⊆ V. As Q ≥0 P is a definable conic set we deduce that C is finitely generated. Hence there exists c 1 , . . . , c k ∈ C such that C = Q ≥0 c 1 + • • • + Q ≥0 c k . As c j ∈ C ⊆ V = Q ≥0 P -Q ≥0 P
, by replacing c j by a vector in N >0 c j we can assume that c j ∈ P -P for every j ∈ {1, . . . , k}. We introduce the following set R:

R =    r ∈ P -P | r = k j=1 λ j c j λ j ∈ Q 0 ≤ λ j < 1    We observe that every vector r ∈ R satisfies ||r|| ∞ ≤ s where s = k j=1 ||c j || ∞ . Hence R ⊆ {-s, .
. . , s} d and we deduce that R is finite.

Let L be the periodic set generated by the finite set R ∪ {c 1 , . . . , c k }. Since this finite set is included in lin(P) we deduce that L ⊆ lin(P). Let us prove the converse inclusion. Let x ∈ lin(P). Since x ∈ C, there exists a sequence (µ j ) 1≤j≤k of rational elements µ j ∈ Q ≥0 such that x = k j=1 µ j c j . Let us introduce n j ∈ N such that λ j = µ j -n j satisfies 0 ≤ λ j < 1. Let r = k j=1 λ j c j . As r = xk j=1 n j c j we get r ∈ P -P. Thus r ∈ R. From x = r + k j=1 n j c j we get x ∈ L. We have proved that lin(P) is the finitely generated periodic set L.

We observe that if the intersection (b 1 + P 1 ) ∩ (b 2 + P 2 ) is empty where b 1 , b 2 ∈ Z d and P 1 , P 2 ⊆ Z d are two asymptotically definable periodic sets then the intersection (b 1 + lin(P 1 )) ∩ (b 2 + lin(P 2 )) may be non empty (see Example 5.3). In this section we show that a dimension is strictly decreasing.

Let us first introduce our definition of dimension. The dimension dim(X) of a nonempty set X ⊆ Z d is the minimal integer r ∈ {0, . . . , d} such that there exists k ∈ N >0 , a sequence (b j ) 1≤j≤k of vectors b j ∈ Z d , and a sequence (V j ) 1≤j≤k of vector spaces

V j ⊆ Q d such that rank(V j ) ≤ r and such that X ⊆ k j=1 b j + V j . The dimension of the empty set is defined by dim(∅) = -1.
In the reminder of this section we prove the following Theorem 5.2. All the other results or definitions introduced in this section are not used in the sequel.

Theorem 5.2. Let b 1 , b 2 ∈ Z d and let P 1 , P 2 be two asymptotically definable periodic sets such that the intersection (b

1 + P 1 ) ∩ (b 2 + P 2 ) is empty. The intersection X = (b 1 + lin(P 1 )) ∩ (b 2 + lin(P 2 )) satisfies: dim(X) < max{dim(b 1 + P 1 ), dim(b 2 + P 2 )}
Example 5.3. Sets introduced in this example are depicted in Fig. 7. Let us introduce the asymptotically definable periodic sets P 1 = {p ∈ N 2 | p(2) ≤ p(1) ≤ 2 p(2) -1} and P 2 = N(1, 0) + N(3, -1). We consider b 1 = (0, 0) and b 2 = (7, 2). We observe that the intersection of b 1 + P 1 and b 2 + P 2 is empty. Note that the intersection X of b 1 + lin(P 1 ) and b 2 + lin(P 2 ) satisfies X = {(7, 2), (10, 1), (13, 0)} + N(1, 0). In particular we have dim(X) = 1 whereas dim(b 1 +lin(P 1 )) = dim(b 2 +lin(P 2 )) = 2. We first characterize the dimension of a periodic set. Lemma 5.4. Let V be the vector space generated by a periodic set P. Then rank(V) = dim(P).

Proof. Let P be a periodic set and let us first prove by induction over k ∈ N >0 that for every sequence (V j ) 1≤j≤k of vector spaces V j ⊆ Q d , the inclusion P ⊆ k j=1 V j implies that there exists j ∈ {1, . . . , k} such that P ⊆ V j . The case k = 1 is immediate. Assume the property proved for an integer k ∈ N >0 and let us assume that P ⊆ k+1 j=1 V j . If P ⊆ V k+1 the property is proved. So we can assume that there exists p ∈ P\V k+1 . Let us prove that P ⊆ k j=1 V j . We consider x ∈ P. Observe that if x ∈ V k+1 then x ∈ k j=1 V j . So we can assume that x ∈ V k+1 . We observe that p + nx ∈ P for every n ∈ N since the set P is periodic. We deduce that there exists j ∈ {1, . . . , k + 1} such that p + nx ∈ V j . Naturally this integer j depends on n. However, since {1, . . . , k + 1} is finite whereas N is infinite, there exists j ∈ {1, . . . , k + 1} and n < n in N such that p + nx and p + n x are both in V j . As V j is a vector space, we deduce that n (p + nx) -n(p + n x) is in V j . Hence p ∈ V j . As p ∈ V k+1 we deduce that j = k + 1. As V j is a vector space we deduce that (p + n x) -(p + nx) ∈ V j . Hence x ∈ V j . We have proved that x ∈ k j=1 V j . Thus P ⊆ k j=1 V j and by induction there exists j ∈ {1, . . . , k} such that P ⊆ V j . We have proved the induction. Now, let us prove the lemma. We consider a periodic set P and we let V be the vector space generated by this set. Since P ⊆ V we deduce that dim(P) ≤ rank(V). For the converse inclusion, since P is non empty we deduce that P ⊆ k j=1 b j + V j where k ∈ N >0 , b j ∈ Z d and V j ⊆ Q d is a vector space such that rank(V j ) ≤ dim(P). Let us consider the set J = {j ∈ {1, . . . , k} | b j ∈ V j } and let us prove that P ⊆ j∈J V j . Let p ∈ P and n ∈ N. Since np ∈ P there exists j ∈ {1, . . . , k} such that np ∈ b j + V j . Hence there exists j ∈ {1, . . . , k} and n < n in N such that np and n p are both in b j + V j . As V j is a vector space we deduce that n p -np ∈ V j . Thus p ∈ V j . Moreover as b j ∈ np -V j ⊆ V j we deduce that j ∈ J. We have prove the inclusion P ⊆ j∈J V j . From the previous paragraph we deduce that there exists j ∈ J such that P ⊆ V j . By minimality of the vector space generated by P we get V ⊆ V j . Hence rank(V) ≤ rank(V j ). Since rank(V j ) ≤ dim(P) we have proved the inequality rank(V) ≤ dim(P).

Next we prove a separation property. Lemma 5.5. Let C ≤ and C ≥ be two finitely generated conic sets that generates the same vector space V and such that the vector space generated by C ≤ ∩ C ≥ is strictly included in V. Then there exists a vector h ∈ V\{0} such that for every # ∈ {≤, ≥}, we have:

C # ⊆ v ∈ V | d i=1 h(i)v(i)#0
Proof. Lemma 3.5 shows that there exists two finite sets H ≤ , H ≥ included in V\{0} such that:

C # = h∈H # v ∈ V | d i=1 h(i)v(i) ≥ 0 int(C # ) = h∈H # v ∈ V | d i=1 h(i)v(i) > 0
Assume by contradiction that the intersection int(C ≤ ) ∩ int(C ≥ ) is non empty and let c be a vector in this set. Observe that there exists ∈ Q >0 such that c + v ∈ C ≤ ∩ C ≥ for every v ∈ V such that ||v|| ∞ < . We deduce that the vector space generated by C ≤ ∩ C ≥ contains V and we get a contradiction.

We deduce that the following intersection is empty where

H = H ≤ ∪ H ≥ h∈H v ∈ V | d i=1 h(i)v(i) > 0
Farkas's Lemma [START_REF] Schrijver | Theory of Linear and Integer Programming[END_REF] shows that there exists a non-zero function f :

H → Q ≥0 such that h∈H f (h)h = 0. Let us introduce a = h∈H ≥ f (h)h and b = h∈H\H ≥ f (h)h.
Assume by contradiction that a = 0. Since a + b = 0 we deduce that b = 0. As f is not the zero function, there exists h ∈ H such that f (h) = 0. Note that either h ∈ H ≥ or h ∈ H\H ≥ . In the first case we deduce that int(C ≥ ) is empty and in the second case we deduce that int(C ≤ ) is empty. Since both cases are impossible we get a contradiction. Thus a = 0. For every c ∈ int(C ≥ ) we have Remark 5.6. The previous Lemma 5.5 is wrong if we remove the finitely generated condition on the conic sets C ≤ and C ≥ . In fact let us consider the conic sets

C ≤ = {x ∈ Q 2 ≥0 | x(1) ≤ √ 2x(2)} and C ≥ = {x ∈ Q 2 ≥0 | x(2) ≥ √ 2x(2)}. Observe that C ≤ ∩ C ≥ = {0}.
Hence the vector space generated by the intersection is strictly included in Q 2 . However there does not exist a vector h ∈ Q 2 \{0} satisfying the separation property required by Lemma 5.5. This problem can be overcome by introducing the vector spaces of R d . We do not introduce this extension to simplify the presentation.

We can now provide a proof for Theorem 5.2. We consider two vectors b 1 , b 2 ∈ Z d and two periodic sets P 1 , P 2 ⊆ Z d such that (b 1 + P 1 ) ∩ (b 2 + P 2 ) = ∅. We introduce the intersection X = (b 1 + lin(P 1 )) ∩ (b 2 + lin(P 2 )). Observe that if X is empty the theorem is proved. So we can assume that there exists a vector b in this intersection. Let us denote by V 1 and V 2 the vector spaces generated by P 1 and P 2 . Lemma 5.4 shows that rank(V j ) = dim(P j ) and from dim(b j + P j ) = dim(P j ) we deduce that dim(b j + P

j ) = rank(V j ). As X is included in b + V where V = V 1 ∩ V 2 ,
we deduce that if V is strictly included in V j for one j ∈ {1, 2} then dim(X) ≤ rank(V) < rank(V j ) = dim(b j + P j ) and the theorem is proved. So we can assume that V 1 = V 2 = V. Let us consider the conic sets C 1 = Q ≥0 P 1 and C 2 = Q ≥0 P 2 . Since P 1 and P 2 are asymptotically definable periodic sets, we deduce that C 1 and C 2 are finitely generated conic sets. Note that C 1 , C 2 ⊆ V. We introduce the intersection

C = C 1 ∩ C 2 .
Assume by contradiction that the vector space generated by C is equal to V. Let us consider a vector c in the interior of C. The characterization given by Lemma 3.5 shows that in this case int

(C) = int(C 1 ) ∩ int(C 2 ). Since int(C j ) = int(Q ≥0 P j ) we deduce that c ∈ (Q ≥0 P 1 ) ∩ (Q ≥0 P 2 ). Lemma 4.5 shows that c ∈ Q ≥0 (P 1 ∩ P 2 )
. By replacing c be a vector in N >0 c we can assume that c ∈ P 1 ∩ P 2 .

Let us prove that there exists

k 1 ∈ N such that b + k 1 c ∈ b 1 + P 1 . From b ∈ b 1 + lin(P 1 ) we deduce that there exists p 1 , p 1 ∈ P 1 such that b = b 1 + p 1 -p 1 .
Since -p 1 is in the vector space generated by C and c is in the interior of C, there exists n 1 ∈ N large enough such that n 1 c + (-p 1 ) ∈ C 1 . Hence there exists

n 1 ∈ N >0 such that n 1 n 1 c -n 1 p 1 ∈ P 1 . Thus n 1 n 1 c -p 1 ∈ (n 1 -1)p 1 + P 1 ⊆ P 1 . Hence b + k 1 c ∈ b 1 + P 1 with k 1 = n 1 n 1 .
Symmetrically we deduce that there exists

k 2 ∈ N such that b+k 2 c ∈ b 2 +P 2 . We have proved that b + (k 1 + k 2 )c ∈ (b 1 + P 1 ) ∩ (b 2 + P 2 )
and we get a contradiction since this intersection is supposed to be empty. We deduce that the vector space generated by C is strictly included in V. Lemma 5.5 shows that there exists a vector h ∈ V\{0} such that:

C 1 ⊆ v ∈ V | d i=1 h(i)v(i) ≥ 0 C 2 ⊆ v ∈ V | d i=1 h(i)v(i) ≤ 0
By replacing h by a vector in N >0 h we can assume that h ∈ Z d . Now let us consider

x ∈ X. Since x -b 1 ∈ C 1 we deduce that d i=1 h(i)(x(i) -b 1 (i)) ≥ 0 and since x - b 2 ∈ C 2 we deduce that d i=1 h(i)(x(i) -b 2 (i)) ≤ 0. We introduce the integers z 1 = d i=1 h(i)b 1 (i) and z 2 = d i=1 h(i)b 2 (i).
We have proved that X can be decomposed into a finite union of slices X = z2 z=z1 X z where:

X z = x ∈ X | d i=1 h(i)x(i) = z
Let us prove that dim(X z ) < rank(V). If X z is empty the relation is immediate. If X z is non empty let us consider x ∈ X z and observe that X z ⊆ x + W where:

W = v ∈ V | d i=1 h(i)v(i) = 0
Note that h ∈ V\W. We deduce that W is strictly included in V and in particular rank(W) < rank(V). Hence dim(X z ) < rank(V).

From X = z2 z=z1 X z and dim(X z ) < rank(V) for every z, we deduce that dim(X) < rank(V) and the theorem is proved.

Presburger Invariants

Given a relation R over Z d and two sets X, Y ⊆ Z d we introduce the forward image post R (X) and the backward image pre R (Y) defined by the following equalities:

post R (X) = x∈X {y ∈ Z d | (x, y) ∈ R} pre R (Y) = y∈Y {x ∈ Z d | (x, y) ∈ R} We say that a set X ⊆ Z d is a forward invariant for R if post R (X) ⊆ X and we say that a set Y ⊆ Z d is a backward invariant for R if pre R (Y) ⊆ Y.
In the reminder of this section we prove the following Theorem 6.1. All the other results or definitions introduced in this section are not used in the sequel. Proof. Let us first prove that post R (X) is an almost semilinear set. We consider a Presburger set S ⊆ Z d . Observe that X × S is a Presburger relation. Since R is an almost semilinear relation we deduce that R ∩ (X × S) can be decomposed into a finite union k j=1 (a j , b j ) + R j with k ∈ N, (a j , b j ) ∈ Z d × Z d and R j is an asymptotically definable periodic relation. We deduce that post R (X) ∩ S = k j=1 b j + P j where

P j = {v ∈ Z d | ∃(u, v) ∈ R j }. Since R j is a periodic relation we deduce that P j is a periodic set. Moreover since Q ≥0 R j is definable we deduce that C j = {v ∈ Q d | ∃(u, v) ∈ Q ≥0 R j } is definable. Let us prove that Q ≥0 P j = C j . By construction we have P j ⊆ C j . Since C j is conic we deduce that Q ≥0 P j ⊆ C j . For the converse inclusion let v ∈ C j . There exists u ∈ Q d such that (u, v) ∈ Q ≥0 R j .
Hence there exists λ ∈ Q ≥0 such that (u, v) ∈ λR j . Let us consider n ∈ N >0 such that nλ j ∈ N and observe that (nu, nv) ∈ (nλ)R j ⊆ R j since R j is periodic. Thus nv ∈ P j and we have proved that v ∈ Q ≥0 P j . Hence Q ≥0 P j = C j is a definable conic set and we have proved that post R (X) is an almost semilinear set. From pre R (Y) = post R -1 (Y) with R -1 = {(y, x) | (x, y) ∈ R} we deduce that pre R (Y) is an almost semilinear set. Now, let us prove Theorem 6.1. We consider a reflexive and transitive almost semilinear relation R * . We introduce the notion of separators. A separator is a couple (X, Y) of Presburger sets such that the intersection R * ∩ (X × Y) is empty. Since R * is reflexive, the intersection X ∩ Y is empty. The Presburger set D = Z d \(X ∪ Y) is called the domain of (X, Y). We observe that a separator (X, Y) with an empty domain is a partition of Z d such that X is a Presburger forward invariant and Y is a Presburger backward invariant. In particular Theorem 6.1 is obtained thanks to the following Lemma 6.3 with an immediate induction. Lemma 6.3. Let (X 0 , Y 0 ) be a separator with a non-empty domain D 0 . There exists a separator (X, Y) with a domain D such that X 0 ⊆ X, Y 0 ⊆ Y and dim(D) < dim(D 0 ).

Proof. We first observe that a couple (X, Y) of Presburger sets is a separator if and

only if post R * (X) ∩ pre R * (Y) = ∅ if and only if post R * (X) ∩ Y = ∅ if and only if pre R * (Y) ∩ X = ∅.
Since R * is an almost semilinear relation we deduce that post R * (X 0 ) is an almost semilinear set. As D 0 is a Presburger set, we deduce that post R * (X 0 ) ∩ D 0 = k j=1 b j + P j where b j ∈ Z d and P j ⊆ Z d is an asymptotically definable periodic set. We introduce the following Presburger set:

S = k j=1 b j + lin(P j ) Observe that post R * (X 0 ) ∩ D 0 ⊆ S. We deduce that the set Y = Y 0 ∪ (D 0 \S) is such that post R * (X 0 ) ∩ Y = ∅. Hence (X 0 , Y) is a separator.
Symmetrically, since R * is an almost semilinear relation we deduce that pre R * (Y) is an almost semilinear set. As D 0 is a Presburger set, we deduce that pre R * (Y)∩D 0 = n l=1 c l + Q l where c l ∈ Z d and Q l ⊆ Z d is an asymptotically definable periodic set. We introduce the following Presburger set:

T = n l=1 c l + lin(Q l ) Observe that pre R * (Y) ∩ D 0 ⊆ T. We deduce that the set X = X 0 ∪ (D 0 \T) is such that pre R * (Y) ∩ X = ∅. Hence (X, Y) is a separator.
Let us introduce the domain D of (X, Y). We have the following equality where Z j,l = (b j + lin(P j )) ∩ (c l + lin(Q l )):

D = D 0 ∩ ( 1≤j≤k 1≤l≤n Z j,l ) As (X, Y) is a separator we deduce that post R * (X)∩pre R * (Y) is empty. As b j +P j ⊆ post R * (X 0 ) ⊆ post R * (X) and c l + Q l ⊆ pre R * (Y)
we deduce that the intersection (b j + P j ) ∩ (c l + Q l ) is empty. Theorem 5.2 shows that dim(Z j,l ) < max{dim(b j + P j ), dim(c l + Q l )}. Since b j + P j ⊆ D 0 and c l + Q l ⊆ D 0 we deduce that dim(b j + P j ) ≤ dim(D 0 ) and dim(c l + Q l ) ≤ dim(D 0 ). We have proved that dim(D) < dim(D 0 ).

Vector Addition Systems

In this section we introduce the Vector Addition Systems, the production relations and a well order over the set of runs of Vector Addition Systems.

A Vector Addition System (VAS) is a finite subset A ⊆ Z d . A marking is a vector m ∈ N d . The semantics of vector addition systems is obtained by introducing for every word w = a 1 . . . a k of vectors a j ∈ A the relation w -→ over the set of markings defined by x w -→ y if there exists a word ρ = m 0 . . . m k of markings m j ∈ N d such that (x, y) = (m 0 , m k ) and m j = m j-1 + a j for every j ∈ {1, . . . , k}. The word ρ is unique and it is called the run from x to y labeled by w. The marking x is called the source of ρ and it is denoted by src(ρ), and the marking y is called the target of ρ and it is denoted by tgt(ρ). The set of runs is denoted by Ω. The following Lemma 7.2 shows that * -→ ρ seens as a subset of Z 2d is periodic for every run ρ as a composition of periodic relations (see Fig. 9). Note that in Section 8 we prove that these periodic relations are asymptotically definable. We introduce a well order over the set of runs based on the following Lemma 7.3

Lemma 7.3. The following inclusion holds for every run ρ:

(src(ρ), tgt(ρ))+ * -→ ρ ⊆ * -→
Proof. Assume that ρ = m 0 . . . m k with m j ∈ N d , and let (r, s) be a couple in the production relation * -→ ρ . Since this relation is defined as a composition, there exists a sequence (v j ) 0≤j≤k+1 of vectors v j ∈ N d satisfying the following relations with v 0 = r and v k+1 = s:

v 0 * -→ m0 v 1 • • • v k * -→ m k v k+1
We introduce the vector a j = m j -m j-1 for every j ∈ {1, . . . , k}. Since m j-1 aj -→ m j we deduce that m j-1 + v j aj -→ m j + v j . Moreover, as v j * -→ mj v j+1 , there exists a word w j ∈ A * such that m j + v j wj --→ m j + v j+1 . We deduce that the following relation holds:

m 0 + v 0 w0a1w1...a k w k ----------→ m k + v k+1 Therefore (m 0 , m k ) + (v 0 , v k+1
) is in the reachability relation.

We introduce the order over the set of runs defined by ρ ρ if the following inclusion holds:

(src(ρ ), tgt(ρ ))+ * -→ ρ ⊆ (src(ρ), tgt(ρ))+ * -→ ρ
In the reminder of this section we prove the following theorem. All the other results or definitions introduced in this section are not used in the sequel.

Theorem 7.4. The order is well.

The order is proved well thanks to the Higmann's Lemma. We first recall this lemma. Let us consider an order over a set S. We introduce the order * over the set of words over S defined by u * v where u = s 1 . . . s k with s j ∈ S if there exists a sequence (t j ) 1≤j≤k with t j ∈ S and s j t j and a sequence (w j ) 0≤j≤k of words w j ∈ S * such that v = w 0 t 1 w 1 . . . t k w k . Lemma 7.5 (Higmann's Lemma). The ordered set (S * , * ) is well for every well ordered set (S, ).

We associate to every run ρ = m 0 . . . m k the word α(ρ) = (a 1 , m 1 ) . . . (a k , m k ) where a j = m j -m j-1 . Note that α(ρ) is a word over the alphabet S = A × N d . We introduce the order over this alphabet by (a, m) (a , m ) if a = a and m ≤ m . Since A is a finite set and ≤ is a well order over N d , we deduce that is a well order over S. From the Higmann's lemma, the order * is well over S * . We introduce the well order ¢ over the set of runs defined by ρ ¢ ρ if α(ρ) * α(ρ ), src(ρ) ≤ src(ρ ) and tgt(ρ) ≤ tgt(ρ ). The following lemma provides a useful characterization of this order.

Lemma 7.6. Let ρ = m 0 . . . m k be a run and let ρ be another run. We have ρ ¢ ρ if and only if there exists a sequence (v j ) 0≤j≤k+1 of vectors in N d such that ρ = ρ 0 . . . ρ k where ρ j is a run from m j + v j to m j + v j+1 .

Proof. We introduce the sequence (a j ) 1≤j≤k defined by a j = m j -m j-1 .

Assume first that ρ ¢ ρ . Since α(ρ) * α(ρ ) we get α(ρ ) = w 0 (a 1 , m 1 )w 1 . . . (a k , m k )w k where w j ∈ S * and m j ≥ m j . We introduce the sequence (v j ) 0≤j≤k+1 defined by v 0 = src(ρ )src(ρ), v k+1 = tgt(ρ ) -tgt(ρ) and v j = m j -m j for every j ∈ {1, . . . , k}. Observe that v j ∈ N d for every j ∈ {0, . . . , k + 1}. We deduce that ρ can be decomposed into ρ = ρ 0 . . . ρ k where ρ j is the run from m j + v j to m j + v j+1 such that α(ρ j ) = w j .

Conversely let (v j ) 0≤j≤k+1 be a sequence of vectors in N d such that ρ = ρ 0 . . . ρ k where ρ j is a run from m j + v j to m j + v j+1 . We deduce that we have the following equality where m j = m j + v j and a j ∈ A:

α(ρ ) = α(ρ 0 )(a 1 , m 1 )α(ρ 1 ) . . . (a k , m k )α(ρ k )
Observe that a j = tgt(ρ j-1 ) -m j = (m j + v j ) -(m j-1 + v j ) and in particular a j = a j . We deduce that α(ρ) * α(ρ ). Moreover, since src(ρ) ≤ src(ρ ) and tgt(ρ) ≤ tgt(ρ ) we deduce that ρ ¢ ρ .

Since ¢ is a well order, the following lemma shows that is a well order. We have proved Theorem 7.4. Lemma 7.7. ρ ¢ ρ implies ρ ρ .

Proof. Assume that ρ = m 0 . . . m k . Lemma 7.6 shows that there exists a sequence (v j ) 0≤j≤k+1 of vectors in N d such that ρ = ρ 0 . . . ρ k where ρ j is a run from m j + v j to m j + v j+1 . Lemma 7.3 shows that (src(ρ j ), tgt(ρ

j ))+ * -→ ρ j ⊆ * -→. Hence (v j , v j+1 )+ * -→ ρ j ⊆ * -→ mj . We deduce that (v 0 , v k+1 )+ * -→ ρ ⊆ *
-→ ρ by composition. Since (src(ρ ), tgt(ρ )) = (src(ρ), tgt(ρ)) + (v 0 , v k+1 ) we get ρ ρ from the previous inclusion.

Asymptotically Definable Production Relations

In this section we prove that production relations are asymptotically definable (Theorem 8.1). All the other results or definitions introduced in the section are not used in the sequel.

Theorem 8.1. Production relations are asymptotically definable.

The following lemma shows that asymptotically definable periodic relations are stable by composition. In particular it is sufficient to prove that production relations * -→ m are asymptotically definable for every marking m ∈ N d in order to deduce that production relations * -→ ρ are asymptotically definable for every run ρ. Lemma 8.2. We have

Q ≥0 (R 1 • R 2 ) = (Q ≥0 R 1 ) • (Q ≥0 R 2 ) for every periodic rela- tions over Z d . Proof. We have R 1 ⊆ Q ≥0 R 1 and R 2 ⊆ Q ≥0 R 2 . Thus R 1 • R 2 ⊆ C where C = (Q ≥0 R 1 ) • (Q ≥0 R 2 ). As C is a conic set we get Q ≥0 (R 1 • R 2 ) ⊆ C. For the converse inclusion, let us consider (x, z) ∈ C. There exists y ∈ Q d such that (x, y) ∈ Q ≥0 R 1 and (y, z) ∈ Q ≥0 R 2 . There exists λ 1 , λ 2 ∈ Q ≥0 such that (x, y) ∈ λ 1 R 1 and (y, z) ∈ λ 2 R 2 .
We introduce n 1 , n 2 ∈ N >0 such that n 1 λ 1 ∈ N and n 2 λ 2 ∈ N and we deduce that n(x, y) ∈ R 1 and n(y,

z) ∈ R 2 with n = n 1 n 2 . Hence n(x, z) ∈ R 1 • R 2 . We deduce that (x, z) ∈ Q ≥0 (R 1 • R 2 ).
Theorem 3.8 shows that the conic set Q ≥0 * -→ m is definable if and only if the following conic set is finitely generated for every vector space

V ⊆ Q d × Q d : (Q ≥0 * -→ m ) ∩ V We introduce the periodic relation * -→ m,V defined as the intersection * -→ m ∩V . Let us observe that (Q ≥0 * -→ m ) ∩ V is equal to Q ≥0 * -→ m,V
. So, we just have to prove that the conic set Q ≥0 * -→ m,V is finitely generated for every m ∈ N d and for every vector space

V ⊆ Q d × Q d . We introduce the set Ω m,V of runs ρ such that (src(ρ), tgt(ρ)) -(m, m) is in (N d × N d ) ∩ V . Note that a couple (r, s) ∈ N d × N d satisfies r * -→ m,V
s if and only if there exists a run ρ ∈ Ω m,V such that src(ρ) = m + r and tgt(ρ) = m + s. We introduce the set Q m,V of markings q that occurs in at least one run ρ ∈ Ω m,V . In general the set Q m,V is infinite. We consider the set I m,V of i ∈ {1, . . . , d} such that {q(i) | q ∈ Q m,V } is infinite. We observe that if i ∈ I m,V there exists a sequence of markings in Q m,V such that the ith component is strictly increasing. We are going to prove that there exists a sequence of markings in Q m,V such that every component in I m,V is strictly increasing. This property is proved by introducing the intraproductions. An intraproduction for (m, V ) is a triple (r, x, s) such that x ∈ N d , (r, s) ∈ (N d × N d ) ∩ V and such that:

r * -→ m x * -→ m s Since *
-→ m is a periodic relation we deduce that the set of intraproductions is stable by addition. In particular m + nx occurs in at least one run of Ω m,V for every intraproduction (r, x, s) and for every n ∈ N. Hence, if x(i) > 0 then i ∈ I m,V . An intraproduction for (m, V ) is said to be total if x(i) > 0 for every i ∈ I m,V . Lemma 8.3. There exists a total intraproduction for (m, V ).

Proof. Since finite sums of intraproductions are intraproductions, it is sufficient to prove that for every i ∈ I m,V there exists an intraproduction (r, x, s) for (m, V ) such that x(i) > 0. We fix i ∈ I.

Let us first prove that there exists q ≤ q in Q m,V such that q(i) < q (i). Since i ∈ I there exists a sequence (q n ) n∈N of markings q n ∈ Q m,V such that (q n (i)) n∈N is strictly increasing. Since (N d , ≤) is well ordered, we can extract for this sequence a subsequence that is non decreasing for ≤. We have proved that there exists q ≤ q in Q m,V such that q(i) < q (i).

As q ∈ Q m,V then q occurs in a run in Ω m,V . Hence there exists (r, s)

∈ (N d × N d ) ∩ V such that: m + r * -→ q * -→ m + s Symmetrically, as q ∈ Q m,V there exists (r , s ) ∈ (N d × N d ) ∩ V such that: m + r * -→ q * -→ m + s
Let us introduce v = qq. We deduce:

-(m + r ) + r * -→ q + r from m + r * -→ q . -q + (v + r) * -→ (m + s) + (v + r) from q * -→ m + s. -(m + r) + (v + s) * -→ q + (v + s) from m + r * -→ q. -q + s * -→ (m + s ) + s from q * -→ m + s .
Since q + r = q + v + r and q + v + s = q + s, we have proved the following relations where x = s + v + r:

r + r * -→ m x * -→ m s + s
As (r+r , s+s ) ∈ (N d ×N d )∩V we deduce that (r+r , x, s+s ) is an intraproduction for (m, V ). Since x(i) > 0 we are done. -→ y if there exists a word ρ = m 0 . . . m k of extended markings relaxed over I such that (x, y) = (m 0 , m k ) and m j (i) = m j-1 (i) + a j (i) for every j ∈ {1, . . . , k} and for every i ∈ {1, . . . , d}\I. The word ρ is unique and it is called the run from x to y labeled by w.

We introduce the finite graph G

m,V = (Q, A, E) where Q = {q I m,V | q ∈ Q m,V } and where E = {(p I m,V , a, q I m,V ) | p, q ∈ Q m,V ∧q = p+a}. We introduce the periodic relation R m,V of couples (r, s) ∈ (N d × N d ) ∩ V such that r(i) = s(i) = 0
for every i ∈ {1, . . . , d}\I m,V and such that there exists a cycle in G m,V on the state m I m,V labeled by a word a 1 . . . a k where a j ∈ A such that r + k j=1 a j = s. Lemma 8.4. The periodic relation R m,V is Presburger.

Proof. This is a classical result based on the fact that the Parikh image of a regular language is Presburger.

Lemma 8.5. The following equality holds:

Q ≥0 R m,V = Q ≥0 * -→ m,V
Proof. Let us first prove the inclusion ⊇. Let (r, s) such that r * -→ m,V s. In this case there exists a word w ∈ A * such that m + r w -→ m + s. Observe that m + nr and m + ns are in Q m,V for every n ∈ N. Hence r(i) > 0 or s(i) > 0 implies i ∈ I m,V and we deduce that m I m,V w -→ m I m,V . Therefore w is the label of cycle in G m,V on m I m,V . We have proved that (r, s) ∈ R m,V . Now let us prove the inclusion ⊆. We consider (r, s) ∈ R m,V . In this case (r, s) ∈ (N d × N d ) ∩ V satisfies r(i) = s(i) = 0 for every i ∈ I m,V and there exists a word w = a 1 . . . a k of vectors a j ∈ A that labels a cycle in G m,V on m I m,V and such that m + r + k j=1 a j = m + s. Let us consider a total intraproduction (r , x, s ) for (m, V ). Given p ∈ N and j ∈ {0, . . . , k} we introduce the following vector m p,j :

m p,j = m + r + px + a 1 + • • • + a j
Let us first prove that there exists p ∈ N such that m p,j (i) ∈ N for every i ∈ I m,V and j ∈ {0, . . . , k}. Let i ∈ I m,V and j ∈ {0, . . . , k}, since x(i) > 0, there exists p i,j ∈ N such that m p,j (i) ∈ N for every p ≥ p i,j . We deduce that there exists p ∈ N such that m p,j (i) ∈ N for every i ∈ I m,V and j ∈ {0, . . . , k}. Now we prove that m p,j (i) ∈ N for every i ∈ {1, . . . , d}\I m,V and j ∈ {0, . . . , k}. Let j ∈ {0, . . . , k}. Since w is the label of a cycle on m I m,V , there exists an extended marking q j relaxed over I m,V such that the following relation holds:

m I m,V a1...aj ----→ q j
We deduce that for every i ∈ {1, . . . , d}\I m,V we have m(i) + a 1 (i) + • • • + a j (i) = q j (i). Since r(i) = 0 and x(i) = 0 we get m p,j (i) ∈ N.

We have proved that m p,j ∈ N d for every j ∈ {0, . . . , k}. Since m p,j -m p,j-1 = a j we deduce that ρ p = m p,0 . . . m p,k is a run. Note that m p,0 = m + px + r and m p,k = m + px + r +

m + pr + nr * -→ m + ps + ns Hence p(r , s ) + N(r, s) ⊆ * -→ m,V . Thus (r, s) ∈ Q ≥0 * -→ m,V . From the inclusion R m,V ⊆ Q ≥0 * -→ m,V we get the inclusion Q ≥0 R m,V ⊆ Q ≥0 * -→ m,V .
Lemma 8.6. The conic set Q ≥0 P is finitely generated for every Presburger periodic set P.

Proof. Let us consider a Presburger periodic set P. Since P is Presburger then P = k j=1 b j + P j where b j ∈ Z d and P j ⊆ Z d is a finitely generated periodic set. We introduce the finitely generated conic set C = k j=1 (Q ≥0 b j + C j ) where C j is the finitely generated conic set C j = Q ≥0 P j . Since P ⊆ C and C is a conic set we deduce the inclusion Q ≥0 P ⊆ C. As C is finitely generated we deduce that C is closed. Hence Q ≥0 P ⊆ C. For the other inclusion let p ∈ P j . For every n ∈ N we have b j +np ∈ P. Hence 1 n b j + p ∈ Q ≥0 P for every n ∈ N >0 . We deduce that p ∈ Q ≥0 P. Therefore P j ⊆ Q ≥0 P. We get C j ⊆ Q ≥0 P. As Q ≥0 b j ⊆ Q ≥0 P ⊆ Q ≥0 P we have proved the inclusion C ⊆ Q ≥0 P. Hence the previous inclusion is in fact an equality. Now, we can prove Theorem 8.1. Lemma 8.4 shows that R m,V is a Presburger periodic relation. Lemma 8.6 proves that the conic set Q ≥0 R m,V is finitely generated. Lemma 8.5 shows that Q ≥0 * -→ m,V is finitely generated. Hence (Q ≥0 * -→ m ) ∩ V is a finitely generated conic set for every vector space V ⊆ Q d × Q d . Theorem 3.8 shows that the conic relation Q ≥0

We are interested in proving that * -→ is an almost semilinear relation. We first inspect the intersection * -→ ∩((m, n) + P ) where (m, n) ∈ N d × N d and P ⊆ N d × N d is a finitely generated periodic relation. We introduce the order ≤ P over P defined by p ≤ P p if p ∈ p + P . Since P is finitely generated we deduce that ≤ P is a well order over P (Dickson's Lemma). We introduce the set Ω m,P,n of runs ρ such that (src(ρ), tgt(ρ)) ∈ (m, n) + P . This set is well ordered by the relation P defined by ρ P ρ if ρ ρ , (src(ρ), tgt(ρ)) -(m, n) ≤ P (src(ρ ), tgt(ρ )) -(m, n). We deduce that min P (Ω m,P,n ) is finite. Let us prove ⊆. Let (x , y ) in the intersection * -→ ∩((m, n) + P ). There exists a run ρ ∈ Ω m,P,n such that x = src(ρ ) and y = tgt(ρ ). Since P is a well order, there exists ρ ∈ min P (Ω m,P,n ) such that ρ P ρ . We deduce that (x , y ) is in (src(ρ), tgt(ρ))+ * -→ ρ . We get (x , y ) ∈ (src(ρ), tgt(ρ)) + ( * -→ ρ ∩P ) and we have proved the inclusion ⊆. Theorem 8.1 shows * -→ ρ is an asymptotically definable periodic relation. Since P is a finitely generated periodic relation we deduce that P is asymptotically definable. Lemma 4.5 shows that the class of asymptotically definable periodic relations is stable by finite intersections. We deduce that * -→ ρ ∩P is asymptotically definable. Thanks to the previous lemma we have proved that * -→ is almost semilinear and Theorem 9.1 is proved.

Conclusion

The reachability problem for Vector Additions Systems consists to decide for a triple (m, A, n) where m, n are two markings of a Vector Addition System A if there exists a word w ∈ A * such that m w -→ n. The following algorithm decides this problem. The correctness is immediate since when the algorithm returns "reachable" we deduce that there exists a word w ∈ A * such that m w -→ n and when it returns "unreachable" we deduce a Presburger formula ψ that denotes a set I satisfying m ∈ I (since ψ(m) is true), n ∈ I (since ¬ψ(n) is true), and such that I is a forward invariant (since x ≥ 0 ∧ y ≥ 0 ∧ ψ(x) ∧ y ∈ x + A ∧ ¬ψ(y) is unsatisfiable). The termination is guaranteed by the following Theorem 10.1.

Theorem 10.1. For every pair of markings (m, n) in the complement of the reachability relation of a Vector Addition System, there exists a partition of the set of markings into a Presburger forward invariant that contains m and a Presburger backward invariant that contains n.

Proof. Let us consider X = {m} and Y = {n} and let R * be the reachability relation of the Vector addition system. Theorem 9.1 shows that R * is an almost semilinear relation. Since R * is reflexive and transitive and such that (X × Y) ∩ R * = ∅, Theorem 6.1 shows that there exists a partition of the set of markings into a Presburger forward invariant set that contains X and a Presburger backward invariant set that contains Y. This algorithm does not require the classical KLMST decomposition. Note however that the complexity of this algorithm is still open. In fact, the complexity depends on the minimal size of a word w ∈ A * such that m w -→ n if m * -→ n, and the minimal size of a Presburger formula ψ(x) denoting a forward invariant I such that m ∈ I and n ∈ I otherwise. We left as an open question the problem of computing lower and upper bounds for these sizes. Note that the VAS exhibiting a large (Ackermann size) but finite reachability set given in [START_REF] Mayr | The complexity of the finite containment problem for petri nets[END_REF] does not directly provide an Ackermann lower-bound for these sizes since Presburger forward invariants can over-approximate reachability sets.

As future work we are interested in providing complexity bounds on formulas in FO (Q, +, ≤, 0, 1) denoting the definable conic sets Q ≥0

Fig. 3 .

 3 Fig. 3. A picture of the duality lemma 3.5

Fig. 5 .

 5 Fig. 5. An asymptotically definable periodic set.

Example 4 . 4 .

 44 The periodic set P

Definition 4 . 6 .

 46 An almost semilinear set is a subset X ⊆ Z d such that for every Presburger set S ⊆ Z d the set X ∩ S is a finite union of sets b + P where b ∈ Z d and P ⊆ Z d is an asymptotically definable periodic set.

Fig. 6 .Example 4 . 7 .

 647 Fig.6. An asymptotically definable periodic set that is not almost semilinear.

  be decomposed as a finite union of sets b + P where b ∈ Z d and P ⊆ Z d is an asymptotically definable periodic set.

Fig. 7 .

 7 Fig. 7. A figure for Theorem 5.2 and Example 5.3.

d

  i=1 a(i)c(i) ≥ 0. Since the set {c ∈ Q d | d i=1 a(i)c(i) ≥ 0} is closed we deduce that for every c ∈ int(C ≥ ) = C ≥ the same inequality holds. Now let us consider c ∈ int(C ≤ ). In this case d i=1 b(i)c(i) ≥ 0. Since a + b = 0 we get d i=1 a(i)c(i) ≤ 0. We deduce that this inequality holds for every c ∈ C ≤ .

Theorem 6 . 1 .Lemma 6 . 2 .

 6162 Let R * be a reflexive and transitive almost semilinear relation over Z d and let X, Y ⊆ Z d be two Presburger sets such that R * ∩(X×Y) is empty. There exists a partition of Z d into a Presburger forward invariant that contains X and a Presburger backward invariant that contains Y. We first prove the following lemma. The sets post R (X) and pre R (Y) are almost semilinear for every almost semilinear relation R ⊆ Z d × Z d and for every Presburger sets X, Y ⊆ Z d

The+ r m + s 0 Fig. 8 .Example 7 . 1 .

 0871 Fig. 8. The production relation of a marking m.

Lemma 7 . 2 .Fig. 9 .

 729 Fig. 9. Production relations are periodic.

  Let us introduce an additional element ∞ ∈ N and let N ∞ = N ∪ {∞}. A vector in N d ∞ is called an extended marking and the set I = {i ∈ {1, . . . , d} | m(i) = ∞} is called the set of relaxed components of an extended marking m. Given a finite set I ⊆ {1, . . . , d} and a marking m ∈ N d , we denote by m I the extended marking defined by m I (i) = ∞ if i ∈ I and m I (i) = m(i) if i ∈ I. Given a word w = a 1 . . . a k of vectors a j ∈ A, we extend the relation w -→ over the set of extended markings relaxed over a set I by x w

k

  j=1 a j = m + px + s. We have proved that the following relation holds: m + px + r w -→ m + px + s In particular (r, s) is in the production relation * -→ m where m = m + px. Since a production relation is periodic we get m + nr * -→ m + ns for every n ∈ N. As (pr , px, ps ) is an intraproduction for (m, V ) we get m + pr * -→ m * -→ m + ps . We deduce the relation (m + pr ) + nr * -→ m + nr from (m + pr ) * -→ m , and the relation m + ns * -→ (m + ps ) + ns from m * -→ (m + ps ). We deduce that the following relation holds for every n ∈ N:

Lemma 9 . 2 .

 92 The following equality holds:* -→ ∩((m, n) + P ) = ρ∈min P (Ω m,P,n ) (src(ρ), tgt(ρ)) + ( * -→ ρ ∩P )Proof. Let us first prove ⊇. Let ρ ∈ Ω m,P,n . Lemma 7.3 shows that the inclusion (src(ρ), tgt(ρ))+ * -→ ρ ⊆ * -→ holds. Since (src(ρ), tgt(ρ)) ∈ (m, n) + P and P is periodic we deduce the inclusion ⊇.

1 9 x

 9 Reachability( m , A , n ) formula ψ of length k 8 if ψ(m) and ¬ψ(n) are true and ≥ 0 ∧ y ≥ 0 ∧ ψ(x) ∧ y ∈ x + A ∧ ¬ψ(y) unsat 10 return ''unreachable'' 11 k ← k + 1

This version extends the POPL'2011 paper with additional figures and examples. Some classes of sets get more intuitive names like the polytope conic sets, the polytope periodic sets, and the Petri sets that are now called the definable conic sets, the asymptotically definable periodic sets, and the almost semilinear sets.