Exploring VASS Parameterised by Geometric Dimension

Czerwiński, Wojciech; Guttenberg, Roland; Orlikowski, Łukasz; Sinclair-Banks, Henry; Zheng, Yangluo

doi:10.4230/LIPIcs.ICALP.2026.177

Exploring VASS Parameterised by Geometric Dimension

Wojciech Czerwiński

University of Warsaw, Poland Roland Guttenberg

University of Warsaw, Poland Łukasz Orlikowski

University of Warsaw, Poland Henry Sinclair-Banks

University of Warsaw, Poland
Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany Yangluo Zheng

BASICS, Shanghai Jiao Tong University, China

Abstract

The geometric dimension $g$ of a Vector Addition System with States (VASS) is the dimension of the vector space generated by cycles in the VASS; this parameter refines the standard dimension $d$ , the number of counters. Recently, it was discovered that the fastest-known algorithm for solving the reachability problem for VASS has the same complexity in terms of $g$ as in terms of $d$ . This suggests that the geometric dimension may in fact be a more adequate parameter for measuring the complexity of VASS reachability problems. We initiate a more systematic study of the geometric dimension. We discuss differences between two parameters: the geometric dimension and the SCC dimension. Our main technical result states that classical results about the coverability and boundedness problems can be improved from dimension $d$ to geometric dimension $g$ . Namely, coverability is witnessed by runs of length $n^{2^{\mathcal{O}(g)}}$ instead of $n^{2^{\mathcal{O}(d)}}$ , and unboundedness can be witnessed by runs of length $n^{2^{\mathcal{O}(g\log g)}}$ instead of $n^{2^{\mathcal{O}(d\log d)}}$ , where $n$ is the size of the instance. We also study integer reachability and simultaneous unboundedness in VASS parameterised by the geometric dimension.

Keywords and phrases:

vector addition systems, Petri nets, geometric dimensions, coverability problem, integer reachability problem, simultaneous unboundedness, reachability problem

Category:

Track B: Automata, Logic, Semantics, and Theory of Programming

Copyright and License:

© Wojciech Czerwiński, Roland Guttenberg, Łukasz Orlikowski, Henry Sinclair-Banks,
and Yangluo Zheng; licensed under Creative Commons License CC-BY 4.0

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Parallel computing models

Related Version:

Full Version: https://arxiv.org/abs/2602.15483

Funding:

The first four authors are supported by the ERC grant INFSYS, agreement no. 950398. Yangluo Zheng is supported by the NSFC (Natural Science Foundation of China) grant no. 62572319.

DOI:

10.4230/LIPIcs.ICALP.2026.177

Event:

53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026)

Editors:

Sayan Bhattacharya, Danupon Nanongkai, Michael Benedikt, and Gabriele Puppis

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Vector Addition Systems with States (VASS), or equivalently Petri nets, are one of the most popular models of concurrent systems with many theoretical and practical applications [17, 45, 48]. VASS can be seen as automata with several nonnegative integer counters, that can be incremented and decremented by transitions, but not tested for equality with zero. Such automata with $d$ counters are called $d$ -dimensional VASS (shortly $d$ -VASS). Investigating algorithmic problems for VASS is an active research field since the ’70s. Reachability is a central problem which asks, for a given VASS and two configurations (states together with counter values), whether there exists a run from the source configuration to the target configuration. Other significant problems include coverability and boundedness. The coverability problem asks whether there is a run from the source configuration to some configuration that is at least the target. The boundedness problem asks whether the set of configurations reachable from the source is finite. Already in 1976, coverability was shown to be ExpSpace-hard [38]. This immediately implies that reachability and boundedness are also ExpSpace-hard (due to trivial reductions). In 1978, Rackoff proved that both coverability and boundedness are in ExpSpace [44]. Three years later, reachability was proved to be decidable [39]. For many subsequent decades, determining the complexity of the reachability problem was a major open problem. Despite plenty of effort, the Ackermannian complexity was only settled in 2021 [35, 13, 34].

Contemporary research efforts have been devoted to studying reachability, coverability, and boundedness with seemingly the most natural VASS parameter: the dimension $d$ (i.e. the number of counters). Examples of this fact are abundant; there is work on reachability in $1$ -VASS [50, 24], $2$ -VASS [3], $3$ -VASS [9], $d$ -VASS for $d\in\{4,\ldots,8\}$ [12, 14], for arbitrary $d$ -VASS [35, 34, 13, 30, 8], and there is even work on reachability in subclasses of VASS [33, 5] that use the dimension $d$ as a parameter. Investigations into the coverability problem [44, 46, 41, 29, 43] and into reachability problems in VASS extended with a pushdown stack [37, 42, 1] or a branching mechanism [32, 21, 18, 40, 2] have predominantly parameterised the VASS in question by the dimension $d$ .

The papers that prove the Ackermannian upper bound of reachability use the dimension $d$ as the parameter: Leroux and Schmitz proved that reachability in $d$ -VASS is in $\mathcal{F}_{d+4}$ [35], then Fu, Yang, and Zheng later improved this to $\mathcal{F}_{d}$ [19, 20]. Here, $\mathcal{F}_{d}$ is the $d$ -th level of the fast growing hierarchy of complexity classes [47]. Recently however, it was observed that the number of counters $d$ is not always the most appropriate parameter for analysing the complexity of reachability problems in VASS. Fu, Yang, and Zheng observed that both the $\mathcal{F}_{d+4}$ and the $\mathcal{F}_{d}$ upper bounds also hold when the VASS is instead parameterised by the geometric dimension $d$ . The geometric dimension of a Strongly Connected Component (SCC) of a VASS is defined to be the dimension of the vector space spanned by the effects of cycles in the SCC. The canonical way of extending this notion to the entire VASS is to take the (Minkowski) sum of the cycle spaces of each SCC. Fu, Yang, and Zheng used this definition of the geometric dimension, denoted $g$ , to parameterise VASS [19, 20]. It is possible however, to take the maximum over the geometric dimensions of the SCCs in the VASS; we call this parameter the SCC dimension, denoted ${g_{\textsc{scc}}}$ . This parameter has been used recently by Guttenberg, Czerwiński, and Lasota when studing reachability problems in VASS extended with nested zero tests (a certain kind of restricted zero-testing ability) [22].

In fact, the reachability algorithm runs in $\mathcal{F}_{d}$ for geometric dimension $d$ in both variants (the geometric dimension and the SCC dimension). Intuitively, the algorithm works in the same complexity if we add new counters which are copies, rescalings, or even linear combinations of existing counters. It even works if the copied counter changes between every SCC (for example, if counter $6$ first copies counter $3$ and then in the next SCC copies counter $1$ ). Notice however, that the coefficients of these linear combinations can be negative and need not be integer, so the VASS with the additional counters may have significantly fewer runs. To illustrate the difference between the geometric dimension $g$ and the SCC dimension ${g_{\textsc{scc}}}$ , consider Linear Path Schemes (LPS) [36, 3, 5], a well-known subclass of VASS. LPS are characterised by their structure: a (simple) path which has disjoint simple cycles at each node along the path. Observe that LPS can have arbitrary geometric dimension $g\in\mathbb{N}$ , but can only have SCC dimension one ${g_{\textsc{scc}}}\leq 1$ . This is because every SCC contains just one cycle but these cycles need not have pairwise linearly dependent effects.

Geometric dimension $g$ of a VASS has a natural connection to the concept of place invariants in Petri nets [31], see [45, Chapters 11–13] for a gentle introduction. A place invariant is a linear combination of token counts that remains unchanged by any transition. When converting a Petri net to a VASS, $g$ is the number of places minus the number of place invariants. Therefore, one can expect lower computational complexity in VASS problems with a smaller geometric dimension, just as in Petri nets with more place invariants.

Our Contributions

In this paper we initiate a more systematic study of two geometric VASS parameters: the geometric dimension and the SCC dimension. Our focus is on the set of classical and more tractable reachability problems in VASS: coverability, simultaneous unboundedness, boundedness, and integer reachability. Algorithms for solving these problems are often used as subroutines in algorithms for solving other problems. We also discuss differences between geometric dimension and SCC dimension taking into account the reachability problem.

Our main technical contribution is a generalisation of the results of [44] and the more recent [29] from VASS parameterised by the dimension $d$ to VASS parameterised by the geometric dimension $g$ . More concretely, Rackoff proved two seminal results for $d$ -VASS of size $n$ [44]. The first is that if there is a run from the source $s$ that covers the target $t$ , then there is also a run of length at most $\max(\textup{size}(t),n)^{2^{\mathcal{O}(d\log(d))}}$ from the source $s$ that covers the target $t$ [44, Section 3]. The second is that if the set of configurations reachable from the source configuration $s$ is infinite, then it is witnessed by a “self-covering run” of length at most $n^{2^{\mathcal{O}(d\log(d))}}$ [44, Section 4]. A self-covering run is one from the source $s$ , that first reaches a configuration $c$ and then goes on to reach a configuration $c^{\prime}$ strictly greater than $c$ . Recently, Künnemann, Mazowiecki, Schütze, Sinclair-Banks, and Węgrzycki improved on Rackoff’s bound for the length of coverability witnesses and showed that if there is a run from the source $s$ that covers the target $t$ , then there is a run from $s$ that covers $t$ of length at most $\max(\textup{size}(t),n)^{2^{\mathcal{O}(d)}}$ [29]. The difference being that the exponent was decreased from $2^{\mathcal{O}(d\log(d))}$ to $2^{\mathcal{O}(d)}$ which matches Lipton’s lower bound on the length of coverability witnesses [38]. We generalise all three of these results to geometric dimension $g$ (Theorem 6, Theorem 23, and Theorem 14). Our main conceptual insights are novel definitions of “clean basis” (Definition 7) and “geometrically small configurations” (Definition 8).

With the aim of delivering a well-designed toolbox for VASS with fixed geometric dimension, we generalise one more classic result that has a similar flavour to the techniques used by Rackoff in [44]. A critical part of the standard approach to solving reachability in VASS, known as the KLM-decomposition, is the following observation about the situation in which all counters are simultaneously unbounded. If, from a given source configuration $s$ , one cannot cover all configurations in some state $q$ , then there exists a bound $C$ such that, on every run starting from $s$ , there is at least one counter whose value is bounded above by $C$ . Importantly, no counter is guaranteed to be bounded in all configurations reachable from $s$ , the bounded counter may depend on the run. Originally, the constant $C$ was nonprimitive-recursive [28], as it was taken from the construction of the Karp-Miller tree [27] However, Leroux and Schmitz later observed in [35] that $C$ can be doubly-exponential (see also [10, Lemma 31] for an explicit statement of this result); this significantly lowered the complexity of their algorithm. We generalise this result to geometric dimension $g$ (Theorem 20).

Furthermore, we consider the integer reachability problem for VASS which asks whether a given target configuration can be reached from a given source configuration by a run in which counters may have negative values. It is folklore (see [23]) that if there is an integer run from the source $s$ to the target $t$ in a $d$ -VASS, for a fixed $d$ , then there is a polynomial length integer run from $s$ to $t$ (with respect to the size of the VASS encoded in unary). We generalise this result to geometric dimension $g$ (Theorem 28).

Finally, we conclude by comparing the two VASS parameters in question: geometric dimension and SCC dimension. For the geometric dimension, we have managed to show that for the classical problems coverability, boundedness, integer reachability, and simultaneous unboundedness the state-of-the-art algorithms can be generalised from the dimension to the geometric dimension. It is known that sometimes geometric dimension behaves differently than the number of counters. For example, reachability in binary VASS with geometric dimension 1 is PSpace-hard [52], in contrast to NP-completeness [24] for binary 1-VASS. By and large however, we do find that geometric dimension behaves very similarly to the number of counters.

The situation is different for the SCC dimension. The algorithm solving the reachability problem for $d$ -VASS [35] works equally well for SCC dimension ${g_{\textsc{scc}}}=d$ , but it seems to be the only case in which we are currently able to generalise existing results from the dimension to the SCC dimension. As corollaries of our results when VASS are parameterised by the geometric dimension $g$ , we obtain upper bounds when the VASS is instead parameterised by the SCC dimension. Specifically, for coverability, boundedness, integer reachability, and simultaneous unboundedness we can use the inequality $g\leq{g_{\textsc{scc}}}\cdot n$ , where $n$ is the number of states in the VASS. Unfortunately, notice that in contrast to fixed geometric dimension $g$ , we do not get polynomial upper bounds on the size of coverability, unboundedness, or integer reachability witnesses for fixed SCC dimension ${g_{\textsc{scc}}}$ . We remark that even for fixed $g$ , our polynomial upper bound on the witness size does not imply NL algorithms. This is because the dimension $d$ is not fixed, so one cannot store a configuration in logarithmic space.

Despite the aforementioned fact that the general VASS reachability algorithm in [35] works fine with respect to the SCC dimension, it seems to be the case that reachability in VASS with fixed SCC dimension ${g_{\textsc{scc}}}$ has higher complexity than reachability in VASS with the corresponding dimension. For this, we provide the following pieces of evidence.

First, as shown in [19], in VASS with $g=2$ the reachability relation is semilinear and can be represented by a finite union of LPSs, similarly as for $2$ -VASS [3]. For $2$ -VASS, these Linear Path Schemes (LPSs) have at most exponential size and contain at most polynomially many cycles. This implies exponential length shortest runs. However, the construction described in [19] does not provide any bound on the size of the constructed LPSs. It seems that the obtained LPSs are of at most doubly-exponential size (due to a polynomial blowup for each increment of the dimension), which would give at most triply-exponential run length, but there is no such claim in [19]. That means that the currently existing techniques could possibly be used to show that the shortest runs witnessing reachability in VASS with SCC dimension ${g_{\textsc{scc}}}=2$ have triple exponential length. In turn, this would yield an 2-ExpSpace upper bound for the reachability problem, in contrast to the PSpace upper bound for reachability in $2$ -VASS [3].

For ${g_{\textsc{scc}}}=3$ , the situation also seems more complicated than for $3$ -VASS. We observe that an example of a binary $4$ -VASS presented in [12, Section 5] has SCC dimension ${g_{\textsc{scc}}}=3$ . In this example, the shortest run between the source and target configuration has double exponential length. Such an example is not known for $3$ -VASS; all known examples have the property that the shortest run between source and target is has at most exponential length. Therefore, the naive PSpace algorithm that enumerates all the possible exponential length runs is insufficient for VASS with SCC dimension ${g_{\textsc{scc}}}=3$ , but such an algorithm can be conjectured to solve reachability in $3$ -VASS.

Last but not least, we consider ${g_{\textsc{scc}}}=4$ . We prove that the reachability problem for VASS with SCC dimension ${g_{\textsc{scc}}}=4$ is Tower-hard (Theorem 29). To contrast it with $d$ -VASS, the lowest number of counters for which reachability is known to be Tower-hard is $d=8$ [14]. Our construction (to prove Theorem 29) follows the same ideas used to obtain Tower-hardness for reachability in $8$ -VASS presented in [14]. This indicates that VASS of low SCC dimension can be more expressive than VASS with a small number of counters.

Paper Organisation

In Section 2, we define preliminary notions and recall useful facts. Sections 3, 4, 5, and 6, contain our main technical results about various algorithmic problems for VASS parameterised by geometric dimension and SCC dimension. In Section 3, we present our results about the coverability problem. Next, we consider simultaneous unboundedness in Section 4. Section 5 is devoted to the boundedness problem. In Section 6, we study the integer reachability problem. In Section 7, we prove Tower-hardness of the reachability problem for VASS with ${g_{\textsc{scc}}}=4$ . Finally, in Section 8, we conclude and present future research directions.

2 Preliminaries

We use $\mathbb{Z},\mathbb{N},\mathbb{Q}$ , and $\mathbb{Q}_{\geq 0}$ to denote the sets of integers, nonnegative integers, rational numbers, and nonnegative rational numbers, respectively. Let $d\in\mathbb{N}$ be a number. We denote $[d]$ for the set $\{1,2,\ldots,d\}$ . In particular $[0]=\emptyset$ is the empty set. Given a $d$ -dimensional vector $\mathbf{x}\in\mathbb{Q}^{d}$ , we write $\mathbf{x}[i]$ for its $i$ -th component, where $i\in[d]$ . Hence $\mathbf{x}=(\mathbf{x}[1],\mathbf{x}[2],\ldots,\mathbf{x}[d])$ . For $q\in\mathbb{Q}$ we denote $\mathbf{q}^{d}=(q,q,\ldots,q)\in\mathbb{Q}^{d}$ , and write $\mathbf{e}_{i}^{d}$ for the $d$ -dimensional vector satisfying $\mathbf{e}_{i}^{d}[i]=1$ and $\mathbf{e}_{i}^{d}[j]=0$ for all $j\neq i$ . When the dimension $d$ is clear from the context, we shall drop the super-script $d$ and simply write $\mathbf{q}$ , $\mathbf{e}_{i}$ for these vectors. Vectors are compared in the component-wise manner. Given $\mathbf{x},\mathbf{y}\in\mathbb{Q}^{d}$ , we have $\mathbf{x}\leq\mathbf{y}$ if $\mathbf{x}[i]\leq\mathbf{y}[i]$ for all $i\in[d]$ . We write $\mathbf{x}<\mathbf{y}$ if $\mathbf{x}\leq\mathbf{y}$ and $\mathbf{x}\neq\mathbf{y}$ . For a vector $\mathbf{x}\in\mathbb{Q}^{d}$ , we will use its max-norm $\lVert\mathbf{x}\rVert_{\infty}=\max_{i\in[d]}\lvert\mathbf{x}[i]\rvert$ and its one-norm $\lVert\mathbf{x}\rVert_{1}=\sum_{i=1}^{d}\lvert\mathbf{x}[i]\rvert$ . For a set of vectors $X\subseteq\mathbb{Q}^{d}$ we write $\lVert X\rVert_{\infty}=\max_{\mathbf{x}\in X}\lVert\mathbf{x}\rVert_{\infty}$ . For $\mathbf{x}\in\mathbb{Q}^{d}$ and $K\subseteq[d]$ we use the notation $\pi_{K}(\mathbf{x})$ for the projection of $\mathbf{x}$ onto indices in $K$ .

