RPTU Kaiserslautern-Landau<EMAIL_ADDRESS>Research partially
supported by the Deutsche Forschungsgemeinschaft (DFG, German Research
Foundation) – 462679611. University of Warsaw, Poland
<EMAIL_ADDRESS>Supported by the ERC grant INFSYS, agreement no.
950398. Max Planck Institute for Software Systems (MPI-SWS) lschuetze@mpi-
sws.org 0000-0003-4002-5491 Centre for Discrete Mathematics and its
Applications (DIMAP) & Department of Computer Science, University of Warwick,
Coventry, UK and http://henry.sinclair-banks.com h.sinclair-
<EMAIL_ADDRESS>https://orcid.org/0000-0003-1653-4069 Supported by EPSRC
Standard Research Studentship (DTP), grant number EP/T5179X/1. Saarland
University and Max Planck Institute for Informatics, Saarbrücken, Germany
<EMAIL_ADDRESS>https://orcid.org/0000-0001-9746-5733 Supported
by the project TIPEA that has received funding from the European Research
Council (ERC) under the European Unions Horizon 2020 research and innovation
programme (grant agreement No. 850979). <ccs2012> <concept>
<concept_id>10003752.10003753</concept_id> <concept_desc>Theory of computation
Models of computation</concept_desc>
<concept_significance>500</concept_significance> </concept> </ccs2012>
[500]Theory of computation Models of computation

###### Acknowledgements.

We would like to thank our anonymous reviewers for their comments, for their
time, and especially for highlighting a piece of related work [30].

# Coverability in VASS Revisited: Improving Rackoff’s Bound to Obtain
Conditional Optimality

Marvin Künnemann  Filip Mazowiecki  Lia Schütze  Henry Sinclair-Banks  Karol
Węgrzycki

###### Abstract

Seminal results establish that the coverability problem for Vector Addition
Systems with States (VASS) is in EXPSPACE (Rackoff, ’78) and is EXPSPACE-hard
already under unary encodings (Lipton, ’76). More precisely, Rosier and Yen
later utilise Rackoff’s bounding technique to show that if coverability holds
then there is a run of length at most $n^{2^{\mathcal{O}(d\log d)}}$, where
$d$ is the dimension and $n$ is the size of the given unary VASS. Earlier,
Lipton showed that there exist instances of coverability in $d$-dimensional
unary VASS that are only witnessed by runs of length at least
$n^{2^{\Omega(d)}}$. Our first result closes this gap. We improve the upper
bound by removing the twice-exponentiated $\log(d)$ factor, thus matching
Lipton’s lower bound. This closes the corresponding gap for the exact space
required to decide coverability. This also yields a deterministic
$n^{2^{\mathcal{O}(d)}}$-time algorithm for coverability. Our second result is
a matching lower bound, that there does not exist a deterministic
$n^{2^{o(d)}}$-time algorithm, conditioned upon the Exponential Time
Hypothesis.

When analysing coverability, a standard proof technique is to consider VASS
with bounded counters. Bounded VASS make for an interesting and popular model
due to strong connections with timed automata. Withal, we study a natural
setting where the counter bound is linear in the size of the VASS. Here the
trivial exhaustive search algorithm runs in $\mathcal{O}(n^{d+1})$-time. We
give evidence to this being near-optimal. We prove that in dimension one this
trivial algorithm is conditionally optimal, by showing that $n^{2-o(1)}$-time
is required under the $k$-cycle hypothesis. In general fixed dimension $d$, we
show that $n^{d-2-o(1)}$-time is required under the 3-uniform hyperclique
hypothesis.

###### keywords:

Vector Addition System, Coverability, Reachability, Fine-Grained Complexity,
Exponential Time Hypothesis, $k$-Cycle Hypothesis, Hyperclique Hypothesis

##  1 Introduction

Vector Addition Systems with States (VASS) are a popular model of concurrency
with a number of applications in database theory [9], business processes [48],
and more (see the survey [46]). A $d$-dimensional VASS ($d$-VASS) consists of
a finite automaton equipped with $d$ non-negative valued counters that can be
updated by transitions. A configuration in a $d$-VASS consists of a state and
a $d$-dimensional vector over the naturals. One of the central decision
problems for VASS is the _coverability problem_ , that asks whether there is a
run from a given initial configuration to some configuration with at least the
counter values of a given target configuration. Coverability finds application
in the verification of safety conditions, which often equate to whether or not
a particular state can be reached without any precise counter values [13, 24].
Roughly speaking, one can use VASS as a modest model for concurrent systems
where the dimension corresponds with the number of locations a process can be
in and each counter value corresponds with the number of processes in a
particular location [21, 25].

In 1978, Rackoff [44] showed that coverability is in EXPSPACE, by proving that
if coverability holds then there exists a run of double-exponential length.
Following, Rosier and Yen [45] analysed and discussed Rackoff’s ideas in more
detail and argued that if a coverability holds then it is witnessed by a run
of length at most $n^{2^{\mathcal{O}(d\log d)}}$, where $n$ is the size of the
given unary encoded $d$-VASS. Furthermore, this yields a
$2^{\mathcal{O}(d\log{d})}\cdot\log(n)$-space algorithm for coverability.
Prior to this in 1976, Lipton [36] proved that coverability is EXPSPACE-hard
even when VASS is encoded in unary, by constructing an instance of
coverability witnessed only by a run of double-exponential length
$n^{2^{\Omega(d)}}$. Rosier and Yen [45] also presented a proof that
generalises Lipton’s constructions to show that
$2^{\Omega(d)}\cdot\log(n)$-space is required for coverability. Although this
problem is EXPSPACE-complete in terms of classical complexity, a gap was left
open for the exact space needed for coverability [45, Section 1]. By using an
approach akin to Rackoff’s argument, we close this thirty-eight-year-old gap
by improving the upper bound to match Lipton’s lower bound.

  1. Result 1:

If coverability holds then there exists a run of length at most
$n^{2^{\mathcal{O}(d)}}$ (Theorem 3.4). Accordingly, we obtain an optimal
$2^{\mathcal{O}(d)}\cdot\log(n)$-space algorithm that decides coverability
(Corollary 3.5).

Our bound also implies the existence of a deterministic
$n^{2^{\mathcal{O}(d)}}$-time algorithm for coverability. We complement this
with a matching lower bound on the deterministic running time that is
conditioned upon the Exponential Time Hypothesis (ETH).

  1. Result 2:

Under ETH, there is no deterministic $n^{2^{o(d)}}$-time algorithm deciding
coverability in unary $d$-VASS (Theorem 4.2).

While our results establish a fast-increasing, conditionally optimal exponent
of $2^{\Theta(d)}$ in the time complexity of the coverability problem, they
rely on careful constructions that enforce the observation of large counter
values. In certain settings, however, it is natural to instead consider a
restricted version of coverability, where all counter values remain _bounded_.
This yields one of the simplest models, fixed-dimension bounded unary VASS,
for which we obtain even tighter results. Decision problems for $B$-bounded
VASS, where $B$ forms part of the input, have been studied due to their strong
connections to timed automata [27, 22, 40]. We consider linearly-bounded unary
VASS, that is when the maximum counter value is bounded above by a constant
multiple of the size of the VASS. Interestingly, coverability and reachability
are equivalent in linearly-bounded unary VASS. The trivial algorithm that
employs depth-first search on the space of configurations runs in
$\mathcal{O}(n^{d+1})$-time for both coverability and reachability. We provide
evidence that the trivial algorithm is optimal.

  1. Result 3:

Reachability in linearly-bounded unary 1-VASS requires $n^{2-o(1)}$-time,
subject to the $k$-cycle hypothesis (Theorem 5.5).

This effectively demonstrates that the trivial algorithm is optimal in the
one-dimensional case. For the case of large dimensions, we show that the
trivial algorithm only differs from an optimal deterministic-time algorithm by
at most an $n^{3+o(1)}$-time factor.

  1. Result 4:

Reachability in linearly-bounded unary $d$-VASS requires $n^{d-2-o(1)}$-time,
subject to the 3-uniform $k$-hyperclique hypothesis (Theorem 5.12).

Broadly speaking, these results add a time complexity perspective to the
already known space complexity, that is for any fixed dimension $d$,
coverability in unary $d$-VASS is NL-complete [44].

#### Organisation and Overview

Section 3 contains our first main result, the improved upper bound on the
space required for coverability. Most notably, in Theorem 3.4 we show that if
coverability holds then there exists a run of length at most
$n^{2^{\mathcal{O}(d)}}$. Then, in Corollary 3.5 we are able to obtain a non-
deterministic $2^{\mathcal{O}(d)}\cdot\log(n)$-space algorithm and a
deterministic $n^{2^{\mathcal{O}(d)}}$-time algorithm for coverability. In
much of the same way as Rackoff, we proceed by induction on the dimension. The
difference is in the inductive step; Rackoff’s inductive hypothesis dealt with
a case where all counters are bounded by the same well-chosen value.
Intuitively speaking, the configurations are bounded within a $d$-hypercube.
This turns out to be suboptimal. This is due to the fact that the volume of a
$d$-hypercube with sides of length $\ell$ is $\ell^{d}$; unrolling the
induction steps gives a bound of roughly $n^{d\cdot(d-1)\cdot\ldots\cdot
1}=n^{d!}=n^{2^{\mathcal{O}(d\log d)}}$, hence the twice-exponentiated
$\log(d)$ factor. The key ingredient in our proof is to replace the
$d$-hypercubes with a collection of objects with greatly reduced volume, thus
reducing the number of configurations in a run witnessing coverability.

Section 4 contains our second main result, the matching lower bound on the
time required for coverability that is conditioned upon ETH. In Lemma 4.3, we
first reduce from finding a $k$-clique in a graph to an instance of
coverability in bounded unary 2-VASS with zero-tests. Then, via Lemma 4.5, we
implement the aforementioned technique of Rosier and Yen to, when there is a
counter bound, remove the zero-tests at the cost of increasing to a
$d$-dimensional unary VASS. Then, in Theorem 4.2 we are able to conclude, by
setting $k=2^{d}$, that if ETH holds, then there is no deterministic
$n^{2^{o(d)}}$-time algorithms for coverability in unary $d$-VASS. This is
because ETH implies that there is no $f(k)\cdot n^{o(k)}$-time algorithm for
finding a $k$-clique in a graph with $n$ vertices (Theorem 4.1).

Section 5 contains our other results where we study bounded fixed dimension
unary VASS. Firstly, Theorem 5.5 states that under the $k$-cycle hypothesis
(Hypothesis 5.2), there does not exist a deterministic $n^{2-o(1)}$-time
algorithm deciding reachability in linearly-bounded unary 1-VASS. Further, we
conclude in Corollary 5.7, if the $k$-cycle hypothesis is assumed then there
does not exist a deterministic $n^{2-o(1)}$-time algorithm for coverability in
(not bounded) unary 2-VASS. Following, we prove Theorem 5.12, that claims
there does not exist a deterministic $n^{d-o(1)}$-time algorithm reachability
in linearly-bounded unary $(d+2)$-VASS under the 3-uniform $k$-hyperclique
hypothesis (Hypothesis 5.11). We achieve this with two components. First, in
Lemma 5.13, we first reduce from finding a $4d$-hyperclique to an instance of
reachability in a bounded unary $(d+1)$-VASS with a fixed number of zero-
tests. Second, via Lemma 5.15, we implement the newly developed controlling
counter technique of Czerwiński and Orlikowski [16] to remove the fixed number
of zero-tests at the cost of increasing the dimension by one.

#### Related Work

The coverability problem for VASS has plenty of structure that still receives
active attention. The set of configurations from which the target can be
covered is upwards-closed, meaning that coverability still holds if the
initial counter values are increased. An alternative approach, the _backwards
algorithm_ for coverability, relies on this phenomenon. Starting from the
target configuration, one computes the set of configurations from which it can
be covered [1]. Thanks to the upwards-closed property, it suffices to maintain
the collection of minimal configurations. The backwards algorithm terminates
due to Dickson’s lemma, however, using Rackoff’s bound one can show it runs in
double-exponential time [10]. This technique has been deeply analysed for
coverability in VASS and some extensions [23, 31]. Despite high complexity,
there are many implementations of coverability relying on the backwards
algorithm that work well in practice. Intuitively, the idea is to prune the
set of configurations, using relaxations that can be efficiently implemented
in SMT solvers [21, 7, 8].

Another central decision problem for VASS is the _reachability problem_ ,
asking whether there is a run from a given initial configuration to a given
target configuration. Reachability is a provably harder problem. In essence,
reachability differs from coverability by allowing one zero-test to each
counter. Counter machines, well-known to be equivalent to Turing machines
[42], can be seen as VASS with the ability to arbitrarily zero-test counters;
coverability and reachability are equivalent here and are undecidable. In
1981, Mayr proved that reachability in VASS is decidable [38], making VASS one
of the richest decidable variants of counter machines. Only recently, after
decades of work, has the complexity of reachability in VASS been determined to
be Ackermann-complete [34, 16, 33]. A widespread technique for obtaining lower
bounds for coverability and reachability problems in VASS is to simulate
counter machines with some restrictions. Our overall approach to obtaining
lower bounds follows suit; we first reduce finding cliques in graphs, finding
cycles in graphs, and finding hypercliques in hypergraphs to various
intermediate instances of coverability in VASS with extra properties such as
bounded counters or a fixed number of zero-tests. These VASS, that are counter
machines restricted in some way, are then simulated by standard higher-
dimensional VASS. Such simulations are brought about by the two previously
developed techniques. Rosier and Yen leverage Lipton’s construction to obtain
VASS that can simulate counter machines with bounded counters [45]. Czerwiński
and Orlikowski have shown that the presence of an additional counter in a
VASS, with carefully chosen transition effects and reachability condition, can
be used to implicitly perform a limited number of zero-tests [16].

