Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Reachability and Related Problems in Vector Addition Systems with Nested Zero Tests

Roland Guttenberg, Wojciech Czerwiński, Sławomir Lasota

TL;DR

This work resolves the Ackermannian upper bound for reachability in Vector Addition Systems with Nested Zero Tests (VASSnz) and extends the framework to related problems such as semilinearity and separability via a uniform approach. The authors convert VASSnz to monotone $ ext{C}$-eVASS and compute an overapproximation of the reachability relation using a KLM-style decomposition grounded in Euler–Kirchhoff (EK) ILPs, yielding rigorous complexity bounds within the fast-growing hierarchy. They provide a precise, dimension- and priority-parameterized analysis (e.g., $ rak{F}_{2kd+2k+2d+4}$ for $d$-dimensional, $k$-priority VASSnz sections and $ rak{F}_{oldsymbol{igomega}}$ for all VASSnz) and show that semilinearity and separability are decidable within the same unified framework. The results unify reachability with semilinearity and separability for VASSnz and related systems, offering a computable route to these properties and suggesting broad applicability to other ordered-counter models.

Abstract

Vector addition systems with states (VASS), also known as Petri nets, are a popular model of concurrent systems. Many problems from many areas reduce to the reachability problem for VASS, which consists of deciding whether a target configuration of a VASS is reachable from a given initial configuration. In this paper, we obtain an Ackermannian (primitive-recursive in fixed dimension) upper bound for the reachability problem in VASS with nested zero tests. Furthermore, we provide a uniform approach which also allows to decide most related problems, for example semilinearity and separability, in the same complexity. For some of these problems like semilinearity the complexity was unknown even for plain VASS.

Reachability and Related Problems in Vector Addition Systems with Nested Zero Tests

TL;DR

This work resolves the Ackermannian upper bound for reachability in Vector Addition Systems with Nested Zero Tests (VASSnz) and extends the framework to related problems such as semilinearity and separability via a uniform approach. The authors convert VASSnz to monotone -eVASS and compute an overapproximation of the reachability relation using a KLM-style decomposition grounded in Euler–Kirchhoff (EK) ILPs, yielding rigorous complexity bounds within the fast-growing hierarchy. They provide a precise, dimension- and priority-parameterized analysis (e.g., for -dimensional, -priority VASSnz sections and for all VASSnz) and show that semilinearity and separability are decidable within the same unified framework. The results unify reachability with semilinearity and separability for VASSnz and related systems, offering a computable route to these properties and suggesting broad applicability to other ordered-counter models.

Abstract

Vector addition systems with states (VASS), also known as Petri nets, are a popular model of concurrent systems. Many problems from many areas reduce to the reachability problem for VASS, which consists of deciding whether a target configuration of a VASS is reachable from a given initial configuration. In this paper, we obtain an Ackermannian (primitive-recursive in fixed dimension) upper bound for the reachability problem in VASS with nested zero tests. Furthermore, we provide a uniform approach which also allows to decide most related problems, for example semilinearity and separability, in the same complexity. For some of these problems like semilinearity the complexity was unknown even for plain VASS.

Paper Structure

This paper contains 19 sections, 53 theorems, 33 equations, 5 figures, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Extended Vector Addition Systems
  4. Algorithm Toolbox
  5. VASSnz and monotone eVASS
  6. Approximating monotone eVASS
  7. Asymptotic Overapproximation
  8. Conclusion
  9. Appendix of Section \ref{['AlgorithmToolbox']}
  10. Appendix of Section \ref{['SectionMainAlgorithm']}
  11. Appendix of Section \ref{['SectionProofTheoremEVASS']}
  12. Example that asymptotic overapproximations have to be basic
  13. Appendix of Section \ref{['SectionHybridization']}
  14. Appendix of Section \ref{['SectionHybridization']}, Part 1
  15. Appendix of Section \ref{['SectionHybridization']}, Part 2
  16. ...and 4 more sections

Key Result

Proposition 2.3

