1 Introduction

Vector addition systems [8] (VAS for short), or equivalently vector addition systems with states [7], or Petri nets are one of the most popular formal methods for the representation and the analysis of parallel processes [3]. The central algorithmic problem is reachability: whether from a given initial configuration there exists a sequence of valid execution steps that reaches a given final configuration. Many important computational problems in logic and complexity reduce or are even equivalent to this problem [6, 22].

After an incomplete proof by Sacerdote and Tenney [20], decidability of the problem was established by Mayr [17, 19], whose proof was then simplified by Kosaraju [9]. Building on the further refinements made by Lambert in the 1990 s [10], in 2015, a first complexity upper-bound of the reachability problem was provided [12] more than thirty years after the presentation of the algorithm introduced by Mayr [9, 10]. The upper-bound given in that paper is “cubic Ackermannian”, i.e. in \(\mathbb {F}_{\omega ^3}\) (see [21]). This complexity bound was obtained by analyzing the Mayr algorithm. With a refined algorithm and a new ranking function for proving termination, an Ackermannian complexity upper-bound was obtained in [15]. This means that the reachability problem can be solved in time bounded by \(F_\omega (p(n))\) where p is a primitive recursive function and where \(F_\omega \) is an Ackermann function. Very recently, this complexity bound was proved to be optimal [2, 14].

While the complexity of the reachability problem is settled, its parameterized version, in fixed dimension d, is still open with a large complexity gap between the lower-bound and the upper-bound. Some recent results provided ways to decrease that gap (see for instance [1, 11]) but the problem remains open. Since there exists d-dimensional VAS with finite but very large reachability sets [18], any reachability algorithm directly based on the Mayr algorithm will necessarily fail in providing a better complexity upper-bound. In fact that algorithm enumerates in some way each possible reachable configurations when the reachability set is finite.

There is another algorithm for deciding the reachability problem independent of the Mayr algorithm. In fact, in [13], we introduced a simple enumerating algorithm for deciding the reachability problem by observing that negative instances of the reachability problem can be witnessed by partitioning the set of configurations into semilinear sets called complete separators. Since we can decide in elementary time if a pair of semilinear sets denotes a complete separator, and the reachability problem is Ackermannian-hard, the size of such a witness is necessarily Ackermannian in the worst case.

In this paper, we take the opportunity to show how to combine papers [15] and [13] to prove that from any negative instance of the reachability problem, we can effectively compute in Ackermannian time a complete separator witnessing that property. This result prove the optimality of algorithms based on complete separators for deciding the general reachability problem. Since this paper is an invited paper at FOSSACS’24, so without any reviewing process, no new proof are given in this paper. If a proof is given, it just to be self-content. But in any case, those proofs are copy-past from [15] and [13].

Even if our result does not provide a better understanding of the complexity of the parameterized reachability problem, it shows that algorithms based on complete separators are optimal in general dimension.

2 Basic Notions

In this section, we introduce basic notions and notation.

Notation for Vectors of Integers. By \(\mathbb {Z}\) we denote the set of integers, and by \(\mathbb {N}\) the set \(\{0,1,2,\dots \}\) of non-negative integers. Given \(d\in \mathbb {N}\), the elements of \(\mathbb {Z}^d\) are called (d-dim) vectors; they are denoted in bold face, and for \(\textbf{x}\in \mathbb {Z}^d\) we put \(\textbf{x}=(\textbf{x}(1),\ldots ,\textbf{x}(d))\) so that we can refer to the vector components. In this context, d is called the dimension of \(\textbf{x}\). We use the component-wise sum \(\textbf{x}+\textbf{y}\) of vectors, and their component-wise order \(\textbf{x}\le \textbf{y}\). For \(c\in \mathbb {N}\), we put \(c\cdot \textbf{x}=(c\cdot \textbf{x}(1),\ldots ,c\cdot \textbf{x}(d))\).