Recently, some work has been dedicated to the coverability problem for low-
dimensional VASS [3, 41]. Furthermore, reachability in low-dimensional VASS
has been given plenty of attention, in particular for 1-VASS [47, 26] and for
2-VASS [28, 6]. In the restricted class of flat VASS, other fixed dimensions
have also been studied [15, 17].

Another studied variant, _bidirected_ VASS, has the property that for every
transition $(p,{\bf x},q)$, the reverse transition $(q,-{\bf x},p)$ is also
present. The reachability problem in bidirected VASS is equivalent to the
uniform word problem in commutative semigroups, both of which are EXPSPACE-
complete [39]; not to be confused with the reversible reachability problem in
general VASS which is also EXPSPACE-complete [32]. In 1982, Meyer and Mayr
listed an open problem that stated, in terms of commutative semigroups, the
best known upper bound for coverability in general VASS [44], the best known
lower bound for coverability in bidirected VASS [36], and asked for
improvements to these bounds [39, Section 8, Problem 3]. Subsequently, Rosier
and Yen refined the upper bound for coverability in general VASS to
$2^{\mathcal{O}(d\log{d})}\cdot\log(n)$-space [45]. Finally, Koppenhagen and
Mayr showed that the coverability problem in bidirected VASS can be decided in
$2^{\mathcal{O}(n)}$-space [30], matching the lower bound.

##  2 Preliminaries

We use bold font for vectors. We index the $i$-th component of a vector ${\bf
v}$ by writing ${\bf v}[i]$. Given two vectors ${\bf u},{\bf
v}\in\mathbb{Z}^{d}$ we write ${\bf u}\leq{\bf v}$ if ${\bf u}[i]\leq{\bf
v}[i]$ for each $1\leq i\leq d$. For every $1\leq i\leq d$, we write ${\bf
e}_{i}\in\mathbb{Z}^{d}$ to represent the $i$-th standard basis vector that
has ${\bf e}_{i}[i]=1$ and ${\bf e}_{i}[j]=0$ for all $j\neq i$. Given a
vector ${\bf v}\in\mathbb{Z}^{d}$ we define $\lVert{\bf
v}\rVert=\max\\{1,\lvert{\bf v}[1]\rvert,\ldots,\lvert{\bf v}[d]\rvert\\}$.
Throughout, we assume that $\log$ has base $2$. We use $\textsf{poly}(n)$ to
denote $n^{\mathcal{O}(1)}$.

A _$d$ -dimensional Vector Addition System with States_ ($d$-VASS)
$\mathcal{V}=(Q,T)$ consists of a non-empty finite set of states $Q$ and a
non-empty set of transitions $T\subseteq Q\times\mathbb{Z}^{d}\times Q$. A
_configuration_ of a $d$-VASS is a pair $(q,{\bf v})\in Q\times\mathbb{N}^{d}$
consisting of the current state $q$ and current counter values ${\bf v}$,
denoted $q({\bf v})$. Given two configurations $p({\bf u})$, $q({\bf v})$, we
write $p({\bf u})\xrightarrow{}q({\bf v})$ if there exists $t=(p,{\bf x},q)\in
T$ where ${\bf x}={\bf v}-{\bf u}$. We may refer to ${\bf x}$ as the _update_
of a transition and may also write $p({\bf v})\xrightarrow{t}q({\bf w})$ to
emphasise the transition $t$ taken.

A _path_ in a VASS is a (possibly empty) sequence of transitions $((p_{1},{\bf
x}_{1},q_{1}),\ldots,(p_{\ell},{\bf x}_{\ell},q_{\ell}))$, where $(p_{i},{\bf
x}_{i},q_{i})\in T$ for all $1\leq i\leq\ell$ and such that the start and end
states of consecutive transitions match $q_{i}=p_{i+1}$ for all $1\leq
i\leq\ell-1$. A _run_ $\pi$ in a VASS is a sequence of configurations
$\pi=(q_{0}({\bf v}_{0}),\ldots,q_{\ell}({\bf v}_{\ell}))$ such that
$q_{i}({\bf v}_{i})\xrightarrow{}q_{i+1}({\bf v}_{i+1})$ for all $1\leq
i\leq\ell-1$. We denote the length of the run by $\mathrm{len}(\pi)=\ell+1$.
If there is such a run $\pi$, we can write $q_{0}({\bf
v}_{0})\xrightarrow{\pi}q_{\ell}({\bf v}_{\ell})$. We may also write $p({\bf
u})\xrightarrow{*}q({\bf v})$ if there exists a run from $p({\bf u})$ to
$q({\bf v})$. The _underlying path_ of a run $\pi$ is sequence of transitions
$(t_{1},\ldots,t_{\ell})$ taken between each of the configurations in $\pi$,
so $q_{i}({\bf v}_{i})\xrightarrow{t_{i+1}}q_{i+1}({\bf v}_{i+1})$ for all
$0\leq i\leq\ell-1$.

A _$B$ -bounded_ $d$-VASS, in short $(B,d)$-VASS, is given as an integer upper
bound on the counter values $B\in\mathbb{N}$ and $d$-VASS $\mathcal{V}$. A
configuration in a $(B,d)$-VASS is a pair $q({\bf v})\in
Q\times\\{0,\ldots,B\\}^{d}$. The notions of paths and runs in bounded VASS
remain the same as for VASS, but are accordingly adapted for the appropriate
bounded configurations. We note that one should think that $B$ forms part of
the problem statement, not the input, as it will be given implicitly by a
function depending on the size of the VASS. For example, we later consider
_linearly-bounded_ $d$-VASS, that represent occasions where
$B=\mathcal{O}(\lVert\mathcal{V}\rVert)$.

We do allow for zero-dimensional VASS, that is VASS with no counters, which
can be seen as just directed graphs. A _hypergraph_ is a generalisation of the
graph. Formally, a hypergraph is a tuple $H=(V,E)$ where $V$ is a set of
vertices and $E$ is a collection of non-empty subsets of $V$ called
_hyperedges_. For an integer $\mu$, a hypergraph is _$\mu$ -uniform_ if each
hyperedge has cardinality $\mu$. Note that a 2-uniform hypergraph is a
standard graph.

We study the complexity of the _coverability problem_. An instance
$(\mathcal{V},p({\bf u}),q({\bf v}))$ of coverability asks whether there is a
run in the given VASS $\mathcal{V}$ from the given initial configuration
$p({\bf u})$ to a configuration $q({\bf v}^{\prime})$ with at least the
counter values ${\bf v}^{\prime}\geq{\bf v}$ of the given target configuration
$q({\bf v})$. At times, we also consider the _reachability problem_ that
additionally requires ${\bf v}^{\prime}={\bf v}$ so that the target
configuration is reached exactly.

To measure the complexity of these problems we need to discuss the encoding
used. In _unary encoding_ , a $d$-VASS $\mathcal{V}=(Q,T)$ has _size_
$\lVert\mathcal{V}\rVert=\lvert Q\rvert+\sum_{(p,{\bf x},q)\in T}\lVert{\bf
x}\rVert$. We define a _unary_ $d$-VASS $\mathcal{U}=(Q^{\prime},T^{\prime})$
to have restricted transitions $T^{\prime}\subseteq
Q^{\prime}\times\\{-1,0,1\\}^{d}\times Q^{\prime}$, the size is therefore
$\lVert\mathcal{U}\rVert=\lvert Q^{\prime}\rvert+\lvert T^{\prime}\rvert$. For
any unary encoded $d$-VASS $\mathcal{V}$ there exists an equivalent unary
$d$-VASS $\mathcal{U}$ such that
$\lVert\mathcal{U}\rVert=\lVert\mathcal{V}\rVert$. An instance
$(\mathcal{V},p({\bf u}),q({\bf v}))$ of coverability has size
$n=\lVert\mathcal{V}\rVert+\lVert{\bf u}\rVert+\lVert{\bf v}\rVert$. An equal
in size, equivalent instance $(\mathcal{V}^{\prime},p^{\prime}({\bf
0}),q^{\prime}({\bf 0}))$ of coverability exists; consider adding an initial
transition $(p^{\prime},{\bf s},p)$ and a final transition $(q,-{\bf
t},q^{\prime})$.

It is well known that for $d$-VASS, the coverability problem can be reduced to
the reachability problem. Indeed, for an instance $(\mathcal{V},p({\bf
u}),q({\bf v}))$ of coverability, define $\mathcal{V}^{\prime}=(Q,T^{\prime})$
that has additional decremental transitions at the target states
$T^{\prime}=T\cup\\{(q,{\bf e}_{i},q):1\leq i\leq d\\}$. It is clear that
$p({\bf u})\xrightarrow{*}q({\bf v}^{\prime})$, for some ${\bf
v}^{\prime}\geq{\bf v}$, in $\mathcal{V}$ if and only if $p({\bf
u})\xrightarrow{*}q({\bf v})$ in $\mathcal{V}^{\prime}$.

######  Lemma 2.1 (folklore).

Let $(\mathcal{V}$, $p({\bf u})$, $q({\bf v}))$ be an instance of
coverability. It can be reduced to an instance of reachability
$(\mathcal{V}^{\prime}$, $p({\bf u})$, $q({\bf v}))$ such that
$\lVert\mathcal{V}^{\prime}\rVert=\mathcal{O}(\lVert\mathcal{V}\rVert)$.

A _$d$ -dimensional Vector Addition System_ ($d$-VAS) $\mathcal{V}$ is a
system without states, consisting only of a non-empty collection of
transitions $\mathcal{V}\subseteq\mathbb{Z}^{d}$. All definitions, notations,
and problems carry over for VAS except that, for simplicity, we drop the
states across the board. For example, a configuration in a VAS is just a
vector ${\bf v}\in\mathbb{N}^{d}$. Another well-known result from the
seventies by Hopcroft and Pansiot, one can simulate the states of a VASS at
the cost of three extra dimensions in a VAS [28]. For clarity, the VAS
obtained has an equivalent reachability relation between configurations; a
configuration $q({\bf x})$ in the original VASS corresponds with a
configuration $({\bf x},a,b,c)$ in the VAS, where $a$, $b$, and $c$ represent
the state $q$.

######  Lemma 2.2 ([28, Lemma 2.1]).

A $d$-VASS $\mathcal{V}$ can be simulated by $(d+3)$-VAS
$\mathcal{\mathcal{V}^{\prime}}$ such that
$\lVert\mathcal{\mathcal{V}^{\prime}}\rVert=\textsf{poly}(\lVert\mathcal{V}\rVert)$.

##  3 Improved Bounds on the Maximum Counter Value

This section is devoted to our improvement of the seminal result of Rackoff.
Throughout, we fix our attention to the arbitrary instance
$(\mathcal{V},p({\bf s}),q({\bf t}))$ of the coverability problem in a
$d$-VASS $\mathcal{V}=(Q,T)$ from the initial configuration $p({\bf s})$ to a
configuration $q({\bf t}^{\prime})$ with at least the counter values of the
target configuration $q({\bf t})$. We denote
$n=\lVert\mathcal{V}\rVert+\lVert{\bf s}\rVert+\lVert{\bf t}\rVert$.
Informally, $n$ may as well be the number of states plus the absolute value of
the greatest update on any transition, for these differences can be subsumed
by the second exponent in our following upper bounds. The following two
theorems follow from Rackoff’s technique and subsequent work by Rosier and
Yen, in particular see [44, Lemma 3.4 and Theorem 3.5] and [45, Theorem 2.1
and Lemma 2.2].

######  Theorem 3.1 (Corollary of [44, Lemma 3.4] and [45, Theorem 2.1]).

Suppose $p({\bf s})\xrightarrow{*}q({\bf t}^{\prime})$ for some ${\bf
t}^{\prime}\geq{\bf t}$. Then there exists a run $\pi$ such that $p({\bf
s})\xrightarrow{\pi}q({\bf t^{\prime\prime}})$ for some ${\bf
t}^{\prime\prime}\geq{\bf t}$ and $\mathrm{len}(\pi)\leq
n^{2^{\mathcal{O}(d\log d)}}$.

######  Theorem 3.2 (cf. [44, Theorem 3.5]).

For a given $d$-VASS $\mathcal{V}$, integer $\ell$, and two configurations
$p({\bf s})$ and $q({\bf t})$, there is an algorithm that determines the
existence of a run $\pi$ of length $\mathrm{len}(\pi)\leq\ell$ that witnesses
coverability, so $p({\bf s})\xrightarrow{\pi}q({\bf t}^{\prime})$ for some
${\bf t}^{\prime}\geq{\bf t}$. The algorithm can be implemented to run in non-
deterministic $\mathcal{O}(d\log(n\cdot\ell))$-space or deterministic
$2^{\mathcal{O}(d\log(n\cdot\ell))}$-time.

######  Proof 3.3.

In runs whose length is bounded by $\ell$, the observed counter values are
trivially bounded by $n\cdot\ell$. Notice that every configuration can be
written in $\mathcal{O}(d\log(n\cdot\ell))$ space. A non-deterministic
algorithm can therefore decide coverability by guessing a path on-the-fly by
only maintaining the current configuration. The algorithm accepts if and only
if ${\bf t}$ is covered by the final configuration.

The second part follows from the standard construction that if a problem can
be solved in $S(n)$ non-deterministic space then it can be solved in
$2^{\mathcal{O}(S(n))}$ deterministic time. Indeed, one can construct the
graph of all configurations and check whether there is a path from the initial
configuration to the final configuration. Since there are at most
$2^{\mathcal{O}(d\log(n\cdot\ell))}$ many configurations, this can be
completed in $2^{\mathcal{O}(d\log(n\cdot\ell))}$-time.