Vector Spaces and Cones

Let $X\subseteq\mathbb{Q}^{d}$ be a finite set of vectors and let $\mathbb{S}\subseteq\mathbb{Q}$ be a set of numbers. The $\mathbb{S}$ -linear combination of $X$ is the set $\mathbb{S}(X)=\{\sum_{i=1}^{m}\lambda_{i}\mathbf{m}_{i}\mid m\in\mathbb{N},% \lambda_{i}\in\mathbb{S},\mathbf{m}_{i}\in X\}$ . The vector space generated by $X$ is defined to be $\mathbb{Q}(X)$ . The (rational) cone generated by $X$ is $\mathop{\operatorname{cone}}\nolimits(X)=\mathbb{Q}_{\geq 0}(X)$ . We also consider the integer cone generated by $X$ , which is $\mathop{\operatorname{cone}}\nolimits_{\mathbb{N}}(X)=\mathbb{N}(X)$ . Carathéodory’s Theorem is a useful tool for cones.

Theorem 1 (Carathéodory’s Theorem for Rational Cones, see e.g. [49, Corollary 7.1i]).

Let $X\subseteq\mathbb{Q}^{d}$ be a finite set of vectors and let $\mathbf{b}\in\mathop{\operatorname{cone}}\nolimits(X)$ . Then there exists a subset $\widehat{X}\subseteq X$ such that $\mathbf{b}\in\mathop{\operatorname{cone}}\nolimits(\widehat{X})$ and $|\widehat{X}|\leq d$ .

We also need the analogy of Carathéodory’s Theorem for integer cones.

Theorem 2 (Carathéodory’s Theorem for Integer Cones, [16, Theorem 1]).

Let $X\subseteq\mathbb{Z}^{d}$ be a finite set of vectors and let $\mathbf{b}\in\mathop{\operatorname{cone}}\nolimits_{\mathbb{N}}(X)$ . Then there exists a subset $\widehat{X}\subseteq X$ such that $\mathbf{b}\in\mathop{\operatorname{cone}}\nolimits_{\mathbb{N}}(\widehat{X})$ and $|\widehat{X}|\leq 2d\log(4dM)$ where $M=\max_{x\in X}\lVert\mathbf{x}\rVert_{\infty}$ .

Vector Addition Systems with States

A $d$ -dimensional vector addition system with states ( $d$ -VASS) is a pair $V=(Q,T)$ where $Q$ is a finite set of states and $T\subseteq Q\times\mathbb{Z}^{d}\times Q$ is the set of transitions. A transition of the form $(p,\mathbf{a},q)$ may be written as $p\xrightarrow{\mathbf{a}}q$ for clarity, and the vector $\mathbf{a}$ is called the effect of this transition. A VASS may be viewed as a directed graph where edges are labeled with integer vectors. Accordingly, a path in a VASS is a sequence of transitions and a cycle is a path that starts and ends at the same state. Given a path (or a cycle) $\pi$ of $V$ , its effect $\textup{eff}(\pi)$ is the sum of effects of all transitions constituting $\pi$ . The max-norm of transitions of $V$ is defined to be $\lVert T\rVert_{\infty}:=\max_{(p,\mathbf{a},q)\in T}\lVert\mathbf{a}\rVert_{\infty}$ . The (unary-encoded) size of $V$ is defined by $\textup{size}(V)=|Q|+|T|\cdot d\cdot(\lVert T\rVert_{\infty}+1)$ .

A configuration of $V$ consists of a state $q\in Q$ and a nonnegative vector $\mathbf{x}\in\mathbb{N}^{d}$ . Such a configuration shall be written as $q(\mathbf{x})$ . For a configuration $c=q(\mathbf{x})$ , its norm is defined by $\lVert c\rVert_{\infty}=\lVert\mathbf{x}\rVert_{\infty}$ and $\lVert c\rVert_{1}=\lVert\mathbf{x}\rVert_{1}$ . We write $c[i]$ for $\mathbf{x}[i]$ where $i\in[d]$ . We remark that coordinates of the vector $\mathbf{x}$ will often be called “counters”, as VASS is a special form of counter automata. Configurations can be compared when they are in the same state. For $c=q(\mathbf{x})$ and $c^{\prime}=q^{\prime}(\mathbf{x}^{\prime})$ , we write $c\leq c^{\prime}$ if $q=q^{\prime}$ and $\mathbf{x}\leq\mathbf{x}^{\prime}$ , and $c<c^{\prime}$ if $q=q^{\prime}$ and $\mathbf{x}<\mathbf{x}^{\prime}$ .

Each transition $u=(p,\mathbf{a},q)$ induces one-step runs $p(\mathbf{x})\xrightarrow{t}q(\mathbf{y})$ between configurations $p(\mathbf{x}),q(\mathbf{y})$ satisfying $\mathbf{x}+\mathbf{a}=\mathbf{y}$ . Similarly, a path $\pi=u_{1}u_{2}\ldots u_{k}$ induces runs of the form $c_{0}\xrightarrow{u_{1}}c_{1}\xrightarrow{u_{2}}c_{2}\cdots\xrightarrow{u_{k}}% c_{k}$ . We emphasize that vectors in each configuration $c_{i}$ along the run should be nonnegative. We write $c\xrightarrow{*}_{V}c^{\prime}$ if there is a run from $c$ to $c^{\prime}$ in $V$ . The subscript $V$ is often omitted when the VASS $V$ is clear from the context. We say a run from $c$ to $c^{\prime}$ covers a configuration $c^{\prime\prime}$ , if it holds that $c^{\prime}\geq c^{\prime\prime}$ .

We also consider $\mathbb{Z}$ -configurations $p(\mathbf{z})$ where the vector $\mathbf{z}\in\mathbb{Z}^{d}$ is allowed to have negative values. Runs over $\mathbb{Z}$ -configurations are defined similarly, and are called $\mathbb{Z}$ -runs.

Problems that are commonly studied on VASS include:

Reachability.: Given a VASS $V$ and configurations $c,c^{\prime}$ , is there a run from $c$ to $c^{\prime}$ in $V$ ?
$\mathbb{Z}$ -Reachability.: Given a VASS $V$ and $\mathbb{Z}$ -configurations $c,c^{\prime}$ , is there a $\mathbb{Z}$ -run from $c$ to $c^{\prime}$ ?
Coverability.: Given a VASS $V$ and configurations $c,c^{\prime}$ , is there a run from $c$ that covers $c^{\prime}$ ?
Boundedness.: Given a VASS $V$ and a configuration $c$ , is the set $\{c^{\prime}\mid c\xrightarrow{*}c^{\prime}\}$ finite?

In this paper we focus on these problems under the parameterisation by geometric dimension which we introduce next.

Geometric Dimension of a VASS

Let $V=(Q,T)$ be a $d$ -VASS and $q\in Q$ be a state. We denote by $\mathsf{Cycle}_{V}(q)=\{\textup{eff}(\theta)\mid\theta\text{ is a cycle % containing }q\}$ the set of effects of all cycles containing the state $q$ . Two types of geometric dimension have been proposed in the literature. The geometric dimension $g(V)$ and its variant the SCC dimension ${g_{\textsc{scc}}}(V)$ are respectively defined by

\displaystyle g(V)=\dim(\mathbb{Q}(\bigcup_{q\in Q}\mathsf{Cycle}_{V}(q)))

\displaystyle{g_{\textsc{scc}}}(V)=\max_{q\in Q}\dim(\mathbb{Q}(\mathsf{Cycle}% _{V}(q)))

In particular, we define the cycle space of $V$ as $\mathsf{CycleSpace}_{\mathbb{Q}}(V)=\mathbb{Q}(\bigcup_{q\in Q}\mathsf{Cycle}_% {V}(q))$ , which is the vector space spanned by the effects of all cycles in $V$ . Hence, the geometric dimension is indeed the dimension of the cycle space of $V$ . We remark that $\mathsf{CycleSpace}_{\mathbb{Q}}(V)$ can be generated from effects of $g(V)$ many simple cycles. Moreover, the generators, and hence both the geometric dimension $g(V)$ and the SCC dimension ${g_{\textsc{scc}}}(V)$ , could easily be computed in polynomial time [52].

Observe that the space $\mathbb{Q}(\mathsf{Cycle}_{V}(q))$ only depends on the strongly connected component (SCC) in $V$ that contains $q$ , hence the maximum can be taken over SCCs instead of states as indicated by the name SCC dimension. From the definitions we observe the following simple fact on the relation between the two types of geometric dimension:

Lemma 3.

Let $V=(Q,T)$ be a VASS. Then $g(V)\leq|Q|\cdot{g_{\textsc{scc}}}(V)$ .

Proof.

For each $q\in Q$ , the vector space $\mathbb{Q}(\mathsf{Cycle}_{V}(q))$ is spanned by at most ${g_{\textsc{scc}}}(V)$ generators. Therefore, the cycle space of $V$ has no more than $|Q|\cdot{g_{\textsc{scc}}}(V)$ generators. $\hfill\blacktriangleleft$

Integer Solutions of Linear Systems

The following result on system of linear equations will be useful.

Lemma 4 ([6, Prop. 4]).

Consider a system $A\cdot\mathbf{x}=\mathbf{b}$ of $d$ Diophantine linear equations with $n$ unknowns, where absolute values of coefficients in $A$ and $\mathbf{b}$ are bounded by $N$ . If the system has a nonnegative integer solution, then it also has one bounded by $\lVert\mathbf{x}\rVert_{\infty}\leq\mathcal{O}(nN)^{d}$ .

Similar bounds also exist for systems of linear inequalities, see e.g. [6, Prop. 3]. In this paper we need a stronger bound that better fits the geometric dimension, in the sense that the exponent depends on the rank of the matrix $A$ instead of the number of variables. The bound shown in the following lemma is an application of a theorem in [51].

Lemma 5.

Consider a system $A\cdot\mathbf{x}\geq\mathbf{b}$ of $d$ Diophantine linear inequalities with $n$ unknowns, where absolute values of coefficitents of $A$ and $\mathbf{b}$ are bounded by $N$ and, moreover, $\mathbf{b}\geq\mathbf{0}$ . If the system has a nonnegative integer solution then it has one of max-norm bounded by $\lVert\mathbf{x}\rVert_{\infty}\leq(r+1)(rN)^{r}$ where $r=\textup{rank}(A)$ .

3 Coverability

We will focus on the coverability problem for VASS parameterised by geometric dimension $g$ . The main result of this section is that coverability is witnessed by doubly-exponential length runs, where the double exponential dependence is only on $g$ , rather than the size or (standard) dimension of the VASS (Theorem 6). This means that coverability in VASS with fixed geometric dimension is witnessed by polynomial length runs.

Throughout this section, unless otherwise specified, we fix our attention on an instance of coverability in a VASS $V=(Q,T)$ , an initial configuration $s(\mathbf{x})$ , and a target configuration $t(\mathbf{y})$ . We also fix the following parameters of $V$ :

$\blacksquare$

$d\in\mathbb{N}$ is the dimension,
$\blacksquare$

$g\leq d$ is the geometric dimension,
$\blacksquare$

$n\coloneqq\lvert Q\rvert$ is the number of states,
$\blacksquare$

$M\coloneqq\max\{\lVert\mathbf{x}\rVert_{\infty}:(p,\mathbf{x},q)\in T\}$ is the magnitude of the greatest effect of any transition.

We can assume, without loss of generality that $V$ consists of a series of strongly connected components (SCC) that are connected by single transitions. This is because a run in $V$ from $s(\mathbf{x})$ that covers $t(\mathbf{y})$ follows a path that traverses a series of SCCs.

Theorem 6.

Let $f:\mathbb{N}\to\mathbb{N}$ , $f(x)\coloneqq(x+1)^{x+1}$ . If there is a run in $V$ from $s(\mathbf{x})$ that covers $t(\mathbf{y})$ , then there exists a run in $V$ from $s(\mathbf{x})$ that covers $t(\mathbf{y})$ of length at most $\textup{poly}(d,n,M,\lVert\mathbf{y}\rVert_{\infty})^{f(g)}$ .

Our proof of Theorem 6 has the same structure as Rackoff’s original proof [44, Section 3] that coverability in VASS is witnessed by double exponential length runs. Roughly speaking, the proof goes as follows. One observes that if a counter becomes “sufficiently large”, then there is no need to worry about that counter dropping below zero for the remainder of the run. Accordingly, the proof goes by induction on the dimension (at each step, another counter is “ignored”). One of the core components in the proof is the definition of “small configurations”, where a configuration $q(\mathbf{v})$ that is not small has a large counter value $\mathbf{v}[i]$ .

The proof of Theorem 6 follows suit, though the definition of what makes a configuration small is noticeably different. Here is where we make our main technical contribution; we define “geometrically small configurations” (Definition 8). Towards proving Theorem 6, after defining geometrically small configurations, we will first state and prove some intermediate facts that will help us then prove an induction-friendly bound on length of the shortest runs witnessing coverability (Lemma 12, which is the core lemma behind Theorem 6).

Definition 7 (Clean basis).

Let $U\subseteq\mathbb{Q}^{d}$ be a $g$ -dimensional vector space. We say that a basis $B=\{\mathbf{b}_{1},\ldots,\mathbf{b}_{g}\}$ of $U$ is clean if there exist coordinates $K=\{k_{1},\ldots,k_{g}\}\subseteq[d]$ such that $\pi_{K}(\mathbf{b}_{1}),\ldots,\pi_{K}(\mathbf{b}_{g})$ forms the $g$ -dimensional identity matrix. Coordinates $K$ are called the distinguished coordinates of $B$ .

Observe that any basis $B$ of a $g$ -dimensional vector space $U\subseteq\mathbb{Q}^{d}$ can be turned into a clean basis using a Gaussian-elimination-style algorithm.

Definition 8 (Geometrically small configurations).

A vector $\mathbf{v}\in\mathbb{N}^{d}$ is $C$ -small with respect to $g$ -dimensional vector space $U\subseteq\mathbb{Q}^{d}$ if there exists a clean basis $B=\{\mathbf{b}_{1},\ldots,\mathbf{b}_{g}\}$ of $U$ with the set $K\subseteq[d]$ of $g$ distinguished coordinates, such that $\mathbf{v}[i]<C$ for all $i\in K$ . Moreover, we say that a configuration $q(\mathbf{v})$ of a VASS $V$ is $C$ -small if $\mathbf{v}$ is $C$ -small with respect to $\mathsf{CycleSpace}_{\mathbb{Q}}(V)$ . If a vector $\mathbf{v}$ or a configuration $q(\mathbf{v})$ is not $C$ -small then we call it $C$ -large.

Now, similar to Rackoff’s original proof, we would like to bound the number of $C$ -small configurations. Unfortunately, there can be an infinite number of $C$ -small configurations as there are no restrictions on the coordinates that are not distinguished. Instead, we will bound the number of $C$ -small configurations that are reachable from some initial configuration (Claim 10).

Before stating Claim 10, we introduce a way of decomposing counter value vectors that will be useful for Claim 10 and later. We can describe a vector $\mathbf{v}$ of counter values of a configuration $q(\mathbf{v})$ as the sum $\mathbf{v}=\mathbf{x}+\mathbf{r}_{q}+\mathbf{w}$ , where $\mathbf{x}$ are the starting counter values, $\mathbf{r}_{q}$ is the effect of some path from $s$ to $q$ , and what remains is $\mathbf{w}$ that belongs to $\mathsf{CycleSpace}_{\mathbb{Q}}(V)$ . In order to meaningfully use this decomposition, we need to argue that we can arbitrarily nominate a path from $s$ to $q$ which allows us to fix $\mathbf{r}_{q}$ , for every state $q$ .

Claim 9.

Let $p,q\in Q$ be two states and let $\rho_{1},\rho_{2}$ be two paths from $p$ to $q$ . The difference between the effects of $\rho_{1}$ and $\rho_{2}$ belongs to $\mathsf{CycleSpace}_{\mathbb{Q}}(V)$ .

Proof Sketch.

First, consider the case when $p$ and $q$ are in the same strongly connected component. Let $\tau$ be any path from $q$ back to $p$ . Then $\rho_{1}\tau$ is a cycle from $p$ to $p$ , and so is $\rho_{2}\tau$ . Thus the difference of the effects of $\rho_{1}\tau$ and $\rho_{2}\tau$ belongs to $\mathsf{CycleSpace}_{\mathbb{Q}}(V)$ . Clearly, the difference in effect between $\rho_{1}\tau$ and $\rho_{2}\tau$ is the same as between the effects of $\rho_{1}$ and $\rho_{2}$ .