Linear and Semilinear Sets. A set \(\textbf{L}\subseteq \mathbb {N}^d\) is linear if there are d-dim vectors \(\textbf{b}\), the basis, and \(\textbf{p}_1,\ldots ,\textbf{p}_k\), the periods (for \(k\in \mathbb {N}\)), such that \(\textbf{L}=\{\textbf{x}\in \mathbb {N}^d\mid \textbf{x}=\textbf{b}+\textbf{u}(1)\cdot \textbf{p}_1 + \cdots + \textbf{u}(k)\cdot \textbf{p}_k\) for some \(\textbf{u}\in \mathbb {N}^k\}\). In this case, by a presentation of \(\textbf{L}\) we mean the tuple \((\textbf{b},\textbf{p}_1,\ldots ,\textbf{p}_k)\).

A set \(\textbf{S}\subseteq \mathbb {N}^d\) is semilinear if it is a finite union of linear sets, i.e. \(\textbf{S}=\textbf{L}_1\cup \cdots \cup \textbf{L}_k\) where \(\textbf{L}_j\) are linear sets for all j. In this case, by a presentation of \(\textbf{S}\) we mean the sequence of presentations of \(\textbf{L}_1,\ldots ,\textbf{L}_k\). When we say that a semilinear set \(\textbf{S}\) is given, we mean that we are given a presentation of \(\textbf{S}\); when we say that \(\textbf{S}\) is effectively constructible in some context, we mean that there is an algorithm computing its presentation (in the respective context).

We recall that a set \(\textbf{S}\subseteq \mathbb {N}^d\) is semilinear if, and only if, it is expressible in Presburger arithmetic [4]; the respective transformations between presentations and formulas are effective and elementary. Hence if \(\textbf{S}\subseteq \mathbb {N}^d\) is semilinear, then also its complement, denoted as \(\overline{\textbf{S}}\), is semilinear, and \(\overline{\textbf{S}}\) is effectively constructible when (a presentation of) \(\textbf{S}\) is given.

Fast Growing Functions. The Grzegorczyk hierarchy [5, 16] is defined thanks to a family \((F_d)_{d\in \mathbb {N}}\) of functions \(F_d:\mathbb {N}\rightarrow \mathbb {N}\) such that every primitive recursive function is asymptotically bounded by some function \(F_d\). This family is defined by \(F_0(n){\mathop {=}\limits ^{{{ \tiny {\text {def}}}}}}n+1\) and inductively by \(F_{d+1}(n){\mathop {=}\limits ^{{{ \tiny {\text {def}}}}}}F_d^{n+1}(n)\) for every \(n,d\in \mathbb {N}\). Observe that \(F_1(n)=2n+1\), \(F_2(n)=2^{n+1}(n+1)-1\), and \(F_3(n)\) grows as a tower of n exponentials. It follows that \(F_3\) is a non elementary function since it eventually exceeds any fixed iteration of the exponential function. An Ackermannian function, denoted as \(F_\omega \) is defined thanks to the diagonal extraction \(F_\omega (n){\mathop {=}\limits ^{{{ \tiny {\text {def}}}}}}F_{n+1}(n)\) for every \(n\in \mathbb {N}\). This function is non primitive recursive.

Vector Addition Systems. A (d-dim) vector addition system (VAS for short) is a finite set \(\textbf{A}\) of vectors in \(\mathbb {Z}^d\) called actions. Vectors \(\textbf{x}\in \mathbb {N}^d\) are called configurations, and with an action \(\textbf{a}\) we associate the binary relation \(\xrightarrow {\textbf{a}}\) on the configurations in \(\mathbb {N}^d\) by putting \(\textbf{x}\xrightarrow {a}\textbf{y}\) for all \(\textbf{x},\textbf{y}\in \mathbb {N}^d\) such that \(\textbf{y}-\textbf{x}=\textbf{a}\). The relations \(\xrightarrow {\textbf{a}}\) are naturally extended to the relations \(\xrightarrow {\sigma }\) for finite sequences \(\sigma =\textbf{a}_1\ldots \textbf{a}_k\) of actions by \(\textbf{x}\xrightarrow {\sigma }\textbf{y}\) if \(\textbf{x}\xrightarrow {\textbf{a}_1}\cdots \xrightarrow {\textbf{a}_k}\textbf{y}\) for all \(\textbf{x},\textbf{y}\in \mathbb {N}^d\).