Note that Theorem 3.1 combined with Theorem 3.2 yield non-deterministic
$2^{\mathcal{O}(d\log d)}$-space and deterministic
$n^{2^{\mathcal{O}(d\log(d))}}$-time algorithms for coverability. Our result
improves this by a $\mathcal{O}(\log(d))$ factor in the second exponent.

######  Theorem 3.4.

Suppose $p({\bf s})\xrightarrow{*}q({\bf t}^{\prime})$ for some ${\bf
t}^{\prime}\geq{\bf t}$. Then there exists a run $\pi$ such that $p({\bf
s})\xrightarrow{\pi}q({\bf t^{\prime\prime}})$ for some ${\bf
t}^{\prime\prime}\geq{\bf t}$ and $\mathrm{len}(\pi)\leq
n^{2^{\mathcal{O}(d)}}$.

This combined with Theorem 3.2 yields the following corollary.

######  Corollary 3.5.

Coverability in $d$-VASS can be decided by both a non-deterministic
$2^{\mathcal{O}(d)}\cdot\log(n)$-space algorithm and a deterministic
$n^{2^{\mathcal{O}(d)}}$-time algorithm.

Note that by Lemma 2.2, we may handle VAS instead of VASS. Recall that, as
there are no states, a $d$-VAS consists only of a set of vectors in
$\mathbb{Z}^{d}$ that we still refer to as transitions. A configuration is
just a vector in $\mathbb{N}^{d}$. Accordingly, we may fix our attention on
the instance $(\mathcal{V},{\bf s},{\bf t})$ of the coverability problem in a
$d$-VAS $\mathcal{V}=\\{{\bf v}_{1},\ldots,{\bf v}_{m}\\}$ from the initial
configuration ${\bf s}$ to a configuration ${\bf t}^{\prime}$ that is at least
as great as the target configuration ${\bf t}$. The rest of this section is
dedicated to the proof of Theorem 3.4. Imitating Rackoff’s proof, we proceed
by induction on the dimension $d$. Formally, we prove a stronger statement;
Theorem 3.4 is a direct corollary of the following lemma.

######  Lemma 3.6.

Define $L_{i}\coloneqq n^{4^{i}}$, and let ${\bf t}\in\mathbb{N}^{d}$ such
that $\lVert{\bf t}\rVert\leq n$. For any ${\bf s}\in\mathbb{N}^{d}$, if ${\bf
s}\xrightarrow{*}{\bf t}^{\prime}$ for some ${\bf t}^{\prime}\geq{\bf t}$ then
there exists a run $\pi$ such that ${\bf s}\xrightarrow{\pi}{\bf
t}^{\prime\prime}$ for some ${\bf t}^{\prime\prime}\geq{\bf t}$ and
$\mathrm{len}(\pi)\leq L_{d}$.

The base case is $d=0$. In a $0$-dimensional VAS, the only possible
configuration is the empty vector $\bm{\varepsilon}$ and therefore there is
only the trivial run $\bm{\varepsilon}\xrightarrow{*}\bm{\varepsilon}$. This
trivially satisfies the lemma.

For the inductive step, when $d\geq 1$, we assume that Lemma 3.6 holds for all
lower dimensions $0,\ldots,d-1$. Let $\pi=({\bf c}_{0},{\bf c}_{1},\ldots,{\bf
c}_{\ell})$ be a run with minimal length such that ${\bf
s}\xrightarrow{\pi}{\bf t}^{\prime}$ for some ${\bf t}^{\prime}\geq{\bf t}$,
so in particular, ${\bf c}_{0}={\bf s}$ and ${\bf c}_{n}={\bf t}^{\prime}$.
Our objective is to prove that $\mathrm{len}(\pi)=\ell+1\leq L_{d}$. Observe
that configurations ${\bf c}_{i}$ need to be distinct, else $\pi$ could be
shortened trivially. We introduce the notion of a _thin configuration_.

######  Definition 3.7 (Thin Configuration).

In a $d$-VAS, we say that a configuration ${\bf c}\in\mathbb{N}^{d}$ is _thin_
if there exists a permutation $\sigma$ of $\\{1,\ldots,d\\}$ such that ${\bf
c}[\sigma(i)]<M_{i}$ for every $i\in\\{1,\ldots,d\\}$, where $M_{0}\coloneqq
n$ and for $i\geq 1$, $M_{i}\coloneqq L_{i-1}\cdot n$.

Recall, from above, the run $\pi=({\bf c}_{0},{\bf c}_{1},\ldots,{\bf
c}_{\ell})$. Let $t\in\\{0,\ldots,\ell\\}$ be the first index where ${\bf
c}_{t}$ is not thin, otherwise let $t=\ell+1$ if every configuration in $\pi$
is thin. We decompose the run about the $t$-th configuration
$\pi=\pi_{\mathrm{thin}}\cdot\pi_{\mathrm{tail}}$, where
$\pi_{\mathrm{thin}}\coloneqq({\bf c}_{0},\ldots,{\bf c}_{t-1})$ and
$\pi_{\mathrm{tail}}\coloneqq({\bf c}_{t},\ldots,{\bf c}_{\ell})$. Note that
$\pi_{\mathrm{thin}}$ or $\pi_{\mathrm{tail}}$ can be empty. Subsequently, we
individually analyse the lengths of $\pi_{\mathrm{thin}}$ and
$\pi_{\mathrm{tail}}$ (see Figure 1). We will also denote ${\bf m}={\bf
c}_{t}$ to be the first configuration that is not thin.

Figure 1: The schematic view of proofs of Claim 1 and Claim 2, restricted to
the two-dimensional case. Note that ${\bf s}$ is the initial configuration and
${\bf t}$ is the target configuration. Every configuration inside the green
shaded polygon is thin, where each rectangular component of the green shaded
polygon corresponds to a permutation of the indices. Observe that ${\bf m}$ is
the first configuration, just outside the green shaded polygon, that is not
thin. Claim 1 bounds $\pi_{\mathrm{thin}}$, and therefore its maximum length,
by the volume of the green polygon. Claim 2 argues that there is an executable
run $\rho$ (drawn in blue) from ${\bf m}$ to ${\bf t}^{\prime\prime}\geq{\bf
t}$ of length at most $L_{d-1}$ that can be used in place of the run
$\pi_{\mathrm{tail}}$ (drawn in red) from ${\bf m}$ to ${\bf
t}^{\prime}\geq{\bf t}$.

######  Claim 1.

$\mathrm{len}(\pi_{\mathrm{thin}})\leq d!\cdot n^{d}\cdot
L_{d-1}\cdot\ldots\cdot L_{0}$.

######  Proof 3.8.

By definition, every configuration in $\pi_{\mathrm{thin}}$ is thin. Moreover,
since $\pi$ has a minimal length, no configurations in $\pi$ repeat, let alone
in $\pi_{\mathrm{thin}}$. We now count the number of possible thin
configurations. There are $d!$ many permutations of $\\{1,\ldots,d\\}$. For a
given permutation $\sigma$ and an index $i\in\\{1,\ldots,d\\}$, we know that
for a thin configuration ${\bf c}$, $0\leq{\bf c}[\sigma(i)]<M_{i}$, so there
are at most $M_{i}=L_{i-1}\cdot n$ many possible values on the $\sigma(i)$-th
counter. Hence the total number of thin configurations is at most
$d!\cdot\prod_{i=1}^{d}(L_{i-1}\cdot n)=d!\cdot n^{d}\cdot
L_{d-1}\cdot\ldots\cdot L_{0}$.

######  Claim 2.

$\mathrm{len}(\pi_{\mathrm{tail}})\leq L_{d-1}.$

######  Proof 3.9.

Consider ${\bf m}\in\mathbb{N}^{d}$, the first configuration of
$\pi_{\mathrm{tail}}$. Let $\sigma$ be a permutation such that ${\bf
m}[\sigma(1)]\leq{\bf m}[\sigma(2)]\leq\ldots\leq{\bf m}[\sigma(d)]$. Given
that ${\bf m}$ is not thin, for every permutation $\sigma^{\prime}$ there
exists an $i\in\\{1,\ldots,d\\}$ such that ${\bf m}[\sigma^{\prime}(i)]\geq
M_{i}$; in particular, this holds for $\sigma$. Note that this also implies
$M_{i}\leq{\bf m}[\sigma(i+1)]\leq\ldots\leq{\bf m}[\sigma(d)]$.

We construct an $(i-1)$-VAS $\mathcal{U}$ from $\mathcal{V}$ by ignoring the
counters $\sigma(i),\ldots,\sigma(d)$. Formally, ${\bf u}\in\mathcal{U}$ if
there is ${\bf v}\in\mathcal{V}$ such that ${\bf u}[j]={\bf v}[\sigma(j)]$ for
each $1\leq j\leq i-1$. In such a case we say ${\bf u}$ is the _projection_ of
${\bf v}$ via $\sigma$. We will use the inductive hypothesis to show that
there is a short path $\rho^{\prime}$ in $\mathcal{U}$ from (the projection
of) ${\bf m}$ covering (the projection of) ${\bf t}$. We will then show that
the remaining components of ${\bf m}$ are large enough that the embedding of
$\rho^{\prime}$ into $\mathcal{V}$ maintains its covering status.

Recall that ${\bf t}^{\prime}$ is the final configuration of the run $\pi$.
Note that the run $\pi_{\mathrm{tail}}$ induces a run
$\pi_{\mathrm{tail}}^{\prime}$ in $\mathcal{U}$ by permuting and projecting
every configuration. More precisely, $({\bf m}[\sigma(1)],\ldots,{\bf
m}[\sigma(i-1)])\xrightarrow{\pi_{\mathrm{tail}}^{\prime}}({\bf
t}^{\prime}[\sigma(1)],\ldots,{\bf t}^{\prime}[\sigma(i-1)])$. By the
inductive hypothesis there exists a run $\rho^{\prime}$ in $\mathcal{U}$ such
that $({\bf m}[\sigma(1)],\ldots,{\bf
m}[\sigma(i-1)])\xrightarrow{\rho^{\prime}}({\bf
t}^{\prime\prime}[\sigma(1)],\ldots,{\bf t}^{\prime\prime}[\sigma(i-1)])$,
such that $({\bf t}^{\prime\prime}[\sigma(1)],\ldots,{\bf
t}^{\prime\prime}[\sigma(i-1)])\geq({\bf t}[\sigma(1)],\ldots,{\bf
t}[\sigma(i-1)])$ and $\mathrm{len}(\rho^{\prime})\leq L_{i-1}$.

Let $({\bf u}_{1},\ldots,{\bf u}_{\mathrm{len}(\rho^{\prime})})$ be the
underlying path of the run $\rho^{\prime}$, that is, the sequence of
transitions in $\mathcal{U}$ that are sequentially added to form the run
$\rho^{\prime}$. By construction, each transition vector ${\bf
u}_{i}\in\mathcal{U}$ has a corresponding transition vector ${\bf
v}_{i}\in\mathcal{V}$ where ${\bf u}_{i}$ is the projection of ${\bf v}_{i}$
via $\sigma$. We will now show that the following run witnesses coverability
of ${\bf t}$.

$\rho=\left({\bf m},\,{\bf m}+{\bf v}_{1},\,{\bf m}+{\bf v}_{1}+{\bf
v}_{2},\,\ldots,\,{\bf m}+\sum_{j=1}^{\mathrm{len}(\rho^{\prime})}{\bf
v}_{j}\right)$

To this end, we verify that (i) $\rho$ is a run, that is, all configurations
lie in $\mathbb{N}^{d}$, and (ii) the final configuration indeed covers ${\bf
t}$. For components $\sigma(1)$, …, $\sigma(i-1)$, this follows directly from
the inductive hypothesis. For all other components we will show that _all_
configurations of $\rho$ are covering ${\bf t}$ in these components. This
satisfies both (i) and (ii).

Let $j$ be any of the remaining components. Recall that by the choice of ${\bf
m}$, ${\bf m}[j]\geq M_{i}=n\cdot L_{i-1}$. Since
$n>\lVert\mathcal{V}\rVert\geq\lVert{\bf v}_{j}\rVert$ for every $1\leq
j\leq\mathrm{len}(\rho^{\prime})$, this means that in a single step, the value
of a counter can change by at most $n$. Given that
$\mathrm{len}(\rho)=\mathrm{len}(\rho^{\prime})\leq L_{i-1}$, the value on
each of the remaining components must be at least $n$ for every configuration
in $\rho$. In particular, observing that $\lVert{\bf t}\rVert\leq n$, the
final configuration of $\rho$ satisfies

${\bf m}+\sum_{j=1}^{\mathrm{len}(\rho^{\prime})}{\bf v}_{j}\geq{\bf t}.$

Finally, observe that $\mathrm{len}(\rho)=\mathrm{len}(\rho^{\prime})\leq
L_{i-1}\leq L_{d-1}$.

To conclude this section, we show that Lemma 3.6 follows from Claim 1 and
Claim 2.

######  Proof 3.10 (Proof of Lemma 3.6).

From Claim 1 and Claim 2,

$\displaystyle\mathrm{len}(\pi)\leq\mathrm{len}(\pi_{\mathrm{thin}})+\mathrm{len}(\pi_{\mathrm{tail}})$
$\displaystyle\,\leq d!\cdot n^{d}\cdot L_{d-1}\cdot\ldots\cdot L_{0}+L_{d-1}$
$\displaystyle\,\leq 2\cdot d!\cdot n^{d}\cdot L_{d-1}\cdot\ldots\cdot L_{0}.$

Recall that $n\geq 2$ and observe that $2\cdot d!\cdot n^{d}\leq n^{2^{d}}$.
Hence,

