LSV Sylvain Schmitz

Automata Column: The Complexity of Reachability in Vector Addition Systems

 proved the first complexity upper bound in the general case. The purpose of this column is to present the main ideas behind these two results, and more generally survey the current state of affairs.

INTRODUCTION

Vector addition systems with states (VASS), or equivalently Petri nets, find a wide range of applications in the modelling of concurrent, chemical, biological, or business processes. Maybe more importantly for this column, their algorithmics, and in particular the decidability of their reachability problem [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] Lambert | A structure to decide reachability in Petri nets[END_REF][START_REF] Leroux | Vector addition system reachability problem: a short self-contained proof[END_REF], is the cornerstone of many decidability results in logic, automata, verification, etc.-see Section 5 for a few examples.

In spite of its importance, fairly little is known about the computational complexity of the reachability problem. Regarding the general case, the inclusive surveys on the complexity of decision problems on VASS by [START_REF] Esparza | Decidability issues for Petri nets -a survey[END_REF] and [START_REF] Esparza | Decidability and complexity of Petri net problems -an introduction[END_REF] could only point to the EXPSPACE lower bound of [START_REF] Lipton | The reachability problem requires exponential space[END_REF] and to the fact that the running time of the known algorithms is not primitive recursive: no complexity upper bound was known, besides decidability first proven in 1981 by Mayr. When turning to restricted versions of the problem, the 2-dimensional case was only known to be in 2-EXP [START_REF] Howell | Some complexity bounds for problems concerning finite and 2-dimensional vector addition systems with states[END_REF] and NP-hard [START_REF] Rosier | A multiparameter analysis of the boundedness problem for vector addition systems[END_REF].

This state of affair has very recently improved with two articles:

- [START_REF] Leroux | Demystifying reachability in vector addition systems[END_REF] have shown that reachability has a 'cubic Ackermann' upper bound, i.e. is in F ω 3 , by analysing the complexity of the classical algorithm developed and refined by [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], and [START_REF] Lambert | A structure to decide reachability in Petri nets[END_REF]. Here, F ω 3 is a non primitive-recursive complexity class, but among the lower multiplyrecursive ones. The main ingredients for this analysis are the fast-growing complexity bounds for termination proofs by well-quasi-orders and ordinal ranking functions from [START_REF] Figueira | Ackermannian and primitive-recursive bounds with Dickson's Lemma[END_REF][START_REF] Schmitz | Complexity bounds for ordinal-based termination[END_REF]]. [START_REF] Blondin | Reachability in two-dimensional vector addition systems with states is PSPACE-complete[END_REF] have shown that reachability in 2-dimensional VASS is PSPACE-complete by a careful analysis of the complexity of the 'flattenings' of [START_REF] Leroux | On flatness for 2-dimensional vector addition systems with states[END_REF] for the upper bound, and by applying recent results on bounded one-counter automata by [START_REF] Fearnley | Reachability in two-clock timed automata is PSPACE-complete[END_REF] for the lower bound.

Organisation of the Column. The main focus of the column is the complexity of the algorithm of [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], and [START_REF] Lambert | A structure to decide reachability in Petri nets[END_REF]. Section 3 presents it in an informal manner on an example before explaining the main points of its complexity analysis following [START_REF] Leroux | Demystifying reachability in vector addition systems[END_REF].

This cubic Ackermann upper bound leaves a considerable gap with the EXPSPACE lower bound of [START_REF] Lipton | The reachability problem requires exponential space[END_REF]. Rather than attacking this complexity gap directly, it makes sense to try to obtain tight complexity bounds on restrictions of the general reachability problem, and we shall see one such restriction in Section 4: the 2dimensional case and its tight PSPACE-completeness proven by [START_REF] Blondin | Reachability in two-dimensional vector addition systems with states is PSPACE-complete[END_REF]. q0 q1 t1 : (1, 1, -1) t2 : (-1, 0, 1) t3 : [START_REF] Schmitz | Complexity hierarchies beyond ELEMENTARY[END_REF]0,0) t5 : (0, 0, 0) t4 : (0, -1, 0) Fig. 1: A 3-dimensional VASS.

The last two sections of the column are more in the spirit of a survey. To better emphasise the importance of the reachability problem, Section 5 provides a glimpse of the many problems known to be interreducible with reachability in VASS. Section 6 finally presents a small selection of VASS extensions and what is known about their reachability problems, pointing to several open problems.

VECTOR ADDITION SYSTEMS WITH STATES

For the needs of the automata column, it is natural to first present vector addition systems with states (VASS) [START_REF] Hopcroft | On the reachability problem for 5-dimensional vector addition systems[END_REF], which are essentially finitestate transition systems with d-dimensional vectors of weights in Z d attached to their transitions. Formally, a VASS is a tuple

V = Q, d, T where Q is a finite set of 'control' states, d in N is a non-negative dimension, and T ⊆ Q × Z d × Q is a finite set of transitions.
Semantics and Runs. The operational semantics of such a system is captured by an infinite transition system S V over the set of configurations Confs

V def = Q × N d , with a step (q, u) t - → V (q , u
+ a) defined whenever t = (q, a, q ) belongs to T ; note that u + a must belong to N d for such a step to be possible. A run from a configuration c 0 to a configuration c is a finite sequence of steps c 0 t1

-→ V c 1 t2 -→ V c 2 • • • c -1 t -→ V c , which can also be written c 0 t1•••t ----→ V c . Finally, let us write c 0 → * V c if there exists a finite sequence of transitions σ ∈ T * such that c 0 σ -→ V c .
Reachability. The reachability problem refers to reachability in the infinite system S V : input: a VASS V and two configurations c and c in Confs V , question: can c reach c , i.e. does c → * V c ? This problem was famously shown to be decidable by [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] Lambert | A structure to decide reachability in Petri nets[END_REF], and [START_REF] Leroux | Vector addition system reachability problem: a short self-contained proof[END_REF] (see Section 3 for more details): THEOREM 2.1 (DECIDABILITY THEOREM). Reachability in VASS is decidable.

Example 2.2. Consider for instance the 3-dimensional VASS of Figure 1 with Q def = {q 0 , q 1 } and T def = {t 1 , t 2 , t 3 , t 4 , t 5 }. One can check that (q 0 , 1, 0, 1) reaches (q 1 , 2, 2, 1), for instance by the run