On the set \(\mathbb {N}^d\) of configurations we define the reachability relation \(\xrightarrow {\textbf{A}^*}\): we put \(\textbf{x}\xrightarrow {\textbf{A}^*}\textbf{y}\) if there is \(\sigma \in \textbf{A}^*\) such that \(\textbf{x}\xrightarrow {\sigma }\textbf{y}\). For \(\textbf{x}\in \mathbb {N}^d\) and \(\textbf{X}\subseteq \mathbb {N}^d\) we put \(\textsc {post}^*_{\textbf{A}}(\textbf{x}){\mathop {=}\limits ^{{{ \tiny {\text {def}}}}}}\{\textbf{y}\in \mathbb {N}^d\mid \textbf{x}\xrightarrow {\textbf{A}^*}\textbf{y}\}\), and \(\textsc {post}^*_{\textbf{A}}(\textbf{X}){\mathop {=}\limits ^{{{ \tiny {\text {def}}}}}}\bigcup _{\textbf{x}\in \textbf{X}} \textsc {post}^*_{\textbf{A}}(\textbf{x})\). Symmetrically, for \(\textbf{y}\in \mathbb {N}^d\) and \(\textbf{Y}\subseteq \mathbb {N}^d\) we put \(\textsc {pre}^*_{\textbf{A}}(\textbf{y}){\mathop {=}\limits ^{{{ \tiny {\text {def}}}}}}\{\textbf{x}\in \mathbb {N}^d\mid \textbf{x}\xrightarrow {\textbf{A}^*}\textbf{y}\}\) and \(\textsc {pre}^*_{\textbf{A}}(\textbf{Y}){\mathop {=}\limits ^{{{ \tiny {\text {def}}}}}}\bigcup _{\textbf{y}\in \textbf{Y}} \textsc {pre}^*_{\textbf{A}}(\textbf{y})\). By \(\textbf{X}\xrightarrow {\textbf{A}^*}\textbf{Y}\) we denote that \(\textbf{x}\xrightarrow {\textbf{A}^*}\textbf{y}\) for some \(\textbf{x}\in \textbf{X}\) and \(\textbf{y}\in \textbf{Y}\).

The semilinear reachability problem takes as input a triple \((\textbf{X},\textbf{A},\textbf{Y})\) where \(\textbf{X},\textbf{Y}\) are (presentations of) semi-linear sets of configurations of a VAS \(\textbf{A}\), and checks if \(\textbf{X}\xrightarrow {\textbf{A}^*}\textbf{Y}\) hold. In the standard definition of the reachability problem the sets \(\textbf{X},\textbf{Y}\) are singletons; the problem is decidable [19], and it has been recently shown to be Ackermann-complete [2, 14, 15]. It is well-known (and easy to show) that the above more general version (the semilinear reachability problem) is tightly related to the standard version, and has thus the same complexity.

3 Separators

A separator is a negative instance of the semilinear reachability problem, i.e. a triple \((\textbf{X},\textbf{A},\textbf{Y})\) where \(\textbf{X},\textbf{Y}\) are semilinear sets of configurations of a VAS \(\textbf{A}\) such that \(\lnot (\textbf{X}\xrightarrow {\textbf{A}^*}\textbf{Y})\). The domain \(\textbf{D}\) of a separator \((\textbf{X},\textbf{A},\textbf{Y})\) is the semilinear set \(\overline{\textbf{X}\cup \textbf{Y}}\). Notice that \(\textbf{X}\), \(\textbf{D}\), and \(\textbf{Y}\) forms a partition of \(\mathbb {N}^d\). When the domain is empty, the separator is said to be complete. Notice that a triple \((\textbf{X},\textbf{A},\textbf{Y})\) is a complete separator if, and only if, \((\textbf{X},\textbf{Y})\) is a partition of \(\mathbb {N}^d\) into semilinear sets such that \(\textbf{y}-\textbf{x}\not =\textbf{a}\) for every \(\textbf{x}\in \textbf{X}\), \(\textbf{y}\in \textbf{Y}\), and \(\textbf{a}\in \textbf{A}\). In particular this property is decidable in elementary time by encoding it as the satisfiabibility of a Presburger formula. A separator \((\textbf{X}',\textbf{Y}')\) is called a completion of a separator \((\textbf{X},\textbf{Y})\) if \((\textbf{X}',\textbf{Y}')\) is complete, \(\textbf{X}\subseteq \textbf{X}'\) and \(\textbf{Y}\subseteq \textbf{Y}'\).