Since $V$ is a line of SCCs, $\rho_{1}$ and $\rho_{2}$ visit the same SCCs. We use the above case for the segments of $\rho_{1}$ and $\rho_{2}$ in the respective SCCs. The difference between the effects of $\rho_{1}$ and $\rho_{2}$ is the sum of differences of each segments, and hence also belongs to $\mathsf{CycleSpace}_{\mathbb{Q}}(V)$ . $\hfill\vartriangleleft$

Claim 10.

For every configuration $p(\mathbf{u})$ and every $C\in\mathbb{N}$ , there are at most $n\cdot(d\cdot C)^{g}$ many $C$ -small configurations reachable from $p(\mathbf{u})$ .

Proof Sketch.

The idea is to prove two facts: 1) For every set $K\subseteq[d]$ of distinguished coordinates, there is at most one clean basis $B$ . 2) If $q(\mathbf{v}),q(\mathbf{v^{\prime}})$ are both reachable from $p(\mathbf{u})$ , and $\pi_{K}(\mathbf{v})=\pi_{K}(\mathbf{v}^{\prime})$ , then $\mathbf{v}=\mathbf{v}^{\prime}$ (here we use Claim 9).

This leads to the given bound of $|Q|\cdot\binom{d}{g}\cdot C^{g}\leq n\cdot(d\cdot C)^{g}$ since any $C$ -small configuration is uniquely determined by its state $q\in Q$ , the subset $K\subseteq[d]$ s.t. it is small w.r.t. the corresponding clean basis $B$ and the vector $\pi_{K}(\mathbf{v})\in[0,C-1]^{g}$ . $\hfill\vartriangleleft$

Now, again similar to Rackoff’s original proof, we would like to argue that if a configuration is $C$ -large, then there is some counter that is sufficiently large (so it can be “ignored”). We aim to prove something stronger. Namely, if a configuration is $C$ -large, then there is a collection of counters which are all sufficiently large and by “ignoring” them, the geometric dimension of the VASS decreases. The following claim states that if a vector $\mathbf{v}$ is $C$ -large, then there is some clean basis $B$ and a vector from this basis $\mathbf{b}_{i}$ which can be used to identify which coordinates of $\mathbf{v}$ are large.

Claim 11.

Let $U\subseteq\mathbb{Q}^{d}$ be a $g$ -dimensional vector space, let $\mathbf{v}\in\mathbb{N}^{d}$ , and let $C\in\mathbb{N}$ . If $\mathbf{v}$ is $C$ -large with respect to $U$ , then there exists a clean basis $B=\{\mathbf{b}_{1},\ldots,\mathbf{b}_{g}\}$ of $U$ and an index $i\in[g]$ such that, for every $j\in[d]$ , $\mathbf{b}_{i}[j]\neq 0$ implies that $\mathbf{v}[j]\geq C$ .

Proof Sketch.

Let $\mathbf{v}$ be a $C$ -large vector. Assume, for sake of contradiction, that there does not exist a clean basis $B$ and an index $i\in[g]$ such that, for every $j\in[d]$ , $\mathbf{b}_{i}[j]\neq 0$ implies that $\mathbf{v}[j]\geq C$ . Consider a clean basis $B=\{\mathbf{b}_{1},\ldots,\mathbf{b}_{g}\}$ with a distinguished set of coordinates $K=\{k_{1},\ldots,k_{g}\}$ . As $\mathbf{v}$ is $C$ -large, there exists $i\in[g]$ such that $\mathbf{v}[k_{i}]\geq C$ . Our assumption says that there also exists $j\in[d]$ such that $\mathbf{b}_{i}[j]\neq 0$ and $\mathbf{v}[j]<C$ . The idea is to construct a new clean basis $B^{\prime}$ and make $j$ the distinguished coordinate instead of $k_{i}$ . This is done by using the non-zero entry $\mathbf{b}_{i}[j]$ to cancel the $j$ -th entry of other base vectors. Let $K^{\prime}$ be the distinguished coordinates of $B^{\prime}$ , which is just $K$ with $k_{i}$ replaced by $j$ . One can observe that $\lVert\pi_{K^{\prime}}(\mathbf{v})\rVert_{1}<\lVert\pi_{K}(\mathbf{v})\rVert_{1}$ because $\mathbf{v}[k_{i}]\geq C$ and $\mathbf{v}[j]<C$ . This norm cannot be decreased infinitely. Hence a contradiction is exhibited. $\hfill\vartriangleleft$

With the definition of geometrically small configurations in hand and an understanding that configurations that are not small will have counters with large values, we are ready to prove Theorem 6. As a first step towards proving Theorem 6, we shall define the bound on the length of runs that we would like to establish.

L_{i}\coloneqq\begin{cases}n-1&\text{ for }i=0\\ n(d(\lVert\mathbf{y}\rVert_{\infty}+M\cdot L_{i-1}))^{i}+L_{i-1}&\text{ for }i% \geq 1\end{cases}

Our goal is to prove that coverability is witnessed by runs of length at most $L_{g}$ (Lemma 12).

Lemma 12.

If there is a run in $V$ from $s(\mathbf{x})$ that covers $t(\mathbf{y})$ , then there is a run from $s(\mathbf{x})$ that covers $t(\mathbf{y})$ of length at most $L_{g}$ .

Proof.

Proof by induction on the geometric dimension $g$ . For $g=0$ , we know that all cycles in $V$ have zero effect. This means that the shortest run between any pair of configurations does not visit a state more than once. Hence, if there is a run in $V$ from $s(\mathbf{x})$ that covers $t(\mathbf{y})$ , then there is one of length at most $L_{0}=n-1$ .

For $g\geq 1$ , we shall assume Lemma 12 holds for VASS with geometric dimension $g-1$ . Now, assume that there is a run in $V$ from $s(\mathbf{x})$ that covers $t(\mathbf{y})$ . Let $s(\mathbf{x})\xrightarrow{\pi}t(\mathbf{y^{\prime}})$ , for some $\mathbf{y}^{\prime}\geq\mathbf{y}$ , be the shortest run from $s(\mathbf{x})$ that covers $t(\mathbf{y})$ . We will split this run about the first configuration that is $C$ -large for $C=M\cdot L_{g-1}+\lVert\mathbf{y}\rVert_{\infty}$ . Precisely, consider the decomposition: $s(\mathbf{x})\xrightarrow{\pi_{\text{small}}}q(\mathbf{m})\xrightarrow{\pi_{% \text{tail}}}t(\mathbf{y^{\prime}})$ , where $q(\mathbf{m})$ is the first $C$ -large configuration.

Since $s(\mathbf{x})\xrightarrow{\pi}t(\mathbf{y^{\prime}})$ has minimal length, we know that no configuration is repeated. This means that the length of $\pi_{\text{small}}$ is at most $n\cdot(d\cdot C)^{g}=n(d(M\cdot L_{g-1}+\lVert\mathbf{y}\rVert_{\infty}))^{g}$ (by Claim 10).

Now, we will use the inductive assumption to bound the length of $\pi_{\text{tail}}$ . Since $q(\mathbf{m})$ is $(M\cdot L_{g-1}+\lVert\mathbf{y}\rVert_{\infty})$ -large, by Claim 11, there exists a clean basis $B=\{\mathbf{b}_{1},\ldots,\mathbf{b}_{g}\}$ and an index $i\in[g]$ such that, for every $j\in[d]$ , if $\mathbf{b}_{i}[j]\neq 0$ , then $\mathbf{m}[j]\geq M\cdot L_{g-1}+\lVert\mathbf{y}\rVert_{\infty}$ . In fact, we shall define $J\coloneqq\{j\in[d]:\mathbf{b}_{i}[j]\neq 0\}$ . Now, we shall remove the counters in $J$ from the VASS $V$ . Let $V^{\prime}=(Q,T^{\prime})$ be the $(d-\lvert J\rvert)$ -VASS obtained by projecting all transition vectors to the coordinates $[d]\setminus J$ . Precisely, $T^{\prime}=\{(p,\pi_{[d]\setminus J}(\mathbf{u}),p^{\prime}):(p,\mathbf{u},p^{% \prime})\in T\}$ . Recall that $B=\{\mathbf{b}_{1},\ldots,\mathbf{b}_{g}\}$ was a basis of $\mathsf{CycleSpace}_{\mathbb{Q}}(V)$ . We will argue that

B^{\prime}=\{\pi_{[d]\setminus J}(\mathbf{b}_{1}),\ldots,\pi_{[d]\setminus J}(% \mathbf{b}_{i-1}),\pi_{[d]\setminus J}(\mathbf{b}_{i+1}),\ldots,\pi_{[d]% \setminus J}(\mathbf{b}_{g})\}

is a generating set of $\mathsf{CycleSpace}_{\mathbb{Q}}(V^{\prime})$ which suffices to prove that the geometric dimension of $V^{\prime}$ is $g-1$ . Since the transition vectors of $V^{\prime}$ are the transition vectors of $V$ projected to counters $[d]\setminus J$ , we know that $\mathsf{CycleSpace}_{\mathbb{Q}}(V^{\prime})$ is just $\mathsf{CycleSpace}_{\mathbb{Q}}(V)$ projected to counters $[d]\setminus J$ . This means that the span of $\{\pi_{[d]\setminus J}(\mathbf{b}_{1}),\ldots,\pi_{[d]\setminus J}(\mathbf{b}_% {g})\}$ is $\mathsf{CycleSpace}_{\mathbb{Q}}(V^{\prime})$ . Now, notice that $\pi_{[d]\setminus J}(\mathbf{b}_{i})=\mathbf{0}$ (by definition of $J$ ). We can therefore remove $\pi_{[d]\setminus J}(\mathbf{b}_{i})$ from this set to obtain the generating set $B^{\prime}$ of size $g-1$ .

Now, we shall analyse the length of the suffix of the run in $V^{\prime}$ . Consider the configuration $q(\pi_{[d]\setminus J}(\mathbf{m}))$ . By the inductive assumption, we know that there is a run in $V^{\prime}$ from $q(\pi_{[d]\setminus J}(\mathbf{m}))$ that covers $t(\pi_{[d]\setminus J}(\mathbf{y}))$ of length at most $L_{g-1}$ . Now, we shall lift this run back to $V$ (by copying the appropriate transitions). It remains to argue that the counters in $J$ remain above $0$ and cover the target $\mathbf{y}$ . For this, recall that for all $j\in J$ , $\mathbf{m}[j]\geq M\cdot L_{g-1}+\lVert\mathbf{y}\rVert_{\infty}$ . The most negative effect of a single transition is $-M$ , thus over the suffix of length $L_{g-1}$ , the greatest possible negative effect is $-M\cdot L_{g-1}$ . This means that all counters in $J$ remain above zero, and at the end have counter values at least $\lVert\mathbf{y}\rVert_{\infty}$ (which guarantees the target is covered). Thus, by following the same suffix from $q(\mathbf{m})$ in $V$ , we obtain a run in $V$ from $q(\mathbf{m})$ that covers $t(\mathbf{y})$ of length at most $L_{g-1}$ . As $\pi_{\text{tail}}$ has minimal length, we therefore conclude that the length of $\pi_{\text{tail}}$ is at most $L_{g-1}$ .

Altogether, the length of $\pi$ is at most the length of $\pi_{\text{small}}$ plus the length of $\pi_{\text{tail}}$ which is $n(d(M\cdot L_{g-1}+\lVert\mathbf{y}\rVert_{\infty}))^{g}+L_{g-1}=L_{g}$ (as required). $\hfill\blacktriangleleft$

Finally, to prove Theorem 6, we only need to argue that $L_{g}$ is indeed bounded by $\textup{poly}(d,n,M,\lVert\mathbf{y}\rVert_{\infty})^{f(g)}$ . This can be obtained by a rather straightforward induction on $g$ .

$\blacktriangleright$ Remark 13.

As a corollary of Theorem 6, one can obtain double exponential length witnesses for coverability in terms of the SCC dimension and the number of states in the VASS. Recall that by Lemma 3, the product of ${g_{\textsc{scc}}}$ and the number of states $n$ is an upper bound of $g$ . Hence, if there is a run from $s(\mathbf{x})$ that covers $t(\mathbf{y})$ , then there is a run from $s(\mathbf{x})$ that covers $t(\mathbf{y})$ of length at most $\textup{poly}(d,n,M,\lVert\mathbf{y}\rVert_{\infty})^{f(n\cdot{g_{\textsc{scc}% }})}$ . Unfortunately, this means that even when the SCC dimension is fixed, the length of the shortest runs witnessing coverability can depend doubly-exponentially on the number of states $n$ .

3.1 Improving Coverability Witness Length Bounds

In this section we continue to study the coverability problem in VASS parameterised by geometric dimension $g$ . Our main result here is an improved version of Theorem 6 with the function $h(x)=2^{x+1}-1$ improving upon function $f(x)=(x+1)^{x}$ from Theorem 6.

Theorem 14.

Let $h:\mathbb{N}\to\mathbb{N}$ , $h(x)\coloneqq 2^{x+1}-1$ . If there is a run in $V$ from $s(\mathbf{x})$ that covers $t(\mathbf{y})$ , then there exists a run in $V$ from $s(\mathbf{x})$ that covers $t(\mathbf{y})$ of length at most $\textup{poly}(d,n,M,\lVert\mathbf{y}\rVert_{\infty})^{h(g)}$ .

Similar to how the proof of Theorem 6 was based on the ideas introduced by Rackoff in [44], the proof of Theorem 14 is based on the ideas from a recent paper by Kunnemann et al. [29], where it was shown that the length of a covering run can be bounded by $\textup{poly}(d,n,M,\lVert\mathbf{y}\rVert_{\infty})^{2^{\mathcal{O}(d)}}$ . Similarly as in [44] the construction from [29] uses an induction on the dimension $d$ . It also uses the fact that if a counter becomes “sufficiently large” then there is no need to worry that this counter will drop below zero and we can simply ignore this counter. The main contribution of [29] is an observation that if a few counters become sufficiently large together we can ignore all of them at once. Therefore, the threshold above which we ignore them is lower. In other words: in [44] a configuration is treated as large if one of its counters exceeds some threshold $C$ , while in [29] a configuration is treated as large if either one of its counters exceeds an appropriate threshold $C_{d-1}$ , or two of its counters exceed some smaller threshold $C_{d-2}$ , or three of its counters exceed some even smaller threshold $C_{d-3}$ , etc., or all of its counters exceed a quite small threshold $C_{0}$ . Towards generalising this result we call vectors which do not satisfy this assumption $\mathbf{C}=(C_{0},\ldots,C_{d-1})$ -bounded and generalise this notion to $\mathbf{C}$ -thin.

Definition 15 (Bounded and thin configurations).

Let $\mathbf{C}=(C_{0},C_{1},\ldots,C_{g-1})\in\mathbb{N}^{g}$ be a vector of constants for some $C_{0}\leq C_{1}\leq\ldots\leq C_{g-1}$ . A vector $\mathbf{v}\in\mathbb{N}^{g}$ is $\mathbf{C}$ -bounded if for all $k\in[g]$ the number of coordinates $i\in[g]$ such that $\mathbf{v}[i]\geq C_{g-k}$ is strictly less than $k$ . A vector $\mathbf{v}\in\mathbb{N}^{d}$ is $\mathbf{C}$ -thin with respect to $g$ -dimensional vector space $U\subseteq\mathbb{Q}^{d}$ if there exists a clean basis $B$ of $U$ with set of distinguished coordinates $K$ such that $\pi_{K}(\mathbf{v})$ is $\mathbf{C}$ -bounded. Moreover, we say that a configuration $q(\mathbf{v})$ of a VASS $V$ is $\mathbf{C}$ -thin if $\mathbf{v}$ is $\mathbf{C}$ -thin with respect to $\mathsf{CycleSpace}_{\mathbb{Q}}(V)$ . If a vector $\mathbf{v}$ or a configuration $q(\mathbf{v})$ is not $\mathbf{C}$ -thin then we call it $\mathbf{C}$ -thick.

Similarly as before we prove that there are not too many $\mathbf{C}$ -thin configurations reachable from a given configuration, we state it in Claim 16. We say that a vector $\mathbf{v}\in\mathbb{N}^{k}$ is sorted if for each $i,j\in[k]$ , $i<j$ we have $\mathbf{v}[i]\leq\mathbf{v}[j]$ .

Claim 16.

For every configuration $p(\mathbf{u})$ and every sorted $\mathbf{C}=(C_{0},C_{1},\ldots,C_{g-1})\in\mathbb{N}^{g}$ there are at most $n\cdot d^{g}\cdot\prod_{i=0}^{g-1}C_{i}$ many $\mathbf{C}$ -thin configurations reachable from $p(\mathbf{u})$ .

Proof.

The proof is similar to the proof of Claim 10. We argue as before that there are at most $d^{g}$ clean basis. For a fixed clean basis and one of $n$ states fixed each configuration corresponds to a $\mathbf{C}$ -bounded vector. The number of such vectors is $\prod_{i=1}^{g}C_{i}$ , therefore the number of $\mathbf{C}$ -thin configurations is bounded by $n\cdot d^{g}\cdot\prod_{i=1}^{g}C_{i}$ , as required. $\hfill\vartriangleleft$

In analogue of Kunnemann et. al., we would like to argue that if a configuration is $\mathbf{C}$ -large, then there is a number of counters that are sufficiently large to be “ignored”. However, as in the proof of Theorem 6 we need to prove something stronger. We show that if a configuration is $\mathbf{C}$ -thick, then there is a collection of counters which are all sufficiently large and by “ignoring” them, the geometric dimension of the VASS decreases appropriately.

Claim 17.