(q 0 , 1, 0, 1) t1 -→ (q 0 , 2, 1, 0) t2 -→ (q 0 , 1, 1, 1) t1 -→ (q 0 , 2, 2, 0) t2 -→ (q 0 , 1, 2, 1) t3 -→ (q 1 , 2, 2, 1) . (1)
This is just one example of a run witnessing reachability; observe that any sequence of transitions in {t 1 t 2 , t 2 t 1 } n+2 t 3 t n 4 for n ≥ 0 would similarly do. Binary Encoding. Regarding complexity, one typically assumes a binary encoding of the integers of a VASS and of the source and target configurations: let

a def = p1 p2 p3 Q-q q t1 t2 t5 t4 t3
Fig. 2: A Petri net equivalent to the VASS of Figure 1.

max 1≤i≤d |a(i)| denote the infinity norm of a vector a in Z d ; then T def = max (q,a,q )∈T a can be exponential in the size of a VASS V = Q, d, T . The choice of a binary rather than a unary encoding has no impact in the general case-because there is a LOGSPACE reduction to the case where T ⊆ Q × {-1, 0, 1} d × Q (at the expense of increasing the dimension) and c = (q, 0) and c = (q , 0) for some states q, q -, but will be important in Section 4 for the 2-dimensional case.

Closely Related Models

Historically, VASS do not seem to have been studied before the works of Greibach [1978, see Section 5.1] and [START_REF] Hopcroft | On the reachability problem for 5-dimensional vector addition systems[END_REF]. Nevertheless, equivalent models had been investigated before, in particular the Petri nets of [START_REF] Petri | Kommunikation mit Automaten[END_REF] and vector addition systems (VAS) of [START_REF] Karp | Parallel program schemata[END_REF]. The absence of explicit control states makes these two classes of models rather convenient for the modelling of concurrent or distributed systems. 2 for the result of this construction on the VASS of Figure 1, where places are depicted as circles, transitions as rectangles, and flows as arrows)-'equivalence' here should be understood as far as the decision problems like reachability are concerned.

2.1.2. Vector Addition Systems. A VAS is a pair d, A where A is a finite subset of actions in Z d [START_REF] Karp | Parallel program schemata[END_REF]. It defines a transition system with configurations u in N d and steps u → u + a for a in A, again implicitly checking that u + a ≥ 0. Put differently, a VAS can be seen as a VASS with a singleton state set. Conversely, the finite control of a d-dimensional VASS can be encoded in an equivalent VAS by increasing the system's dimension to d + 3 [Hopcroft and Pansiot 1979, Lemma 2.1].

DECIDING REACHABILITY

Considered as one of the great achievements of theoretical computer science, the seminal 1981 decidability proof for the reachability problem by [START_REF] Mayr | An algorithm for the general Petri net reachability problem[END_REF] is the culmination of more than a decade of research into the topic, and builds notably on an q0, ω, ω, ω q1, ω, ω, ω q0, 1, 0, 1 q1, 2, 2, 1 t1 : (1, 1, -1)

t2 : (-1, 0, 1)

t3 : (1, 0, 0) t5 : (0, 0, 0) t4 : (0, -1, 0)

Fig. 3: The initial marked witness graph sequence ξ 0 = M 0 .

incomplete proof by [START_REF] Sacerdote | The decidability of the reachability problem for vector addition systems[END_REF]. This proof has been simplified two times since: one year later by [START_REF] Kosaraju | Decidability of reachability in vector addition systems[END_REF], and another ten years later by [START_REF] Lambert | A structure to decide reachability in Petri nets[END_REF]. At the heart of these three proofs lies a decomposition technique, which is called the Kosaraju-Lambert-Mayr-Sacerdote-Tenney (KLMST) decomposition. In a nutshell, the KLMST decomposition defines both -a structure (resp. regular constraint graphs for Mayr, generalised VASS for Kosaraju, and marked graph-transition sequences for Lambert) and -a condition for this structure to represent in some way the set of all runs witnessing reachability (resp. consistent marking, the θ condition, and the perfect condition).

The algorithms advanced by Mayr, Kosaraju, and Lambert compute this decomposition by successive refinements of the structure until the condition is fulfilled, by which time the existence of a run becomes trivial.

The KLMST decomposition has also been employed by [START_REF] Leroux | The general vector addition system reachability problem by Presburger inductive invariants[END_REF] to derive a new, very simple algorithm for reachability based on Presburger inductive invariants. [START_REF] Leroux | Vector addition system reachability problem: a short self-contained proof[END_REF] then re-proved the correctness of this new algorithm without referring to the KLMST decomposition, yielding an independent, compact self-contained decidability proof for VASS reachability.

In the following we will however focus on the 'classical' decomposition algorithm, and present the following result from [START_REF] Leroux | Demystifying reachability in vector addition systems[END_REF]]: THEOREM 3.1 (UPPER BOUND THEOREM). Reachability in VASS is in F ω 3 .

We will see in Section 3.2 what is F ω 3 . But let us first have a look at the KLMST decomposition algorithm.

An Example of a KLMST Decomposition

The reader is referred to the original article, and to the excellent accounts by M üller [1985] and [START_REF] Reutenauer | The mathematics of Petri nets[END_REF] for examples and details on the KLMST decomposition as defined by [START_REF] Kosaraju | Decidability of reachability in vector addition systems[END_REF]. Here we shall keep the description at an informal level, and see how the decomposition algorithm works in the case of Example 2.2 without entering its details. A witness graph is a finite strongly connected directed graph G = (S, E) with vertices S ⊆ Q × N d ω , and labelled edges E ⊆ S × T × S, such that the edge labels from T are consistent with the vertices from S. This means that, if (s, t, s ) is an edge in E with transition t = (q, a, q ) from T as label, then s = (q, u) for some u in N d ω and s = (q , u + a). Note that these conditions together imply that all the vertices in the graph share the same set I ⊆ {1, . . . , d} of ω-components.

A marked witness graph M = (G, c in , s in , c out , s out ) is further endowed with distinguished input and output vertices s in and s out from S, along with input and output constraints c in and c out taken from Q × N d ω , such that for all 1 ≤ i ≤ d, s in (i) = ω implies c in (i) = s in (i), and similarly for the output vertex and constraint. In other words, s in and c in agree on their finite components. This entails that I in the set of ω-components of c in is a subset of I the set of ω-components of s in , and similarly I out ⊆ I.