In [15] we proved that every separator can be effectively completed. In this paper, we show how this result can be extended with optimal complexity bounds. More formally, we prove that any separator can be completed in Ackermannian time. The Ackermannian lower-bound is immediate since the reachability problem for VAS is Ackermannian-complete and as already mentioned, we can check in elementary time if a pair of semilinear sets is a completion of a separator. The most difficult part of the result is the Ackermannian upper-bound.

4 Semi-Pseudo-Linear Sets

Given two semilinear sets \(\textbf{X},\textbf{Y}\) of configurations of a VAS \(\textbf{A}\), the sets \(\textsc {post}^*_{\textbf{A}}(\textbf{X})\cap \textbf{Y}\) and \(\textsc {pre}^*_{\textbf{A}}(\textbf{Y})\cap \textbf{X}\) are not semilinear in general. However, we proved in [13] that those sets are semi-pseudo-linear, a class of sets that can be tightly over-approximated by semilinear sets called linearizations. Linearizations are obtained by solving several instances of the semilinear reachability problem. Since in [2, 14], we provided an Ackermannian upper-bounds on that decision problem, we can reasonably think that the completion of separators can be done in Ackermannian time. To prove that result, in this section we provide complexity bounds on the size of linearizations. Those linearizations will be used in the next section for completing separators in Ackermannian time.

Let us recall some definitions. A monoid \(\textbf{M}\) is a set of configurations such that \(\textbf{0}\in \textbf{M}\), and such that \(\textbf{M}+\textbf{M}\subseteq \textbf{M}\). The monoid spanned by a set \(\textbf{P}\subseteq \mathbb {N}^d\) is the set of finite sums of vectors in \(\textbf{P}\). It is denoted as \(\Sigma \textbf{P}\). A vector \(\textbf{a}\in \mathbb {N}^d\) is called an interior vector of a monoid \(\textbf{M}\), if for every \(\textbf{m}\in \textbf{M}\), there exists a natural number \(n\ge 1\) such that \(n\textbf{a}\in \textbf{m}+\textbf{M}\).

A pseudo-linear set is a set \(\textbf{X}\subseteq \mathbb {N}^d\) such that there exists a linear set \(\textbf{L}=\textbf{b}+\textbf{M}\) where \(\textbf{M}\) is the monoid spanned by the periods of \(\textbf{L}\), such that \(\textbf{X}\subseteq \textbf{L}\) and such that for every finite set \(\textbf{R}\) of interior vectors of \(\textbf{M}\), there exists \(\textbf{x}\in \textbf{X}\) such that \(\textbf{x}+\Sigma \textbf{R}\subseteq \textbf{X}\). In that case, the linear set \(\textbf{L}\) is called a linearization of \(\textbf{X}\). A semi-pseudo-linear set \(\textbf{X}\) is a finite union of pseudo-linear sets \(\textbf{X}=\textbf{X}_1\cup \ldots \cup \textbf{X}_k\). In that case a semilinear set of the form \(\textbf{L}_1\cup \ldots \cup \textbf{L}_k\) where \(\textbf{L}_j\) is a linearization of \(\textbf{X}_j\) is a called a linearization of \(\textbf{X}\).