Let $U\subseteq\mathbb{Q}^{d}$ be a $g$ -dimensional vector space, let $\mathbf{v}\in\mathbb{N}^{d}$ , and let $\mathbf{C}=(C_{0},\ldots,C_{g-1})\in\mathbb{N}^{g}$ be sorted. If $\mathbf{v}$ is $\mathbf{C}$ -thick with respect to $U$ , then there exists a clean basis $B=\{\mathbf{b}_{1},\ldots,\mathbf{b}_{g}\}$ of $U$ , a number $k\in[g]$ and a set $S=\{i_{1},\ldots,i_{k}\}\subseteq[g]$ of $k$ indices such that for every $i\in S$ and every $j\in[d]$ , $\mathbf{b}_{i}[j]\neq 0$ implies that $\mathbf{v}[j]\geq C_{g-k}$ .

Proof.

The proof of Claim 17 is similar to the proof of Claim 11. The difference is as follows. In Claim 11 we need to find one vector $\mathbf{b}_{i}$ in some clean basis $B$ such that all the coordinates affected by $\mathbf{b}_{i}$ (namely $j\in[d]$ such that $\mathbf{b}_{i}[j]\neq 0$ ) have at least value $C$ in our vector $\mathbf{v}$ . Here our task is more challenging. Besides the choice of $B$ we also have a choice of the number $k\in[g]$ indicating how many vectors from $B$ we plan to ignore. For a chosen $k\in[g]$ we need to find vectors $\mathbf{b}_{i_{1}},\ldots,\mathbf{b}_{i_{k}}$ from $B$ such that all the coordinates affected by them have a value at least $C_{g-k}$ .

Even though the task seems more complicated the proof is essentially proceeding the same as the proof of Claim 11. We mainly present here the parts which differ.

Assume, for sake of contradiction, that $\mathbf{v}$ is $\mathbf{C}$ -thick and there does not exist a clean basis $B$ , a number $k\in[g]$ and a set of indices $S=\{i_{1},\ldots,i_{k}\}$ such that for every index $i\in S$ and for every $j\in[d]$ , $\mathbf{b}_{i}[j]\neq 0$ implies that $\mathbf{v}[j]\geq C_{g-k}$ . Consider a clean basis $B=\{\mathbf{b}_{1},\ldots,\mathbf{b}_{g}\}$ with a distinguished set of coordinates $K=\{k_{1},\ldots,k_{g}\}$ of minimal $N\coloneqq\lVert\pi_{K}(\mathbf{v})\rVert_{1}$ .

Now, our goal is to construct a new clean basis $B^{\prime}$ with a distinguished set of coordinates $K^{\prime}$ such that $\lVert\pi_{K^{\prime}}(\mathbf{v})\rVert_{1}$ is less than $N$ . Since $\mathbf{v}$ is $\mathbf{C}$ -thick we know that $\pi_{K}(\mathbf{v})$ is not $\mathbf{C}$ -bounded. That means that there is a number $k\in[g]$ such that the number of coordinates $i\in[g]$ such that $\mathbf{v}[i]\geq C_{g-k}$ is at least $k$ . Let $S=\{i_{1},\ldots,i_{k}\}$ be a set of some $k$ coordinates such that $\mathbf{v}[i_{\ell}]\geq C_{g-k}$ for all $\ell\in[k]$ . Now, using our assumption we get that there is some index $i\in S$ and some coordinate $j\in[d]$ such that $\mathbf{b}_{i}[j]\neq 0$ , but $\mathbf{v}[j]<C_{g-k}$ . That means that substituting the distinguished coordinate $k_{i}$ by the coordinate $j$ will decrease the sum of values $\mathbf{v}[i]$ for distinguished coordinates $i$ , exactly as in the proof of Claim 11.

The rest of the proof is literally the same as for Claim 11. We recall here the definition of the new basis $B^{\prime}$ . We set $B^{\prime}=\{\mathbf{b}^{\prime}_{1},\ldots,\mathbf{b}^{\prime}_{g}\}$ by $\mathbf{b}^{\prime}_{i}\coloneqq{\mathbf{b}_{i}}/{(\mathbf{b}_{i}[j])}$ , and $\mathbf{b}^{\prime}_{k}\coloneqq\mathbf{b}_{k}-\mathbf{b}_{k}[j]\cdot\mathbf{b% }^{\prime}_{i}$ for all $k\neq i$ . We identify the set of distinguished coordinates $K^{\prime}=\{k_{1},\ldots,k_{i-1},j,k_{i+1},\ldots,k_{g}\}$ . Verification that $B^{\prime}$ is a clean basis is performed exactly as in the proof of Claim 11. Finally, we also verify that $\lVert\pi_{K^{\prime}}(\mathbf{v})\rVert_{1}<N$ exactly in the same way as before. The intuition is that $\mathbf{v}[k_{i}]$ was replaced by a smaller value $\mathbf{v}[j]$ , thus $\lVert\pi_{K^{\prime}}(\mathbf{v})\rVert_{1}$ decreased. This contradicts minimality of $N$ and finishes the proof. $\hfill\vartriangleleft$

With the understanding that in a $\mathbf{C}$ -thick configuration one can ignore some coordinates to decrease the geometric dimension we are ready to prove Theorem 14. We first define the bounds on the length of runs that we would like to establish.

K_{i}\coloneqq\begin{cases}n-1&\text{ for }i=0\\ n\cdot d^{i}\cdot\prod_{j=0}^{i-1}(\lVert\mathbf{y}\rVert_{\infty}+M\cdot K_{j% })+K_{i-1}&\text{ for }i\geq 1\end{cases}

Our goal is to prove that coverability is witnessed by runs of length at most $K_{g}$ .

Lemma 18.

If there is run in $V$ from $s(\mathbf{x})$ that covers $t(\mathbf{y})$ , then there is a run from $s(\mathbf{x})$ that covers $t(\mathbf{y})$ of length at most $K_{g}$ .

Proof.

The proof proceeds similarly to the proof of Lemma 12, so we focus on the differences while only sketching the identical parts.

The proof is by induction on the geometric dimension $g$ . The case of $g=0$ is easy and the same as for Lemma 12. For $g\geq 1$ we assume that Lemma 18 holds for VASS with geometric dimension less than $g$ . Now, assume that there is a run in $V$ from $s(\mathbf{x})$ that covers $t(\mathbf{y})$ . Let $s(\mathbf{x})\xrightarrow{\pi}t(\mathbf{y^{\prime}})$ , for some $\mathbf{y}^{\prime}\geq\mathbf{y}$ , be the shortest run from $s(\mathbf{x})$ that covers $t(\mathbf{y})$ . We will split this run at the first configuration that is $\mathbf{C}$ -thick for $\mathbf{C}=(C_{0},C_{1},\ldots,C_{g-1})$ , where $C_{i}=M\cdot K_{i}+\lVert\mathbf{y}\rVert_{\infty}$ . Precisely, consider the decomposition: $s(\mathbf{x})\xrightarrow{\pi_{\text{small}}}q(\mathbf{m})\xrightarrow{\pi_{% \text{tail}}}t(\mathbf{y^{\prime}})$ , where $q(\mathbf{m})$ is the first $\mathbf{C}$ -thick configuration.

Since $s(\mathbf{x})\xrightarrow{\pi}t(\mathbf{y^{\prime}})$ has minimal length, we know that no configuration is repeated. As all the configurations before $q(\mathbf{m})$ are $\mathbf{C}$ -thin we know by Claim 16 that the length of $\pi_{\text{small}}$ is at most $n\cdot d^{g}\cdot\prod_{i=0}^{g-1}C_{i}$ .

Now let us focus on bounding the length of $\pi_{\text{tail}}$ . Since $q(\mathbf{m})$ is $\mathbf{C}$ -thick by Claim 17 we know that there is a clean basis $B=\{\mathbf{b}_{1},\ldots,\mathbf{b}_{g}\}$ of $U$ , a number $k\in[g]$ and a set $S=\{i_{1},\ldots,i_{k}\}\subseteq[g]$ of $k$ indices such that for every $i\in S$ and every $j\in[d]$ , $\mathbf{b}_{i}[j]\neq 0$ implies that $\mathbf{v}[j]\geq C_{g-k}$ . In other words it means that all the coordinates influenced by basis vectors $\mathbf{b}_{i_{1}},\ldots,\mathbf{b}_{i_{k}}$ are of size at least $C_{g-k}$ .

We now sketch bounding $\pi_{\text{tail}}$ without going into details, since the details are the same as in Lemma 12. We consider a VASS $V^{\prime}$ , which is exactly $V$ with coordinates in $J$ removed, where $J$ contains all the coordinates on which one of the $\mathbf{b}_{i_{j}}$ is non-zero (for $j\in[k]$ ). Let $J^{\prime}=[d]\setminus J$ be the complement of $J$ . Removing all the coordinates in $J$ implies that $\dim(\mathsf{CycleSpace}_{\mathbb{Q}}(V^{\prime}))\leq\dim(\mathsf{CycleSpace}% _{\mathbb{Q}}(V))-k$ decreased by $k$ , since all the basis vectors $\mathbf{b}_{i_{j}}$ for $j\in[k]$ are zero vectors after removing coordinates in $J$ . Therefore $V^{\prime}$ has geometric dimension at most $g-k$ and by induction assumption there is a covering run from $q(\mathbf{\pi_{J^{\prime}}(m)})$ to $t(\mathbf{\pi_{J^{\prime}}(y)})$ of length at most $K_{g-k}$ . Now consider this run lifted back to $V$ , with coordinates from $J$ added back. Since max-norm of $V$ is $M$ the run of length $K_{g-k}$ decreases counters in $J$ by at most $M\cdot K_{g-k}$ . Recall however that for each $i\in J$ we have $\mathbf{m}[i]\geq C_{g-k}=M\cdot K_{i}+\lVert\mathbf{y}\rVert_{\infty}$ . That means that after decreasing by $M\cdot K_{g-k}$ all the counters in $J$ still have value at least $\lVert\mathbf{y}\rVert_{\infty}$ . This is sufficient to cover $t(\mathbf{y})$ , so indeed the presented run covers $t(\mathbf{y})$ . Its length is at most the length of $\pi_{\text{small}}$ plus $K_{g-k}\leq K_{g-1}$ , which equals $n\cdot d^{g}\cdot\prod_{i=0}^{g-1}C_{i}+K_{g-1}=K_{g}$ , as required. $\hfill\blacktriangleleft$

In order to prove Theorem 14, we only need to argue that $K_{g}$ is indeed bounded by $\textup{poly}(d,n,M,\lVert\mathbf{y}\rVert_{\infty})^{h(g)}$ , which we show in the following claim.

Claim 19.

For any $g\in\mathbb{N}$ we have $K_{g}\leq\textup{poly}(d,n,M,\lVert\mathbf{y}\rVert_{\infty})^{h(g)}$ for $h(x)=2^{x+1}-1$ .

4 Simultaneous Unboundedness

Viewed as a decision problem, simultaneous unboundedness asks, from a given initial configuration $s(\mathbf{x})$ , whether it is possible to reach a given target state $q$ with counter values $\mathbf{v}\geq(G,\ldots,G)$ , for a given target value $G\in\mathbb{N}$ . One can observe that if such a run does not exist, then there is a bound $H$ such that, for every run, there is a counter which does not exceed $H$ . This observation is a necessary ingredient in the standard approach for solving reachability in VASS (i.e. this is used as a tool in the KLM decomposition) [28, 35]. Simultaneous unboundedness, as well as other variants of (un)boundedness have already been studied in VASS parameterised by the dimension $d$ [15, 7]. In this section, we study simultaneous unboundedness in VASS parameterised by the geometric dimension $g$ .

Throughout this section, unless otherwise specified, we fix our attention to a VASS $V=(Q,T)$ . We also fix the following parameters of $V$ :

$\blacksquare$

$d\in\mathbb{N}$ is the dimension,
$\blacksquare$

$g\leq d$ is the geometric dimension,
$\blacksquare$

$n\coloneqq\lvert Q\rvert$ is the number of states,
$\blacksquare$

$M\coloneqq\max\{\lVert\mathbf{x}\rVert_{\infty}:(p,\mathbf{x},q)\in T\}$ is the magnitude of the greatest effect of any transition.

We will prove that, for all $G\in\mathbb{N}$ , there are $H,L\in\mathbb{N}$ of size $\textup{poly}(d,n,G,M)^{f(g)}$ for some exponential function $f$ s.t. if there is a run in which every counter observes a value $\geq H$ (not necessarily at the same time), then there is a run of length $\leq L$ in which all counters are $\geq G$ simultaneously. The relationship between $G$ , $H$ , and $L$ is detailed in Theorem 20 and their precise values are provided ahead of Lemma 21.

Theorem 20.

Let $f:\mathbb{N}\to\mathbb{N}$ , $f(x)\coloneqq(x+1)^{x+1}$ . For every $G\in\mathbb{N}$ , there exist $H,L\in\mathbb{N}$ such that $H,L\leq\textup{poly}(d,n,G,M)^{f(g)}$ and, if there exists a run from $s(\mathbf{x})$ to $q(\mathbf{u})$ in which, for every $i\in[d]$ , there is a configuration $p_{i}(\mathbf{h}_{i})$ with $\mathbf{h}_{i}[i]\geq H$ , then there exists a run from $s(\mathbf{x})$ to $q(\mathbf{v})$ of length at most $L$ , such that $\mathbf{v}\geq(G,\ldots,G)$ .

The proof of Theorem 20 is very similar to the proof of Theorem 6 which is based on Rackoff’s proof that coverability is witnessed by a double exponential length run [44]. We will sketch the ideas behind the proof of Theorem 20 first for the scenario in which the VASS is parameterised by its dimension $d$ (not its geometric dimension). Given the assumption that there is a run in which every counter exceeds the threshold $H$ (at some point), we can “ignore” the first counter that exceeds this threshold. This idea is that, if in a $(d-1)$ -VASS, we can prove that there is a run that witnesses simultaneous unboundedness of length $L$ , and we know that $H\geq M\cdot L+G$ , then we can “safely ignore” the counter that exceeded the threshold $H$ . Accordingly, we proceed by induction on the dimension with appropriately chosen values for $H$ and $L$ . In our case, we are considering VASS parameterised by the geometric dimension $g$ . Just like the proof of Theorem 6, we instead wish to ignore multiple counters at the same time in order to decrease the geometric dimension by 1 for the inductive step. For this, we consider two levels of “large”: a large upper bound $C$ and very large threshold $H$ . We use the idea that, from a geometrically $C$ -large configuration, we can “safely ignore” a collection of counters that will decrease the geometric dimension. However, after the first $C$ -large configuration is observed, we have to prove that we still fulfill the induction hypothesis that there is a run which observes a large value on every counter. In order to still observe configurations that exceed the threshold, we need to set the threshold $H$ to be (significantly) larger than $C$ . Next, we will precisely define the threshold and upper bound values. Fix $G\in\mathbb{N}$ . Let us inductively define three sequences of numbers.

C_{i}=\begin{cases}0&i=0,\\ M\cdot L_{i-1}+G&i\geq 1.\end{cases}\qquad H_{i}=\begin{cases}n\cdot(d+1)\cdot M% +G&i=0,\\ n\cdot M\cdot(d\cdot C_{i})^{i}+H_{i-1}&i\geq 1.\end{cases}

L_{i}=\begin{cases}n\cdot(d+1)&i=0,\\ n\cdot(d\cdot C_{i})^{i}+L_{i-1}&i\geq 1.\end{cases}

Lemma 21.

If there exists a run from $s(\mathbf{x})$ to $q(\mathbf{u})$ in which, for every $i\in[d]$ , there is a configuration $p_{i}(\mathbf{h}_{i})$ with $\mathbf{h}_{i}[i]\geq H_{g}$ , then there exists a run from $s(\mathbf{x})$ to $q(\mathbf{v})$ of length at most $L_{g}$ , such that $\mathbf{v}\geq(G,\ldots,G)$ .

Proof.

In this proof, we shall refer to the configurations $p_{i}(\mathbf{h}_{i})$ as high configurations.

This proof goes by induction on $g$ . For $g=0$ , consider a run from $s(\mathbf{x})$ to $q(\mathbf{u})$ and consider every high configuration $p_{i}(\mathbf{h}_{i})$ . We shall mark the starting configuration $s(\mathbf{x})$ , every high configuration $p_{i}(\mathbf{h}_{i})$ , and the final configuration $q(\mathbf{u})$ . Since $g=0$ , all cycles have zero effect. This means that, between every consecutive marked configuration, we can remove simple cycles. We remark that we cannot simply remove simple cycles from the entire run, as it may be the case that a high configuration is observed by using a cycle. Indeed, a particular counter may exceed the threshold $H_{0}$ by making use of a cycle that may change its value throughout the course of the cycle (even though the cycle overall has zero effect). Now, we know that there is a run from $s(\mathbf{x})$ to $q(\mathbf{u})$ which observes every high configuration $p_{i}(\mathbf{h}_{i})$ , and whose length is bounded by $n(d+1)=L_{0}$ . Now, we will argue that $\mathbf{u}\geq(G,\ldots,G)$ . Consider the $i$ -th counter: it is at least $H_{0}=n\cdot(d+1)\cdot M+G$ at $p_{i}(\mathbf{h}_{i})$ . Notice that the run from $p_{i}(\mathbf{h}_{i})$ to $q(\mathbf{u})$ has length at most $(d+1)\cdot n$ . This means that at the end of the run, the $i$ -th counter will be at least $n\cdot(d+1)\cdot M+G-(d+1)\cdot n\cdot M\geq G$ (as required).