Finally, a marked witness graph sequence ξ is a sequence

ξ = M 0 , t 1 , M 1 , . . . , t k , M k (2)
that alternates between marked witness graphs M 0 , . . . , M k and transitions t 1 , . . . , t k taken from T . Let us write M j = (G j , c in j , s in j , c out j , s out j ) and t j = (q j , a j , q j ) for all j. It is also required that, for all 1 ≤ j ≤ k, c out j-1 = (q j , u j ) for some u j and c in j = (q j , u j ) for some u j . In such a sequence, c in 0 is the source and c out k is the target. Figure 3 displays a marked witness graph for the VASS of Example 2.2, with input constraint (q 0 , 1, 0, 1) on the input vertex (q 0 , ω, ω, ω) and output constraint (q 1 , 2, 2, 1) on the output vertex (q 1 , ω, ω, ω).

3.1.2. The Decomposition Algorithm. The KLMST decomposition algorithm builds a sequence Ξ 0 , Ξ 1 , Ξ 2 , . . . of finite sets of marked witness graph sequences. At step n, it checks whether all the sequences ξ in Ξ n are perfect (in the sense of [START_REF] Lambert | A structure to decide reachability in Petri nets[END_REF], or equivalently fulfil the θ-condition of [START_REF] Kosaraju | Decidability of reachability in vector addition systems[END_REF]) and stops if this is the case; then either Ξ n is empty and the algorithm answers 'not reachable', or Ξ n is not empty and the algorithm answers 'reachable'.

If however some sequence ξ from Ξ n is not perfect, then it is decomposed into a finite set of marked witness graph sequences dec(ξ)-which is possibly empty. Then we let

Ξ n+1 def = (Ξ \ {ξ}) ∪ dec(ξ) (3)
and the algorithm proceeds to the next step.

The perfectness condition comprises two sub-conditions, along with the corresponding ways of decomposing marked witness graph sequences when the sub-conditions are violated. We are going to illustrate these two sub-conditions in the upcoming §3. 1.3 and §3.1.4, in the case of Example 2.2, and starting from Ξ 0 = {ξ 0 }.

3.1.3. Flow Constraints. Consider a path from the source to the target in the graph of Figure 3: denoting by z j the number of times transition t j is used along this path for j ∈ {1, . . . , 5}, we can see that

z 3 = z 5 + 1 . (4)
Consider now a run in the VASS of Figure 1, which follows a path in the marked witness graph of Figure 3 from (q 0 , 1, 0, 1) to (q 1 , 2, 2, 1), i.e. with overall effect (1, 2, 0). Then, considering the effect of these transitions for each coordinate i in {1, 2, 3},

z 1 + z 3 = z 2 + 1 , z 1 = z 4 + 2 , z 1 = z 2 .
(5)

The system of equations (4-5) requires z 3 = 1 and z 5 = 0; z 1 , z 2 and z 4 are on the other hand unbounded. This shows that the marked witness graph sequence ξ 0 of Figure 3 is too permissive, allowing to follow paths that do not bring the source of the sequence to its target. We therefore decompose it, using the fact that t 3 must be employed exactly once and that t 5 is never employed: dec(ξ 0 ) = {ξ 1 } where the new sequence ξ 1 is depicted in Figure 4; it contains two marked witness graphs M 0 and M 1 connected by a transition t 3 . q0, ω, ω, ω q0, 1, 0, 1 q0, ω, ω, ω q1, ω, ω, ω q1, ω, ω, ω q1, 2, 2, 1

t1 : (1, 1, -1) t2 : (-1, 0, 1) t3 : (1, 0, 0) t4 : (0, -1, 0)
Fig. 4: The next marked witness graph sequence

ξ 1 = M 0 , t 3 , M 1 . q0, 1, ω, 1 q0, 2, ω, 0 q0, 0, ω, 2 q0, 1, 0, 1 q0, 1, ω, 1 q1, 2, ω, 1 q1, 2, ω, 1 q1, 2, 2, 1 t1 : (1, 1, -1) t2 : (-1, 0, 1) t2 : (-1, 0, 1) t1 : (1, 1, -1) t3 : (1, 0, 0) t4 : (0, -1, 0)
Fig. 5: The final marked witness graph sequence ξ 2 = M 0 , t 3 , M 1 .

3.1.4. Pumpability. A marked witness graph M is forward pumpable if there exist runs in the VASS following paths of M and starting from the input vertex which, when applied to the input constraint, allow to 'pump' arbitrarily high values in the (necessarily common) components labelled ω in the vertices of the graph.

On the one hand, M 0 in Figure 4 is not forward pumpable: any run of the VASS of Figure 1 starting from (q 0 , 1, 0, 1) and using only t 1 and t 2 can indeed reach arbitrarily high values on the second component, but the first and third components are bounded.

On the other hand, M 1 is forward pumpable, but not backward pumpable: starting from (q 1 , 2, 2, 1) and applying t 4 in reverse allows to reach arbitrarily high values on the second component, but the first and third components are again bounded.

Again, the decomposition algorithm will observe that the current marked witness graph sequence over-approximates the possible behaviours of the VASS, and refine M 0 and M 1 using their bounded components; the values of these bounds can be computed in practice using the coverability tree construction of [START_REF] Karp | Parallel program schemata[END_REF]. Propagating the flow constraints, we obtain the final marked witness sequence depicted in Figure 5. This sequence is perfect, and captures in some sense1 all the runs from (q 0 , 1, 0, 1) to (q 1 , 2, 2, 1) in the VASS of Example 2.2.

3.1.5. Termination. The termination of the KLMST decomposition algorithm relies on a ranking function r mapping marked witness graph sequences to elements of a wellorder, and ensuring r(ξ) > r(ξ ) whenever ξ belongs to dec(ξ) [START_REF] Kosaraju | Decidability of reachability in vector addition systems[END_REF]]. More precisely, the ranking function r associates to ξ a multiset of triples of natural numbers, one triple for each marked witness graph in the sequence. These triples consist of (1) |I|, the number of ω-components of the marked witness graph, (2) |E|, the number of transitions of the marked witness graph, and (3) |I in | + |I out |, the number of ωcomponents in the input and output constraints. This results for the sequences ξ 0 , ξ 1 , and ξ 2 of our example in the multisets