By combining the proof of [13, Theorem 6.4] with [15], we deduce the following theorem where \(f_d\) is a function of the form \(F_{d+3}(Cn)\) for some constant C independent of d. In this theorem, the size in binary or in unary does not change the result and there is a lot of freedom in the definition of the size of presentations of semilinear sets and VAS.

Theorem 1

Given two semilinear sets \(\textbf{X}\) and \(\textbf{Y}\) of configurations of a d-dim VAS \(\textbf{A}\), the sets \(\textsc {post}^*_{\textbf{A}}(\textbf{X})\cap \textbf{Y}\) and \(\textsc {pre}^*_{\textbf{A}}(\textbf{Y})\cap \textbf{X}\) are semi-pseudo-linear. Moreover, we can effectively compute in time \(f_d(n)\) where n is the size of the input, presentations of linearizations of those sets.

The tightness of linearization approximations can be emphasis by introducing the notion of rankFootnote 1 given in [13]. Formally, the rank of a set \(\textbf{X}\subseteq \mathbb {N}^d\), denoted as \({\text {rank}}{\textbf{X}}\) is the minimal \(r\in \{-\infty ,0,\ldots ,d\}\) such that there exists a semi-linear set \(\textbf{S}\) that contains \(\textbf{X}\) of the form \(\textbf{b}_1+\textbf{M}_1\cup \ldots \cup \textbf{b}_k+\textbf{M}_k\) where \(\textbf{M}_1,\ldots ,\textbf{M}_k\) are monoids spanned by at most r vectors. In [13], we prove that \({\text {rank}}(\textbf{X})=-\infty \) iff \(\textbf{X}\) is empty, \({\text {rank}}(\textbf{X})\le {\text {rank}}(\textbf{Y})\) if \(\textbf{X}\subseteq \textbf{Y}\), and the following theorem.

Theorem 2

(Proposition 7.10 of [13]). Let \(\textbf{S}_1,\textbf{S}_2\) be linearizations of two non-empty semi-pseudo-linear sets \(\textbf{X}_1,\textbf{X}_2\) with an empty intersection. We have:

$${\text {rank}}(\textbf{S}_1\cap \textbf{S}_2)<{\text {rank}}(\textbf{X}_1\cup \textbf{X}_2)$$

5 Ackermannian Completion

We show in this section who a separator \((\textbf{X},\textbf{A},\textbf{Y})\) can be completed in Ackermannian time. We follow the algorithm introduced in [13] by first proving that if \((\textbf{X},\textbf{A},\textbf{Y})\) is not complete, i.e. if the domain \(\textbf{D}\) is non empty, we can effectively compute a separator \((\textbf{X}',\textbf{A},\textbf{Y}')\) with a domain \(\textbf{D}'\) such that \(\textbf{X}\subseteq \textbf{X}'\), \(\textbf{Y}\subseteq \textbf{Y}'\), and such that \({\text {rank}}(\textbf{D}')<{\text {rank}}(\textbf{D})\). It follows that by applying at most d times this algorithm where d is the dimension of \(\textbf{A}\), we get a complete separator.

Let n be the size of the separator \((\textbf{X},\textbf{A},\textbf{Y})\).

The set \(\textbf{Y}'\) is obtained as follows. Since \(\textbf{D}\) is semilinear and effectively computable in elementary time, it follows from Theorem 1 that we can compute in time \(f_d(E(n))\) where E is some fixed elementary function a linearization \(\textbf{U}\) of the semi-pseudo-linear set \(\textsc {post}^*_{\textbf{A}}(\textbf{X})\cap \textbf{D}\). We introduce \(\textbf{Y}'{\mathop {=}\limits ^{{{ \tiny {\text {def}}}}}}\textbf{Y}\cup (\textbf{D}\setminus \textbf{U})\).