For the induction step, assume that Lemma 21 is true for all geometric dimensions less than $g$ . Now suppose that there is a run $s(\mathbf{x})\xrightarrow{\rho}q(\mathbf{u})$ in which, for every $i\in[d]$ , there is a configuration $p_{i}(\mathbf{h}_{i})$ with $\mathbf{h}_{i}[i]\geq H_{g}$ . Recall Definition 8 and split $\rho$ at the first $C_{g}$ -large configuration $p(\mathbf{m})$ to obtain $s(\mathbf{x})\xrightarrow{\rho_{\text{small}}}p(\mathbf{m})\xrightarrow{\rho_{% \text{tail}}}q(\mathbf{u})$ . In fact, let $s(\mathbf{x})\xrightarrow{\rho}q(\mathbf{u})$ be the shortest such run.

By the minimality of the length of $s(\mathbf{x})\xrightarrow{\rho}q(\mathbf{u})$ , we know that no configuration is repeated. Thus, by Claim 10, we know that $|\rho_{\text{small}}|\leq n\cdot(d\cdot C_{g})^{g}$ .

Moreover, by Claim 11, there is a clean basis $B=\{\mathbf{b}_{1},\ldots,\mathbf{b}_{g}\}$ and an index $i\in[g]$ such that, for every $j\in[d]$ , if $\mathbf{b}_{i}[j]\neq 0$ then $\mathbf{m}[j]\geq C_{g}$ . In the same way as in the proof of Lemma 12, we will project away all counters $J=\{j\in[d]:\mathbf{b}_{i}[j]\neq 0\}$ to obtain a VASS $V^{\prime}$ of dimension $d-\lvert J\rvert$ but, crucially, of geometric dimension $\leq g-1$ .

Additionally, for every $i\in[d]$ , there is a high configuration $p_{i}(\mathbf{h}_{i})$ observed during $s(\mathbf{x})\xrightarrow{\rho}q(\mathbf{u})$ such that $\mathbf{h}_{i}[i]\geq H_{g}$ . Our goal is to replace $\rho_{\text{tail}}$ with a sufficiently short run using the inductive assumption. Roughly speaking, after projecting away counters in $J$ , we wish to identify a run in $V^{\prime}$ starting from $p(\pi_{[d]\setminus J}(\mathbf{m}))$ which ends with all counter values at least $G$ . To do this, we need to identify configurations in $p(\mathbf{m})\xrightarrow{\rho_{\text{tail}}}q(\mathbf{u})$ which are high. Specifically, for every $i\in[d]\setminus J$ , we need to identify a configuration $p_{i}(\mathbf{h}_{i})$ that occurs in $p(\mathbf{m})\xrightarrow{\rho_{\text{tail}}}q(\mathbf{u})$ that satisfies $\mathbf{h}_{i}[i]\geq H_{g-1}$ . We remark that the original high configuration $p_{i}(\mathbf{h}_{i})$ may be observed during $\rho_{\text{small}}$ or $\rho_{\text{tail}}$ ; clearly if the high configuration $p_{i}(\mathbf{h}_{i})$ , for $i\in[d]\setminus J$ , is observed during $\rho_{\text{tail}}$ , then it satisfies $\mathbf{h}_{i}[i]\geq L_{g}>L_{g-1}$ . For the high configurations $p_{i}(\mathbf{h}_{i})$ that are observed during $\rho_{\text{small}}$ , we will prove that there is a configuration observed during $\rho_{\text{tail}}$ that is sufficiently high on the same counter. In fact, we will prove that this configuration is $p(\mathbf{m})$ . Namely, for every $i\in[d]\setminus J$ , for which $p_{i}(\mathbf{h}_{i})$ occurs in $s(\mathbf{x})\xrightarrow{\rho_{\text{small}}}p(\mathbf{m})$ , it is true that $\mathbf{m}[i]\geq H_{g-1}$ . This is because $H_{g}=n\cdot(d\cdot C_{g})^{g}\cdot M+H_{g-1}\geq\lvert\rho_{\text{small}}% \rvert\cdot M+H_{g-1}$ .

Therefore, we can apply the induction assumption on $V^{\prime}$ starting from $p(\pi_{[d]\setminus J}(\mathbf{m}))$ to find a run $p(\pi_{[d]\setminus J}(\mathbf{m}))\xrightarrow{\pi}q(\mathbf{u^{\prime}})$ , of length at most $L_{g-1}$ , such that $\mathbf{u}^{\prime}\geq(G,\ldots,G)$ . Since all the ignored counters have value at least $C_{g}=M\cdot L_{g-1}+G$ in the configuration $p(\mathbf{m})$ , we deduce that the run $p(\mathbf{m})\xrightarrow{\pi^{\prime}}q(\mathbf{w})$ in $V$ obtained by following the same path as $\pi$ has length at most $L_{g-1}$ and $\mathbf{w}\geq(G,\ldots,G)$ . Finally, the concatenation of $\rho_{\text{small}}$ and $\pi^{\prime}$ has length at most $n\cdot(d\cdot C_{g})^{g}+L_{g-1}=L_{g}$ . $\hfill\blacktriangleleft$

Now, to conclude this section by proving Theorem 20, we only need to argue that $L_{g}$ and $H_{g}$ are indeed bounded by $\textup{poly}(d,n,M,G)^{f(g)}$ , which can be shown by induction on $g$ .

5 Boundedness

In this section we study the boundedness problem in VASS parameterized by geometric dimension, which asks whether infinitely many configurations can be reached from a fixed source. We first recall that unboundedness is witnessed by any run that contains a configuration strictly covering a previous configuration. Consider a run of the form $c_{0}\xrightarrow{u_{1}}c_{1}\xrightarrow{u_{2}}c_{2}\cdots\xrightarrow{u_{m}}% c_{m}$ . We say it is an unboundedness witness for $c_{0}$ if there is an index $i<m$ such that $c_{i}<c_{m}$ . In this case, observe that the cycle from $c_{i}$ to $c_{m}$ can be fired any number of times from $c_{m}$ to reach infinitely many configurations. On the other hand, assume the reachable set from $c_{0}$ is indeed infinite. The configurations reachable from $c_{0}$ naturally form a finite-branching tree with root $c_{0}$ . By König’s Lemma there must be an infinite branch in this tree. Using the fact that $\leq$ is a well-quasi-order over configurations, we are able to extract an unboundedness witness from this branch.

Lemma 22 ([44, Lemma 4.2]).

Let $V$ be a VASS and $c$ be a configuration of $V$ . Then $\{c^{\prime}\mid c\xrightarrow{*}c^{\prime}\}$ is infinite if and only if there is an unboundedness witness for $c$ .

We remark that unboundedness witnesses were called self-covering paths in [44]. Now the boundedness problem is reduced to finding unboundedness witnesses. Our result, resembling that of Rackoff [44], gives length bounds on shortest unboundedness witnesses in terms of the geometric dimension. Similarly as in Section 3 we fix the following parameters of $V$ :

$\blacksquare$

$d\in\mathbb{N}$ is the dimension,
$\blacksquare$

$g\leq d$ is the geometric dimension,
$\blacksquare$

$n\coloneqq\lvert Q\rvert$ is the number of states,
$\blacksquare$

$M\coloneqq\max\{\lVert\mathbf{x}\rVert_{\infty}:(p,\mathbf{x},q)\in T\}$ is the magnitude of the greatest effect of any transition.

Theorem 23.

Let $f:\mathbb{N}\to\mathbb{N}$ , $f(x)\coloneqq(4x+2)^{2x+1}$ . If there is an unboundedness witness in VASS $V$ for some configuration $s$ then there is also one of length bounded by $\textup{poly}(d,n,M)^{f(g)}$ .

$\blacktriangleright$ Remark 24.

Observe that in Theorem 23 if we fix the geometric dimension $g$ then the corresponding bound is polynomial w.r.t. $d, n,$ and $M$ . Moreover, the bounds do not depend on the configuration $s$ .

$\blacktriangleright$ Remark 25.

Similar to Remark 13, using Lemma 3 we can obtain a length bound on unboundedness witnesses in terms of the SCC dimension ${g_{\textsc{scc}}}$ and the number of states, namely $\textup{poly}(d,n,M)^{f(n\cdot{g_{\textsc{scc}}})}$ .

5.1 Length Bound of Unboundedness Witnesses

We will actually prove Theorem 23 for a generalized model called VASS extended with integer counters, which allow some counters to take negative values in a run.

Formally, a $d$ -VASS extended with integer counters is given by a triple $V_{\mathbb{Z}}=(V,I_{\mathbb{N}},I_{\mathbb{Z}})$ where $V=(Q,T)$ is a $d$ -VASS and $I_{\mathbb{N}},I_{\mathbb{Z}}$ is a partition of $[d]$ . We remark that the underlying VASS $V$ will be the one under consideration of this section. And we use its parameters $g, n, M$ as fixed at the beginning of this section. The set of legal configurations of $V_{\mathbb{Z}}$ is given by $\{q(\mathbf{x})\in Q\times\mathbb{Z}^{d}\mid\mathbf{x}[i]\in\mathbb{N}\text{ % for all }i\in I_{\mathbb{N}}\}$ . That is, counters indexed by $I_{\mathbb{Z}}$ are allowed to take negative values while other counters must be kept nonnegative. Unboundedness witnesses are defined in the same way as for standard VASS. So an unboundedness witness for configuration $c$ is a run $\pi=\pi_{1}\pi_{2}$ starting from $c$ such that $\pi_{2}$ is a cycle with positive effect $\textup{eff}(\pi_{2})>\mathbf{0}$ . However, as opposed to prior sections, VASS extended with integers counters have two natural notions of geometric dimension. We define the geometric dimension of $V_{\mathbb{Z}}$ to be the geometric dimension $g$ of $V$ , i.e. using all counters. We also define the restricted geometric dimension of $V_{\mathbb{Z}}$ , denoted $k_{\textsc{res}}(V_{\mathbb{Z}})$ , to be the geometric dimension of the VASS obtained from $V$ by removing all counters in $I_{\mathbb{Z}}$ . That is,

k_{\textsc{res}}(V_{\mathbb{Z}})=\dim(\pi_{I_{\mathbb{N}}}(\mathsf{CycleSpace}% _{\mathbb{Q}}(V))).

(1)

We will prove Theorem 23 for VASS extended with integer counters. As first step, we define the bounds on the length of unboundedness witnesses that we would like to establish.

\displaystyle L_{i}=\begin{cases}D^{g+1}&\text{for }i=0\\ (D\cdot(d\cdot M\cdot L_{i-1})^{4i})^{g+1}+L_{i-1}&\text{for }i\geq 1\end{cases}

where $D=(5d^{2}n^{2}M)^{2}$ . We are going to prove the following lemma.

Lemma 26.

If there is an unboundedness witness in $V_{\mathbb{Z}}=(V,I_{\mathbb{N}},I_{\mathbb{Z}})$ for some configuration $s$ , then there is also one of length bounded by $L_{k}$ where $k=k_{\textsc{res}}(V_{\mathbb{Z}})\leq g$ .

For a standard VASS $V$ we have $k_{\textsc{res}}(V)=g$ . Therefore, Lemma 26 bounds the length of shortest unboundedness witnesses by $L_{g}$ . It can be verified that $L_{g}$ is indeed at most doubly exponential, hence Theorem 23 is implied by Lemma 26.

The rest of this section is devoted to proving Lemma 26. Let $V_{\mathbb{Z}}=(V,I_{\mathbb{N}},I_{\mathbb{Z}})$ be the considered $d$ -VASS extended with integer counters, and $s$ be a configuration of $V$ such that there is an unboundedness witness $\pi$ for $s$ . Suppose $V=(Q,T)$ . Moreover, we may assume w.l.o.g. that $V$ contains only those transitions in $\pi$ . Under this assumption, the structure of $V$ is simply a series of SCCs, and Claim 9 can be applied. In the following we show Lemma 26 by induction on the restricted geometric dimension $k=k_{\textsc{res}}(V)$ .

The Base Case

First we consider the case that $k=0$ , which means that every cycle $\theta$ in $V$ satisfies $\pi_{I_{\mathbb{N}}}(\textup{eff}(\theta))=\mathbf{0}$ . Observe however that transitions may still have effects on $\mathbb{N}$ -counters, hence it is not obvious that they can be ignored. The following claim crucially uses our above assumption that $V$ contains only those transitions on the run $\pi$ .

Claim 27.

Any path $\rho$ in $V$ can be lifted to a run $s\xrightarrow{\rho}c$ for some configuration $c$ . Moreover, for any reachable configuration $q(\mathbf{y})$ and any configuration $q(\mathbf{y}_{\pi})$ on the unboundedness witness $\pi$ (with the same state), we have $\pi_{I_{\mathbb{N}}}(\mathbf{y}_{\pi})=\pi_{I_{\mathbb{N}}}(\mathbf{y})$ .

By Claim 27, in order to find an unboundedness witness it is enough to find paths with certain effects, since every path can be lifted to a run. Therefore in the following we assume $I_{\mathbb{N}}=\emptyset$ , that is, $V_{\mathbb{Z}}$ has only integer counters. We decompose the unboundedness witness $\pi$ as $\pi=\pi_{1}\pi_{2}$ such that $\pi_{2}$ is a cycle with $\textup{eff}(\pi_{2})>\mathbf{0}$ . Since all counters are integer counters, we can replace $\pi_{1}$ by a simple path connecting its source and target states, so that $|\pi_{1}|\leq n$ . We now express $\pi_{2}$ as a solution of a system of linear inequalities, and rely on Lemma 5 to obtain a bound of its length. Let $Q^{\prime}\subseteq Q$ and $T^{\prime}\subseteq T$ be the subsets of states and transitions that appear in $\pi_{2}$ . Simple cycles that use only transitions from $T^{\prime}$ will be called $T^{\prime}$ -cycles. We first shrink $\pi_{2}$ into a short run $\sigma$ as follows: whenever there is a simple cycle $\theta$ as an infix of $\pi_{2}$ , such that every state visited by $\theta$ is also visited by the prefix of $\pi_{2}$ before $\theta$ , we remove $\theta$ from $\pi_{2}$ . Notice that $\sigma$ also visits every state in $Q^{\prime}$ . Also observe that $|\sigma|\leq n^{2}$ as $\sigma$ visits every state at most $n$ times. Let $\mathcal{S}$ be the set of simple cycles removed from $\pi_{2}$ . For each cycle $\theta\in\mathcal{S}$ we have $\textup{{norm}}(\textup{eff}(\theta))\leq nM$ as it is a simple cycle. Observe that $\textup{eff}(\pi_{2})-\textup{eff}(\sigma)\in\mathop{\operatorname{cone}}% \nolimits_{\mathbb{N}}(\textup{eff}(\mathcal{S}))$ . Therefore, because of Theorem 2 we can choose $\mathcal{C}\subseteq\mathcal{S}$ such that $|\mathcal{C}|\leq 2d\log(4dnM)\leq 4d^{2}nM$ and $\textup{eff}(\pi_{2})-\textup{eff}(\sigma)\in\mathop{\operatorname{cone}}% \nolimits_{\mathbb{N}}(\textup{eff}(\mathcal{C}))$ . We define a system $U$ of $d$ linear inequalities, with unknowns $x_{\theta}$ correspond to $T^{\prime}$ -cycles $\theta$ from $\mathcal{C}$ . Concretely, for $i\in[1,d]$ we have the following inequality, where $[]$ is the Iverson bracket.:

\displaystyle\sum_{\theta\in\mathcal{C}}x_{\theta}\cdot\textup{eff}(\theta)[i]% +\textup{eff}(\sigma)[i]\geq[\textup{eff}(\pi_{2})[i]>0]

(2)

Any solution of $U$ induces a run $\pi_{2}^{\prime}$ obtained by attaching to $\sigma$ each cycle $\theta\in\mathcal{C}$ repeated for $x_{\theta}$ times. This is possible as $\sigma$ visits every state in $Q^{\prime}$ . Also, Equation 2 ensures that $\textup{eff}(\pi_{2}^{\prime})>\mathbf{0}$ . Thus $\pi^{\prime}:=\pi_{1}\pi_{2}^{\prime}$ is also an unboundedness witness for $s$ .

Clearly $U$ has a nonnegative integer solution, namely the one obtained from $\pi_{2}$ by setting $x_{\theta}$ ’s to be the coefficients witnessing $\textup{eff}(\pi_{2})-\textup{eff}(\sigma)\in\mathop{\operatorname{cone}}% \nolimits_{\mathbb{N}}(\textup{eff}(\mathcal{C}))$ . Suppose $U$ is expressed in the form $A\mathbf{x}\geq\mathbf{b}$ . Then columns of $A$ are effects of simple cycles. We conclude that $\textup{rank}(A)\leq g$ . Also, each entry in $A$ and $\mathbf{b}$ is bounded in absolute value by $Mn^{2}$ . Hence, by Lemma 5, we can bound the max-norm of minimal solutions of $U$ by $(g+1)(g\cdot Mn^{2})^{g}\leq(2gMn^{2})^{g+1}\leq(2dMn^{2})^{g+1}$ . The length of $\pi_{2}^{\prime}$ yielded by any minimal solution is then bounded by $(4d^{2}nM)\cdot n\cdot(2dMn^{2})^{g+1}+n^{2}\leq(4d^{2}n^{2}M)^{2g+2}$ . Therefore, the length of the new unboundedness witness $\pi_{1}\pi_{2}^{\prime}$ is bounded by $(4d^{2}n^{2}M)^{2g+2}+n\leq(5d^{2}n^{2}M)^{2g+2}=L_{0}$ . This completes the proof of the base case.