r(ξ 0 ) = {(3, 5, 0)} , r(ξ 1 ) = {(3, 2, 3), (3, 1, 3)} , r(ξ 2 ) = {(1, 4, 1), (1, 1, 1)} . (6)
Let us consider the lexicographic ordering over N 3 ; finite multisets of triples in N 3 are then well-ordered using the ordering of [START_REF] Dershowitz | Proving termination with multiset orderings[END_REF].

Observe that we can see the KLMST algorithm as building in general a forest of marked witness graph sequences, with the elements of Ξ 0 as its finitely many roots, and where each imperfect marked witness graph sequence ξ is the parent of the sequences in dec(ξ). The ranking function r then shows that the trees in this forest are of finite height; since dec(ξ) is finite for all ξ, they are also of finite branching degree, hence the trees are finite by Kőnig's Lemma and the algorithm terminates.

Fast-Growing Upper Bounds

Hopefully, the reader has now some vague intuition about the KLMST decomposition algorithm. The key point for complexity considerations is the termination argument by a ranking function explained in §3.1.5: we know that any sequence ξ 0 , ξ 1 , ξ 2 , . . . of marked witness graph sequences with

ξ n+1 ∈ dec(ξ n ) is finite since r(ξ 0 ) > r(ξ 1 ) > r(ξ 2 ) > • • • (7)
is a decreasing sequence in the well-order of multisets of triples of naturals. In order to bound the complexity of the KLMST decomposition algorithm, we are going to bound the length L of such sequences. We shall relate this length with the order type of the ranking function.

3.2.1. Order Types. Recall that an ordinal α < ε 0 (these are rather small, computable, countable ordinals) can be written uniquely in Cantor normal form (CNF) as an ordinal term

α = ω α1 + • • • + ω αn (8)
where the ω-exponents α > α 1 ≥ • • • ≥ α n are written themselves in CNF; the case where n = 0 then corresponds to the ordinal 0. Equivalently, when gathering summands with the same ω-exponent α i , this can be written as

α = ω α1 • c 1 + • • • + ω αn • c n (9) with α > α 1 > • • • > α n and finite coefficients 0 < c i < ω.
One can compare two ordinals α = ω α1 +• • •+ω αn and β = ω β1 +• • •+ω βm syntactically based on their CNFs (8): α < β if and only if there exists k ≤ m such that α j = β j for all 1 ≤ j < k with j ≤ n, and n < k or α k < β k .

The order type of multisets of triples of natural numbers is ω ω 3 [Dershowitz and Manna 1979], and we can equivalently see the ranking function r of §3.1.5 as ranging over ordinals below ω ω 3 : the ranks in [START_REF] Leroux | Vector Addition System Reversible Reachability Problem[END_REF] then become

r(ξ 0 ) = ω ω 2 •3+ω•5 , r(ξ 1 ) = ω ω 2 •3+ω•2+3 + ω ω 2 •3+ω+3 , r(ξ 2 ) = ω ω 2 +ω•4+1 + ω ω 2 +ω+1 . ( 10
)
3.2.2. Controlled Sequences and Length Function Theorems. Although sequences like ( 7) are always finite, they can be of arbitrary length in general. For instance, the sequences [START_REF] Leroux | Demystifying reachability in vector addition systems[END_REF] are decreasing for all n, and have length n + 2.