Let us prove that \((\textbf{X},\textbf{A},\textbf{Y}')\) is a separator. By contradiction, assume that \(\textbf{X}\xrightarrow {\textbf{A}^*}\textbf{Y}'\). Since \(\lnot (\textbf{X}\xrightarrow {\textbf{A}^*}\textbf{Y})\), and \(\textbf{Y}'=\textbf{Y}\cup (\textbf{D}\setminus \textbf{U})\), we deduce that \(\textbf{X}\xrightarrow {\textbf{A}^*}(\textbf{D}\setminus \textbf{U})\). However, since \(\textsc {post}^*_{\textbf{A}}(\textbf{X})\cap \textbf{D}\subseteq \textbf{U}\) we get a contradiction. Hence \((\textbf{X},\textbf{A},\textbf{Y}')\) is a separator and its domain is equal to \(\textbf{D}\cap \textbf{U}\).

The set \(\textbf{X}'\) is obtained symmetrically. Since \(\textbf{D}\cap \textbf{U}\) is semilinear and effectively computable in elementary time, it follows from Theorem 1 that we can compute in time \(f_d(E'(f_d(E(n))))\) where \(E'\) is some fixed elementary function a linearization \(\textbf{V}\) of the semi-pseudo-linear set \(\textsc {pre}^*_{\textbf{A}}(\textbf{Y}')\cap \textbf{D}\cap \textbf{U}\). We introduce \(\textbf{X}'{\mathop {=}\limits ^{{{ \tiny {\text {def}}}}}}\textbf{X}\cup ((\textbf{D}\cap \textbf{U})\setminus \textbf{V})\).

Symmetrically, we deduce that \((\textbf{X}',\textbf{A},\textbf{Y}')\) is a separator and its domain \(\textbf{D}'\) is equal to \(\textbf{D}\cap \textbf{U}\cap \textbf{V}\).

Since \((\textbf{X},\textbf{A},\textbf{Y}')\) is a separator, it follows that \(\textsc {post}^*_{\textbf{A}}(\textbf{X})\) and \(\textsc {pre}^*_{\textbf{A}}(\textbf{Y}')\) have an empty intersection. In particular the semi-pseudo-linear sets \(\textsc {post}^*_{\textbf{A}}(\textbf{X})\cap \textbf{D}\) and \(\textsc {pre}^*_{\textbf{A}}(\textbf{Y}')\cap \textbf{D}\cap \textbf{U}\) have an empty intersection. If one of those semi-pseudo-linear sets is empty then \(\textbf{D}'\) is empty and in particular \({\text {rank}}(\textbf{D}')<{\text {rank}}(\textbf{D})\). Otherwise, from Theorem 2 we deduce that the rank of \(\textbf{U}\cap \textbf{V}\) is strictly bounded by the rank of the union of \(\textsc {post}^*_{\textbf{A}}(\textbf{X})\cap \textbf{D}\) and \(\textsc {pre}^*_{\textbf{A}}(\textbf{Y}')\cap \textbf{D}\cap \textbf{U}\). Since this set is included in \(\textbf{D}\), and \(\textbf{D}'\) is included in \(\textbf{U}\cap \textbf{V}\), we deduce that \({\text {rank}}(\textbf{D}')<{\text {rank}}(\textbf{D})\).

By replacing E and \(E'\) by \(E+E'\), we can assume without loss of generality that \(E=E'\). By iterating the previous construction at most d times, we deduce that from any separator \((\textbf{X},\textbf{A},\textbf{Y})\) of size n, we can compute in time \((f_d\circ E)^{2d}(n)\) a completion of it. We deduce the main theorem of that paper.

Theorem 3

Separators can be completed in Ackermannian time.

6 Conclusion

In this paper, we have shown that separators can be completed in Ackermannian time. Our computation is based on a generic algorithm given in Sect. 5. This algorithm can be implemented as soon as we have an oracle computing semilinear sets over-approximating the sets \(\textsc {post}^*_{\textbf{A}}(\textbf{X})\cap \textbf{D}\) and \(\textsc {pre}^*_{\textbf{A}}(\textbf{Y})\cap \textbf{D}\). If those approximations are not linearizations, the termination of the algorithm is no longer true in general. However, since its correctness is maintained, it should be interesting to benchmark such an algorithm when using heuristics for implementing oracles computing reachability set over-approximations (based on abstract interpretation, acceleration techniques, parameterized invariant, and so on).