$\mathrm{len}(\pi)\leq n^{2^{d}}\cdot L_{d-1}\cdot\ldots\cdot L_{0}.$

Next, we use the definition of $L_{i}\coloneqq n^{4^{i}}$ to show

$\mathrm{len}(\pi)\leq n^{2^{d}}\cdot\prod_{i=0}^{d-1}n^{4^{i}}\leq
n^{\left(2^{d}+\sum_{i=0}^{d-1}4^{i}\right)}.$

Finally, when $d\geq 1$, $2^{d}+\sum_{i=0}^{d-1}4^{i}\leq 4^{d}$ holds,
therefore

$\mathrm{len}(\pi)\leq n^{4^{d}}=L_{d}.$

##  4 Conditional Time Lower Bound for Coverability

In this section, we present a conditional lower bound based on the
_Exponential Time Hypothesis_ (ETH) [29]. Roughly speaking, ETH is a
conjecture that an $n$-variable instance of $3$-SAT cannot be solved by a
deterministic $2^{o(n)}$-time algorithm (for a modern survey, see [37]). In
our reductions, it will be convenient for us to work with the $k$-clique
problem instead. In the $k$-clique problem we are given a graph $G=(V,E)$ as
an input and the task is to decide whether there is a set of $k$ pairwise
adjacent vertices in $V$. The naive algorithm for $k$-clique runs in
$\mathcal{O}(n^{k})$ time. Even though the exact constant in the dependence on
$k$ can be improved [43], ETH implies that the exponent must have a linear
dependence on $k$.

######  Theorem 4.1 ([11, Theorem 4.2], [12, Theorem 4.5], and [14, Theorem
14.21]).

Assuming the Exponential Time Hypothesis, there is no algorithm running in
time $f(k)\cdot n^{o(k)}$ for the $k$-clique problem for any computable
function $f$. Moreover one can assume that $G$ is $k$-partite, i.e.
$G=(V_{1}\cup\ldots\cup V_{k},E)$ and edges belong to $V_{i}\times V_{j}$ for
$i\neq j\in\\{1,\ldots,k\\}$.

We will use Theorem 4.1 to show the following conditional lower bound for
coverability in unary $d$-VASS, which is proved at the end of this section.

######  Theorem 4.2.

Assuming the Exponential Time Hypothesis, there does not exist an
$n^{2^{o(d)}}$-time algorithm deciding coverability in a unary $d$-VASS with
$n$ states.

We first reduce the $k$-clique problem to coverability in bounded 2-VASS with
the ability to perform a fixed number of zero-tests. We will then leverage a
result by Rosier and Yen to construct an equivalent, with respect to
coverability, $(\mathcal{O}(\log k))$-VASS without zero-tests.

######  Lemma 4.3.

Given a $k$-partite graph $G=(V_{1}\cup\cdots\cup V_{k},E)$ with $n$ vertices,
there exists a unary $(\mathcal{O}(n^{2k}),2)$-VASS with $\mathcal{O}(k^{2})$
zero-tests $\mathcal{T}$ such that there is a $k$-clique in $G$ if and only if
there exists a run from $q_{I}({\bf 0})$ to $q_{F}({\bf v})$ in $\mathcal{T}$,
for some ${\bf v}\geq{\bf 0}$. Moreover,
$\lVert\mathcal{T}\rVert\leq\textsf{poly}(n+k)$ and $\mathcal{T}$ can be
constructed in $\textsf{poly}(n+k)$-time.

######  Proof 4.4.

Without loss of generality, we may assume that each of the $k$ vertex subsets
in the graph has the same size $\lvert V_{1}\rvert=\ldots=\lvert
V_{k}\rvert=\ell$. Thus $n=k\cdot\ell$. For convenience, we denote
$V=\\{1,\ldots,k\\}\times\\{1,\ldots,\ell\\}$.

We begin by sketching the main ideas behind the reduction before they are
implemented. We start by finding the first $n=k\cdot\ell$ primes and
associating a distinct prime $p_{i,j}$ to each vertex $(i,j)\in V$. Note that
a product of $k$ different primes uniquely corresponds to selecting $k$
vertices. Thus the idea is to guess such a product, and test whether the
corresponding verticies form a $k$-clique. To simplify the presentation we
present VASS also as counter programs, inspired by Esparza’s presentation of
Lipton’s lower bound [20, Section 7].

We present an overview of our construction in Algorithm 1. Note that the
counter $\mathsf{y}$ is used only by subprocedures. Initially both counter
values are $0$, as in the initial configuration of the coverability instance.
The program is non-deterministic and we are interested in the existence of a
certain run. One should think that coverability holds if and only if there is
a run through the code without getting stuck so to say. In this example a run
can be stuck only in the Edge$[e]$ subprocedure, that will be explained later.
The precise final counter values are not important, as we are simply aiming to
cover the target counter values ${\bf 0}$. The variable $i$ (in the first
loop) and variables $i$ and $j$ (in the second loop) are just syntactic sugar
for copying similar code multiple times. The variables $j$ (in the first loop)
and $e$ (in the second loop) allow us to neatly represent non-determinism in a
VASS.

input : $\mathsf{x}=0$, $\mathsf{y}=0$

$\mathsf{x}\,+$$=1$

for  _$i\leftarrow 1$ to $k$_ do

$\textbf{guess }j\in\\{1,\ldots,\ell\\}$

Multiply$[\mathsf{x},p_{i,j}]$

end for

for  _$(i,j)\in\\{1,\ldots,k\\}^{2}$ , $i\neq j$_ do

$\textbf{guess }e\in E\cap(V_{i}\times V_{j})$

Edge$[e]$

end for

Algorithm 1 A counter program for a VASS with zero tests with two counters
$\mathsf{x}$ and $\mathsf{y}$.

Algorithm 1 uses the Multiply$[\mathsf{x},p]$ and Edge$[e]$ subprocedures.
These two subprocedures will be implemented later. Note that
Multiply$[\mathsf{x},p]$ takes a counter $\mathsf{x}$ as input as we later
reuse this subprocedure when there is more than one counter subject to
multiplication. The intended behaviour of Multiply$[\mathsf{x},p]$ is that it
can be performed if and only if as a result we get $\mathsf{x}=\mathsf{x}\cdot
p$, despite the fact that VASS can only additively increase and decrease
counters. The subprocedure Edge$[e]$ can be performed if and only if both
vertices of the edge $e$ are encoded in the value of the counter $\mathsf{x}$.
Overall, Algorithm 1 is designed so that in the first part the variable
$\mathsf{x}$ is multiplied by $p_{i,j}$, where for every $i$ one $j$ is
guessed. This equates to selecting one vertex from each $V_{i}$. Then the
second part the algorithm checks whether between every pair of selected
vertices from $V_{i}$ and $V_{j}$ there is an edge. Clearly there is a run
through the program that does not get stuck if and only if there is $k$-clique
in $G$.

$q_{I}$$q_{I}$$q_{F}$Multiply$[\mathsf{x},p_{v_{1,1}}]$Multiply$[\mathsf{x},p_{v_{1,2}}]$$\cdots$Multiply$[\mathsf{x},p_{v_{1,\ell}}]$$\cdots$$\cdots$$\cdots$Multiply$[\mathsf{x},p_{v_{k,1}}]$Multiply$[\mathsf{x},p_{v_{k,2}}]$$\cdots$Multiply$[\mathsf{x},p_{v_{k,\ell}}]$$\mathsf{x}\,+$$=1$

$q_{F}$$q_{I}$Edge$[\\{u_{1},u_{2}\\}]$Edge$[\\{v_{1},v_{2}\\}]$$\cdots$Edge$[\\{w_{1},w_{2}\\}]$$V_{1}\times
V_{2}\cap E$$\cdots$$\cdots$$\cdots$$V_{i}\times V_{j}\cap
E$Edge$[\\{u_{k-1},u_{k}\\}]$Edge$[\\{v_{k-1},v_{k}\\}]$$\cdots$Edge$[\\{w_{k-1},w_{k}\\}]$$V_{k-1}\times
V_{k}\cap E$

Figure 2: The top part of the VASS implements the first line and the first
loop in Algorithm 1. The variable $\mathsf{x}$ is multiplied by $k$ non-
deterministically chosen primes $p_{i,j}$, each corresponding to a vertex in
$V_{i}$. The bottom part of the VASS implements the second loop in Algorithm
1. For every pair $i\neq j$ the VASS non-deterministically chooses $e\in
V_{i}\cap V_{j}$ and invokes the subprocedure Edge$[e]$.

In Figure 2 we present a VASS with zero-tests implementing Algorithm 1. The
construction will guarantee that $q_{F}({\bf 0})$ can be covered from
$q_{I}({\bf 0})$ if and only if there is a $k$-clique in $G$.

It remains to define the subprocedures. One should think that every call of a
subprocedure corresponds to a unique part of the VASS, like a gadget of sorts.
To enter and leave the subprocedure one needs to add trivial transitions that
to do not change the counter values. All subprocedures rely on the invariant
$\mathsf{y}=0$ at the beginning and admit the invariant at the end.

We start with Multiply$[\mathsf{x},p]$ and Divide$[\mathsf{x},p]$ that indeed
multiply and divide $\mathsf{x}$ by $p$, respectively. See Algorithm 2 for the
counter program and VASS implementations. Notice that the repeat loops
correspond to the self-loops in the VASS. In the Multiply$[\mathsf{x},p]$
gadget, it is easy to see that a run passes through the procedure if and only
if the counter $\mathsf{x}$ is multiplied by $p$. Similarly, in the
Divide$[\mathsf{x},p]$ gadget, it is easy to see that a run pass through the
procedure if and only if the counter $\mathsf{x}$ is divided by $p$ wholly.
Indeed, the division procedure would get stuck if $p\nmid\mathsf{x}$ because
it will be impossible to exit the first loop.

input : $\mathsf{x}=v$, $\mathsf{y}=0$

output : $\mathsf{x}=v\cdot p$, $\mathsf{y}=0$

repeat

$\mathsf{x}\,-$$=1$; $\mathsf{y}\,+$$=1$

until  _$\mathsf{x}=0$_

repeat

$\mathsf{x}\,+$$=p$; $\mathsf{y}\,-$$=1$

until  _$\mathsf{y}=0$_

$\mathsf{x}=0$$\mathsf{y}=0$

$\mathsf{x}\,-$$=1$$\mathsf{y}\,+$$=1$$\mathsf{x}\,+$$=p$$\mathsf{y}\,-$$=1$
input : $\mathsf{x}=v\cdot p$, $\mathsf{y}=0$

output : $\mathsf{x}=v$, $\mathsf{y}=0$

repeat

$\mathsf{x}\,-$$=p$; $\mathsf{y}\,+$$=1$

until  _$\mathsf{x}=0$_

repeat

$\mathsf{x}\,+$$=1$; $\mathsf{y}\,-$$=1$

until  _$\mathsf{y}=0$_

$\mathsf{x}=0$$\mathsf{y}=0$

$\mathsf{x}\,-$$=p$$\mathsf{y}\,+$$=1$$\mathsf{x}\,+$$=1$$\mathsf{y}\,-$$=1$

Algorithm 2 The counter program of Multiply$[\mathsf{x},p]$ above its VASS
implementation (left) and the counter program of Divide$[\mathsf{x},p]$ above
its VASS implementation (right).

The procedure Edge$[\\{u,v\\}]$ is very simple, it is a sequence of four
subprocedures, see Algorithm 3. Indeed, to check if the vertices from edge $e$
are encoded in $\mathsf{x}$ we simply check whether $\mathsf{x}$ is divisible
by the corresponding primes. Afterwards we multiply $\mathsf{x}$ with the same
primes so that the value does not change and it is ready for future edge
checks.

input : $\mathsf{x}=v$, $\mathsf{y}=0$

output : $\mathsf{x}=v$, $\mathsf{y}=0$

Divide$[\mathsf{x},p_{u}]$

Multiply$[\mathsf{x},p_{u}]$

Divide$[\mathsf{x},p_{v}]$

Multiply$[\mathsf{x},p_{v}]$

Divide$[\mathsf{x},p_{u}]$Multiply$[\mathsf{x},p_{u}]$Divide$[\mathsf{x},p_{v}]$Multiply$[\mathsf{x},p_{v}]$

Algorithm 3 The counter program for Edge$[\\{u,v\\}]$ and its VASS
implementation.

It remains to analyse the size of the VASS and its construction time in this
reduction time. In every run from $q_{I}({\bf 0})$ to $q_{F}({\bf v})$, for
some ${\bf v}\geq{\bf 0}$, the greatest counter value observable can be
bounded above by $p^{k}$ where $p$ is the $n$-th prime. By the Prime Number
Theorem (for example, see [50]), we know that
$p^{k}\leq\mathcal{O}((n\log(n))^{k})\leq\mathcal{O}(n^{2k})$ is an upper
bound on the counter values observed. Hence $\mathcal{T}$ is an
$\mathcal{O}(n^{2k})$-bounded unary 2-VASS.

Now, we count the number of zero-tests performed in each run from $q_{I}({\bf
0})$ to $q_{F}({\bf v})$, for some ${\bf v}\geq{\bf 0}$. The only zero-tests
occur in the instances of the Multiply and Divide subprocedures, each
performing two zero-tests. In the first part of $\mathcal{T}$, a run will
encounter $k$ many Multiply subprocedures, contributing $2k$ many zero-tests.
In the second part of $\mathcal{T}$, a run will encounter $k\choose 2$ many
Edge subprocedures, each containing two Multiply subprocedures and two Divide
subprocedures, in total contributing $8{k\choose 2}$ many zero-tests.
Together, every run encounters exactly $2k+8{k\choose 2}=2k(2k-1)$ many zero-
tests. Hence $\mathcal{T}$ is an $\mathcal{O}(n^{2k})$-bounded unary 2-VASS
with $2k(2k-1)$ zero-tests.