ω > n > n -1 > n -2 > • • • > 0 (
Thankfully, the sequences of ranks built by the KLMST decomposition algorithm are not arbitrary. The ordinal terms appearing in [START_REF] Leroux | Vector Addition System Reversible Reachability Problem[END_REF] during the course of the KLMST decomposition algorithm are indeed controlled, meaning that 'jumps' to arbitrary high coefficients as in [START_REF] Leroux | Demystifying reachability in vector addition systems[END_REF] cannot occur. More formally, let us define a norm on ordinals below ε 0 as the maximal coefficient appearing in their CNF (9): given

α = ω α1 • c 1 + • • • + ω α n • c n with α > α 1 > • • • > α n , N α def = max 1≤j≤n (c j , N α j ).
For instance, N r(ξ 0 ) = 5, N r(ξ 1 ) = 3, and N r(ξ 2 ) = 4 in (10). Let now g: N → N be a strictly increasing function and n be a natural in N. A sequence α 0 , α 1 , . . . of ordinals below ε 0 is (g, n)-controlled if N α j ≤ g j (n) the jth iterate of g. This means in particular that N α 0 ≤ n, while g bounds the amortised growth of the norm at each step.

The interest of (g, n)-controlled descending sequences of ordinals below some α is that they have a bounded length, which we shall see as a function g α (n) of the initial norm n. When n ≥ N α, the length function theorem in [START_REF] Schmitz | Complexity bounds for ordinal-based termination[END_REF] shows that g α is exactly the αth function in the Cicho ń hierarchy [Cicho ń and Tahhan [START_REF] Cicho | Ordinal recursive bounds for Higman's Theorem[END_REF]]-a consequence of general results on ordinal-recursive functions [e.g. [START_REF] Wilfried Buchholz | A uniform approach to fundamental sequences and hierarchies[END_REF]. This provides a transfinite inductive definition of the function g α :

g 0 (n) = 0 , g α+1 (n) = 1 + g α (g(n)) , g λ (n) = g λ(n) (n) , (12)
where, for a limit ordinal λ, λ(n) is the nth element of its fundamental sequence, also defined by transfinite induction:

(γ + ω β+1 )(n) def = γ + ω β • (n + 1) , (γ + ω λ )(n) def = γ + ω λ(n) . ( 13
)
For instance, ω(n

) = n + 1 and ω ω 3 (n) = ω ω 3 (n) = ω ω 2 •(n+1) ; g k (n) = k for all k, n ∈ N and g, g ω (n) = g n+1 (n) = n + 1, g ω+1 (n) = 1 + g ω (g(n)) = 2 + g(n)
. With higher ordinal indices, these functions grow very fast: using H(n

) def = n + 1 as control function, H ω 2 (n) = H ω•(n+1) (n) = (2 n+1 -1)(n + 1)
, H ω 3 is a non-elementary function akin to a tower of exponentials of height n, and H ω ω is a non-primitive-recursive function akin to the Ackermann function.

Going back to our main purpose, if we provide an initial norm n ≥ 3 and a control function g for sequences like [START_REF] Leroux | Vector Addition System Reversible Reachability Problem[END_REF], we will obtain an

L = g ω ω 3 (n) (14)
bound on their lengths. Regarding the initial norm, the maximum of the sizes of the initial sequences in Ξ 0 will do, and is bounded by the size of the reachability instance.

For the control function, it suffices to bound the size of the marked witness graph sequences in dec(ξ) compared to that of ξ; in the case of the flow conditions of §3.1.3, the blow-up is at most exponential, but in the case of the pumping conditions of §3.1.4, the blow-up is Ackermannian-i.e. in F ω in the extended Grzegorczyk hierarchy of [START_REF] Löb | Hierarchies of number-theoretic functions[END_REF]-due to the use of coverability trees [START_REF] Figueira | Ackermannian and primitive-recursive bounds with Dickson's Lemma[END_REF]]. Overall, an Ackermannian control function g fits. The bound in ( 14) also provides a bound g L (n), i.e. of L iterations of the function g, on the size of the marked witness graph sequences constructed by the KLMST decomposition algorithm. Defining g α (n) def = g gα(n) (n), we find a related hierarchy of functions called the Hardy hierarchy, which allows by Savitch's Theorem to bound the space required by the KLMST decomposition algorithm by a polynomial in

g L (n) = g ω ω 3 (n) . ( 15
)
3.2.3. Complexity Classes. The announced F ω 3 upper bound on the complexity of the reachability problem is then just a matter of finding a suitable complexity class. We shall use the fast-growing complexity classes from [START_REF] Schmitz | Complexity hierarchies beyond ELEMENTARY[END_REF]], defined for α ≥ 3 by where F <α = β<α F β in the extended Grzegorczyk hierarchy. This means that F α is the class of problems decidable in deterministic time H ω α -i.e. the ω α th function in the Hardy hierarchy for H(n) = n + 1-of some 'smaller' function f (n) of the size n of the instance. These classes are very robust, and F ω 3 captures computations in g ω ω 3 (n) space for an Ackermannian function g in F ω (see [Schmitz 2016, Section 4] for details). Figure 6 depicts the (F α ) α classes and pinpoints F ω 3 's position among them.

F α def = f ∈F<α DTIME(H ω α (f (n))) ( 16
) ELEMENTARY F3 = TOWER k F k = PRIMITIVE-RECURSIVE Fω F ω 2 F ω 3 k F ω k = MULTIPLY-RECURSIVE Fωω

Discussion

Lower Bounds.

Facing such a huge upper bound, it is natural to ask how it tight it might be. The best complexity lower bound currently known for the reachability problem is the following result of [START_REF] Lipton | The reachability problem requires exponential space[END_REF] (see also the presentation given by [START_REF] Esparza | Decidability and complexity of Petri net problems -an introduction[END_REF]): THEOREM 3.2 (LOWER BOUND THEOREM). Reachability in VASS is EXPSPACEhard.

This leaves an enormous gap between EXPSPACE and F ω 3 . Nevertheless, the upper bound is obtained with a specific algorithm, the KLMST decomposition algorithm, which-due to its use of coverability trees-is known to require at least an Ackermannian time in the worst case [M üller 1985], i.e. there is an F ω lower bound for that particular algorithm. Hence, besides the main open question about the exact complexity of the reachability problem, there is a possibly easier open question about the complexity of the KLMST decomposition algorithm, with a smaller complexity gap between F ω and F ω 3 .

Alternative Algorithms.

The F ω lower bound on the KLMST decomposition algorithm means that it might be worth looking for more efficient algorithms. Unfortunately, the other algorithm using Presburger inductive invariants by [START_REF] Leroux | The general vector addition system reachability problem by Presburger inductive invariants[END_REF][START_REF] Leroux | Vector addition system reachability problem: a short self-contained proof[END_REF] does not fare better: the 2010 proof using the KLMST decomposition is likely to yield essentially the same F ω 3 upper bound, while the alternative 2011 proof using almost semilinear sets does not easily lend itself to a complexity analysis.

REACHABILITY IN DIMENSION 2

While the exact complexity of the reachability problem is a long-lasting open problem, there are tight complexity bounds for several restricted variants. A natural way of q0 q1 t1 : (0, -1) t3 : (0, 1) t2 : (1, 1) Fig. 7: A 2-dimensional VASS, from [START_REF] Blondin | Reachability in two-dimensional vector addition systems with states is PSPACE-complete[END_REF].

restricting the reachability problem is to fix the dimension. For instance, in dimension one, VASS reachability is NP-complete [START_REF] Haase | Reachability in succinct and parametric one-counter automata[END_REF]] when integers are encoded in binary (and NL-complete when they are encoded in unary [START_REF] Demri | The effects of bounding syntactic resources on Presburger LTL[END_REF])this is a subcase of reachability in one-counter automata.

In the 2-dimensional case, [START_REF] Hopcroft | On the reachability problem for 5-dimensional vector addition systems[END_REF] were the first to show decidability by showing that the reachability set from a given initial configuration c was effectively semilinear, i.e. that one could compute for each state q a representation of the set of vectors u such that c → * V (q, u) as a finite union of linear sets L(b, {p 1 , . . . ,

p n }) def = {b + λ 1 p 1 + • • • + λ n p n | λ 1 , . . . , λ n ∈ N} (17)
defined by a base b in Z d and a finite set of periods p j in Z d -equivalently, these sets are definable in Presburger arithmetic FO(Z, +, ≤). Hopcroft and Pansiot [1979, Lemma 2.8] also showed that there exists a 3-dimensional VASS with a non-semilinear reachability set, so that this result does not generalise to higher dimensions. [START_REF] Howell | Some complexity bounds for problems concerning finite and 2-dimensional vector addition systems with states[END_REF] then showed that this construction was in 2-NEXP and improved it to obtain a 2-EXP algorithm. This left a gap with the NP-hardness proven by Rosier and Yen the same year, which was only closed in 2015 by Blondin, Finkel, Göller, Haase, and McKenzie:

THEOREM 4.1 (2-DIMENSIONAL COMPLEXITY). Reachability in 2-dimensional VASS is PSPACE-complete.

Flattable VASS

The crux of the proof of Blondin et al. is a careful analysis and refinement of a result by [START_REF] Leroux | On flatness for 2-dimensional vector addition systems with states[END_REF]: 2-dimensional VASS are flattable. In general, a VASS is flattable if its reachability relation, which is for each pair of states q, q the set {(u, u ) ∈ N 2d | (q, u) → * V (q , u )}, can be obtained in full when only following transition sequences taken from the language of a finite set S of regular expressions, each of the form [START_REF] Mayr | An algorithm for the general Petri net reachability problem[END_REF] for some finite sequences v 0 , w 1 , v 1 , . . . , w k , v k of transitions in T . Such regular expressions are called semilinear path schemes (one will typically require the full sequence v 0 w 1 v 1 • • • w k v k to be a path in the VASS, and each w j to be a cycle). Let us

v 0 w * 1 v 1 • • • w * k v k (
call |v 0 w 1 v 1 • • • w k v k |
its length and k its width. A set S of semilinear path schemes is complete if, for all q, q in Q and u, u in N 2 , (q, u) → * V (q , u ) if and only if there exist σ in the language of S such that (q, u) σ -→ V (q , u ). By synchronising the VASS with the semilinear path schemes, one obtains a flat VASS, i.e. without nested loops when seen as a directed graph.

Example 4.2. Consider the 2-dimensional of Figure 7, taken from the article of [START_REF] Blondin | Reachability in two-dimensional vector addition systems with states is PSPACE-complete[END_REF]. Although it is has two nested loops t 3 and t 2 t 1 in q 1 , it is nevertheless flattable. Observe indeed that the occurrences of t 3 can be commuted to occur before those of t 2 t 1 . This results for the relation between q 0 and q 1 in a complete set {t 1 t * 3 , t 1 t * 3 t 2 (t 1 t 2 ) * t 1 } (the first holding for the case where t 2 is never used).

A flat VASS has necessarily a semilinear reachability relation, and a fortiori a semilinar reachability set: given a semilinear path scheme as in [START_REF] Mayr | An algorithm for the general Petri net reachability problem[END_REF], one can compute a linear set with basis the sum of the effects of the transitions in v 0 v 1 • • • v k , and a period for the effect of each cycle w j . Perhaps more surprisingly, the converse is true: Leroux [2013a] showed that any VASS with a semilinear reachability set is flattable.

Complexity Bounds

The main technical result of [START_REF] Blondin | Reachability in two-dimensional vector addition systems with states is PSPACE-complete[END_REF] is their Theorem 1:

THEOREM 4.3 (2-DIMENSIONAL SEMILINEAR DECOMPOSITION).
Given a 2dimensional VASS V = Q, 2, T , there exists a complete set S of semilinear path schemes, all of length bounded by (|Q| + T ) C and width bounded by C • |Q|2 for some constants C, C .

They employ then bounds from integer linear programming to show that, if (q, u) → * V (q , u ), and thus (q, u)

σ -→ V (q , u) where σ = v 0 w e1 1 v 1 • • • w e k k v k
for some e 1 , . . . , e k in N and some semilinear path scheme

v 0 w * 1 v 1 • • • w * k v k
from the complete set S provided by Theorem 4.3, then all the e j can be bounded by a value exponential in |Q| but polynomial in T , u , and u . This run can thus be guessed nondeterministically in polynomial space, yielding the upper bound in Theorem 4.1.

The matching PSPACE lower bound is a consequence of the same bound [START_REF] Fearnley | Reachability in two-clock timed automata is PSPACE-complete[END_REF] for reachability in 1-dimensional VASS, when one additionally requires the values to remain bounded by some B (given as input, in binary).

As a final note, this approach also yields an NP upper bound when integers are encoded in unary instead of binary. However, the best known lower bound in this case is NL-hardness, leaving a complexity gap [START_REF] Blondin | Reachability in two-dimensional vector addition systems with states is PSPACE-complete[END_REF].

Discussion

Although there is no hope of seeing the approach through linear paths schemes be immediately generalised to arbitrary dimensions-because starting with dimension three, VASS reachability sets are no longer semilinear [Hopcroft and Pansiot 1979, Lemma 2.8]-there is nevertheless a promising open question: the result of [START_REF] Blondin | Reachability in two-dimensional vector addition systems with states is PSPACE-complete[END_REF] could be read as providing complexity bounds for flat 2-dimensional VASS: could it be generalised to flat VASS of arbitrary dimension?

Finally, the restriction of the reachability problem to 2-dimensional systems is far from being the only interesting one. The best known variant of the reachability problem is arguably the coverability problem, where one asks instead for the existence of a configuration c such that c → V c and c ≥ c for the product ordering over configurations. 2 Coverability in VASS is EXPSPACE-hard using the argument by [START_REF] Lipton | The reachability problem requires exponential space[END_REF], but importantly, it is in EXPSPACE as shown by [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF]. The coverability problem is sufficient in many cases, and unlike the reachability problem, there are several implementations, with increasing success at solving it on large practical instances [e.g. [START_REF] Kaiser | A widening approach to multithreaded program verification[END_REF][START_REF] Esparza | An SMTbased approach to coverability analysis[END_REF][START_REF] Blondin | Approaching the coverability problem continuously[END_REF]].

The same tight EXPSPACE upper bound applies to the boundedness problem, which asks given a VASS V and a configuration c whether the set of configurations reachable from c is finite [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF]]. Many more decision problems on VASS have been shown EXPSPACE-complete based on the techniques of Rackoff [e.g. Rosier and Yen 1986;[START_REF] Faouzi | On Yen's path logic for Petri nets[END_REF][START_REF] Blockelet | Model-checking coverability graphs of vector addition systems[END_REF][START_REF] Demri | On selective unboundedness of VASS[END_REF][START_REF] Leroux | A relational trace logic for vector addition systems with application to context-freeness[END_REF]. Notably, the reversible reachability problem is also EXPSPACE-complete [Leroux 2013b]: this variant of reachability asks whether both c → * V c and c → * V c, and the proof for the upper bound combines insights from both [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF]] and the KLMST decomposition algorithm.

A FEW EQUIVALENT PROBLEMS

The centrality of the reachability problem was recognised early on; Hack [1975a] in particular identified its recursive equivalence with the liveness, single-place reachability, persistence, and language emptiness problems for Petri nets. What is remarkable however is the regularity with which decision problems-in seemingly unrelated areas-turn out to be interreducible with the reachability problem. In fact, given its importance in many fields, it would be no exaggeration to define a complexity class REACHABILITY for the class of problems reducible3 to VASS reachability. Here we will see only a small sample of the problems interreducible with reachability.

Formal Languages

The transitions of a VASS can be labelled with symbols from Σ∪{ε}, where Σ is a finite alphabet and ε denotes the empty string. Formally, we let in this case T ⊆ Q×Z d ×(Σ∪ {ε}) × Q, and denote by π Σ the projection T * → Σ * defined by π Σ (q, a, b, q ) def = b. This allows to define the (reachability) language of a labelled VASS V between an initial configuration c and a final configuration c as the union over all runs from c to c in S V of the concatenations of labels:

L V (c, c ) def = {π Σ (σ) | c σ -→ V c } . (19)
The non-emptiness problem for such languages is thus equivalent to the reachability problem. Labelled VASS are also known as partially blind multicounter automata [START_REF] Greibach | Remarks on blind and partially blind one-way multicounter machines[END_REF]] and can also be recognised by suitable valence automata over polycyclic monoids [Render and Kambites 2009, Proposition 5.1]. The study of this class of languages was already under way for Petri nets before 1978; see e.g. [Hack 1975b].