The Induction Step

Now we consider the case that $k=k_{\textsc{res}}(V_{\mathbb{Z}})>0$ . Let $V_{\mathbb{N}}$ be the $d^{\prime}$ -VASS obtained from $V_{\mathbb{Z}}$ by removing all counters in $I_{\mathbb{Z}}$ , so $d^{\prime}=|I_{\mathbb{N}}|$ . Recall the definition of $C$ -small/large configurations for standard VASS (Definition 8). Here we say a configuration $q(\mathbf{x})$ in $V_{\mathbb{Z}}$ is $C$ -small/large if the projected configuration $q(\pi_{I_{\mathbb{N}}}(\mathbf{x}))$ is $C$ -small/large in $V_{\mathbb{N}}$ . Take $C=L_{k-1}\cdot M$ . We consider two cases depending on whether the unboundedness witness $\pi$ for $s$ contains a $C$ -large configuration.

Case 1.

Assume $\pi$ contains a $C$ -large configuration. Let $q(\mathbf{m})$ be the first $C$ -large configuration on $\pi$ , which splits $\pi$ into $s\xrightarrow{\pi_{\text{small}}}q(\mathbf{m})\xrightarrow{\pi_{\text{tail}}}t$ . By definition of unboundedness witness, $\pi$ can also be factored into $\pi=\pi_{1}\pi_{2}$ with $\pi_{2}$ being a cycle satisfying $\textup{eff}(\pi_{2})>\mathbf{0}$ . Observe that $\pi^{\prime}:=\pi_{\text{tail}}\pi_{2}$ is an unboundedness witness for $q(\mathbf{m})$ . The strategy is to use the induction hypothesis to replace $\pi^{\prime}$ by a length-bounded run.

Since $q(\mathbf{m})$ is $C$ -large, by Claim 11 there exists a clean basis $B=\{\mathbf{b}_{1},\ldots,\mathbf{b}_{k}\}$ of the vector space $\mathsf{CycleSpace}_{\mathbb{Q}}(V_{\mathbb{N}})$ and an index $i\in[k]$ , such that for all $j\in I_{\mathbb{N}}$ , $\mathbf{m}[j]\geq C$ whenever $\mathbf{b}_{i}[j]\neq 0$ . Let $I:=\{j\in I_{\mathbb{N}}\mid\mathbf{b}_{i}[j]\neq 0\}$ . We turn every counter in $I$ into an integer counter. That is, we consider the VASS $V_{\mathbb{Z}}^{\prime}:=(V,I_{\mathbb{N}}\setminus I,I_{\mathbb{Z}}\cup I)$ . It is easy to see that $k_{\textsc{res}}(V_{\mathbb{Z}}^{\prime})<k_{\textsc{res}}(V_{\mathbb{Z}})=k$ , and that $\pi^{\prime}$ is still an unboundedness witness for $q(\mathbf{m})$ in $V_{\mathbb{Z}}^{\prime}$ . By induction hypothesis, there is also an unboundedness witness $\rho$ for $q(\mathbf{m})$ in $V_{\mathbb{Z}}^{\prime}$ with $|\rho|\leq L_{k-1}$ . We claim that $\rho$ induces a legal run in $V_{\mathbb{Z}}$ from $q(\mathbf{m})$ . For this we only need to consider counters in $I$ . Notice that for any $j\in I$ , $\mathbf{m}[j]\geq C\geq|\rho|\cdot M$ , while for any prefix $\rho$ of $\rho$ we have $\textup{eff}(\rho^{\prime})[j]\leq|\rho|\cdot M$ . So values of counters in $I$ will not drop below zero along $\rho$ . This shows that $\rho$ is an unboundedness witness for $q(\mathbf{m})$ also in $V_{\mathbb{Z}}$ , and thus $\pi_{\text{small}}\rho$ is an unboundedness witness for $s$ . Now it is safe to remove from $\pi_{\text{small}}$ any cycle $\theta$ with $\pi_{I_{\mathbb{N}}}(\textup{eff}(\theta))=\mathbf{0}$ , which has no effect on the $\mathbb{N}$ -counters. So we assume that no two configurations on $\pi_{\text{small}}$ have the same values on counters in $I_{\mathbb{N}}$ , and moreover, all configurations on $\pi_{\text{small}}$ except the last one are $C$ -small. By Claim 10 we deduce that $|\pi_{\text{small}}|\leq n\cdot(d\cdot C)^{k}$ . Hence, $|\pi_{\text{small}}\rho|\leq n\cdot(d\cdot C)^{k}+L_{k-1}\leq L_{k}$ .

Case 2.

Assume all configurations on $\pi$ are $C$ -small. Split $\pi$ into $\pi_{1}\pi_{2}$ where $\pi_{2}$ is a cycle with $\textup{eff}(\pi_{2})>\mathbf{0}$ . If $\pi_{I_{\mathbb{N}}}(\textup{eff}(\pi_{2}))>\mathbf{0}$ , then by repeating $\pi_{2}$ sufficiently many times one eventually encounters a $C$ -large configuration, which reduces to Case 1. Hence, we assume next that $\pi_{I_{\mathbb{N}}}(\textup{eff}(\pi_{2}))=\mathbf{0}$ . The strategy is to encode the $\mathbb{N}$ -counters into states and reduce to the base case where $k_{\textsc{res}}(V_{\mathbb{Z}})=0$ .

Let $S:=\{(q,\pi_{I_{\mathbb{N}}}(\mathbf{y}))\mid q(\mathbf{y})\text{ is a $C$-% small configuration reachable from }s\}$ . By Claim 10 we have $|S|\leq n\cdot(d\cdot C)^{k}$ . We construct a VASS $V^{\prime}$ whose states are $S$ and whose transitions are of the form $(p,\mathbf{m})\xrightarrow{\pi_{I_{\mathbb{Z}}}(\mathbf{a})}(q,\mathbf{n})$ if there is a transition $p\xrightarrow{\mathbf{a}}q$ in $V_{\mathbb{Z}}$ with $\pi_{I_{\mathbb{N}}}(\mathbf{a})=\mathbf{n}-\mathbf{m}$ . We set all counters in $V^{\prime}$ to be integer counters, so $k_{\textsc{res}}(V^{\prime})=0$ . Now the unboundedness witness $\pi=\pi_{1}\pi_{2}$ can be mapped to a run $\pi^{\prime}=\pi_{1}^{\prime}\pi_{2}^{\prime}$ in $V^{\prime}$ . Moreover, $\pi_{2}^{\prime}$ is still a cycle in $V^{\prime}$ as we have assumed that $\pi_{I_{\mathbb{N}}}(\textup{eff}(\pi_{2}))=\mathbf{0}$ . Also, $\textup{eff}(\pi_{2}^{\prime})=\pi_{I_{\mathbb{Z}}}(\textup{eff}(\pi_{2}))>% \mathbf{0}$ . Hence $\pi^{\prime}$ is an unboundedness witness in $V^{\prime}$ . Using the induction base, there is an unboundedness witness $\rho$ with the same source as $\pi^{\prime}$ such that $|\rho|\leq(5d^{2}|S|^{2}M)^{2g+2}\leq(5d^{2}M(n\cdot(d\cdot C)^{k})^{2})^{2g+2% }\leq L_{k}$ . Finally it is easy to observe that $\rho^{\prime}$ can be mapped back to a run in $V_{\mathbb{Z}}$ that is also an unboundedness witness for $s$ .

6 Integer Reachability in Geometric Dimension

In this section we prove that in geometric dimension, $\mathbb{Z}$ -reachability behaves the same as in the case when we parameterise by the number of counters. We have the following theorem:

Theorem 28.

Let $V$ be a VASS of geometric dimension $g$ . For any two $\mathbb{Z}$ -configurations $s$ and $t$ such that $t$ is reachable from $s$ by a $\mathbb{Z}$ -run, there exists also a $\mathbb{Z}$ -run $\pi$ from $s$ to $t$ such that $|\pi|\leq\mathcal{O}(M)^{6g+1}$ where $M=\max(\textup{size}(V),\lVert s\rVert_{\infty},\lVert t\rVert_{\infty})$ .

Proof.

Let $s=q(w)$ and $t=q(w^{\prime})$ . Let $\sigma$ be a $\mathbb{Z}$ -run between $s$ and $t$ . Similar to what we have done in the base case of Lemma 26 (see Page 5.1), we express a $\mathbb{Z}$ -run between $s$ and $t$ as a solution of a Diophantine system of linear equations, and rely on Lemma 4. Let $Q^{\prime}\subseteq Q$ and $T^{\prime}\subseteq T$ be the subsets of states and transitions that appear in $\sigma$ . Simple cycles that use only transitions from $T^{\prime}$ we call $T^{\prime}$ -cycles. The $\mathbb{Z}$ -run $\sigma$ decomposes into a $\mathbb{Z}$ -run $\sigma_{0}$ that visits all states of $Q^{\prime}$ and set $\mathcal{S}$ of simple $T^{\prime}$ -cycles. Choose the shortest such $\sigma_{0}$ . Observe, that $\sigma_{0}$ visits each state at most $|Q^{\prime}|\leq|Q|\leq M$ times, as otherwise it could be shortened, and therefore its effect has norm at most $M^{3}$ . For each cycle $\theta\in\mathcal{S}$ we have $\lVert\textup{eff}(\theta)\rVert_{\infty}\leq M^{2}$ as it is a simple cycle. Observe, that $t-s-\textup{eff}(\sigma_{0})\in\mathop{\operatorname{cone}}\nolimits_{\mathbb{% N}}(\textup{eff}(\mathcal{S}))$ . Therefore, because of Theorem 2 we can choose $\mathcal{C}\subseteq\mathcal{S}$ such that $|\mathcal{C}|\leq 2d\log(4dM)\leq 8d^{2}M\leq 8M^{3}$ such that $t-s-\textup{eff}(\sigma_{0})\in\mathop{\operatorname{cone}}\nolimits_{\mathbb{% N}}(\textup{eff}(\mathcal{C}))$ . We define a system $U$ of $d$ linear equations (one for each dimension), whose unknowns $x_{\theta}$ correspond to $T^{\prime}$ -cycles $\theta$ from $\mathcal{C}$ :

\sum_{\theta\in\mathcal{C}}x_{\theta}\cdot\textup{eff}(\theta)=t-s-\textup{eff% }(\sigma_{0})

The system has a nonnegative integer solution, namely the one obtained from the fact that $t-s-\textup{eff}(\sigma_{0})\in\mathop{\operatorname{cone}}\nolimits_{\mathbb{% N}}(\textup{eff}(\mathcal{C}))$ . The system $U$ can be expressed as $A\cdot x=b$ for some matrix $A$ . Observe, that rank of the matrix $A$ is at most $g$ as columns of $A$ are effects of simple cycles in $V$ . Hence we can choose at most $g$ linearly independent equations from the system $U$ and create a system $U^{\prime}$ , which can be expressed as $A^{\prime}\cdot x=b^{\prime}$ for some $A^{\prime}\in\mathbb{Z}^{g\times|\mathcal{C}|}$ and $b^{\prime}\in\mathbb{Z}^{g}$ . As all coefficients of $U^{\prime}$ are bounded by $\mathcal{O}(M^{3})$ , by Lemma 4 the system has a solution of norm $\mathcal{O}((|\mathcal{C}|M^{3}))^{g}=\mathcal{O}(M)^{6g}$ . The solution yields a $\mathbb{Z}$ -run $\pi$ from $s$ to $t$ of length $|\sigma_{0}|+M\cdot\mathcal{O}(M)^{6g}=\mathcal{O}(M)^{6g+1}$ , consisting, of $\sigma_{0}$ with attached all cycles $\theta\in\mathcal{C}$ (this is possible, as $\sigma_{0}$ visits all states used by the cycles), each $\theta$ iterated $x_{\theta}$ times. $\hfill\blacktriangleleft$

7 Tower-Hardness of Reachability in SCC Dimension 4

In this section we sketch the proof of the following theorem.

Theorem 29.

Reachability in VASS of SCC dimension ${g_{\textsc{scc}}}=4$ is Tower-hard.

The proof is based on a modification of [14, Theorem 4] which showed Tower-hardness for 8-VASS. The general strategy is to reduce from the Tower-bounded reachability problem in two-counter machines. Two-counter machines can be viewed as 2-VASSes enhanced with the ability of testing equality with zero on each counter, while Tower-boundedness requires values of both counter to stay below $\textsc{Tower}(n)$ , where $n\in\mathbb{N}$ is part of the input. We have to implement zero-tests on bounded counters in VASS without increasing the SCC dimension too much. We will rely on a useful gadget called multiplication triples [11].

A multiplication triple consists of three VASS counters $\texttt{b},\texttt{c},\texttt{d}$ holding values $B,C,B\cdot C$ . For any counter x bounded by $B$ we can simulate $C/2$ zero tests on it. The procedure is as follows: we try to move values from b to x and then back to b, in the meantime we decrease d by the amount of value actually moved. Finally, c is decreased by two. Since x is bounded by $B$ , d was decreased by at most $2B$ . To maintain $\texttt{d}\leq\texttt{b}\cdot\texttt{c}$ , we must have been able to decrease d by $2B$ , i.e. we must have $\texttt{x}=0$ . This can be extended to zero-testing multiple counters $\texttt{x}_{1},\texttt{x}_{2},\ldots,\texttt{x}_{k}$ , by moving values between b and these counters like a chain, see [14]. We call d the sensor counter of this multiplication triple. It is important to notice that we always maintain the invariant $\texttt{b}+\texttt{x}_{1}+\texttt{x}_{2}+\cdots+\texttt{x}_{k}=B$ , wherefore counter b does not increase the SCC dimension ${g_{\textsc{scc}}}$ , i.e. a multiplication triple increases ${g_{\textsc{scc}}}$ only by $2$ .

We shall construct a VASS of two parts: the first part generates a multiplication triple $\texttt{b},\texttt{c},\texttt{d}$ with $\texttt{b}=\textsc{Tower}(n)$ , and the second part simulates the 2-counter machine using this triple. As noted above, the SCC dimension in the second half is at most $2+2=4$ , however the first part requires more care.

In order to generate the tower-sized multiplication triple, a so-called amplifier was utilized in [14]. An amplifier consumes a multiplication triple with values $(\texttt{b},\texttt{c},\texttt{d})=(B,C,B\cdot C)$ and generates a new one with values $(\texttt{b}^{\prime},\texttt{c}^{\prime},\texttt{d}^{\prime})=(2^{B},C^{\prime% },2^{B}\cdot C^{\prime})$ . Intuitively, it starts with a triple $(\texttt{b}^{\prime},\texttt{c}^{\prime},\texttt{d}^{\prime})=(1,C^{\prime},C^% {\prime})$ and doubles $\texttt{b}^{\prime}$ and $\texttt{c}^{\prime}$ for $B$ times. Each doubling requires zero-tests, which are implemented using the triple $(\texttt{c},\texttt{b},\texttt{d})$ , with the roles of $\texttt{b},\texttt{c}$ swapped to ensure the doubling is performed exactly $B$ times. The amplifier needs zero-tests on three counters: $\texttt{b}^{\prime},\texttt{d}^{\prime}$ and an additional counter used to store the result of each doubling. This gives SCC dimension $3+2=5$ , which is not optimal. To improve this, notice that if we have two identical copies of the input triple $(\texttt{b},\texttt{c},\texttt{d})$ , we can amplify $\texttt{b}^{\prime}$ and $\texttt{d}^{\prime}$ separately. Now each amplification procedure yields SCC dimension $4$ . Of course, we need to generate two identical copies of $\texttt{b}^{\prime},\texttt{c}^{\prime},\texttt{d}^{\prime}$ to continue this amplification. But adding copies of counters does not change the SCC dimension. Notice that the amplifier succeeds if and only if the sensor counters in the two copies of its input triples become zero at the end.

By concatenating $n$ copies of the amplifier, we are able to generate the $\textsc{Tower}(n)$ -multiplication triple. We remark that each amplifier should use fresh new counters for its output. This does not increase the SCC dimension as each amplifier works in its own SCC. This way, we are allowed to check if all amplifiers and multiplication triples function correctly by checking whether all the sensor counters equal zero at the end of the run, which can be encoded into the reachability problem. Therefore, we conclude that reachability in VASS of ${g_{\textsc{scc}}}=4$ is Tower-hard.

8 Future Research

In Section 3, we proved that coverability in VASS parameterised by geometric dimension $g$ is witnessed by double exponential length runs. Specifically, we argued that the exponent only depends on $g$ (Theorem 6). As we touched on in Remark 13, this does not allow us to obtain runs with less than double exponential length for instances of coverability in VASS with fixed SCC dimension ${g_{\textsc{scc}}}$ . However, we conjecture that the coverability problem in VASS with fixed SCC dimension can be witnessed by exponential length runs.

Conjecture 30.

For every fixed ${g_{\textsc{scc}}}\in\mathbb{N}$ , the coverability problem in VASS with SCC dimension ${g_{\textsc{scc}}}$ is in PSpace.

Unlike for geometric dimension, one cannot hope for sub-exponential length runs for coverability in VASS with fixed SCC dimension; see the following example.

Example 31.