Finally, the Multiply and Divide subprocedures contain three states and five
transitions. Since the $n$-th prime is bounded above by
$\mathcal{O}(n\log(n))$, we also get
$\lVert\mathcal{T}\rVert=\mathcal{O}(n\log(n))$, hence our VASS can be
represented using unary encoding. Analysing Algorithm 1, it is easy to see
that overall the number of states is polynomial in $n$. Finally, the first $n$
primes can be found in $\mathcal{O}(n^{1+o(1)})$ time [2]. Therefore, in total
$\mathcal{T}$ has size $\lVert\mathcal{T}\rVert=\textsf{poly}(n+k)$ and can be
constructed in $\textsf{poly}(n+k)$ time.

To attain conditional lower bounds for coverability we must replace the zero-
tests. We make use of a technique of Rosier and Yen [45] that relies on the
construction of Lipton [36]. They show that a $(2n)^{2^{k}}$-bounded counter
machine with finite state control can be simulated by a unary
$(\mathcal{O}(k))$-VASS with $n$ states. As Rosier and Yen detail after their
proof, it is possible to apply this technique to multiple counters with zero-
tests at once [45]. This accordingly results in the number of VASS counters
increasing, but we instantiate this with just two counters. We remark that the
VASS constructed in Lemma 4.3 is structurally bounded, so for any initial
configuration there is a limit on the largest observable counter value, as is
the VASS Lipton constructed.

######  Lemma 4.5 (Corollary of [45, Lemma 4.3]).

Let $\mathcal{T}$ be an $n$-state unary $(n^{\mathcal{O}(k)},2)$-VASS with
zero-tests, for some parameter $k$. Then there exists an
$\mathcal{O}(n)$-state $(\mathcal{O}(\log{k}))$-VASS $\mathcal{V}$, such that
there is a run from $q_{I}({\bf 0})$ to $q_{F}({\bf v})$, for some ${\bf
v}\geq{\bf 0}$, in $\mathcal{T}$ if and only if there is a run from
$q_{I}^{\prime}({\bf 0})$ to $q_{F}^{\prime}({\bf w})$, for some ${\bf
w}\geq{\bf 0}$, in $\mathcal{V}$. Moreover, $\mathcal{V}$ has size
$\mathcal{O}(\lvert\mathcal{T}\rvert)$ and can be constructed in the same
time.

With this, we can finish the proof of our main theorem for this section.

######  Proof 4.6 (Proof of Theorem 4.2).

Let $k=2^{d}$. We instantiate Lemma 4.3 on $k$-partite graphs $G$ with $n$
vertices. We therefore obtain a unary $(n^{2^{\mathcal{O}(d)}},2)$-VASS with
zero tests $\mathcal{T}$ such that $G$ contains a $k$-clique if and only if
there is a run from $q_{I}({\bf 0})$ to $q_{F}({\bf v})$, for some ${\bf
v}\geq{\bf 0}$, in $\mathcal{T}$.

Given the bound on the value of the counters, we can apply Lemma 4.5 to
$\mathcal{T}$. This gives us an $\mathcal{O}(n)$-state $(\mathcal{O}(d))$-VASS
$\mathcal{V}$ such that $G$ contains a $k$-clique if and only if there is a
run from $q_{I}^{\prime}({\bf 0})$ to $q_{F}^{\prime}({\bf w})$, for some
${\bf w}\geq{\bf 0}$, in $\mathcal{V}$.

By Theorem 4.1 we conclude that under the Exponential Time Hypothesis there
does not exist an $n^{2^{o(d)}}$-time algorithm deciding coverability in unary
$d$-VASS.

##  5 Coverability and Reachability in Bounded Unary VASS

In this section, we give even tighter bounds for coverability in _bounded_
fixed dimension unary VASS. Specifically, for a time constructible function
$B(n)$, the coverability problem in $(B(n),d)$-VASS asks, for a given
$(B(n),d)$-VASS $\mathcal{V}=(Q,T)$ of size $n$ as well as configurations
$p({\bf u})$, $q({\bf v})$, whether there is a run in $\mathcal{V}$ from
$p({\bf u})$ to $q({\bf v}^{\prime})$ for some ${\bf v}^{\prime}\geq{\bf v}$
such that each counter value remains in $\\{0,\ldots,B(n)\\}$ throughout. We
would like to clarify the fact that the bound is not an input parameter. We
focus on the natural setting of linearly-bounded fixed dimension VASS, that is
$(\mathcal{O}(n),d)$-VASS. There is simple algorithm, presented in the proof
of in Observation 5, that yields an immediate $\mathcal{O}(n^{d+1})$ upper
bound for the time needed to decide the coverability problem. We accompany
this observation with closely matching lower bounds, please see Table 1 for an
overview.

$d$ | Lower Bound | Upper Bound
---|---|---
$0$ |  $\Omega(n)$ (trivial) | $\mathcal{O}(n)$
$1$ |  $n^{2-o(1)}$ (Theorem 5.5) | $\mathcal{O}(n^{2})$
$2$ |  $n^{2-o(1)}$ (from above) | $\mathcal{O}(n^{3})$
$3$ |  $n^{2-o(1)}$ (from above) | $\mathcal{O}(n^{4})$
$d\geq 4$ |  $n^{d-2-o(1)}$ (Theorem 5.12) | $\mathcal{O}(n^{d+1})$
Table 1: Conditional lower bounds and upper bounds of the time complexity of
coverability and reachability in unary $(\mathcal{O}(n),d)$-VASS. For clarity,
we remark that Theorem 5.5 is subject to Hypothesis 5.2 and that Theorem 5.12
is subject to Hypothesis 5.11. Note that the lower bounds for dimensions $d=2$
and $d=3$ follow from Theorem 5.5 by just adding components consisting of only
zeros. All upper bounds follow from Observation 5.

Coverability in an $n$-sized unary $(B(n),d)$-VASS can be solved in
$\mathcal{O}(n(B(n)+1)^{d})$-time.

######  Proof 5.1.

Since all configuration in a $(B(n),d)$-VASS belong to the finite set
$Q\times\\{0,\ldots,B(n)\\}^{d}$, we can exhaustively explore all
configurations reachable from $p({\bf v})$ using a straightforward depth-first
search. Each state $q\in Q$ and each transition $t\in T$ will be considered at
most once for each admissible vector in $\\{0,\ldots,B(n)\\}^{d}$, requiring
time $\mathcal{O}(n(B(n)+1)^{d})$ since $\lvert Q\rvert,\lvert T\rvert\leq n$.
We accept the instance if and only if we ever witnessed a configuration
$q({\bf v}^{\prime})$ for some ${\bf v}^{\prime}\geq{\bf v}$.

### Lower Bounds for Coverability in Linearly-Bounded VASS

Now, we consider lower bounds for the coverability problem in linearly-bounded
fixed dimension unary VASS. Firstly, in dimension one, we show that quadratic
running time is conditionally optimal under the $k$-cycle hypothesis.
Secondly, in dimensions four and higher, we require a running time at least
$n^{d-2-o(1)}$ under the 3-uniform hyperclique hypothesis. Together, this
provides evidence that the simple $\mathcal{O}(n^{d+1})$ algorithm for
coverability in $(\mathcal{O}(n),d)$-VASS is close to optimal, as summarised
in Table 1.

######  Hypothesis 5.2 ($k$-Cycle Hypothesis).

For every $\varepsilon>0$, there exists some $k$ such that there does not
exist a $\mathcal{O}(m^{2-\varepsilon})$-time algorithm for finding a
$k$-cycle in directed graphs with $m$ edges.

The $k$-cycle hypothesis arises from the state-of-the-art
$\mathcal{O}(m^{2-\frac{c}{k}+o(1)})$-time algorithms, where $c$ is some
constant [4, 49, 19]. It has been previously used as an assumption for
hardness results, for example, see [35, 5, 18]. It is a standard observation,
due to colour-coding arguments, that we may without loss of generality assume
that the graph given is a $k$-circle-layered graph [35, Lemma 2.2].
Specifically, we can assume that the input graph $G=(V,E)$ has vertex
partition $V=V_{0}\cup\cdots\cup V_{k-1}$ such that each edge $\\{u,v\\}\in E$
is in $V_{i}\times V_{i+1\,(\mathrm{mod}\ k)}$ for some $0\leq i<k$.
Furthermore, we may assume $|V|\leq|E|$.

######  Lemma 5.3.

Given a $k$-circle-layered graph $G=(V_{0}\cup\cdots\cup V_{k-1},E)$ with $m$
edges, there exists a unary $(\mathcal{O}(n),1)$-VASS $\mathcal{V}$ such that
there is a $k$-cycle in $G$ if and only if there exists a run from $p(0)$ to
$q(0)$ in $\mathcal{V}$. Moreover, $\mathcal{V}$ has size
$n\leq\mathcal{O}(m)$ and can be constructed in $\mathcal{O}(m)$ time.

$P_{0}$$p_{v_{1}}$$p_{v_{2}}$$\cdots$$p_{v_{\ell}}$$+1$$+1$$+1$$Q_{0}$$q_{v_{\ell}}$$\cdots$$q_{v_{2}}$$q_{v_{1}}$$-1$$-1$$-1$$S_{1}$$S_{2}$$\cdots$$S_{k-1}$
Figure 3: The $(\mathcal{O}(n),1)$-VASS $\mathcal{V}$ of size
$n\leq\mathcal{O}(m)$ for finding $k$-cycle in a $k$-circle-layered graphs
with $m$ edges. Note that unlabelled transitions have zero effect. Observe
that the graph is mostly copied into the states and transitions of the
linearly-bounded 1-VASS. Importantly, two copies of $V_{0}$ are created. By
starting at $p_{v_{1}}(0)$ in the first copy, a vertex from $V_{0}$ belonging
to the $k$-cycle can be selected by loading the sole counter with a value
corresponding to that vertex. Then, in the second copy, $q_{v_{1}}(0)$ can
only be reached if the state first arrived at corresponds to the vertex
selected in the beginning. Accordingly, there is a run from $p_{v_{1}}(0)$ to
$q_{v_{1}}(0)$ if and only if there exists a $k$-cycle, since the states
visited in the underlying path of the run correspond to the vertices of the
$k$-cycle.

######  Proof 5.4.

Consider the unary $(\mathcal{O}(m),1)$-VASS $\mathcal{V}=(Q,T)$ that is
defined as follows, please also refer back to Figure 3. For ease of
construction let us number the vertices in $V_{0}$, so suppose that
$V_{0}=\\{v_{1},\ldots,v_{\ell}\\}$.

Let us define the set of states $Q$. There are two copies of the vertex subset
$V_{0}$, namely $P_{0}=\\{p_{v_{1}},\ldots,p_{v_{\ell}}\\}$ and
$Q_{0}=\\{q_{v_{1}},\ldots,q_{v_{\ell}}\\}$. There are also copies of each of
the vertex subsets $V_{1},V_{2},\ldots,V_{k-1}$, namely $S_{i}=\\{s_{v}:v\in
V_{i}\\}$ for each $1\leq i\leq k-1$.

$Q=P_{0}\cup S_{1}\cup S_{2}\cup\cdots\cup S_{k-1}\cup Q_{0}$

Now, we define the set of transitions $T$. There are three kinds of
transitions, the initial _vertex selection_ transitions $T_{I}$, the
intermediate transitions $T_{E}$, and the final _vertex checking_ transitions
$T_{F}$.

$T=T_{I}\cup T_{E}\cup T_{F}$

The initial transitions connect states in $P_{0}$ sequentially. Each
transition increments the counter. Intuitively speaking, the counter takes a
value corresponding to the vertex in $V_{0}$ that will belong to the $k$-cycle
in $G$.

$T_{I}=\\{(p_{v_{i}},1,p_{v_{i+1}}):1\leq i<\ell\\}$

The intermediate transitions are directed copies of the edges in the original
graph. The only difference is that edges between $V_{0}$ and $V_{1}$ are now
transitions from $P_{0}$ to $S_{1}$ and edges between $V_{k-1}$ and $V_{0}$
become transitions from $S_{k-1}$ to $Q_{0}$.

$\displaystyle T_{E}=\,$ $\displaystyle\\{(p_{u},0,s_{v}):\\{u,v\\}\in
V_{0}\times V_{1}\\}\,\cup\,\\{(s_{u},0,q_{v}):\\{u,v\\}\in V_{k-1}\times
V_{0}\\}\,\cup$ $\displaystyle\\{(s_{u},0,s_{v}):\\{u,v\\}\in V_{i}\times
V_{i+1}\text{ for some }1\leq i<k-1\\}$

The final transitions connect the states in $Q_{0}$ sequentially. Each such
transition decrements the counter. Intuitively speaking, if the state reached
in $Q_{0}$ matches the counter that has a value corresponding to the vertex in
$V_{0}$ then the final state $q_{v_{1}}$ can be reached with counter value
zero.

$T_{F}=\\{(q_{v_{i+1}},-1,q_{v_{i}}):1\leq i<\ell\\}$

Importantly, there is a run from the initial configuration $p_{v_{1}}(0)$ to
the target configuration $q_{v_{1}}(0)$ in $\mathcal{V}$ if and only if there
is a $k$-cycle in the $k$-circle-layered graph $G$. In closing, observe that
$\lvert Q\rvert\leq 2|V|$ and $\lvert T\rvert\leq 2|V|+|E|$. Therefore,
$\mathcal{V}$ has size $\mathcal{O}(m)$. We remark that the greatest possible
counter value is trivially bounded above by $\lvert Q\rvert$, hence
$\mathcal{V}$ is a unary $(\mathcal{O}(m),1)$-VASS of size $\mathcal{O}(m)$.