The equivalence between the reachability problem and language emptiness is rather natural one, but there are some less obvious connections, for instance:

The Szilard language S(G) of a context-free grammar G is the set of sequences of names of the productions used in grammar derivations. [START_REF] Crespi | Petri nets and Szilard languages[END_REF] show that the problem, given a context-free grammar G and a regular language R, of whether S(G) ∩ R is non-empty, is recursively equivalent to VASS reachability. The shuffle closure Shuffle(L) of a language L is obtained by shuffling, i.e. interspersing, an arbitrary number of words from L. [START_REF] Gischer | Shuffle languages, Petri nets, and context-sensitive grammars[END_REF] showed that the shuffle closure Shuffle(R) of any regular language is always a VASS language. [START_REF] Boja Ńczyk | Two-variable logic on data words[END_REF] strengthened this result and showed that the non-emptiness problem for data automata, which is equivalent to checking the non-emptiness of Shuffle(R 1 )∩R 2 for R 1 and R 2 two regular languages, is interreducible with VASS reachability.

Logic

There is a natural connection between logic and VASS reachability through modelchecking: the model-checking problem for a logic allowing to express reachability in the infinite transition system S V will be at least as hard as reachability. It turns out that many temporal logics able to express reachability have an undecidable modelchecking problem on VASS-with a few notable exceptions [START_REF] Howell | A taxonomy of fairness and temporal logic problems for Petri nets[END_REF]Jančar 1990].

Here are some more surprising examples of connections between VASS and logic: Note that the cases of data logics on data trees [START_REF] Boja Ńczyk | Two-variable logic on data trees and XML reasoning[END_REF][START_REF] Dimino | FO 2 (<, +1, ∼) on data trees, data tree automata and branching vector addition systems[END_REF]] and of larger fragments of propositional linear logic [START_REF] Lazić | Non-elementary complexities for branching VASS, MELL, and extensions[END_REF]] can be approached through branching extensions of VASS; see §6.2.2.

Data Logics. A data

Concurrent Systems

Vector addition systems and Petri nets are especially suited for the modelling of finitestate processes running concurrently, and the reachability problem naturally pops up when trying to verify their correctness. What is perhaps less obvious is that this idea can be applied beyond the verification of safety properties on finite-state processes.

For instance, [START_REF] German | Reasoning about systems with many processes[END_REF] show that concurrent systems consisting of a main control process along with an arbitrary number of user processes can be checked against specifications written in linear temporal logic-including liveness conditionsby a reduction to the reachability problem. As another example, [START_REF] Ganty | Algorithmic verification of asynchronous programs[END_REF] prove that liveness of a class of recursive asynchronous programs is equivalent to VASS reachability.

Process Calculi

There is a rich literature on the use of Petri net executions as event structures to provide process semantics [e.g. [START_REF] Nielsen | Petri nets, event structures and domains, part I[END_REF][START_REF] Degano | Axiomatizing net computations and processes[END_REF]]. Petri nets themselves fit in the hierarchies of process calculi among the rather low-level ones [START_REF] Mayr | Process rewrite systems[END_REF]].

But even very expressive calculi tend to have practically useful fragments that can be reduced to VASS. For instance, [START_REF] Meyer | A theory of structural stationarity in the pi-calculus[END_REF] describes a fragment of the π-calculus with restricted usage of names, which can be translated into Petri nets. Larger fragments can also be tackled through VASS extensions with data [Rosa-Velardo and Martos-Salgado 2012], see Section 6.3 for related models.

A FEW EXTENSIONS

The decidability of the reachability problem for VASS is an intricate result, and undecidability is never very far. This section is an opportunity to see how far the Decidability Theorem can be pushed, but also to advertise for a few open problems.

Zero Tests

A zero test is a special type of transition t = (q, zero i , q ) where i ranges over {1, . . . , d}, allowing a step (q, u) t -→ (q , u) if u(i) = 0. Allowing unrestricted zero tests yields a Minsky machine, with an undecidable reachability problem already in dimension two-even coverability is undecidable on such systems.

However, reachability in VASS extended with the ability to test a single component for zero-for instance always the first component-remains decidable. It still remains decidable if several components can be tested with a hierarchical policy: component i 1 can be freely tested for zero, but i 2 can only be tested for zero in configurations where the i 1 th component is zero, and i 3 only in configurations where both the i 1 th and i 2 th components are zero, etc. [START_REF] Reinhardt | Reachability in Petri nets with inhibitor arcs[END_REF][START_REF] Bonnet | Theory of Well-Structured Transition Systems and Extended Vector-Addition Systems[END_REF]. The complexity of reachability in these models is widely open; the best known lower bound is still Lipton's EXPSPACE-hardness, and no upper bound is known.

Recursion and Nesting