Consider a $d$ -VASS with $d$ states $q_{1},\ldots,q_{d}$ . For every $i\in[d-1]$ , we have a transition $q_{i}\xrightarrow{\mathbf{0}}q_{i+1}$ . Furthermore, for every $i\in[d]\setminus\{1\}$ , there is a self-loop $q_{i}\xrightarrow{-2\mathbf{e}_{i-1}+\mathbf{e}_{i}}q_{i}$ ; and we also add the self-loop $q_{1}\xrightarrow{\mathbf{e}_{1}}q_{1}$ . The shortest run from $q_{1}(\mathbf{0})$ that covers $q_{d}(\mathbf{e}_{d})$ is

q_{1}(\mathbf{0})\rightarrow q_{1}(2^{d-1}\mathbf{e}_{1})\rightarrow q_{2}(2^{% d-1}\mathbf{e}_{1})\rightarrow q_{2}(2^{d-2}\mathbf{e}_{2})\\ \rightarrow q_{3}(2^{d-2}\mathbf{e}_{2})\rightarrow q_{3}(2^{d-3}\mathbf{e}_{3% })\rightarrow\ldots\rightarrow q_{d-1}(2\mathbf{e}_{d-1})\rightarrow q_{d}(2% \mathbf{e}_{d-1})\rightarrow q_{d}(\mathbf{e}_{d}).

The length of this run is exponential in $d$ .

One attempt to prove Conjecture 30 would be the following strong-linearity conjecture in VASS parameterised by geometric dimension. Conjecture 32 is a substantial strengthening of Theorem 6 which has already been stated for VASS parameterised by the standard dimension $d$ [25, 26, 43].

Conjecture 32.

There is some exponential function $f:\mathbb{N}\to\mathbb{N}$ such that, if there is a run in $V$ from $s(\mathbf{x})$ that covers $t(\mathbf{y})$ , then there exists a run in $V$ from $s(\mathbf{x})$ that covers $t(\mathbf{y})$ of length at most $\lVert\mathbf{y}\rVert_{\infty}\cdot\textup{poly}(d,n,M)^{f(g)}$ .

Proof of Conjecture 30 assuming Conjecture 32.

It is well-known that a bound $L$ on the length of a covering run implies that the backward coverability algorithm stabilises after at most $L$ many steps (and vice versa). We consider the backward coverability algorithm, starting from the target configuration $t(\mathbf{y})$ . We first focus on the last SCC. By Conjecture 32, one can observe that running the backwards coverability algorithm in the last SCC takes at most $\lVert\mathbf{y}\rVert_{\infty}\cdot\textup{poly}(d,n,M)^{f(g)}$ steps. This means that minimal configurations that can cover the target configuration are of size at most $L\cdot M\cdot\textup{poly}(d,n,M)^{f(g)}=L\cdot\textup{poly}(d,n,M)^{f(g)}$ . Then, we repeat this argument for each SCC in reverse order to obtain a bound on the size of the minimal configurations that can cover the target configuration (in particular the length of the shortest covering run) equal to $\lVert\mathbf{y}\rVert_{\infty}\cdot\textup{poly}(d,n,M)^{|Q|\cdot f({g_{% \textsc{scc}}})}$ , which for fixed ${g_{\textsc{scc}}}$ is $\lVert\mathbf{y}\rVert_{\infty}\cdot\textup{poly}(d,n,M)^{|Q|}=f_{g}(d,n,M,L)$ , for some exponential function $f_{g}$ . Hence coverability in VASS with fixed SCC dimension ${g_{\textsc{scc}}}$ is witnessed by exponential length runs which allows us to conclude that coverability is in PSpace. $\hfill\blacktriangleleft$

Another direction for future research is the boundedness problem. Example 31 can be adapted to boundedness rather easily, proving that similar to coverability the shortest run witnessing unboundedness is either exponential or doubly-exponential when the SCC dimension is fixed. We conjecture that it is actually exponential.

Conjecture 33.

For every $g\in\mathbb{N}$ there is an exponential function $f_{g}$ such that for every $d$ -VASS $V=(Q,T)$ with ${g_{\textsc{scc}}}(V)=g$ , if there is an unboundedness witness for configuration $s$ then there is also one of length at most $f_{g}(d,n,M)$ where $n=|Q|$ and $M=\lVert T\rVert_{\infty}$ .

Finally, while the general VASS reachability algorithm works for SCC dimension ${g_{\textsc{scc}}}$ , in low SCC dimension no tight complexity bounds are known, as opposed to the parameterisations by the number of counters $d$ [4] and geometric dimension $g$ [52]. Another natural direction for future research is to study these complexities, we conjecture the following.

Conjecture 34.

Reachability in VASS of SCC dimension ${g_{\textsc{scc}}}=2$ and ${g_{\textsc{scc}}}=3$ is in PSpace and ExpSpace, respectively.

References

[1] Clotilde Bizière and Wojciech Czerwinski. Reachability in One-Dimensional Pushdown Vector Addition Systems Is Decidable. In Proceedings of STOC 2025, pages 1851–1862. ACM, 2025. doi:10.1145/3717823.3718149.
[2] Clotilde Bizière, Thibault Hilaire, Jérôme Leroux, and Grégoire Sutre. On the Reachability Problem for Two-Dimensional Branching VASS. In Proceedings of MFCS 2025, volume 345 of LIPIcs, pages 22:1–22:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2025. doi:10.4230/LIPIcs.MFCS.2025.22.
[3] Michael Blondin, Matthias Englert, Alain Finkel, Stefan Göller, Christoph Haase, Ranko Lazic, Pierre McKenzie, and Patrick Totzke. The Reachability Problem for Two-Dimensional Vector Addition Systems with States. J. ACM, 68(5):34:1–34:43, 2021. doi:10.1145/3464794.
[4] Michael Blondin, Alain Finkel, Stefan Göller, Christoph Haase, and Pierre McKenzie. Reachability in Two-Dimensional Vector Addition Systems with States Is PSPACE-Complete. In Proceedings of LICS 2015, pages 32–43. IEEE Computer Society, 2015. doi:10.1109/LICS.2015.14.
[5] Dmitry Chistikov, Wojciech Czerwinski, Filip Mazowiecki, Lukasz Orlikowski, Henry Sinclair-Banks, and Karol Wegrzycki. The Tractability Border of Reachability in Simple Vector Addition Systems with States. In Proceedings of FOCS 2024, pages 1332–1354. IEEE, 2024. doi:10.1109/FOCS61266.2024.00086.
[6] Dmitry Chistikov and Christoph Haase. The Taming of the Semi-Linear Set. In 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, pages 128:1–128:13, 2016. doi:10.4230/LIPIcs.ICALP.2016.128.
[7] Wojciech Czerwinski, Piotr Hofman, and Georg Zetzsche. Unboundedness problems for languages of vector addition systems. In Ioannis Chatzigiannakis, Christos Kaklamanis, Dániel Marx, and Donald Sannella, editors, 45th International Colloquium on Automata, Languages, and Programming, ICALP 2018, Prague, Czech Republic, July 9-13, 2018, volume 107 of LIPIcs, pages 119:1–119:15. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2018. doi:10.4230/LIPIcs.ICALP.2018.119.
[8] Wojciech Czerwinski, Ismaël Jecker, Slawomir Lasota, Jérôme Leroux, and Lukasz Orlikowski. New Lower Bounds for Reachability in Vector Addition Systems. In Proceedings of FSTTCS 2023, volume 284 of LIPIcs, pages 35:1–35:22. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPIcs.FSTTCS.2023.35.
[9] Wojciech Czerwinski, Ismaël Jecker, Slawomir Lasota, and Lukasz Orlikowski. Reachability in 3-VASS Is Elementary. In Proceedings of ICALP 2025, volume 334 of LIPIcs, pages 153:1–153:20. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2025. doi:10.4230/LIPIcs.ICALP.2025.153.
[10] Wojciech Czerwinski, Ismaël Jecker, Slawomir Lasota, and Lukasz Orlikowski. Reachability in 3-VASS is Elementary. CoRR, abs/2502.13916, 2025. doi:10.48550/arXiv.2502.13916.
[11] Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki. The Reachability Problem for Petri Nets is not Elementary. In STOC, pages 24–33. ACM, 2019. doi:10.1145/3313276.3316369.
[12] Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki. Reachability in Fixed Dimension Vector Addition Systems with States. In Proceedings of CONCUR 2020, volume 171 of LIPIcs, pages 48:1–48:21. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2020. doi:10.4230/LIPIcs.CONCUR.2020.48.
[13] Wojciech Czerwinski and Lukasz Orlikowski. Reachability in Vector Addition Systems is Ackermann-Complete. In Proceedings of FOCS 2021, pages 1229–1240. IEEE, 2021. doi:10.1109/FOCS52979.2021.00120.
[14] Wojciech Czerwinski and Lukasz Orlikowski. Lower Bounds for the Reachability Problem in Fixed Dimensional VASSes. In Proceedings of LICS 2022, pages 40:1–40:12. ACM, 2022. doi:10.1145/3531130.3533357.
[15] Stéphane Demri. On selective unboundedness of vass. Journal of Computer and System Sciences, 79(5):689–713, 2013. doi:10.1016/j.jcss.2013.01.014.
[16] Friedrich Eisenbrand and Gennady Shmonin. Carathéodory bounds for integer cones. Oper. Res. Lett., 34(5):564–568, 2006. doi:10.1016/J.ORL.2005.09.008.
[17] Javier Esparza and Mogens Nielsen. Decidability Issues for Petri Nets - a survey. Bull. EATCS, 52:244–262, 1994.
[18] Diego Figueira, Ranko Lazic, Jérôme Leroux, Filip Mazowiecki, and Grégoire Sutre. Polynomial-Space Completeness of Reachability for Succinct Branching VASS in Dimension One. In Procedings of ICALP 2017, volume 80 of LIPIcs, pages 119:1–119:14. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2017. doi:10.4230/LIPIcs.ICALP.2017.119.
[19] Yuxi Fu, Qizhe Yang, and Yangluo Zheng. Improved Algorithm for Reachability in d-VASS. In Proceedings of ICALP 2024, volume 297 of LIPIcs, pages 136:1–136:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPIcs.ICALP.2024.136.
[20] Yuxi Fu, Yangluo Zheng, and Qizhe Yang. Reachability in Geometrically d-Dimensional VASS. CoRR, abs/2504.12302, 2025. doi:10.48550/arXiv.2504.12302.
[21] Stefan Göller, Christoph Haase, Ranko Lazic, and Patrick Totzke. A polynomial-time algorithm for reachability in branching VASS in dimension one. In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, Rome, Italy, July 11-15, 2016, volume 55 of LIPIcs, pages 105:1–105:13. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2016. doi:10.4230/LIPIcs.ICALP.2016.105.
[22] Roland Guttenberg, Wojciech Czerwinski, and Slawomir Lasota. Reachability and Related Problems in Vector Addition Systems with Nested Zero Tests. In Proceedings of LICS 2025, pages 581–593. IEEE, 2025. doi:10.1109/LICS65433.2025.00050.
[23] Christoph Haase and Simon Halfon. Integer Vector Addition Systems with States. In Proceedings of RP 2014, volume 8762 of Lecture Notes in Computer Science, pages 112–124. Springer, 2014. doi:10.1007/978-3-319-11439-2_9.
[24] Christoph Haase, Stephan Kreutzer, Joël Ouaknine, and James Worrell. Reachability in Succinct and Parametric One-Counter Automata. In Proceedings of CONCUR 2009, pages 369–383. Springer Berlin Heidelberg, 2009. doi:10.1007/978-3-642-04081-8_25.
[25] Michel Hack. Decidability questions for Petri Nets. PhD thesis, Massachusetts Institute of Technology, Cambridge, MA, USA, 1976. URL: https://hdl.handle.net/1721.1/27441.
[26] Ismaël Jecker. Open problems in automata theory: 22.1 Complexity of fixed VAS reachability, 2022. Webpage accessed on 2025-05-13. URL: https://automata.exchange/22.01-complexity-fixed-vas-reachability/.
[27] Richard M. Karp and Raymond E. Miller. Parallel program schemata. J. Comput. Syst. Sci., 3(2):147–195, 1969. doi:10.1016/S0022-0000(69)80011-5.
[28] S. Rao Kosaraju. Decidability of Reachability in Vector Addition Systems. In STOC, pages 267–281. ACM, 1982.
[29] Marvin Künnemann, Filip Mazowiecki, Lia Schütze, Henry Sinclair-Banks, and Karol Wegrzycki. Coverability in VASS Revisited: Improving Rackoff’s Bound to Obtain Conditional Optimality. In Proceedings of ICALP 2023, volume 261 of LIPIcs, pages 131:1–131:20. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPIcs.ICALP.2023.131.
[30] Slawomir Lasota. Improved Ackermannian Lower Bound for the Petri Nets Reachability Problem. In Proceedings of STACS 2022, volume 219 of LIPIcs, pages 46:1–46:15. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2022. doi:10.4230/LIPIcs.STACS.2022.46.
[31] Kurt Lautenbach. Linear algebraic techniques for place/transition nets. In Wilfried Brauer, Wolfgang Reisig, and Grzegorz Rozenberg, editors, Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, Part I, Proceedings of an Advanced Course, Bad Honnef, Germany, 8-19 September 1986, Lecture Notes in Computer Science, pages 142–167. Springer, 1986. doi:10.1007/BFB0046839.
[32] Ranko Lazic and Sylvain Schmitz. Nonelementary complexities for branching vass, mell, and extensions. ACM Trans. Comput. Log., 16(3):20:1–20:30, 2015. doi:10.1145/2733375.
[33] Jérôme Leroux. Flat petri nets (invited talk). In Petri Nets, volume 12734 of Lecture Notes in Computer Science, pages 17–30. Springer, 2021. doi:10.1007/978-3-030-76983-3_2.
[34] Jérôme Leroux. The Reachability Problem for Petri Nets is Not Primitive Recursive. In Proceedings of FOCS 2021, pages 1241–1252. IEEE, 2021. doi:10.1109/FOCS52979.2021.00121.
[35] Jérôme Leroux and Sylvain Schmitz. Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension. In LICS, pages 1–13. IEEE, 2019. doi:10.1109/LICS.2019.8785796.
[36] Jérôme Leroux and Grégoire Sutre. On Flatness for 2-Dimensional Vector Addition Systems with States. In Proceedings of CONCUR 2004, volume 3170 of Lecture Notes in Computer Science, pages 402–416. Springer, 2004. doi:10.1007/978-3-540-28644-8_26.
[37] Jérôme Leroux, Grégoire Sutre, and Patrick Totzke. On the coverability problem for pushdown vector addition systems in one dimension. In Proceedings of ICALP 2015, volume 9135 of Lecture Notes in Computer Science, pages 324–336. Springer, 2015. doi:10.1007/978-3-662-47666-6_26.
[38] Richard J. Lipton. The Reachability Problem Requires Exponential Space. Technical report, Yale University, 1976.
[39] Ernst W. Mayr. An Algorithm for the General Petri Net Reachability Problem. In Proceedings of STOC 1981, pages 238–246. ACM, 1981. doi:10.1145/800076.802477.
[40] Filip Mazowiecki and Michal Pilipczuk. Reachability for bounded branching VASS. In Wan J. Fokkink and Rob van Glabbeek, editors, 30th International Conference on Concurrency Theory, CONCUR 2019, Amsterdam, The Netherlands, August 27-30, 2019, volume 140 of LIPIcs, pages 28:1–28:13. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2019. doi:10.4230/LIPIcs.CONCUR.2019.28.
[41] Filip Mazowiecki, Henry Sinclair-Banks, and Karol Wegrzycki. Coverability in 2-VASS with One Unary Counter is in NP. In Proceedings of FoSSaCS 2023, volume 13992 of Lecture Notes in Computer Science, pages 196–217. Springer, 2023. doi:10.1007/978-3-031-30829-1_10.
[42] Guillermo A. Pérez and Shrisha Rao. On continuous pushdown VASS in one dimension. In Rupak Majumdar and Alexandra Silva, editors, 35th International Conference on Concurrency Theory, CONCUR 2024, Calgary, Canada, September 9-13, 2024, volume 311 of LIPIcs, pages 34:1–34:20. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPIcs.CONCUR.2024.34.
[43] Michal Pilipczuk, Sylvain Schmitz, and Henry Sinclair-Banks. A Note on the Parameterised Complexity of Coverability in Vector Addition Systems. In Proceedings of IPEC 2025, volume 358 of LIPIcs, pages 24:1–24:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2025. doi:10.4230/LIPIcs.IPEC.2025.24.
[44] Charles Rackoff. The Covering and Boundedness Problems for Vector Addition Systems. TCS, 6:223–231, 1978. doi:10.1016/0304-3975(78)90036-1.
[45] Wolfgang Reisig. Understanding Petri Nets - Modeling Techniques, Analysis Methods, Case Studies. Springer, 2013. doi:10.1007/978-3-642-33278-4.
[46] Louis E. Rosier and Hsu-Chun Yen. A multiparameter analysis of the boundedness problem for vector addition systems. J. Comput. Syst. Sci., 32(1):105–135, 1986. doi:10.1016/0022-0000(86)90006-1.
[47] Sylvain Schmitz. Complexity Hierarchies beyond Elementary. ACM Trans. Comput. Theory, 8(1):3:1–3:36, 2016. doi:10.1145/2858784.
[48] Sylvain Schmitz. The complexity of reachability in vector addition systems. ACM SIGLOG News, 3(1):4–21, 2016. doi:10.1145/2893582.2893585.
[49] Alexander Schrijver. Theory of linear and integer programming. John Wiley & Sons, 1998.
[50] Leslie G. Valiant and Mike Paterson. Deterministic one-counter automata. J. Comput. Syst. Sci., 10(3):340–350, 1975. doi:10.1016/S0022-0000(75)80005-5.
[51] Joachim von zur Gathen and Malte Sieveking. A bound on solutions of linear integer equalities and inequalities. Proceedings of the American Mathematical Society, 72(1):155–158, October 1978. doi:10.1090/s0002-9939-1978-0500555-0.
[52] Yangluo Zheng. Reachability in Vector Addition System with States Parameterized by Geometric Dimension. In Proceedings of CONCUR 2025, volume 348 of LIPIcs, pages 38:1–38:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2025. doi:10.4230/LIPIcs.CONCUR.2025.38.