FigueiraFSS11 Let $k, \gamma \geq 1$ and $f\in\mathfrak{F}_{\gamma}$ be a monotone function with $f(x) \geq x$ for all $x$. Then the function mapping $m \in \mathbb{N}$ to the length of the longest $(f,m)$-controlled sequence in $\mathbb{N}^k$ without an increasing pair is in $\mathfrak{F}_{\gamma+k

Figures (5)

  • Figure 1: Left: Illustration of $\dim(\mathbf{L} \setminus (\mathbf{p}+\mathbf{L}))<\dim(\mathbf{L})$ with $\mathbf{L}=\mathbb{N}^2$ and $\mathbf{x}=(3,4)$. The dimension drops from 2 to 1, since the set is now coverable by finitely many lines. Right: $\mathbf{X}=\{(x,y)\in \mathbb{N}^2 \mid y \leq x^2\}$ has the asymptotic overapproximation $\mathbb{N}^2$. It is $g$-bounded for a quadratic function $g$.
  • Figure 2: Example that asymptotic overapproximations have to be basic.
  • Figure 3: Left: The set $\mathbf{X}:=\{(x,y) \in \mathbb{N}^2 \mid x \geq y \geq \log_2(x+1)\}$ (blue region) $\cup${x-axis} (red) fulfills $\mathop{\mathrm{\mathbf{P}_{\mathbf{X}}}}\nolimits=\{\mathbf{0}\}$. Namely vectors $(x,y)$ with $y>0$ are $\not \in \mathop{\mathrm{\mathbf{P}_{\mathbf{X}}}}\nolimits$ because of the red points, and for $x>0, y=0$ the reason is the blue region. Right: The blue $\{(x,y) \in \mathbb{N}^2 \mid 0 \leq y \leq 2x\}$ and the red $1 \leq y \leq 1+x$ regions depict linear sets. $\mathbf{L}_1 \cap \mathbf{L}_2$ is not linear anymore, as it requires both the black points as base points.
  • Figure 4: Left: Consider the following example of an $\mathbb{N}$-g. set from GuttenbergRE23: $\mathbb{N}(\mathbf{F})$ for $\mathbf{F}:=\{(1,0), (1,2), (1,3)\}$. This set fulfills $\mathbb{Q}_{\geq 0}(\mathbf{F}) \cap \mathbb{Z}(\mathbf{F})=\{(x,y) \mid 0 \leq y \leq 3x\}$, and is almost equal to this, except for the points with $y=1$: These are holes, as they were called in GuttenbergRE23. Right: The blue $\{(x,y) \in \mathbb{N}^2 \mid 0 \leq y \leq x^2\}$ has the set of Pumps $\{(0,0)\} \cup \{(x,y) \in \mathbb{N}^2 \mid x>0\}$. After the second application we stabilize to $\mathbb{N}^2$. This happens with any set which has a partner $\mathbf{L}$ for $\mathbf{X} \trianglelefteq \mathbf{L}$: The second application of $\mathop{\mathrm{Pumps}}\nolimits$ adds the boundary, stabilizing to $\mathbf{L}$.
  • Figure 5: Left: The set $\mathbf{X}=\mathbf{X}_1 \cup \mathbf{X}_2$ with $\mathbf{X}_1:=\{(x,y) \mid \log_2(x+1) \leq y \leq x\}$ and $\mathbf{X}_2:=\{(x,y) \mid y=0\}$ (the blue and red parts respectively) fulfills $\mathop{\mathrm{\mathbf{P}_{\mathbf{X}}}}\nolimits=\{0\}$. Namely a vector $(x,y)$ with $y>0$ is not a preservant due to the red points, and if $y=0$ then the blue points are the problem. However, $\mathop{\mathrm{Pumps}}\nolimits(\mathbf{X})=\{(x,y) \mid 0 \leq y \leq x\}$ does not see this problem at all. Intuitively, $\mathop{\mathrm{Pumps}}\nolimits(\mathbf{X})$ consider pumps which work somewhere, and $\mathop{\mathrm{\mathbf{P}_{\mathbf{X}}}}\nolimits$ contains pumps which work everywhere. Right: In case of the depicted blue set, we would find a complete extraction. However, clearly we are not reducible yet: We have to do a recursive call on the red lines.

Theorems & Definitions (113)

  • Definition 2.1
  • Example 2.2
  • Proposition 2.3
  • Definition 4.1
  • Example 4.2
  • Lemma 4.2
  • proof : Proof idea
  • Definition 4.3
  • Lemma 4.4: Cor. D.2 in Leroux13
  • Lemma 4.5
  • ...and 103 more