######  Theorem 5.5.

Assuming the $k$-cycle hypothesis, there does not exist an
$\mathcal{O}(n^{2-o(1)})$-time algorithm deciding coverability or reachability
in unary $(\mathcal{O}(n),1)$-VASS of size $n$.

######  Proof 5.6.

Assume for contradiction that reachability in a unary
$(\mathcal{O}(n),1)$-VASS of size $n$ can be solved in time
$\mathcal{O}(n^{2-\varepsilon})$ for some $\varepsilon>0$. By the $k$-cycle
hypothesis (Hypothesis 5.2), there exists a $k$ such that the problem of
finding a $k$-cycle in a $k$-circle layered graph with $m$ vertices cannot be
solved in time $\mathcal{O}(m^{2-\varepsilon})$. Via the reduction presented
above in Lemma 5.3, we create a $(\mathcal{O}(n),1)$-VASS $\mathcal{V}$ of
size $n\leq\mathcal{O}(m)$ together with an initial configuration $p(0)$ and a
target configuration $q(0)$, such that deciding reachability from $p(0)$ to
$q(0)$ in $\mathcal{V}$ determines the existence of a $k$-cycle in $G$. Thus
the $\mathcal{O}(n^{2-\varepsilon})$ algorithm for reachability would give a
$\mathcal{O}(m^{2-\varepsilon})$ algorithm for finding $k$-cycles,
contradicting the $k$-cycle hypothesis.

By the equivalence of coverability and reachability in unary
$(\mathcal{O}(n),1)$ VASS in Lemma 5.9, the same lower bound holds for
coverability.

######  Corollary 5.7.

Assuming the $k$-cycle hypothesis, there does not exist an
$\mathcal{O}(n^{2-o(1)})$-time algorithm for coverability in unary 2-VASS of
size $n$.

######  Proof 5.8.

Consider a standard modification of the reduction presented for Lemma 5.3,
that is to increase the dimension of $\mathcal{V}=(Q,T)$ by one by adding an
opposite counter of sorts, yielding a 2-VASS $\mathcal{W}=(Q,T^{\prime})$. For
every transition $(p,t,q)\in T$, create a transition also modifying the
opposite counter, $(p,(t,-t),q)\in T^{\prime}$. Now, the instance
$(\mathcal{W},p(0,n),q(0,n))$ of coverability holds if and only if the
instance $(\mathcal{V},p(0),q(0))$ of reachability holds. The rest follows by
Theorem 5.5.

Reachability in $(\mathcal{O}(n),d)$-VASS can be decided in
$\mathcal{O}(n(B(n)+1)^{d})$-time using the simple algorithm in Observation 5
with a trivially modified acceptance condition. It turns out that coverability
and reachability are equivalent in unary $(\mathcal{O}(n),d)$-VASS. This is
true in the sense that it may hold that for example coverability in a
$(100n,d)$-VASS may be reduced in linear time to reachability in a
$(3n,d)$-VASS. Conversely, reachability in some linearly-bounded $d$-VASS can
be reduced in linear time to a corresponding instance of coverability in a
linearly-bounded $d$-VASS. Note that perversely, it appears plausible that
instances of coverability in a $(100n,d)$-VASS could in fact be simpler to
solve than in a $(3n,d)$-VASS.

######  Lemma 5.9.

For a $(B(n),d)$-VASS, let $C^{B(n)}(n)$ and $R^{B(n)}(n)$ denote the optimal
running times for coverability and reachability, respectively. For any
$\gamma>0$, there exists some $\delta>0$ such that $C^{\gamma\cdot
n}(n)\leq\mathcal{O}(R^{\delta\cdot n}(n))$. Conversely, for any $\gamma>0$,
there exists some $\delta>0$ such that $R^{\gamma\cdot
n}(n)\leq\mathcal{O}(C^{\delta\cdot n}(n))$.

######  Proof 5.10.

Given an instance $(\mathcal{V},p({\bf u}),p({\bf v}))$, of size $n$, of
coverability in $B(n)$-bounded VASS $\mathcal{V}$. We construct a
$B(n)$-bounded VASS $\mathcal{V}^{\prime}$ from $\mathcal{V}$ by adding
transitions $(q,-{\bf e}_{i},q)$ for every $1\leq i\leq d$. It is easy to see
that there exists a run from $p({\bf u})$ to $q({\bf v})$ in
$\mathcal{V}^{\prime}$ if and only if there exists and a run from $p({\bf u})$
to $q({\bf v}^{\prime})$ for some ${\bf v}^{\prime}\geq{\bf v}$, in
$\mathcal{V}$. Since $\lVert\mathcal{V}^{\prime}\rVert=\mathcal{O}(n)$, for
$B(n)=\gamma\cdot n$ we can ensure that
$B(n)=\delta\cdot\lVert\mathcal{V}^{\prime}\rVert$ for an appropriately
selected $\delta$. Thus, $C^{\gamma n}(n)\leq\mathcal{O}(R^{\delta
n}(\mathcal{O}(n)))\leq\mathcal{O}(R^{\delta n}(n))$.

Conversely, consider an instance $(\mathcal{V},p({\bf u}),p({\bf v}))$, of
size $n$, of reachability in a $B(n)$-bounded VASS $\mathcal{V}$, again denote
$n=\lVert\mathcal{V}\rVert$. We construct the VASS $B(n)$-bounded VASS
$\mathcal{V}^{\prime}$ from $\mathcal{V}$ by adding a path from $q$ to a new
state $r$ whose transitions update the counters by $-{\bf v}$. This is easily
implementable by a path of length at most $B(n)$, for if $\lVert{\bf
v}\rVert>B(n)$ this instance is trivially false. We then append a path from
$r$ to a new state $s$ whose transitions add $B(n)$ to every counter. It is
easy to see that there is a run from $p({\bf u})$ to $s(B(n)\cdot{\bf 1})$ in
$\mathcal{V}^{\prime}$ if and only if there exists a run from $p({\bf u})$ to
$q({\bf v})$ in $\mathcal{V}$. Since
$\lVert\mathcal{V}^{\prime}\rVert=\mathcal{O}(n+B(n))$, for $B(n)=\gamma\cdot
n$ we can ensure that
$B(\lVert\mathcal{V}^{\prime}\rVert)=\delta\lVert\mathcal{V}^{\prime}\rVert$
for some $\delta$. Thus, $R^{\gamma n}(n)\leq\mathcal{O}(C^{\delta
n}(\mathcal{O}(n)))\leq\mathcal{O}(C^{\delta n}(n))$.

### Lower Bounds for Reachability in Linearly-Bounded VASS

To obtain further lower bounds for the coverability problem in
$(\mathcal{O}(n),d)$-VASS, by Lemma 5.9, we can equivalently find lower bounds
for the reachability problem in $(\mathcal{O}(n),d)$-VASS. In Theorem 5.12, we
will assume a well-established hypothesis concerning the time required to find
hypercliques in 3-uniform hypergraphs. In fact, Lincoln, Vassilevska Williams,
and Williams state and justify an even stronger hypothesis about $\mu$-uniform
hypergraphs for every $\mu\geq 3$ [35, Hypothesis 1.4]. We will use this
computational complexity hypothesis to expose precise lower bounds on the time
complexity of reachability in linearly-bounded fixed dimension unary VASS.

######  Hypothesis 5.11 ($k$-Hyperclique Hypothesis [35, Hypothesis 1.4]).

Let $k\geq 3$ be an integer. On Word-RAM with $\mathcal{O}(\log(n))$ bit
words, finding an $k$-hyperclique in a $3$-uniform hypergraph on $n$ vertices
requires $n^{k-o(1)}$ time.

For the remainder of this section, we focus on the proof of the following
Theorem.

######  Theorem 5.12.

Assuming Hypothesis 5.11, reachability in unary $(\mathcal{O}(n),d+2)$-VASS of
size $n$ requires $n^{d-o(1)}$ time.

The lower bound is obtained via reduction from finding hyperclique in
$3$-uniform hypergraphs, hence the lower bound is subject to the
$k$-Hyperclique Hypothesis. We present our reduction in two steps. The first
step is an intermediate step, in Lemma 5.13 we offer a reduction to an
instance of reachability in unary VASS with a limited number of zero-tests.
The second step extends the first, in Lemma 5.15 we modify the reduction by
adding a counter so zero-tests are absented. This extension leverages the
recently developed _controlling counter technique_ of Czerwiński and
Orlikowski [16]. This technique allows for implicit zero-tests to be performed
in the presence of a dedicated counter whose transition effects and
reachability condition ensure these implicit zero-tests were indeed performed
correctly.

It has been shown that we may as assume that the hypergraph is $\ell$-partite
for the $k$-Hyperclique Hypothesis [35, Theorem 3.1]. Thus, we may assume that
the vertices can be partitioned into $\ell$ disjoint subsets
$V=V_{1}\cup\cdots\cup V_{\ell}$ and all hyperedges contain three vertices
from distinct subsets $\\{u,v,w\\}\in V_{i}\times V_{j}\times V_{k}$ for some
$1\leq i<j<k\leq\ell$.

######  Lemma 5.13.

Let $d\geq 1$ be a fixed integer. Given a $4d$-partite $3$-uniform hypergraph
$H=(V_{1}\cup\ldots\cup V_{4d},E)$ with $n$ vertices, there exists a unary
$(\mathcal{O}(n^{4+o(1)}),d+1)$-VASS with $\mathcal{O}(d^{3})$ zero-tests
$\mathcal{T}$ such that there is a $4d$-hyperclique in $H$ if and only if
there is a run from $q_{I}({\bf 0})$ to $q_{F}({\bf v})$, for some ${\bf
v}\geq{\bf 0}$, in $\mathcal{T}$. Moreover, $\mathcal{T}$ can be constructed
in $\textsf{poly}(d)\cdot n^{4+o(1)}$ time.

######  Proof 5.14.

We will re-employ some of the ideas already used in the constructions in the
proof of Lemma 4.3. In particular, we will use Multiply and Divide
subprocedures, see Algorithm 2. Let us denote the $d+1$ counters
$\mathsf{x}_{1},\ldots,\mathsf{x}_{d},\mathsf{y}$. The collective role of
$\mathsf{x}_{1},\ldots,\mathsf{x}_{d}$ is to maintain a representation of the
$4d$ vertices forming the $4d$-hyperclique. The role of $\mathsf{y}$ is to
ensure multiplications and divisions are completed correctly. Just as
previously seen, before the execution of Multiply or Divide, we require
$\mathsf{y}=0$. We will combine these subprocedures to construct new
subprocedures for unary $(d+1)$-VASS with zero-tests to verify properties
related to $3$-uniform hypergraphs.

We start by finding the first $4d\cdot\ell$ primes. We associate a distinct
prime $p_{v}$ to each vertex $v\in V$. Now we encode the chosen $4d$ vertices
that will form the $4d$-clique by storing, on $d$ many counters, products of
four primes corresponding to four of the selected vertices. Therefore, after
the initial guessing part, the value of counter $\mathsf{x}_{i}$ will be
$p_{t}\cdot p_{u}\cdot p_{v}\cdot p_{w}$ for some vertices $t,u,v,w\in V$.
Roughly speaking, we store the product of four primes on one counter so that
the maximum observable counter value matches the size of the resulting VASS
with zero-tests.

input : $\mathsf{x}_{1},\ldots,\mathsf{x}_{d},\mathsf{y}=0$

for  _$i\leftarrow 1$ to $d$_ do

$\mathsf{x}_{i}\,+$$=1$

for  _$j\leftarrow 1$ to $4$_ do

$\textbf{guess }k\in\\{1,\ldots,n\\}$

Multiply$[\mathsf{x}_{i},p_{k}]$

end for

end for

for  _$(i,j,k)\in\\{1,\ldots,4d\\}^{3}$ , $i\neq j\neq k\neq i$_ do

$\textbf{guess }e\in E\cap(V_{i}\times V_{j}\times V_{k})$

HyperEdge$[e]$

end for

Algorithm 4 A counter program representing the VASS with zero tests. As seen
earlier, the variables in for are just syntactic sugar for repeating similar
lines of code, corresponding to states in the VASS. Similarly, the variables
in guess represent non-deterministic branching transitions in a VASS.

#### Guessing part

The VASS presented in Algorithm 4 implements the following algorithm. Guess
$4d$ vertices, not necessarily distinct, and check whether they form a
$4d$-hyperclique. Note that this algorithm is correct because guessing
vertices that are the same or in the same $V_{i}$ does not help us. In
contrast to Algorithm 1, the main difference is that the guessed vertices are
encoded as quadruple products of primes across counters $\mathsf{x}_{1}$, …,
$\mathsf{x}_{d}$. We do not store the entire product of $4d$ primes
explicitly, only the values of each counter.

#### Checking part

In the second part, we verify that we have selected a $4d$-hyperclique by
testing for each of the ${{4d}\choose 3}$ hyperedges. This is achieved
essentially in the same way as Edge$[e]$ was implemented in Algorithm 3. We
check that between every triplet of vertex subsets there is a hyperedge that
has all of the vertices selected in the first part. We implement HyperEdge
subprocedure for checking an individual hyperedge, see Figure 5. This
subprocedure checks that the three primes corresponding to the three vertices
in the hyperedge can divide one of the values stored in
$\mathsf{x}_{1},\ldots,\mathsf{x}_{d}$. For ease of presentation and as
previously mentioned, we introduce a VertexSelected subprocedure that checks
whether a given vertex has been selected, see Figure 4.