[bib.bib1] [1] Clotilde Bizière and Wojciech Czerwinski. Reachability in One-Dimensional Pushdown Vector Addition Systems Is Decidable. In Proceedings of STOC 2025, pages 1851–1862. ACM, 2025. doi:10.1145/3717823.3718149.

[bib.bib2] [2] Clotilde Bizière, Thibault Hilaire, Jérôme Leroux, and Grégoire Sutre. On the Reachability Problem for Two-Dimensional Branching VASS. In Proceedings of MFCS 2025, volume 345 of LIPIcs, pages 22:1–22:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2025. doi:10.4230/LIPIcs.MFCS.2025.22.

[bib.bib3] [3] Michael Blondin, Matthias Englert, Alain Finkel, Stefan Göller, Christoph Haase, Ranko Lazic, Pierre McKenzie, and Patrick Totzke. The Reachability Problem for Two-Dimensional Vector Addition Systems with States. J. ACM, 68(5):34:1–34:43, 2021. doi:10.1145/3464794.

[bib.bib4] [4] Michael Blondin, Alain Finkel, Stefan Göller, Christoph Haase, and Pierre McKenzie. Reachability in Two-Dimensional Vector Addition Systems with States Is PSPACE-Complete. In Proceedings of LICS 2015, pages 32–43. IEEE Computer Society, 2015. doi:10.1109/LICS.2015.14.

[bib.bib5] [5] Dmitry Chistikov, Wojciech Czerwinski, Filip Mazowiecki, Lukasz Orlikowski, Henry Sinclair-Banks, and Karol Wegrzycki. The Tractability Border of Reachability in Simple Vector Addition Systems with States. In Proceedings of FOCS 2024, pages 1332–1354. IEEE, 2024. doi:10.1109/FOCS61266.2024.00086.

[bib.bib6] [6] Dmitry Chistikov and Christoph Haase. The Taming of the Semi-Linear Set. In 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, pages 128:1–128:13, 2016. doi:10.4230/LIPIcs.ICALP.2016.128.

[bib.bib7] [7] Wojciech Czerwinski, Piotr Hofman, and Georg Zetzsche. Unboundedness problems for languages of vector addition systems. In Ioannis Chatzigiannakis, Christos Kaklamanis, Dániel Marx, and Donald Sannella, editors, 45th International Colloquium on Automata, Languages, and Programming, ICALP 2018, Prague, Czech Republic, July 9-13, 2018, volume 107 of LIPIcs, pages 119:1–119:15. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2018. doi:10.4230/LIPIcs.ICALP.2018.119.

[bib.bib8] [8] Wojciech Czerwinski, Ismaël Jecker, Slawomir Lasota, Jérôme Leroux, and Lukasz Orlikowski. New Lower Bounds for Reachability in Vector Addition Systems. In Proceedings of FSTTCS 2023, volume 284 of LIPIcs, pages 35:1–35:22. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPIcs.FSTTCS.2023.35.

[bib.bib9] [9] Wojciech Czerwinski, Ismaël Jecker, Slawomir Lasota, and Lukasz Orlikowski. Reachability in 3-VASS Is Elementary. In Proceedings of ICALP 2025, volume 334 of LIPIcs, pages 153:1–153:20. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2025. doi:10.4230/LIPIcs.ICALP.2025.153.

[bib.bib10] [10] Wojciech Czerwinski, Ismaël Jecker, Slawomir Lasota, and Lukasz Orlikowski. Reachability in 3-VASS is Elementary. CoRR, abs/2502.13916, 2025. doi:10.48550/arXiv.2502.13916.

[bib.bib11] [11] Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki. The Reachability Problem for Petri Nets is not Elementary. In STOC, pages 24–33. ACM, 2019. doi:10.1145/3313276.3316369.

[bib.bib12] [12] Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki. Reachability in Fixed Dimension Vector Addition Systems with States. In Proceedings of CONCUR 2020, volume 171 of LIPIcs, pages 48:1–48:21. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2020. doi:10.4230/LIPIcs.CONCUR.2020.48.

[bib.bib13] [13] Wojciech Czerwinski and Lukasz Orlikowski. Reachability in Vector Addition Systems is Ackermann-Complete. In Proceedings of FOCS 2021, pages 1229–1240. IEEE, 2021. doi:10.1109/FOCS52979.2021.00120.

[bib.bib14] [14] Wojciech Czerwinski and Lukasz Orlikowski. Lower Bounds for the Reachability Problem in Fixed Dimensional VASSes. In Proceedings of LICS 2022, pages 40:1–40:12. ACM, 2022. doi:10.1145/3531130.3533357.

[bib.bib15] [15] Stéphane Demri. On selective unboundedness of vass. Journal of Computer and System Sciences, 79(5):689–713, 2013. doi:10.1016/j.jcss.2013.01.014.

[bib.bib16] [16] Friedrich Eisenbrand and Gennady Shmonin. Carathéodory bounds for integer cones. Oper. Res. Lett., 34(5):564–568, 2006. doi:10.1016/J.ORL.2005.09.008.

[bib.bib17] [17] Javier Esparza and Mogens Nielsen. Decidability Issues for Petri Nets - a survey. Bull. EATCS, 52:244–262, 1994.

[bib.bib18] [18] Diego Figueira, Ranko Lazic, Jérôme Leroux, Filip Mazowiecki, and Grégoire Sutre. Polynomial-Space Completeness of Reachability for Succinct Branching VASS in Dimension One. In Procedings of ICALP 2017, volume 80 of LIPIcs, pages 119:1–119:14. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2017. doi:10.4230/LIPIcs.ICALP.2017.119.

[bib.bib19] [19] Yuxi Fu, Qizhe Yang, and Yangluo Zheng. Improved Algorithm for Reachability in d-VASS. In Proceedings of ICALP 2024, volume 297 of LIPIcs, pages 136:1–136:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPIcs.ICALP.2024.136.

[bib.bib20] [20] Yuxi Fu, Yangluo Zheng, and Qizhe Yang. Reachability in Geometrically d-Dimensional VASS. CoRR, abs/2504.12302, 2025. doi:10.48550/arXiv.2504.12302.

[bib.bib21] [21] Stefan Göller, Christoph Haase, Ranko Lazic, and Patrick Totzke. A polynomial-time algorithm for reachability in branching VASS in dimension one. In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, Rome, Italy, July 11-15, 2016, volume 55 of LIPIcs, pages 105:1–105:13. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2016. doi:10.4230/LIPIcs.ICALP.2016.105.

[bib.bib22] [22] Roland Guttenberg, Wojciech Czerwinski, and Slawomir Lasota. Reachability and Related Problems in Vector Addition Systems with Nested Zero Tests. In Proceedings of LICS 2025, pages 581–593. IEEE, 2025. doi:10.1109/LICS65433.2025.00050.

[bib.bib23] [23] Christoph Haase and Simon Halfon. Integer Vector Addition Systems with States. In Proceedings of RP 2014, volume 8762 of Lecture Notes in Computer Science, pages 112–124. Springer, 2014. doi:10.1007/978-3-319-11439-2_9.

[bib.bib24] [24] Christoph Haase, Stephan Kreutzer, Joël Ouaknine, and James Worrell. Reachability in Succinct and Parametric One-Counter Automata. In Proceedings of CONCUR 2009, pages 369–383. Springer Berlin Heidelberg, 2009. doi:10.1007/978-3-642-04081-8_25.

[bib.bib25] [25] Michel Hack. Decidability questions for Petri Nets. PhD thesis, Massachusetts Institute of Technology, Cambridge, MA, USA, 1976. URL: https://hdl.handle.net/1721.1/27441.

[bib.bib26] [26] Ismaël Jecker. Open problems in automata theory: 22.1 Complexity of fixed VAS reachability, 2022. Webpage accessed on 2025-05-13. URL: https://automata.exchange/22.01-complexity-fixed-vas-reachability/.

[bib.bib27] [27] Richard M. Karp and Raymond E. Miller. Parallel program schemata. J. Comput. Syst. Sci., 3(2):147–195, 1969. doi:10.1016/S0022-0000(69)80011-5.

[bib.bib28] [28] S. Rao Kosaraju. Decidability of Reachability in Vector Addition Systems. In STOC, pages 267–281. ACM, 1982.

[bib.bib29] [29] Marvin Künnemann, Filip Mazowiecki, Lia Schütze, Henry Sinclair-Banks, and Karol Wegrzycki. Coverability in VASS Revisited: Improving Rackoff’s Bound to Obtain Conditional Optimality. In Proceedings of ICALP 2023, volume 261 of LIPIcs, pages 131:1–131:20. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPIcs.ICALP.2023.131.

[bib.bib30] [30] Slawomir Lasota. Improved Ackermannian Lower Bound for the Petri Nets Reachability Problem. In Proceedings of STACS 2022, volume 219 of LIPIcs, pages 46:1–46:15. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2022. doi:10.4230/LIPIcs.STACS.2022.46.

[bib.bib31] [31] Kurt Lautenbach. Linear algebraic techniques for place/transition nets. In Wilfried Brauer, Wolfgang Reisig, and Grzegorz Rozenberg, editors, Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, Part I, Proceedings of an Advanced Course, Bad Honnef, Germany, 8-19 September 1986, Lecture Notes in Computer Science, pages 142–167. Springer, 1986. doi:10.1007/BFB0046839.

[bib.bib32] [32] Ranko Lazic and Sylvain Schmitz. Nonelementary complexities for branching vass, mell, and extensions. ACM Trans. Comput. Log., 16(3):20:1–20:30, 2015. doi:10.1145/2733375.

[bib.bib33] [33] Jérôme Leroux. Flat petri nets (invited talk). In Petri Nets, volume 12734 of Lecture Notes in Computer Science, pages 17–30. Springer, 2021. doi:10.1007/978-3-030-76983-3_2.

[bib.bib34] [34] Jérôme Leroux. The Reachability Problem for Petri Nets is Not Primitive Recursive. In Proceedings of FOCS 2021, pages 1241–1252. IEEE, 2021. doi:10.1109/FOCS52979.2021.00121.

[bib.bib35] [35] Jérôme Leroux and Sylvain Schmitz. Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension. In LICS, pages 1–13. IEEE, 2019. doi:10.1109/LICS.2019.8785796.

[bib.bib36] [36] Jérôme Leroux and Grégoire Sutre. On Flatness for 2-Dimensional Vector Addition Systems with States. In Proceedings of CONCUR 2004, volume 3170 of Lecture Notes in Computer Science, pages 402–416. Springer, 2004. doi:10.1007/978-3-540-28644-8_26.

[bib.bib37] [37] Jérôme Leroux, Grégoire Sutre, and Patrick Totzke. On the coverability problem for pushdown vector addition systems in one dimension. In Proceedings of ICALP 2015, volume 9135 of Lecture Notes in Computer Science, pages 324–336. Springer, 2015. doi:10.1007/978-3-662-47666-6_26.

[bib.bib38] [38] Richard J. Lipton. The Reachability Problem Requires Exponential Space. Technical report, Yale University, 1976.

[bib.bib39] [39] Ernst W. Mayr. An Algorithm for the General Petri Net Reachability Problem. In Proceedings of STOC 1981, pages 238–246. ACM, 1981. doi:10.1145/800076.802477.

[bib.bib40] [40] Filip Mazowiecki and Michal Pilipczuk. Reachability for bounded branching VASS. In Wan J. Fokkink and Rob van Glabbeek, editors, 30th International Conference on Concurrency Theory, CONCUR 2019, Amsterdam, The Netherlands, August 27-30, 2019, volume 140 of LIPIcs, pages 28:1–28:13. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2019. doi:10.4230/LIPIcs.CONCUR.2019.28.

[bib.bib41] [41] Filip Mazowiecki, Henry Sinclair-Banks, and Karol Wegrzycki. Coverability in 2-VASS with One Unary Counter is in NP. In Proceedings of FoSSaCS 2023, volume 13992 of Lecture Notes in Computer Science, pages 196–217. Springer, 2023. doi:10.1007/978-3-031-30829-1_10.

[bib.bib42] [42] Guillermo A. Pérez and Shrisha Rao. On continuous pushdown VASS in one dimension. In Rupak Majumdar and Alexandra Silva, editors, 35th International Conference on Concurrency Theory, CONCUR 2024, Calgary, Canada, September 9-13, 2024, volume 311 of LIPIcs, pages 34:1–34:20. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPIcs.CONCUR.2024.34.

[bib.bib43] [43] Michal Pilipczuk, Sylvain Schmitz, and Henry Sinclair-Banks. A Note on the Parameterised Complexity of Coverability in Vector Addition Systems. In Proceedings of IPEC 2025, volume 358 of LIPIcs, pages 24:1–24:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2025. doi:10.4230/LIPIcs.IPEC.2025.24.

[bib.bib44] [44] Charles Rackoff. The Covering and Boundedness Problems for Vector Addition Systems. TCS, 6:223–231, 1978. doi:10.1016/0304-3975(78)90036-1.

[bib.bib45] [45] Wolfgang Reisig. Understanding Petri Nets - Modeling Techniques, Analysis Methods, Case Studies. Springer, 2013. doi:10.1007/978-3-642-33278-4.

[bib.bib46] [46] Louis E. Rosier and Hsu-Chun Yen. A multiparameter analysis of the boundedness problem for vector addition systems. J. Comput. Syst. Sci., 32(1):105–135, 1986. doi:10.1016/0022-0000(86)90006-1.

[bib.bib47] [47] Sylvain Schmitz. Complexity Hierarchies beyond Elementary. ACM Trans. Comput. Theory, 8(1):3:1–3:36, 2016. doi:10.1145/2858784.

[bib.bib48] [48] Sylvain Schmitz. The complexity of reachability in vector addition systems. ACM SIGLOG News, 3(1):4–21, 2016. doi:10.1145/2893582.2893585.

[bib.bib49] [49] Alexander Schrijver. Theory of linear and integer programming. John Wiley & Sons, 1998.

[bib.bib50] [50] Leslie G. Valiant and Mike Paterson. Deterministic one-counter automata. J. Comput. Syst. Sci., 10(3):340–350, 1975. doi:10.1016/S0022-0000(75)80005-5.

[bib.bib51] [51] Joachim von zur Gathen and Malte Sieveking. A bound on solutions of linear integer equalities and inequalities. Proceedings of the American Mathematical Society, 72(1):155–158, October 1978. doi:10.1090/s0002-9939-1978-0500555-0.

[bib.bib52] [52] Yangluo Zheng. Reachability in Vector Addition System with States Parameterized by Geometric Dimension. In Proceedings of CONCUR 2025, volume 348 of LIPIcs, pages 38:1–38:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2025. doi:10.4230/LIPIcs.CONCUR.2025.38.

Exploring VASS Parameterised by Geometric Dimension

Abstract

Keywords and phrases:

Category:

Copyright and License:

2012 ACM Subject Classification:

Related Version:

Funding:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

Our Contributions

Paper Organisation

2 Preliminaries

Vector Spaces and Cones

Theorem 1 (Carathéodory’s Theorem for Rational Cones, see e.g. [49, Corollary 7.1i]).

Theorem 2 (Carathéodory’s Theorem for Integer Cones, [16, Theorem 1]).

Vector Addition Systems with States

Geometric Dimension of a VASS

Lemma 3.

Proof.

Integer Solutions of Linear Systems

Lemma 4 ([6, Prop. 4]).

Lemma 5.

3 Coverability

Theorem 6.

Definition 7 (Clean basis).

Definition 8 (Geometrically small configurations).

Claim 9.

Proof Sketch.

Claim 10.

Proof Sketch.

Claim 11.

Proof Sketch.

Lemma 12.

Proof.

▶ Remark 13.

3.1 Improving Coverability Witness Length Bounds

Theorem 14.

Definition 15 (Bounded and thin configurations).

Claim 16.

Proof.

Claim 17.

Proof.

Lemma 18.

Proof.

Claim 19.

4 Simultaneous Unboundedness

Theorem 20.

Lemma 21.

Proof.

5 Boundedness

Lemma 22 ([44, Lemma 4.2]).

Theorem 23.

▶ Remark 24.

▶ Remark 25.

5.1 Length Bound of Unboundedness Witnesses

Lemma 26.

The Base Case

Claim 27.

The Induction Step

Case 1.

Case 2.

6 Integer Reachability in Geometric Dimension

Theorem 28.

Proof.

7 Tower-Hardness of Reachability in SCC Dimension 4

Theorem 29.

8 Future Research

Conjecture 30.

Example 31.

Conjecture 32.

Proof of Conjecture 30 assuming Conjecture 32.

Conjecture 33.

Conjecture 34.

References

$\blacktriangleright$ Remark 13.

$\blacktriangleright$ Remark 24.

$\blacktriangleright$ Remark 25.