Motivated by the need to model distributed systems with some recursive behaviour, there is a variety of VASS extensions that include recursion in some manner, and differing on the (sometimes subtle) way in which they allow interactions between recursion and the integer components. For instance, nested counter systems [START_REF] Lomazova | Some decidability results for nested Petri nets[END_REF][START_REF] Decker | Ordered navigation on multiattributed data words[END_REF]] act on finite multisets of finite multisets of . . . of finite multisets of states as configurations, allowing to model hierarchical computations, but have an undecidable reachability problem. On the other hand, the process rewrite systems of [START_REF] Mayr | Process rewrite systems[END_REF] perform prefix rewrites on terms of a process algebra, and generalise in a sense both VASS and pushdown systems, but still enjoy a decidable reachability problem-with unknown complexity.

6.2.1. Pushdown VASS. One natural way to extend VASS to handle recursion is to add new push and pop operations acting on a pushdown stack with a finite stack alphabet. Note that this generalises VASS with a single zero test, since the particular component tested for zero could be implemented as a stack with a distinguished bottom-of-stack symbol. The decidability of reachability is currently open, but here at least we have better lower bounds: Lazić [2013] showed indeed the problem to be TOWER-hard.

Alternating Branching VASS.

A different way of adding a pushdown stack to a VASS is to let it store vectors from N d on its stack. The system can then add a vector a from Z d to the vector u currently on top of the stack. The key question is which semantics to employ when popping u and pushing multiple vectors, say u 1 and u 2 , to the top of the stack. For instance, if we allow to duplicate the vector u so that u = u 1 = u 2 , then we obtain the model of alternating VASS [e.g. [START_REF] Courtois | Alternating vector addition systems with states[END_REF], which have an undecidable reachability problem.

A very interesting case occurs when we split u nondeterministically into u 1 and u 2 such that u = u 1 + u 2 . This model of branching VASS was introduced by Rambow [1994] in computational linguistics, and independently rediscovered on several occasions since [see the survey in [START_REF] Schmitz | On the computational complexity of dominance links in grammatical formalisms[END_REF]. The decidability of the reachability problem for branching VASS is a major open problem4 already mentioned in this column [START_REF] Boja | Some open problems in automata and logic[END_REF]-it is in particular equivalent to provability in MELL, the multiplicative exponential fragment of linear logic [START_REF] De Groote | Vector addition tree automata[END_REF]]. As with pushdown VASS, although we do not know whether reachability is decidable, 4 we have again a TOWER lower bound [START_REF] Lazić | Non-elementary complexities for branching VASS, MELL, and extensions[END_REF]].

Data

The model of data nets of [START_REF] Lazić | Nets with tokens which carry data[END_REF] extends Petri nets with the ability to manipulate data from some infinite domain D. Dif-ferent variants exist, all with an undecidable reachability problem, except for one case: unordered data Petri nets, where the system can only manipulate data as pure names through equality and disequality constraints. In more concrete terms, the configurations of such a system no longer carry a single vector from N d , but a finite multiset of them, padded with infinitely many 0's. Transitions nondeterministically select some (bounded) number of such vectors u 1 , . . . , u k , and apply some translations a 1 , . . . , a k from Z d to each one. The decidability of the reachability problem for this model is open, with a TOWER lower bound proven by [START_REF] Lazić | Nets with tokens which carry data[END_REF]

2. 1 . 1 .

 11 Petri Nets. A Petri net is a tuple N = P, T, W where P is a finite set of places, T is a finite set of transitions, and W : (P × T ) ∪ (T × P ) → N is a (weighted) flow function. It defines a transition system with configurations in N P -i.e. multisets of places, also called markings-and steps m t -→ m whenever m(p) ≥ W (p, t) and m (p) = m(p) -W (p, t) + W (t, p) for all p in P . A Petri net can be encoded as an equivalent |P |-dimensional VASS with |T | + 1 states, and conversely a d-dimensional VASS can be encoded as an equivalent Petri net with d + 2 places (see Figure

3. 1 . 1 .

 11 Marked Witness Graph Sequences. Let us first complete N with a top element ω and write N ω def = N {ω} for the result; also let ω + z = z + ω = ω for all z in Z.

Fig. 6 :

 6 Fig. 6: Pinpointing F ω 3 among the complexity classes beyond ELEMENTARY.

  word is a sequence of pairs (b, d) where b is a label taken from a finite alphabet and d is a datum from an infinite countable data domain. Data logics allow to reason on such words but can only compare data for equality and disequality. The satisfiability problem for several different such logics on data words is interreducible with VASS reachability [e.g.[START_REF] Boja Ńczyk | Two-variable logic on data words[END_REF][START_REF] Kanovich | Petri nets, Horn programs, linear logic and vector games[END_REF][START_REF] Demri | Reasoning about data repetitions with counter systems[END_REF][START_REF] Decker | Ordered navigation on multiattributed data words[END_REF][START_REF] Colcombet | Generalized data automata and fixpoint logic[END_REF]. Linear Logic. VASS are convenient to describe the usage of discrete resources, and they have been used as models of linear logic fragments [e.g.[START_REF] Engberg | Completeness results for linear logic on Petri nets[END_REF]. More to the point of this column, VASS reachability is equivalent to validity in the !-Horn fragment of linear logic[START_REF] Kanovich | Petri nets, Horn programs, linear logic and vector games[END_REF]].

It represents exactly the downward closure of the set of runs from (q 0 , 1, 0, 1) to (q 1 ,

2, 2, 1); see the Decomposition Theorem of[START_REF] Leroux | Demystifying reachability in vector addition systems[END_REF], which might also help the reader build an intuition about marked witness graph sequences and the KLMST decomposition algorithm.

Over configurations, (q, u) ≤ (q , u ) if and only if q = q and u(i) = u (i) for all 1 ≤ i ≤ d.

Due to the unknown exact complexity of the reachability problem, the class of reductions we could afford when defining this class is unclear; some of the examples here use many-one EXPSPACE reductions.

There is a recent claim that the problem is decidable[START_REF] Bimbó | The decidability of the intensional fragment of classical linear logic[END_REF]], but I have been unable to verify its proof.

ACKNOWLEDGMENTS

I thank Mikołaj Boja ńczyk, Christoph Haase, and Ranko Lazić for their comments on a draft of this column. I am of course the one to blame for the remaining mistakes and inaccuracies.