VertexSelected$[v]$Divide$[\mathsf{x}_{1},p_{v}]$Multiply$[\mathsf{x}_{1},p_{v}]$Divide$[\mathsf{x}_{2},p_{v}]$Multiply$[\mathsf{x}_{2},p_{v}]$$\cdots$$\cdots$Divide$[\mathsf{x}_{d},p_{v}]$Multiply$[\mathsf{x}_{d},p_{v}]$
Figure 4: The VertexSelected subprocedure implemented in a unary $(d+1)$-VASS
with zero-tests. To instantiate this subprocedure, a vertex $v$ is specified
so that the $d$ counters can be checked for divisibility by the prime $p_{v}$,
with the effect of checking whether the vertex $v$ has been selected. The
counter $y$ is used by the Divide and Multiply subprocedures to ensure the
division and multiplications are completed correctly.
HyperEdge$[\\{u,v,w\\}]$VertexSelected$[u]$VertexSelected$[v]$VertexSelected$[w]$
Figure 5: The HyperEdge subprocedure implemented in a unary $(d+1)$-VASS with
zero-tests. Note that the three vertices of the given hyperedge may be stored
across any of the $d$ counters $\mathsf{x}_{1},\ldots,\mathsf{x}_{d}$.
Therefore, we make use of the VertexSelected subprocedure three times to check
if indeed $u$, $v$, and $w$ have been selected.

Now, we use the aforementioned subprocedures to construct the checking part of
$\mathcal{T}$. This part consists of a sequence of ${{4d}\choose 3}$ non-
deterministic branching sections, one for each triplet of vertex subsets
$U\times V\times W$. In each branching section, there is an instance of the
HyperEdge subprocedure for each of the hyperedges $\\{u,v,w\\}\in U\times
V\times W$. In order to reach the final state $q_{F}$, there must be a
hyperedge between each of the $4d$ vertices selected in the first part of
$\mathcal{T}$. Thus, there is a $4d$-hyperclique in $H$ if and only if there
is a run from $q_{I}({\bf 0})$ to $q_{F}({\bf v})$ for some ${\bf v}\geq{\bf
0}$ in $\mathcal{T}$.

$q_{F}$HyperEdge$[\\{u_{1},u_{2},u_{3}\\}]$HyperEdge$[\\{v_{1},v_{2},v_{3}\\}]$$\cdots$HyperEdge$[\\{w_{1},w_{2},w_{3}\\}]$$V_{1}\times
V_{2}\times V_{3}\cap E$$\cdots$$\cdots$$\cdots$$V_{i}\times V_{j}\times
V_{k}\cap
E$HyperEdge$[\\{u_{4d-2},u_{4d-1},u_{4d}\\}]$HyperEdge$[\\{v_{4d-2},v_{4d-1},v_{4d}\\}]$$\cdots$HyperEdge$[\\{w_{4d-2},w_{4d-1},w_{4d}\\}]$$V_{4d-2}\times
V_{4d-1}\times V_{4d}\cap E$ Figure 6: The check part of the unary
$(d+1)$-VASS with zero-tests $\mathcal{T}$ for finding a $4d$-hyperclique in
$4d$-partite hypergraph.

We are now able to finalize the proof. First, we will carefully analyse the
maximum counter value observed on any run and count the number of zero-tests
performed on any run. Then, we will evaluate the size of $\mathcal{T}$.

The highest counter value observed by each counter
$\mathsf{x}_{1},\ldots,\mathsf{x}_{d}$ is the product of four primes. The
highest counter value observed by $\mathsf{y}$ is equal to the highest counter
value observed by any of the other counters
$\mathsf{x}_{1},\ldots,\mathsf{x}_{d}$. Therefore the bound on the highest
value observed, altogether can be bounded about by $p^{4}$ where $p$ is the
$n$-th prime. By the Prime Number Theorem (for example, see [50]) we know that
$p\in\mathcal{O}(n\log(n))$. Therefore, every run from $q_{I}({\bf 0})$ to
$q_{F}({\bf v})$, for some ${\bf v}\geq{\bf 0}$, in $\mathcal{T}$ is
$\mathcal{O}(n^{4+o(1)})$-bounded.

Zero-tests are only performed by the Multiply and Divide subprocedures, each
instance of these subprocedures contains two zero-tests. It remains to count
the number of these subprocedures are executed on any run. In the guessing
part, there is one Multiply subprocedure for each of the $4d$ vertices
selected to form a $4d$-hyperclique. In the checking part, there is a sequence
of ${{4d}\choose 3}$ many HyperEdge subprocedures. Each HyperEdge subprocedure
contains three instances of the VertexSelected subprocedure which executes one
Divide subprocedure and one Multiply subprocedure. In total, there are
$2(4d+6{{4d}\choose 3})\in\mathcal{O}(d^{3})$ many zero-tests are performed in
any run from $q_{I}({\bf 0})$ to $q_{F}({\bf v})$, for some ${\bf v}\geq{\bf
0}$, in $\mathcal{T}$.

Finally, each instance of the Multiply and Divide subprocedures has size
$\mathcal{O}(n\log{n})$. Note that the first $n$ primes can be found in
$\mathcal{O}(n^{1+o(1)})$-time [2]. In the guessing part, there are $4dn$
instances of the Multiply subprocedure. In the checking part, there is an
instance of the HyperEdge subprocedure for each edge in the hypergraph. The
HyperEdge subprocedures themselves appear in ${{4d}\choose 3}$ many
collections, one for each triplet of vertex subsets. Each HyperEdge
subprocedure contains three instances of the VertexSelected subprocedure,
which contains $d$ instances of the Multiply subprocedure and $d$ instances of
the Divide subprocedure. Therefore, in total $\mathcal{T}$ has polynomial size
and can be constructed in time $\mathcal{O}(dn\cdot
n\log{n}+m\cdot\binom{4d}{3}\cdot d\cdot n\log{n})$, where
$m\in\mathcal{O}(n^{3})$ is the total number of hyperedges.

Consider our earlier described two-step approach towards proving Theorem 5.12
by first obtaining a unary $(d+1)$-VASS $\mathcal{T}$ with zero-tests, then
obtaining a unary $(d+2)$-VASS $\mathcal{V}$ by increasing the dimension by
one and removing the zero-tests. In actuality, both steps occur together to
prove Theorem 5.12. Ultimately, the $d+2$ counters of $\mathcal{V}$ have the
following roles. The counters $\mathsf{x}_{1},\ldots,\mathsf{x}_{d}$ are used
to store the products of primes corresponding to vertices of hyperclique. The
counter $\mathsf{y}$ is used to complete multiplications and divisions. In the
remainder of this section, we add the $d+2$-nd counter that is used to ensure
the (implicit) zero-tests are performed faithfully. We achieve this by
leveraging the _controlling counter technique_ introduced by Czerwiński and
Orlikowski [16]. The following is the restatement of their technique, their
lemma has been restricted to our scenario and rewritten using the notation of
this paper.

######  Lemma 5.15 ([16, Lemma 10]).

Let $\rho$ be a run in a $(d+2)$-VASS such that $q_{I}({\bf
0})\xrightarrow{\rho}q_{F}({\bf 0})$. Further, let $q_{0}({\bf
v}_{0}),q_{1}({\bf v}_{1})\ldots,q_{r}({\bf v}_{r})$ be some distinguished
configurations observed along the run $\rho$ with $q_{0}({\bf
v}_{0})=q_{I}({\bf 0})$ and $q_{r}({\bf v}_{r})=q_{F}({\bf 0})$ and let
$\rho_{j}$ be the segment of $\rho$ that is between $q_{j-1}({\bf v}_{j-1})$
and $q_{j}({\bf v}_{j})$, so $\rho$ can be described as

$q_{I}({\bf 0})=q_{0}({\bf v}_{1})\xrightarrow{\rho_{1}}q_{1}({\bf
v}_{1})\rightarrow\cdots\rightarrow q_{r-1}({\bf
v}_{r-1})\xrightarrow{\rho_{r}}q_{r}({\bf v}_{r})=q_{F}({\bf 0}).$

Let $S_{1},\ldots,S_{d},S_{d+1}\subseteq\\{0,1,\ldots,r\\}$ be the sets of
indices of the distinguished configurations where zero-tests could be
performed on counters $\mathsf{x}_{1},\ldots,\mathsf{x}_{d},\mathsf{x}_{d+1}$,
respectively. Let $t_{j,i}=\lvert\\{s\geq j:s\in S_{i}\\}\rvert$ be the number
of zero-test for the counter $\mathsf{x}_{i}$ in the remainder of the run
$\rho_{j+1}\cdots\rho_{r}$. Given that ${\bf v}_{0}={\bf 0}$ and ${\bf
v}_{r}={\bf 0}$, if

$\mathrm{eff}(\rho_{j})[d+2]=\sum_{i=1}^{d+1}t_{j,i}\cdot\mathrm{eff}(\rho_{j})[i],$
(1)

then for every $i\in\\{1,\ldots,d,d+1\\}$ and $j\in S_{i}$, we know that ${\bf
v}_{j}[i]=0$.

With Lemma 5.15 in hand we can ensure that every zero-test is executed
correctly and conclude this section with a proof of Theorem 5.12.

######  Proof 5.16 (Proof of Theorem 5.12).

Consider the reduction, presented in Lemma 5.13, from finding a
$4d$-hyperclique in a $4d$-partite $3$-uniform hypergraph $H$ to reachability
in $(\mathcal{O}(n^{4+o(1)}),d+1)$-VASS with $\mathcal{O}(d^{3})$ zero-tests.
Now, given Lemma 5.15, we will add a controlling counter to $\mathcal{T}$ so
that the zero-tests on the $d+1$ counters
$\mathsf{x}_{1},\ldots,\mathsf{x}_{d},\mathsf{y}$ are instead performed
implicitly. So we introduce another counter $\mathsf{z}$ that receives updates
on transitions, consistent with Equation 1, whenever any of the other counters
are updated. Note that counters $\mathsf{y}$ and $\mathsf{z}$, for the sake of
a succinct and consistent description, are respectively referred to as
counters $\mathsf{x}_{d+1}$ and $\mathsf{x}_{d+2}$ in the statement of Lemma
5.15. Moreover, notice that the maximum value of $\mathsf{z}$ is bounded by
$\textsf{poly}(d)\cdot\left(\sum_{i=1}^{d+1}\mathsf{x}_{i}\right)\in\textsf{poly}(d)\cdot
n^{4+o(1)}$.

Therefore, we have constructed a unary $(\textsf{poly}(d)\cdot
n^{4+o(1)},d+2)$-VASS $\mathcal{V}$ with the property that there $H$ contains
a $4d$-hyperclique if and only if there is a run from $q_{I}^{\prime}({\bf
0})$ to $q_{F}^{\prime}({\bf 0})$ in $\mathcal{V}$. Such a
$(\textsf{poly}(d)\cdot n^{4+o(1)},d+2)$-VASS $\mathcal{V}$ has size
$\mathcal{O}(t\cdot\lvert\mathcal{T}\rvert)$ where $t\in\textsf{poly}(d)$ is
the number of zero-tests performed on the run from $q_{I}({\bf 0})$ to
$q_{F}({\bf 0})$ in $\mathcal{T}$. Moreover, $\mathcal{V}$ can be constructed
in $\textsf{poly}(d)\cdot n^{4+o(1)}$ time. Hence, if reachability in
$(\mathcal{O}(n),d+2)$-VASS of size $n$ can be solved faster than
$n^{d-o(1)}$, then one can find a $4d$-hyperclique in a $3$-uniform hypergraph
faster than $n^{4d-o(1)}$, contradicting Hypothesis 5.11.

##  6 Conclusion

#### Summary

In this paper, we have revisited a classical problem of coverability in
$d$-VASS. We have closed the gap left by Rosier and Yen [45] on the length of
runs witnessing instances of coverability in $d$-VASS. We have lowered the
upper bound of $n^{2^{\mathcal{O}(d\log d)}}$, from Rackoff’s technique [44],
to $n^{2^{\mathcal{O}(d)}}$ (Theorem 3.4), matching the $n^{2^{\Omega(d)}}$
lower bound from Lipton’s construction [36]. This accordingly closes the gap
on the exact space required for the coverability problem and yields a
deterministic $n^{2^{\mathcal{O}(d)}}$-time algorithm for coverability in
$d$-VASS (Corollary 3.5). We complement this with a matching lower bound
conditional on ETH; there does not exist a deterministic $n^{2^{o(d)}}$-time
algorithm for coverability (Theorem 4.2). By and large, this settles the exact
space and time complexity of coverability in VASS.

In addition, we study linearly-bounded unary $d$-VASS. Here, coverability and
reachability are equivalent and the trivial exhaustive search
$\mathcal{O}(n^{d+1})$ algorithm is near-optimal. We prove that reachability
in linearly-bounded 1-VASS requires $n^{2-o(1)}$-time under the $k$-cycle
hypothesis (Theorem 5.5), matching the trivial upper bound. We further prove
that reachability in linearly-bounded $(d+2)$-VASS requires $n^{d-o(1)}$ time
under the $3$-uniform hyperclique hypothesis (Theorem 5.12).

#### Open Problems

The _boundedness problem_ , a problem closely related to coverability, asks
whether, from a given initial configuration, the set of all reachable
configurations is finite. This problem was also studied by Lipton then Rackoff
and is EXPSPACE-complete [36, 44]. Boundedness was further analysed by Rosier
and Yen [45, Theorem 2.1] and the same gap also exists for the exact space
required. We leave the same improvement, to eliminate the same twice-
exponentiated $\log(d)$ factor, as an open problem.

Our lower bounds for the time complexity of coverability and reachability in
linearly-bounded unary $d$-VASS, for $d\geq 2$, leave a gap of up to
$n^{3+o(1)}$, see Table 1. We leave it as an open problem to either improve
upon the upper bound $\mathcal{O}(n^{d+1})$ given by the trivial algorithm, or
to raise our conditional lower bounds.

## References

  * [1] Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, and Yih-Kuen Tsay.  Algorithmic analysis of programs with well quasi-ordered domains.  Inf. Comput., 160(1-2):109–127, 2000.  doi:10.1006/inco.1999.2843.
  * [2] Manindra Agrawal, Neeraj Kayal, and Nitin Saxena.  Primes is in P.  Annals of mathematics, pages 781–793, 2004.
  * [3] Shaull Almagor, Nathann Cohen, Guillermo A. Pérez, Mahsa Shirmohammadi, and James Worrell.  Coverability in 1-VASS with Disequality Tests.  In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), volume 171 of LIPIcs, pages 38:1–38:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020\.  doi:10.4230/LIPIcs.CONCUR.2020.38.
  * [4] Noga Alon, Raphael Yuster, and Uri Zwick.  Finding and counting given length cycles.  Algorithmica, 17(3):209–223, 1997.  doi:10.1007/BF02523189.
  * [5] Bertie Ancona, Monika Henzinger, Liam Roditty, Virginia Vassilevska Williams, and Nicole Wein.  Algorithms and hardness for diameter in dynamic graphs.  In Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi, editors, 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, July 9-12, 2019, Patras, Greece, volume 132 of LIPIcs, pages 13:1–13:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.  doi:10.4230/LIPIcs.ICALP.2019.13.
  * [6] Michael Blondin, Matthias Englert, Alain Finkel, Stefan Göller, Christoph Haase, Ranko Lazić, 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.
  * [7] Michael Blondin, Alain Finkel, Christoph Haase, and Serge Haddad.  Approaching the Coverability Problem Continuously.  In Marsha Chechik and Jean-François Raskin, editors, Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9636 of Lecture Notes in Computer Science, pages 480–496. Springer, 2016.  doi:10.1007/978-3-662-49674-9\\_28.
  * [8] Michael Blondin, Christoph Haase, and Philip Offtermatt.  Directed reachability for infinite-state systems.  In Jan Friso Groote and Kim Guldstrand Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II, volume 12652 of Lecture Notes in Computer Science, pages 3–23. Springer, 2021\.  doi:10.1007/978-3-030-72013-1\\_1.
  * [9] Mikołaj Bojańczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc Segoufin.  Two-variable logic on data words.  ACM Trans. Comput. Log., 12(4):27:1–27:26, 2011.  doi:10.1145/1970398.1970403.
  * [10] Laura Bozzelli and Pierre Ganty.  Complexity analysis of the backward coverability algorithm for VASS.  In Giorgio Delzanno and Igor Potapov, editors, Reachability Problems - 5th International Workshop, RP 2011, Genoa, Italy, September 28-30, 2011. Proceedings, volume 6945 of Lecture Notes in Computer Science, pages 96–109. Springer, 2011.  doi:10.1007/978-3-642-24288-5\\_10.
  * [11] Jianer Chen, Benny Chor, Mike Fellows, Xiuzhen Huang, David W. Juedes, Iyad A. Kanj, and Ge Xia.  Tight lower bounds for certain parameterized NP-hard problems.  Inf. Comput., 201(2):216–231, 2005.  doi:10.1016/j.ic.2005.05.001.
  * [12] Jianer Chen, Xiuzhen Huang, Iyad A. Kanj, and Ge Xia.  Strong computational lower bounds via parameterized complexity.  J. Comput. Syst. Sci., 72(8):1346–1367, 2006.  doi:10.1016/j.jcss.2006.04.007.
  * [13] Hubert Comon and Yan Jurski.  Multiple counters automata, safety analysis and presburger arithmetic.  In Alan J. Hu and Moshe Y. Vardi, editors, Computer Aided Verification, 10th International Conference, CAV ’98, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings, volume 1427 of Lecture Notes in Computer Science, pages 268–279. Springer, 1998.  doi:10.1007/BFb0028751.
  * [14] Marek Cygan, Fedor V. Fomin, Łukasz Kowalik, Daniel Lokshtanov, Dániel Marx, Marcin Pilipczuk, Michał Pilipczuk, and Saket Saurabh.  Parameterized Algorithms.  Springer, 2015.  doi:10.1007/978-3-319-21275-3.
  * [15] Wojciech Czerwiński, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki.  Reachability in Fixed Dimension Vector Addition Systems with States.  In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), volume 171 of LIPIcs, pages 48:1–48:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020\.  doi:10.4230/LIPIcs.CONCUR.2020.48.
  * [16] Wojciech Czerwiński and Łukasz Orlikowski.  Reachability in Vector Addition Systems is Ackermann-complete.  In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 1229–1240. IEEE, 2021.  doi:10.1109/FOCS52979.2021.00120.
  * [17] Wojciech Czerwiński and Łukasz Orlikowski.  Lower Bounds for the Reachability Problem in Fixed Dimensional VASSes.  In Christel Baier and Dana Fisman, editors, LICS ’22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022, pages 40:1–40:12. ACM, 2022.  doi:10.1145/3531130.3533357.
  * [18] Mina Dalirrooyfard, Ce Jin, Virginia Vassilevska Williams, and Nicole Wein.  Approximation Algorithms and Hardness for n-Pairs Shortest Paths and All-Nodes Shortest Cycles.  In 63rd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2022, Denver, CO, USA, October 31 - November 3, 2022, pages 290–300. IEEE, 2022.  doi:10.1109/FOCS54457.2022.00034.
  * [19] Mina Dalirrooyfard, Thuy Duong Vuong, and Virginia Vassilevska Williams.  Graph pattern detection: Hardness for all induced patterns and faster noninduced cycles.  SIAM J. Comput., 50(5):1627–1662, 2021.  doi:10.1137/20M1335054.
  * [20] Javier Esparza.  Decidability and Complexity of Petri Net Problems - An Introduction.  In Wolfgang Reisig and Grzegorz Rozenberg, editors, Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, the volumes are based on the Advanced Course on Petri Nets, held in Dagstuhl, September 1996, volume 1491 of Lecture Notes in Computer Science, pages 374–428. Springer, 1996.  doi:10.1007/3-540-65306-6\\_20.
  * [21] Javier Esparza, Ruslán Ledesma-Garza, Rupak Majumdar, Philipp J. Meyer, and Filip Niksic.  An SMT-Based Approach to Coverability Analysis.  In Armin Biere and Roderick Bloem, editors, Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, volume 8559 of Lecture Notes in Computer Science, pages 603–619. Springer, 2014.  doi:10.1007/978-3-319-08867-9\\_40.
  * [22] John Fearnley and Marcin Jurdziński.  Reachability in Two-Clock Timed Automata Is PSPACE-Complete.  In Fedor V. Fomin, Rusins Freivalds, Marta Z. Kwiatkowska, and David Peleg, editors, Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II, volume 7966 of Lecture Notes in Computer Science, pages 212–223. Springer, 2013.  doi:10.1007/978-3-642-39212-2\\_21.
  * [23] Diego Figueira, Santiago Figueira, Sylvain Schmitz, and Philippe Schnoebelen.  Ackermannian and Primitive-Recursive Bounds with Dickson’s Lemma.  In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada, pages 269–278. IEEE Computer Society, 2011.  doi:10.1109/LICS.2011.39.
  * [24] Pierre Ganty and Rupak Majumdar.  Algorithmic verification of asynchronous programs.  ACM Trans. Program. Lang. Syst., 34(1):6:1–6:48, 2012.  doi:10.1145/2160910.2160915.
  * [25] Steven M. German and A. Prasad Sistla.  Reasoning about systems with many processes.  J. ACM, 39(3):675–735, 1992.  doi:10.1145/146637.146681.
  * [26] Christoph Haase, Stephan Kreutzer, Joël Ouaknine, and James Worrell.  Reachability in Succinct and Parametric One-Counter Automata.  In Mario Bravetti and Gianluigi Zavattaro, editors, CONCUR 2009 - Concurrency Theory, 20th International Conference, CONCUR 2009, Bologna, Italy, September 1-4, 2009. Proceedings, volume 5710 of Lecture Notes in Computer Science, pages 369–383. Springer, 2009.  doi:10.1007/978-3-642-04081-8\\_25.
  * [27] Christoph Haase, Joël Ouaknine, and James Worrell.  On the relationship between reachability problems in timed and counter automata.  In Alain Finkel, Jérôme Leroux, and Igor Potapov, editors, Reachability Problems - 6th International Workshop, RP 2012, Bordeaux, France, September 17-19, 2012. Proceedings, volume 7550 of Lecture Notes in Computer Science, pages 54–65. Springer, 2012.  doi:10.1007/978-3-642-33512-9\\_6.
  * [28] John E. Hopcroft and Jean-Jacques Pansiot.  On the Reachability Problem for 5-Dimensional Vector Addition Systems.  Theor. Comput. Sci., 8:135–159, 1979.  doi:10.1016/0304-3975(79)90041-0.
  * [29] Russell Impagliazzo and Ramamohan Paturi.  On the Complexity of k-SAT.  J. Comput. Syst. Sci., 62(2):367–375, 2001.  doi:10.1006/jcss.2000.1727.
  * [30] Ulla Koppenhagen and Ernst W. Mayr.  Optimal algorithms for the coverability, the subword, the containment, and the equivalence problems for commutative semigroups.  Inf. Comput., 158(2):98–124, 2000.  doi:10.1006/inco.1999.2812.
  * [31] Ranko Lazic and Sylvain Schmitz.  The ideal view on Rackoff’s coverability technique.  Inf. Comput., 277:104582, 2021.  doi:10.1016/j.ic.2020.104582.
  * [32] Jérôme Leroux.  Vector addition system reversible reachability problem.  Log. Methods Comput. Sci., 9(1), 2013.  doi:10.2168/LMCS-9(1:5)2013.
  * [33] Jérôme Leroux.  The Reachability Problem for Petri Nets is Not Primitive Recursive.  In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 1241–1252. IEEE, 2021.  doi:10.1109/FOCS52979.2021.00121.
  * [34] Jérôme Leroux and Sylvain Schmitz.  Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension.  In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1–13. IEEE, 2019.  doi:10.1109/LICS.2019.8785796.
  * [35] Andrea Lincoln, Virginia Vassilevska Williams, and R. Ryan Williams.  Tight hardness for shortest cycles and paths in sparse graphs.  In Artur Czumaj, editor, Proceedings of the Twenty-Ninth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2018, New Orleans, LA, USA, January 7-10, 2018, pages 1236–1252. SIAM, 2018.  doi:10.1137/1.9781611975031.80.
  * [36] Richard Lipton.  The Reachability Problem Requires Exponential Space.  Department of Computer Science. Yale University, 62, 1976.
  * [37] Daniel Lokshtanov, Dániel Marx, and Saket Saurabh.  Lower bounds based on the Exponential Time Hypothesis.  Bulletin of EATCS, 3(105), 2013.
  * [38] Ernst W. Mayr.  An Algorithm for the General Petri Net Reachability Problem.  SIAM J. Comput., 13(3):441–460, 1984.  doi:10.1137/0213029.
  * [39] Ernst W. Mayr and Albert R. Meyer.  The complexity of the word problems for commutative semigroups and polynomial ideals.  Advances in Mathematics, 46(3):305–329, 1982.  URL: https://www.sciencedirect.com/science/article/pii/0001870882900482, doi:https://doi.org/10.1016/0001-8708(82)90048-2.
  * [40] Filip Mazowiecki and Michał Pilipczuk.  Reachability for Bounded Branching VASS.  In Wan J. Fokkink and Rob van Glabbeek, editors, 30th International Conference on Concurrency Theory, CONCUR 2019, August 27-30, 2019, Amsterdam, the Netherlands, 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 Węgrzycki.  Coverability in 2-VASS with One Unary Counter is in NP.  In Orna Kupferman and Paweł Sobociński, editors, Foundations of Software Science and Computation Structures, pages 196–217. Springer Nature Switzerland, 2023.  doi:10.1007/978-3-031-30829-1_10.
  * [42] Marvin L. Minsky.  Computation: Finite and Infinite Machines.  Prentice-Hall, Inc., 1967.
  * [43] Jaroslav Nešetřil and Svatopluk Poljak.  On the complexity of the subgraph problem.  Commentationes Mathematicae Universitatis Carolinae, 26(2):415–419, 1985.
  * [44] Charles Rackoff.  The Covering and Boundedness Problems for Vector Addition Systems.  Theor. Comput. Sci., 6:223–231, 1978.  doi:10.1016/0304-3975(78)90036-1.
  * [45] 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.
  * [46] Sylvain Schmitz.  The Complexity of Reachability in Vector Addition Systems.  ACM SIGLOG News, 3(1):4–21, 2016.  URL: https://dl.acm.org/citation.cfm?id=2893585.
  * [47] 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.
  * [48] Wil M. P. van der Aalst.  Verification of Workflow Nets.  In Pierre Azéma and Gianfranco Balbo, editors, Application and Theory of Petri Nets 1997, 18th International Conference, ICATPN ’97, Toulouse, France, June 23-27, 1997, Proceedings, volume 1248 of Lecture Notes in Computer Science, pages 407–426. Springer, 1997.  doi:10.1007/3-540-63139-9\\_48.
  * [49] Raphael Yuster and Uri Zwick.  Detecting short directed cycles using rectangular matrix multiplication and dynamic programming.  In J. Ian Munro, editor, Proceedings of the Fifteenth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2004, New Orleans, Louisiana, USA, January 11-14, 2004, pages 254–260. SIAM, 2004.  URL: http://dl.acm.org/citation.cfm?id=982792.982828.
  * [50] Don Zagier.  Newman’s short proof of the prime number theorem.  The American mathematical monthly, 104(8):705–708, 1997.