Max Planck Institute for Software Systems (MPI-SWS), Germanyganardi@mpi-
sws.orghttps://orcid.org/0000-0002-0775-7781Max Planck Institute for Software
Systems (MPI-SWS), Germanyrupak@mpi-
sws.orghttps://orcid.org/0000-0003-2136-0542Aarhus University, Aabogade 34,
8200, Aarhus,
Denmarkpavlogiannis@cs.au.dkhttps://orcid.org/0000-0002-8943-0722Max Planck
Institute for Software Systems (MPI-SWS), Germanylschuetze@mpi-
sws.orghttps://orcid.org/0000-0003-4002-5491Max Planck Institute for Software
Systems (MPI-SWS), Germanygeorg@mpi-
sws.orghttps://orcid.org/0000-0002-6421-4388 <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 Moses Ganardi, Rupak
Majumdar, Andreas Pavlogiannis, Lia Schütze, Georg Zetzsche

# Reachability in Bidirected Pushdown VASS

Moses Ganardi  Rupak Majumdar  Andreas Pavlogiannis  Lia Schütze  Georg
Zetzsche

###### Abstract

A pushdown vector addition system with states (PVASS) extends the model of
vector addition systems with a pushdown store. A PVASS is said to be
_bidirected_ if every transition (pushing/popping a symbol or modifying a
counter) has an accompanying opposite transition that reverses the effect.
Bidirectedness arises naturally in many models; it can also be seen as a
overapproximation of reachability. We show that the reachability problem for
_bidirected_ PVASS is decidable in Ackermann time and primitive recursive for
any fixed dimension. For the special case of one-dimensional bidirected PVASS,
we show reachability is in $\mathsf{PSPACE}$, and in fact in polynomial time
if the stack is polynomially bounded. Our results are in contrast to the
_directed_ setting, where decidability of reachability is a long-standing open
problem already for one dimensional PVASS, and there is a
$\mathsf{PSPACE}$-lower bound already for one-dimensional PVASS with bounded
stack.

The reachability relation in the bidirected (stateless) case is a congruence
over $\mathbb{N}^{d}$. Our upper bounds exploit saturation techniques over
congruences. In particular, we show novel elementary-time constructions of
semilinear representations of congruences generated by finitely many vector
pairs. In the case of one-dimensional PVASS, we employ a saturation procedure
over bounded-size counters.

We complement our upper bound with a $\mathsf{TOWER}$-hardness result for
arbitrary dimension and $k$-$\mathsf{EXPSPACE}$ hardness in dimension $2k+6$
using a technique by Lazić and Totzke to implement iterative exponentiations.

###### keywords:

Vector addition systems, Pushdown, Reachability, Decidability, Complexity

##  1 Introduction

The reachability problem for infinite-state systems is one of the most basic
and well-studied tasks in verification. Given an infinite-state system and two
configurations $c_{1}$ and $c_{2}$ in the system, it asks: Is there a run from
$c_{1}$ to $c_{2}$? _Pushdown systems_ (PDS) and _vector addition systems with
states_ (VASS) are prominent models for which the reachability problem has
been studied extensively. Each of them features a finite set of control states
and a storage mechanism that holds an unbounded amount of information. In a
PDS, there is a stack where we can push and pop letters. In a VASS, there is a
set of counters which can be _incremented_ and _decremented_ , but not tested
for zero. Reachability in both models is understood in isolation [5, 11, 36,
12, 37], but the reachability problem for their _combination_ is a long-
standing open problem.

#### Pushdown VASS

A _pushdown VASS_ (PVASS) combines PDS and VASS. A PVASS consists of finitely
many control states and has access to both a pushdown stack (as in PDS) and
counters (as in VASS). A PVASS is _$d$ -dimensional_ if it has $d$ counters. A
PVASS is a natural combination of the simple building blocks of PDS and VASS.
The reachability problem for PVASS has remained a long-standing open problem
[38, 50, 15], even if we combine a pushdown with a single counter.

#### Bidirectedness

A step toward deciding reachability is to first study natural relaxations of
the reachability relation. A relaxation that has recently attracted attention
is _bidirectedness_. Bidirectedness assumes that for each transition from
state $p$ to $q$ in our infinite-state system, there exists a transition from
$q$ to $p$ with opposite effect. For example, in bidirected pushdown systems,
for each transition from $p$ to $q$ pushing $\gamma$ on the stack, there is a
transition from $q$ to $p$ that pops $\gamma$. Likewise, in bidirected VASS,
if there is a transition from $p$ to $q$ that adds some vector
$\bm{v}\in\mathbb{Z}^{d}$ to counters, then there is a transition from $q$ to
$p$ adding $-\bm{v}$. It turns out that several tasks in program analysis can
be formulated or practically approximated as reachability in bidirected
pushdown systems [8, 54] or bidirected multi-pushdown systems [51, 52, 55, 39,
40, 30]. Bidirected systems have also been considered in algorithmic group
theory as an algorithmic framework to provide simple algorithms for the
membership problem in subgroups [41].

Reachability in bidirected systems is usually considerably more efficient than
in the general case. In bidirected pushdown systems, reachability can be
solved in almost linear time [8] whereas a truly subcubic algorithm for the
general case is a long-standing open problem [25, 9]. Reachability in
bidirected VASS is equivalent to the uniform word problem in finitely
presented commutative semigroups, which is
${\small\mathsf{EXPSPACE}}$-complete [42]. A separate polynomial time
algorithm for bidirected two-dimensional VASS was given in [40]. Moreover,
recent results on reachability in bidirected valence systems shows complexity
drops across a large variety of infinite-state systems [20]: For almost every
class of systems studied in [20], the complexity of bidirected reachability is
lower than in the general case (the only exception being pushdown systems,
where the complexity is ${\small\mathsf{P}}$-complete in both settings). For
example, reachability in bidirected $\mathbb{Z}$-VASS, and even in bidirected
$\mathbb{Z}$-PVASS, is in ${\small\mathsf{P}}$ [20].

However, little is known about bidirected PVASS. They have recently been
studied in [30], where decidability of reachability in dimension one is shown.
However, as in the non-bidirected case, decidability of reachability in
bidirected PVASS is hitherto not known.

#### Contributions

We show that in bidirected PVASS (of arbitrary dimension), reachability is
decidable. Moreover, we provide an Ackermann complexity upper bound, and show
that in any fixed dimension, reachability is primitive recursive.

######  Theorem 1.1.

Reachability in bidirected pushdown VASS is in ${\small\mathsf{ACKERMANN}}$,
and primitive recursive (in ${\small\mathsf{F}}_{4d+11}$) if the dimension $d$
is fixed.

Here, $({\small\mathsf{F}}_{\alpha})_{\alpha}$ is an ordinal-indexed hierarchy
of fast-growing complexity classes [48], including
${\small\mathsf{F}}_{3}={\small\mathsf{TOWER}}$ and
${\small\mathsf{F}}_{\omega}={\small\mathsf{ACKERMANN}}$. The formal
definition of the hierarchy can be found in Section 4.3. A recurring theme in
our upper bounds is that saturation techniques, the standard method to analyze
pushdown systems, combine surprisingly well with counters in the bidirected
setting. Saturation is used in each of our upper bounds. In Section 3, we
begin the exposition with a short, self-contained proof that reachability is
decidable in bidirected PVASS. It shows that non-reachability is always
certified by an inductive invariant of a particular saturation procedure. In
Section 4, we show the Ackermann upper bound. Here, we saturate a congruence
relation that encodes the reachability relation. The upper bound relies on two
key ingredients. First, we use results about Gröbner bases of polynomial
ideals to show that in elementary time, one can construct a Presburger formula
for the congruence generated by finitely many vector pairs. This construction
serves as one step in the saturation. To show termination in Ackermannian
time, we rely on a technique from [16] to bound the length of strictly
ascending chains of upward closed sets of vectors. Here, the difficulty is to
transfer this bound from chains of upward closed sets to chains of
congruences.

In Section 5 we present a ${\small\mathsf{PSPACE}}$ algorithm for bidirected
PVASS in dimension one.

######  Theorem 1.2.

Reachability in 1-dimensional bidirected pushdown VASS is in
${\small\mathsf{PSPACE}}$.

Here, we rely on an observation from [30] that reachability in bidirected one-
dimensional PVASS reduces to (i) coverability in bidirected one-dimensional
PVASS and (ii) reachability in one-dimensional bidirected $\mathbb{Z}$-PVASS.
Since (ii) is known to be in ${\small\mathsf{P}}$ [20], we show that (i) can
be done in ${\small\mathsf{PSPACE}}$. For this, we use saturation to compute,
for each state pair $(p,q)$, three bounds on counter values that determine
whether coverability holds. We show that these bounds have at most exponential
absolute value, which yields a ${\small\mathsf{PSPACE}}$ procedure.

Finally in Section 6, we show that reachability in bidirected PVASS is
${\small\mathsf{TOWER}}$-hard. For this, we adapt a technique from [32] that
shows a ${\small\mathsf{TOWER}}$ lower bound for general PVASS.

######  Theorem 1.3.

Reachability in bidirected PVASS is ${\small\mathsf{TOWER}}$-hard, and
$k$-${\small\mathsf{EXPSPACE}}$-hard in dimension $2k+6$.

#### Related work

The model of pushdown VASS is surrounded by extensions and restrictions of the
storage mechanism for which decidability is understood, the most prominent
being the recent Ackermann-completeness for reachability in VASS [11, 36, 12,
37]. If instead of the stack, we have a counter with zero tests, then
reachability is still decidable [47, 4]. Here, decidability even holds if we
have a zero-testable counter and one additional counter that can be reset [18,
17]. Furthermore, the extension of VASS by _nested zero tests_ , where for
each $i\in\\{1,\ldots,d\\}$, we have an instruction that tests all counters
$1,\ldots,i$ for zero simultaneously, also allows deciding reachability [47,
3] and can be seen as a special case of pushdown VASS [1]. Another
decidability result concerns the _coverability problem_ : Here, we are given a
configuration $c_{1}$ and a control state $q$ and want to know whether from
$c_{1}$, one can reach some configuration in control state $q$. It is known
that the reachability problem for $d$-dimensional PVASS reduces to
coverability in $(d+1)$-dimensional PVASS, and that coverability in
$1$-dimensional PVASS is decidable [38]. According to [15], the latter problem
is ${\small\mathsf{PSPACE}}$-hard and in ${\small\mathsf{EXPSPACE}}$.
Furthermore, if the counters in a PVASS are allowed to go negative during a
run, then we speak of an _integer PVASS_ ($\mathbb{Z}$-PVASS). For these,
reachability is known to be decidable [24] and ${\small\mathsf{NP}}$-complete
[23]. However, if we extend the model of PVASS by allowing resets on the
counters, then even coverability is undecidable in dimension one [50].

For VASS, several generalizations of bidirectedness have been studied. It is
${\small\mathsf{EXPSPACE}}$-complete whether given two configurations are
mutually reachable [34]. Moreover, if two configurations are mutually
reachable, then their distance is at most doubly exponential (linear for fixed
dimension) in their size [35]. Furthermore, for cyclic VASS (where each
transition can be reversed by some execution), it is known that the
reachability set has a semilinear representation of at most exponential size
[6]. Let us note that in the VASS/Petri net literature, sometimes [6] (but not
entirely consistently [34]) the term _reversible_ is used to mean bidirected.
However, this clashes with the reversibility notion in dynamical systems [29].

##  2 Preliminaries

#### Vectors and semilinear sets

We denote integer vectors by bold letters $\bm{x}$. The maximum norm of
$\bm{x}$ is denoted by $\|\bm{x}\|$. The $i$-th unit vector is denoted by
$\bm{e}_{i}$. The componentwise order $\leq$ on $\mathbb{N}^{d}$ is a well-
quasi order (wqo), i.e. for any infinite sequence
$\bm{x}_{1},\bm{x}_{2},\dots$ over $\mathbb{N}^{d}$ there exist $i<j$ with
$\bm{x}_{i}\leq\bm{x}_{j}$. We write $\bm{x}<\bm{y}$ if $\bm{x}\leq\bm{y}$ and
$\bm{x}\neq\bm{y}$. This implies that the set $\min(X)$ of minimal elements in
any $X\subseteq\mathbb{N}^{d}$ is finite. We denote by
$X{\uparrow}=\\{\bm{y}\in\mathbb{N}^{k}\mid\exists\bm{x}\in
X\colon\bm{x}\leq\bm{y}\\}$ the upwards closure of $X$. We also write
$\bm{x}{\uparrow}$ for $\\{\bm{x}\\}{\uparrow}$. A congruence on a commutative
monoid $(M,+)$, for example $M=\mathbb{N}^{d}$, is an equivalence relation
$\mathcal{Q}\subseteq M\times M$ where $(a,b)\in\mathcal{Q}$ implies
$(a+c,b+c)\in\mathcal{Q}$ for all $a,b,c\in M$. We also write
$a\sim_{\mathcal{Q}}b$ instead of $(a,b)\in\mathcal{Q}$.

For $X\subseteq\mathbb{N}^{k}$ we denote by $X^{*}$ the submonoid generated by
$X$. A set $L\subseteq\mathbb{N}^{k}$ is linear if it is of the form
$L=\bm{b}+P^{*}$ for some base vector $\bm{b}\in\mathbb{N}^{k}$ and some
finite set $P\subseteq\mathbb{N}^{k}$ of period vectors. Finite unions of
linear sets are called semilinear. It is well-known that a set is semilinear
if and only if it is definable in Presburger arithmetic, i.e. first-order
logic over $(\mathbb{N},+,\leq,0,1)$. Furthermore, one can effectively convert
between these formats in elementary time: While defining semilinear sets in
Presburger arithmetic is straightforward, for the converse we can use Cooper’s
quantifier elimination [10] running in triply exponential time [43], see also
[22] for an excellent overview. We will confuse a semilinear $S$ with its
representation, which is either a list of base and period vectors for each
linear set or a defining Presburger formula, and denote by $\|S\|$ the size of
its representation.

#### Pushdown VASS

A $d$-dimensional pushdown VASS (PVASS) is a tuple $\mathcal{P}=(Q,\Gamma,T)$
where $Q$ is a finite set of states, $\Gamma$ is a finite stack alphabet, and
$T\subseteq Q\times\mathbb{Z}^{d}\times\mathsf{Op}(\Gamma)\times Q$ is a
finite set of transitions. Here $\mathsf{Op}(\Gamma)=\\{a,\bar{a}\mid
a\in\Gamma\\}\cup\\{\varepsilon\\}$ is the set of operations on the stack. A
configuration over $\mathcal{P}$ is a tuple $(q,\bm{x},s)\in
Q\times\mathbb{N}^{d}\times\Gamma^{*}$. The one-step relation $\to$ is the
smallest binary relation on configurations such that for all
$(p,\bm{v},\alpha,q)\in T$ and $\bm{x}\in\mathbb{N}^{d}$ with
$\bm{x}+\bm{v}\geq\bm{0}$ we have: (i) If
$\alpha\in\Gamma\cup\\{\varepsilon\\}$ then
$(p,\bm{x},s)\to(q,\bm{x}+\bm{v},s\alpha)$ (ii) if $\alpha=\bar{a}$ then
$(p,\bm{x},sa)\to(q,\bm{x}+\bm{v},s)$. Its transitive-reflexive closure is
denoted by $\xrightarrow{*}$. We say that $\mathcal{P}$ is bidirected if
$(p,\bm{v},\alpha,q)\in T$ implies $(q,-\bm{v},\bar{\alpha},p)\in T$ where we
set $\bar{\bar{a}}=a$ for $a\in\Gamma$ and $\bar{\varepsilon}=\varepsilon$.
The reachability problem for bidirected PVASS asks: Given a bidirected PVASS
$\mathcal{P}$ and two states $s,t$, does
$(s,\bm{0},\varepsilon)\xrightarrow{*}(t,\bm{0},\varepsilon)$ hold?

The counter updates $\bm{u}$ in a PVASS transition $(p,\bm{u},q)$ can be given
in either unary or binary encoding since there are logspace translations in
both directions: To add a binary encoded number $u$ to a counter we push the
binary notation of $u$ to the stack, and repeatedly decrement the stack
counter while incrementing $u$. Since this computation is deterministic, the
simulation also works for bidirected PVASS.

For the Ackermann upper bound it is convenient to use pushdown VASS with a
single state. A pushdown VAS (PVAS) $\mathcal{P}=(\Gamma,T)$ in dimension $d$
consists of a finite stack alphabet $\Gamma$ and a finite set of transitions
$T\subseteq\mathbb{N}^{d}\times\mathbb{N}^{d}\times(\Gamma\cup\bar{\Gamma}\cup\\{\varepsilon\\})$.
Here, a configuration is a pair $(\bm{x},s)\in\mathbb{N}^{d}\times\Gamma^{*}$.
The effect of a transition $(\bm{u},\bm{v},\alpha)$ is subtracting $\bm{u}$
from the $d$ counters, assuming that the counters stay non-negative, and then
adding $\bm{v}$. A PVAS $\mathcal{P}$ is bidirected if $(\bm{u},\bm{v},a)\in
T$ implies $(\bm{v},\bm{u},\bar{a})\in T$. A bidirected PVASS in dimension $d$
can be simulated by a bidirected PVAS in dimension $d+2$ where the two
additional counters add up to the number of states and specify the current
state. Hence, one can reduce the reachability problem for bidirected PVASS to
the reachability problem for bidirected PVAS: Given a bidirected PVAS
$\mathcal{P}$ and two vectors $\bm{s},\bm{t}\in\mathbb{N}^{d}$, does
$(\bm{s},\varepsilon)\xrightarrow{*}(\bm{t},\varepsilon)$ hold?

##  3 Decidability

In this section, we present a simple and self-contained proof that
reachability is decidable in bidirected PVASS. Consider the reachability
relation between configurations with empty stack. For any states $p,q$, define
the set $R_{p,q}\subseteq\mathbb{N}^{d}\times\mathbb{N}^{d}$ with

$R_{p,q}=\\{(\bm{u},\bm{v})\mid\bm{u},\bm{v}\in\mathbb{N}^{d},\leavevmode\nobreak\
(p,\bm{u},\varepsilon)\xrightarrow{*}(q,\bm{v},\varepsilon)\\}.$

We will prove that each $R_{p,q}$ is semilinear, for which we rely on the fact
that these sets are slices. A _slice_ is a subset $S\subseteq\mathbb{N}^{k}$
such that if $\bm{u},\bm{u}+\bm{v},\bm{u}+\bm{w}\in S$ for some
$\bm{u},\bm{v},\bm{w}\in\mathbb{N}^{k}$, then $\bm{u}+\bm{v}+\bm{w}\in S$.
Observe that each $R_{p,q}\subseteq\mathbb{N}^{2d}$ is a slice. This is
because if
$(\bm{u},\bm{v}),(\bm{u}+\bm{u}_{1},\bm{v}+\bm{v}_{1}),(\bm{u}+\bm{u}_{2},\bm{v}+\bm{v}_{2})\in
R_{p,q}$, then there is a run

$(p,\bm{u}+\bm{u}_{1}+\bm{u}_{2},\varepsilon)\xrightarrow{*}(q,\bm{v}+\bm{v}_{1}+\bm{u}_{2},\varepsilon)\xrightarrow{*}(p,\bm{u}+\bm{v}_{1}+\bm{u}_{2},\varepsilon)\xrightarrow{*}(q,\bm{v}+\bm{v}_{1}+\bm{v}_{2},\varepsilon),$

where the middle part exists due to bidirectedness. Thus, the pair
$(\bm{u}+\bm{u}_{1}+\bm{u}_{2},\bm{v}+\bm{v}_{1}+\bm{v}_{2})$ belongs to
$R_{p,q}$. The following was first shown in [14, Proposition 7.3].

######  Theorem 3.1 (Eilenberg & Schützenberger 1969).

Every slice is semilinear.

This seems to be stronger than the somewhat better-known fact that each
congruence on $\mathbb{N}^{d}$ is semilinear: Observe that every congruence on
$\mathbb{N}^{d}$, seen as a subset of $\mathbb{N}^{2d}$, is a slice. In the
case of congruences, a relatively simple proof was obtained by Hirshfeld [26].
We present a proof of Theorem 3.1 that combines ideas from both [14] and [26]
and is (in our opinion) simpler than each.

For a set $X\subseteq\mathbb{N}^{k}$, let $\min X$ be the set of minimal
elements of $X$, with respect to the usual component-wise ordering $\leq$ on
$\mathbb{N}^{k}$. Since this ordering is a well-quasi ordering, $\min X$ is
finite for every set $X$. Suppose $S\subseteq\mathbb{N}^{k}$ is a slice. For
each $\bm{u}\in S$, let
$S-\bm{u}:=\\{\bm{v}\in\mathbb{N}^{k}\mid\bm{u}+\bm{v}\in S\\}$. Then
$\bm{u}\leq\bm{v}$ implies $S-\bm{u}\subseteq S-\bm{v}$. Consider for each
$\bm{u}\in S$ the submonoid

$M_{\bm{u}}=(\min(S-\bm{u}\setminus\\{\bm{0}\\}))^{*}.$

In other words, $M_{\bm{u}}$ is the submonoid of $\mathbb{N}^{k}$ generated by
the non-zero minimal elements of $S-\bm{u}$. Note that for $\bm{u},\bm{v}\in
S$, we have $M_{\bm{u}}=M_{\bm{v}}$ if and only if
$(S-\bm{u}\setminus\\{\bm{0}\\})\mathop{\uparrow}=(S-\bm{v}\setminus\\{\bm{0}\\})\mathop{\uparrow}$.
Since $S$ is a slice, we have $\bm{u}+M_{\bm{u}}\subseteq S$ for every
$\bm{u}\in S$. Since $\bm{u}\in\bm{u}+M_{\bm{u}}$, we trivially have

$S=\bigcup_{\bm{u}\in S}\bm{u}+M_{\bm{u}}.$

Since each $\bm{u}+M_{\bm{u}}$ is semilinear, it suffices to show that $S$ is
covered by finitely many sets $\bm{u}+M_{\bm{u}}$. We first observe that if
$\bm{u}\leq\bm{v}$ and $M_{\bm{u}}=M_{\bm{v}}$, then $\bm{u}+M_{\bm{u}}$
already covers $\bm{v}+M_{\bm{v}}$.

######  Lemma 3.2.

Let $\bm{u},\bm{v}\in S$. If $\bm{u}\leq\bm{v}$ and $M_{\bm{u}}=M_{\bm{v}}$,
then $\bm{v}+M_{\bm{v}}\subseteq\bm{u}+M_{\bm{u}}$.

######  Proof 3.3.

We will use the following claim: For every $\bm{w}\in S$ with
$\bm{u}\leq\bm{w}\leq\bm{v}$, we have $M_{\bm{u}}=M_{\bm{w}}=M_{\bm{v}}$.
Indeed, since $M_{\bm{u}}=M_{\bm{v}}$, we have
$\min(S-\bm{u}\setminus\\{\bm{0}\\})=\min(S-\bm{v}\setminus\\{\bm{0}\\})$.
Moreover, since $S$ is a slice, we have $S-\bm{u}\subseteq S-\bm{w}\subseteq
S-\bm{v}$. Therefore, $\min(S-\bm{w}\setminus\\{\bm{0}\\})$ coincides with
$\min(S-\bm{u}\setminus\\{\bm{0}\\})$ and
$\min(S-\bm{v}\setminus\\{\bm{0}\\})$, which implies
$M_{\bm{w}}=M_{\bm{u}}=M_{\bm{v}}$.

Let us prove the lemma. We proceed by induction on $\|\bm{v}-\bm{u}\|$. If
$\bm{u}=\bm{v}$, then we are done. Otherwise, there exists an
$\bm{m}\in\min(S-\bm{u}\setminus\\{\bm{0}\\})$ such that
$\bm{u}+\bm{m}\leq\bm{v}$. By our claim, we have
$M_{\bm{u}}=M_{\bm{u}+\bm{m}}=M_{\bm{v}}$. Therefore, induction implies
$\bm{v}\in\bm{u}+\bm{m}+M_{\bm{u}+\bm{m}}$. But since $\bm{m}\in M_{\bm{u}}$
and $M_{\bm{u}+\bm{m}}\subseteq M_{\bm{u}}$, this implies
$\bm{v}\in\bm{u}+M_{\bm{u}}$.

The following implies semilinearity of $S$.

######  Lemma 3.4.

There is a finite set $F\subseteq S$ such that $S=\bigcup_{\bm{u}\in
F}\bm{u}+M_{\bm{u}}$.

######  Proof 3.5.

Suppose not. Then there is an infinite sequence
$\bm{u}_{1},\bm{u}_{2},\ldots\in S$ such that each set
$\bm{u}_{i}+M_{\bm{u}_{i}}$ contributes a new element. By Dickson’s lemma
$\bm{u}_{1},\bm{u}_{2},\ldots$ contains a subsequence
$\bm{v}_{1},\bm{v}_{2},\ldots$ with $\bm{v}_{i}\leq\bm{v}_{i+1}$ for all
$i\geq 1$. Since then $S-\bm{v}_{1}\subseteq S-\bm{v}_{2}\subseteq\cdots$, the
sequence
$(S-\bm{v}_{1}\setminus\\{\bm{0}\\})\mathop{\uparrow}\subseteq(S-\bm{v}_{2}\setminus\\{\bm{0}\\})\mathop{\uparrow}\subseteq\cdots$
becomes stationary, again by Dickson’s lemma, and therefore also the sequence
$M_{\bm{v}_{1}},M_{\bm{v}_{2}},\ldots$. By Lemma 3.2, this means that only
finitely many terms in the sequence
$\bm{v}_{1}+M_{\bm{v}_{1}},\bm{v}_{2}+M_{\bm{v}_{2}},\ldots$ contribute new
elements, a contradiction.

#### Saturation invariants

We have seen that the reachability relations $R_{p,q}$ are all semilinear.
However, since the semilinearity proof is non-constructive, this does not
explain how to decide reachability. Nevertheless, we shall use semilinearity
to show that in case of non-reachability, there exists a certificate. This
yields a decision procedure consisting of two semi-algorithms in the style of
Leroux’s algorithm for reachability in VASS [33]: One semi-algorithm
enumerates potential runs, and one enumerates potential certificates for non-
reachability.

We assume that we are given a bidirected $d$-dimensional PVASS with state set
$Q$ and stack alphabet $\Gamma$. We may assume that all transitions are of the
form $p\xrightarrow{\gamma}q$ or $p\xrightarrow{\bar{\gamma}}q$ for
$\gamma\in\Gamma$ or $p\xrightarrow{\bm{v}}q$ for $\bm{v}\in\mathbb{Z}^{d}$.
Our certificates for non-reachability will be in the form of what we call
saturation invariants. Imagine a (non-terminating) naive saturation algorithm
that attempts to compute the sets $R_{p,q}$ by adding vector pairs one-by-one
to finite sets $F_{p,q}$. It would start with $F_{p,q}=\emptyset$ and then add
pairs: For each transition $p\xrightarrow{\bm{v}}q$ and each vector
$\bm{u}\in\mathbb{N}^{d}$ with $\bm{u}+\bm{v}\in\mathbb{N}^{d}$, it would add
the pair $(\bm{u},\bm{u}+\bm{v})$ to $F_{p,q}$. Moreover, if
$(\bm{u},\bm{v})\in F_{p,q}$ and $(\bm{v},\bm{w})\in F_{q,r}$, it would add
$(\bm{u},\bm{w})$ to $F_{p,r}$. Finally, if there are transitions
$p\xrightarrow{\gamma}p^{\prime}$ and $q^{\prime}\xrightarrow{\bar{\gamma}}q$
and there is a $(\bm{u},\bm{v})\in F_{p^{\prime},q^{\prime}}$, then it would
add $(\bm{u},\bm{v})$ to $F_{p,q}$.

Intuitively, a saturation invariant is a forward inductive invariant of this
naive saturation algorithm. Let us make this precise. For subsets
$R_{1},R_{2}\subseteq\mathbb{N}^{d}\times\mathbb{N}^{d}$, we define

$R_{1}\circ
R_{2}=\\{(\bm{u},\bm{w})\in\mathbb{N}^{d}\times\mathbb{N}^{d}\mid\exists\bm{v}\in\mathbb{N}^{d}\colon(\bm{u},\bm{v})\in
R_{1},\leavevmode\nobreak\ (\bm{v},\bm{w})\in R_{2}\\}.$

A _saturation invariant_ consists of a family $(I_{p,q})_{(p,q)\in Q^{2}}$ of
sets $I_{p,q}\subseteq\mathbb{N}^{d}\times\mathbb{N}^{d}$ for which

  1. 1.

For each transition $p\xrightarrow{\bm{v}}q$, $\bm{v}\in\mathbb{Z}^{d}$, each
$\bm{u}\in\mathbb{N}^{d}$ with $\bm{u}+\bm{v}\in\mathbb{N}^{d}$, we have
$(\bm{u},\bm{u}+\bm{v})\in I_{p,q}$.

  2. 2.

For each $p,q,r\in Q$, we have $I_{p,q}\circ I_{q,r}\subseteq I_{p,r}$.

  3. 3.

For each $p,p^{\prime},q,q^{\prime}\in Q$ for which there are transitions
$p\xrightarrow{\gamma}p^{\prime}$, $q^{\prime}\xrightarrow{\bar{\gamma}}q$ for
some $\gamma\in\Gamma$, we have $I_{p^{\prime},q^{\prime}}\subseteq I_{p,q}$.

There is a natural ordering of such families $(I_{p,q})_{(p,q)\in Q^{2}}$
defined by inclusion: We write $(I_{p,q})_{(p,q)\in
Q^{2}}\leq(J_{p,q})_{(p,q)\in Q^{2}}$, if $I_{p,q}\subseteq J_{p,q}$ for each
$p,q\in Q$. In this sense, we can speak of a smallest saturation invariant.

######  Lemma 3.6.

The family $(R_{p,q})_{(p,q)\in Q^{2}}$ is the smallest saturation invariant.

######  Proof 3.7.

By induction on the length of a run, it follows that $(R_{p,q})_{(p,q)\in
Q^{2}}$ is included in every saturation invariant. Moreover,
$(R_{p,q})_{(p,q)\in Q^{2}}$ is clearly a saturation invariant itself.

Our certificates will consist of saturation invariants defined in Presburger
arithmetic. A family $(I_{p,q})_{(p,q)\in Q^{2}}$ is _Presburger-definable_ if
for each $(p,q)\in Q^{2}$, the set $I_{p,q}$ is semilinear. According to
Theorem 3.1, the family $(R_{p,q})_{(p,q)\in Q^{2}}$ is Presburger-definable.
Therefore, the following is a direct consequence of Lemma 3.6.

######  Theorem 3.8.

For each $s,t\in Q$, we have $(\bm{0},\bm{0})\notin R_{s,t}$ if and only if
there exists a Presburger-definable saturation invariant $(I_{p,q})_{(p,q)\in
Q^{2}}$ such that $(\bm{0},\bm{0})\notin I_{s,t}$.

This yields our algorithm: One semi-algorithm enumerates transition sequences
and terminates if one of them is a run witnessing
$(s,\bm{0},\varepsilon)\xrightarrow{*}(t,\bm{0},\varepsilon)$. The other semi-
algorithm enumerates Presburger-definable families $(I_{p,q})_{(p,q)\in
Q^{2}}$ in the form of Presburger formulas. Using Presburger arithmetic, it is
then easy to check whether (i) $(I_{p,q})_{(p,q)\in Q^{2}}$ is a saturation
invariant and (ii) $(\bm{0},\bm{0})\notin I_{s,t}$. If a saturation invariant
is found, the semi-algorithm reports non-reachability. By Theorem 3.8, one of
the two semi-algorithms must terminate.

##  4 Ackermann upper bound

In this section, we show that reachability in bidirected PVASS is solvable in
Ackermann time in the general case and in primitive recursive complexity in
every fixed dimension.

One way to avoid enumeration in the algorithm of Section 3 would be to start
with the semilinear one-step relation described in the first condition of
saturation invariants, and then to enlarge it according to the second and
third condition. Moreover, one could take the slice closure (the smallest
slice that includes the current set) after each enlargement. Since slices
satisfy an ascending chain condition [14, Corollary 12.3], this would ensure
termination. In fact, computing the slice closure of a semilinear set is
possible with an algorithm by Grabowski [21]. Unfortunately, the latter is
itself based on enumeration and we are not aware of any complexity bounds for
computing slice closures. Therefore, we use an analogous algorithm that uses
congruences instead of slices. Since congruences can be encoded in polynomial
ideals, we can tap into the rich toolbox of Gröbner bases to compute the
congruence generated by a semilinear set.

###  4.1 The saturation algorithm

In the following we will work with pushdown VAS instead of pushdown VASS. Our
decision procedure for bidirected reachability relies on the crucial fact that
the reachability relation
$R_{\mathcal{P}}=\\{(\bm{s},\bm{t})\in\mathbb{N}^{d}\times\mathbb{N}^{d}\mid(\bm{s},\varepsilon)\xrightarrow{*}(\bm{t},\varepsilon)\\}$
of a bidirected pushdown VAS $\mathcal{P}$ is a congruence: It is always
reflexive, transitive and additive, even for directed pushdown VAS, and
symmetric for bidirected systems. Therefore, whenever we have found an
underapproximation $R\subseteq R_{\mathcal{P}}$ we can replace $R$ by the
smallest congruence containing $R$. The smallest congruence containing a set
$R\subseteq\mathbb{N}^{d}\times\mathbb{N}^{d}$ is denoted by
$\mathsf{Cong}(R)$. We also say that $R$ is a basis of (or generates)
$\mathsf{Cong}(R)$. Recall that every congruence on $\mathbb{N}^{d}$ is a
slice. Therefore, congruences are semilinear and ascending chains of
congruences stabilize.

Data: Bidirected $d$-dim. PVAS $\mathcal{P}=(\Gamma,T)$

1 $R_{0}:=\mathsf{Cong}(\\{(\bm{u},\bm{v})\mid(\bm{u},\bm{v},\varepsilon)\in
T\\})$;

2 for  _$i=1,2,\dots$_ do

3 $R_{i}\leftarrow R_{i-1}$;

4 for  _$(\bm{u},\bm{u}^{\prime},a)\in T$ and
$(\bm{v}^{\prime},\bm{v},\bar{a})\in T$_ do

5 $R_{i}\leftarrow
R_{i}\cup\\{(\bm{x}+\bm{u},\bm{y}+\bm{v})\mid(\bm{x}+\bm{u}^{\prime},\bm{y}+\bm{v}^{\prime})\in
R_{i-1},\,\bm{x},\bm{y}\in\mathbb{N}^{d}\\}$;

6

7 $R_{i}\leftarrow\mathsf{Cong}(R_{i})$;

8 if  _$R_{i}=R_{i-1}$_ then return _$R_{i}$_ ;

9

Algorithm 1 Algorithm for bidirected reachability in PVAS.

Algorithm 1 is a saturation algorithm that computes a semilinear
representation for $R_{\mathcal{P}}$. The sets $R_{i}$ are maintained by
semilinear representations or Presburger formulas. Since in this section we
only prove elementary complexity bounds, we can use both formats
interchangeably. Observe that the update in line 1 and the equality test in
line 1 can be expressed in Presburger arithmetic. The computation of
$\mathsf{Cong}(\cdot)$ will be explained in the next subsection. Consider the
values of $R_{i}$ for $i\geq 1$ after line 1 of Algorithm 1. They form an
ascending chain of congruences $(R_{i})_{i\geq 1}$, which implies that the
algorithm must terminate. For the correctness one can prove by induction on
$i$ that $(\bm{x},\bm{y})\in R_{i}$ if and only if there exists a run between
$(\bm{x},\varepsilon)$ and $(\bm{y},\varepsilon)$ whose stack height does not
exceed $i$. Moreover, if the algorithm terminates after $k$ iterations then
$R_{k}=R_{\mathcal{P}}$.

We will use a primitive recursive algorithm (which is elementary in fixed
dimension) to compute $\mathsf{Cong}(R_{i})$ from a semilinear representation
for $R_{i}$. Using the tools from [49] we can then prove upper bounds for the
length of the ascending chain.

###  4.2 Semilinear representations for congruences

In this section, we present an algorithm that, for a given semilinear
representation for a set $R\subseteq\mathbb{N}^{d}\times\mathbb{N}^{d}$,
computes a semilinear representation for $\mathsf{Cong}(R)$. Its run time is
bounded by a tower of exponentials in $\|R\|$ of height $O(d)$ (Theorem 4.4).
Note that for bidirected VASS, it is known that in exponential space, one can
compute a semilinear representation of the reachability set [31, 6]. In other
words, one can compute in exponential space a representation of the congruence
class of a given vector $\bm{x}\in\mathbb{N}^{d}$. In contrast, our algorithm
computes a semilinear representation of the entire congruence.

Let the function $\exp^{k}$ be inductively defined by $\exp^{0}(x)=x$ and
$\exp^{k+1}(x)=\exp^{k}(2^{x})$. In the following we show how to compute a
semilinear representation for a congruence $\mathcal{Q}$ given by a semilinear
basis $R\subseteq\mathbb{N}^{d}\times\mathbb{N}^{d}$ in time
$\exp^{O(d)}(\|R\|)$. In fact, we can assume that $R$ is finite since a linear
set $L=\bm{b}+P^{*}$ is contained in $\mathsf{Cong}(F_{L})$ where
$F_{L}=\\{\bm{b},\bm{b}+\bm{p}\mid\bm{p}\in P\\}$, and, therefore, a
semilinear set $\bigcup_{i=1}^{m}L_{i}$ generates the same congruence as
$\bigcup_{i=1}^{m}F_{L_{i}}$. The semilinear representation of $\mathcal{Q}$
will be obtained by induction on the dimension $d$ via a decomposition of
$\mathbb{N}^{d}$ into smaller regions. A region is a linear set
$L=\bm{b}+P^{*}\subseteq\mathbb{N}^{d}$ where
$P\subseteq\\{\bm{e}_{1},\dots,\bm{e}_{d}\\}$. Its dimension is $|P|$. In
particular all sets
$\bm{b}{\uparrow}=\bm{b}+\\{\bm{e}_{1},\dots,\bm{e}_{d}\\}^{*}$ are regions.
For a region $L=\bm{b}+P^{*}$ and a congruence $\mathcal{Q}$, we define the
congruence
$\mathcal{Q}_{L}=\\{(\bm{x},\bm{y})\in(P^{*})^{2}\mid(\bm{b}+\bm{x},\bm{b}+\bm{y})\in\mathcal{Q}\\}$
on the submonoid $P^{*}$.

A submonoid $S\subseteq\mathbb{N}^{k}$ is subtractive if $\bm{x},\bm{y}\in S$
and $\bm{x}\leq\bm{y}$ implies $\bm{y}-\bm{x}\in S$. For example, the non-
negative restriction $G\cap\mathbb{N}^{k}$ of a group
$G\subseteq\mathbb{Z}^{k}$ is a subtractive submonoid. The following lemma is
well-known, see [14, Proposition 7.1] or Appendix A for a proof.

######  Lemma 4.1.

Every subtractive submonoid $S\subseteq\mathbb{N}^{k}$ is of the form
$S=M^{*}$ where $M$ is the finite set of the minimal nonzero elements in $S$.

Eilenberg and Schützenberger observed that for every slice $S$ there exists an
element $\bm{s}\in S$ such that $S-\bm{s}$ is a subtractive submonoid [14,
Proposition 7.2]. As a consequence, for every congruence $\mathcal{Q}$ on
$\mathbb{N}^{d}$ there exists $\bm{b}\in\mathbb{N}^{d}$ such that
$\mathcal{Q}_{\bm{b}{\uparrow}}$ is a subtractive submonoid. We provide an
elementary bound on $\bm{b}$.

######  Lemma 4.2.

Given a finite basis $R$ for a congruence $\mathcal{Q}$ on $\mathbb{N}^{d}$,
one can compute in elementary time a vector $\bm{b}\in\mathbb{N}^{d}$ and a
finite set $M\subseteq\mathbb{N}^{2d}$ such that
$\mathcal{Q}_{\bm{b}{\uparrow}}=M^{*}$.

#### Gröbner bases

It remains to compute a semilinear representation of $\mathcal{Q}$ on the
complement of ${\bm{b}{\uparrow}}$. We will decompose
$\mathbb{N}^{d}\setminus{\bm{b}{\uparrow}}$ into disjoint $(d-1)$-dimensional
regions $L_{j}$, compute bases for the restrictions $\mathcal{Q}_{L_{j}}$, and
proceed inductively. To compute the bases for $\mathcal{Q}_{L_{j}}$, we will
exploit the well-studied connection between congruences on $\mathbb{N}^{d}$
and binomial ideals [42]. Let $\mathbb{Z}[\bm{x}]$ be the polynomial ring in
the variables $\bm{x}=(x_{1},\dots,x_{d})$ over $\mathbb{Z}$. We write
$\bm{x}^{\bm{u}}$ for the monomial $x_{1}^{\bm{u}(1)}\cdots
x_{d}^{\bm{u}(d)}$. An ideal is a nonempty set $I\subseteq\mathbb{Z}[\bm{x}]$
such that $f,g\in I$ and $h\in\mathbb{Z}[\bm{x}]$ implies $f+g,hf\in I$. An
ideal $I$ is finitely represented by a basis $B$, i.e. $I$ is the smallest
ideal containing $B$. By Hilbert’s basis theorem any ideal
$I\subseteq\mathbb{Z}[\bm{x}]$ has a finite basis. One of the main tools in
computer algebra for handling polynomial ideals are Gröbner bases, e.g. to
solve the ideal membership problem. We defer the reader to [2] for details on
Gröbner bases and only mention the properties required for our purposes. A
Gröbner basis is defined with respect to an admissible monomial ordering, e.g.
a lexicographic ordering on the monomials. Buchberger’s algorithm [7] computes
for a given basis for an ideal $I$ the unique reduced Gröbner basis for $I$ in
doubly exponential space [13].

A basis $R$ for a congruence $\mathcal{Q}$ on $\mathbb{N}^{d}$ can be
translated into the polynomial ideal $I\subseteq\mathbb{Z}[\bm{x}]$ generated
by $B_{R}=\\{\bm{x}^{\bm{u}}-\bm{x}^{\bm{v}}\mid(\bm{u},\bm{v})\in R\\}$. It
is known that $\bm{s}\sim_{\mathcal{Q}}\bm{t}$ if and only if
$\bm{x}^{\bm{s}}-\bm{x}^{\bm{t}}\in I$ [42, Lemma 1 and 2]. Moreover, the
reduced Gröbner basis of $I$ with respect to an admissible monomial order
always consists of differences of monomials $\bm{x}^{\bm{s}}-\bm{x}^{\bm{t}}$
[28, Theorem 2.7].

The following lemma can be reduced to two known applications of Gröbner bases.
Let $I\subseteq\mathbb{Z}[\bm{x}]$ be an ideal. For a subsequence $\bm{y}$ of
$\bm{x}$ we call $I\cap\mathbb{Z}[\bm{y}]$ the elimination ideal, which is
indeed an ideal in $\mathbb{Z}[\bm{y}]$. For $\bm{b}\in\mathbb{N}^{d}$ we
define the ideal quotient $I:\bm{x}^{\bm{b}}=\\{p\in\mathbb{Z}[\bm{x}]\mid
p\bm{x}^{\bm{b}}\in I\\}$, which is also an ideal. It is known that one can
compute Gröbner bases for $I\cap\mathbb{Z}[\bm{y}]$ and $I:\bm{x}^{\bm{b}}$ in
elementary time [2, Section 6], see Appendix A for more details.

######  Lemma 4.3.

Given a finite basis $R$ for a congruence $\mathcal{Q}$ on $\mathbb{N}^{d}$
and a region $L\subseteq\mathbb{N}^{d}$, one can compute in elementary time a
finite basis for $\mathcal{Q}_{L}$.

We are ready to compute a semilinear representation of $\mathsf{Cong}(R)$ in
$\exp^{O(d)}(n)$ time. We proceed by induction over $d$. Using Lemma 4.2 we
can write $\mathcal{Q}_{\bm{b}{\uparrow}}=M^{*}$. We decompose
$\mathbb{N}^{d}=\bigcup_{i=0}^{m}L_{j}$ into regions where
$L_{0}=\bm{b}{\uparrow}$ and $L_{1},\dots,L_{m}$ are $(d-1)$-dimensional
regions. By Lemma 4.3 we can compute bases for $\mathcal{Q}_{L_{i}}$ for
$i\in[1,m]$ and by induction hypothesis semilinear representations for
$\mathcal{Q}_{L_{i}}$. In this way, we obtain semilinear representations for
the restrictions $Q_{i}=\mathcal{Q}\cap L_{i}^{2}$ for each $i\in[0,m]$.
Finally, we can express $\bm{s}\sim_{\mathcal{Q}}\bm{t}$ by a Presburger
formula that says that there exists a sequence of intermediate vectors of
length $2(m+1)$ where adjacent elements are related by an $R$-step or are
contained in some relation $Q_{i}$.

######  Theorem 4.4.

Given a semilinear basis $R$ for a congruence $\mathcal{Q}$ on
$\mathbb{N}^{d}$, one can compute a semilinear representation for
$\mathcal{Q}$ in time $\exp^{c_{1}d}(n)$ for some absolute constant $c_{1}$.

###  4.3 Ascending chains of congruences

To bound the length of the chain of congruences $R_{i}$ in Algorithm 1 we use
a length function theorem [49, Theorem 3.15], see also [16]. In general, such
theorems allow to derive complexity bounds for algorithms whose termination
arguments are based on well-quasi orders.

#### Fast-growing complexity classes

In the following we state a simplified version of [49, Theorem 3.15], which is
sufficient for our application. We start by introducing fast-growing functions
and complexity classes. Recall that the Cantor normal form of an ordinal
$\alpha\leq\omega^{\omega}$ is the unique representation
$\alpha=\omega^{\alpha_{1}}+\dots+\omega^{\alpha_{p}}$ where
$\alpha>\alpha_{1}\geq\dots\geq\alpha_{p}$. In this form $\alpha$ is a limit
ordinal if and only if $p>0$ and $\alpha_{p}>0$. A fundamental sequence for a
limit ordinal $\lambda$ is a sequence $(\lambda(x))_{x<\omega}$ of ordinals
with supremum $\lambda$. Given a limit ordinal $\lambda\leq\omega^{\omega}$
whose Cantor normal form is $\lambda=\beta+\omega^{k+1}$, we use the standard
fundamental sequence $(\lambda(x))_{x<\omega}$, defined inductively as
$\omega^{\omega}(x)=\omega^{x+1}$ and
$(\beta+\omega^{k+1})(x)=\beta+\omega^{k}\cdot(x+1)$. Given a function
$h\colon\mathbb{N}\to\mathbb{N}$ the Hardy hierarchy
$(h^{\alpha})_{\alpha\leq\omega^{\omega}}$ relative to $h$ is defined by

$\displaystyle h^{0}(x)$ $\displaystyle=x,$ $\displaystyle h^{\alpha+1}(x)$
$\displaystyle=h^{\alpha}(h(x)),$ $\displaystyle h^{\lambda}(x)$
$\displaystyle=h^{\lambda(x)}(x).$

Using the Hardy functions $(H^{\alpha})_{\alpha}$ relative to $H(x)=x+1$ we
can define the fast-growing complexity classes
$({\small\mathsf{F}}_{\alpha})_{\alpha}$ from [48]. We denote by
$\mathscr{F}_{<\alpha}$ the class of functions computed by deterministic
Turing machines in time $O(H^{\beta}(n))$ for some $\beta<\omega^{\alpha}$. By
${\small\mathsf{F}}_{\alpha}$ we denote the class of decision problems solved
by deterministic Turing machines in time $O(H^{\omega^{\alpha}}(p(n)))$ for
some function $p\in\mathscr{F}_{<\alpha}$. We define
$\text{${\small\mathsf{PRIMITIVE}}$-${\small\mathsf{RECURSIVE}}$}=\bigcup_{k<\omega}{\small\mathsf{F}}_{k}$
and ${\small\mathsf{ACKERMANN}}={\small\mathsf{F}}_{\omega}$.

#### Controlled bad sequences

By Dickson’s lemma, any sequence of vectors $\bm{x}_{1},\bm{x}_{2},\dots$ with
$x_{i}\not\leq x_{j}$ for all $i<j$ must be finite. Such a sequence is also
called bad. To obtain complexity bounds on the length of bad sequences we need
to restrict to sequences that do not grow in an uncontrolled fashion. In the
following let $g\colon\mathbb{N}\to\mathbb{N}$ be monotone, strictly
inflationary, i.e. $g(x)>x$ for all $x$, and super-homogeneous, i.e.
$g(xy)\geq g(x)\cdot y$ for all $x,y\geq 1$. A sequence of vectors
$\bm{x}_{0},\bm{x}_{1},\dots,\bm{x}_{\ell}$ is $(g,n)$-controlled if
$\|\bm{x}_{i}\|\leq g^{i}(n)$ for all $i\in[0,\ell]$. The following statement
follows from [49, Theorem 3.15] and [49, Eq. (3.13)].

######  Theorem 4.5.

Any $(g,n)$-controlled bad sequence over $\mathbb{N}^{k}$ has length at most
$g^{\omega^{k}}(nk)$.

A chain in $\mathbb{N}^{k}$ is a sequence $S_{0}\subsetneq
S_{1}\subsetneq\dots\subsetneq S_{\ell}$ of subsets
$S_{i}\subseteq\mathbb{N}^{k}$. The chain is $(g,n)$-controlled if for each
$i\in[0,\ell-1]$ there exists $\bm{s}_{i}\in S_{i+1}\setminus S_{i}$ with
$\|\bm{s}_{i}\|\leq g^{i}(n)$. A set $X\subseteq\mathbb{N}^{k}$ is upwards
closed if $X=X{\uparrow}$. Observe that any $(g,n)$-controlled chain of
upwards closed sets in $\mathbb{N}^{k}$ is bounded by $1+g^{\omega^{k}}(nk)$
since we obtain a $(g,n)$-controlled bad sequence
$\bm{s}_{0},\bm{s}_{1},\dots,\bm{s}_{\ell-1}$ by picking arbitrary
$\bm{s}_{i}\in S_{i+1}\setminus S_{i}$ with $\|\bm{s}_{i}\|\leq g^{i}(n)$.

#### Translating congruences into upwards closed sets

The key trick in our upper bound for ascending chains of congruences is to
translate congruences into upwards closed sets. This allows us to translate
bounds on the length of ascending chains of upward closed sets into
corresponding bounds for congruences. The translation works as follows. To
each congruence $\mathcal{Q}$ on $\mathbb{N}^{d}$, we associate the upwards
closed set $U(\mathcal{Q})\subseteq\mathbb{N}^{4d}$ with

$U(\mathcal{Q})=\\{(\bm{x},\bm{y},\bm{u},\bm{v})\mid(\bm{x},\bm{y})\in\mathcal{Q},\,(\bm{x}+\bm{u},\bm{y}+\bm{v})\in\mathcal{Q},\,(\bm{u},\bm{v})\neq(\bm{0},\bm{0})\\}{\uparrow}.$

Clearly $\mathcal{Q}_{1}\subseteq\mathcal{Q}_{2}$ implies
$U(\mathcal{Q}_{1})\subseteq U(\mathcal{Q}_{2})$. In fact, strict inclusion is
also preserved:

######  Lemma 4.6.

Let $\mathcal{Q}_{1}$ and $\mathcal{Q}_{2}$ be congruences with
$\mathcal{Q}_{1}\subseteq\mathcal{Q}_{2}$. Then (i)
$U(\mathcal{Q}_{1})\subseteq U(\mathcal{Q}_{2})$ and (ii) for each
$\bm{q}\in\mathcal{Q}_{2}\setminus\mathcal{Q}_{1}$, there is a $\bm{p}\in
U(\mathcal{Q}_{2})\setminus U(\mathcal{Q}_{1})$ with
$\|\bm{p}\|\leq\|\bm{q}\|$.

######  Proof 4.7.

Statement (i) is immediate. For statement (ii) let
$(\bm{s},\bm{t})\in\mathcal{Q}_{2}\setminus\mathcal{Q}_{1}$ be minimal. Since
$(\bm{0},\bm{0})\in\mathcal{Q}_{1}$ we must have
$(\bm{s},\bm{t})\neq(\bm{0},\bm{0})$ and there exists
$(\bm{x},\bm{y})\in\mathcal{Q}_{1}$ with $(\bm{x},\bm{y})<(\bm{s},\bm{t})$. We
choose such a vector $(\bm{x},\bm{y})$ in which
$(\bm{u},\bm{v}):=(\bm{s},\bm{t})-(\bm{x},\bm{y})$ is minimal. Clearly,
$(\bm{x},\bm{y},\bm{u},\bm{v})\in U(\mathcal{Q}_{2})$. We claim that
$(\bm{x},\bm{y},\bm{u},\bm{v})\notin U(\mathcal{Q}_{1})$. Towards a
contradiction, suppose that there exists
$(\bm{x}_{1},\bm{y}_{1},\bm{u}_{1},\bm{v}_{1})\leq(\bm{x},\bm{y},\bm{u},\bm{v})$
with $(\bm{x}_{1},\bm{y}_{1})\in\mathcal{Q}_{1}$,
$(\bm{u}_{1},\bm{v}_{1})\neq(\bm{0},\bm{0})$, and
$(\bm{x}_{1}+\bm{u}_{1},\bm{y}_{1}+\bm{v}_{1})\in\mathcal{Q}_{1}$. Since
$\mathcal{Q}_{1}$ is a congruence we have

$\displaystyle\bm{x}+\bm{u}_{1}=(\bm{x}-\bm{x}_{1})+\bm{x}_{1}+\bm{u}_{1}$
$\displaystyle\sim_{\mathcal{Q}_{1}}(\bm{x}-\bm{x}_{1})+\bm{y}_{1}+\bm{v}_{1}$
$\displaystyle\sim_{\mathcal{Q}_{1}}(\bm{x}-\bm{x}_{1})+\bm{x}_{1}+\bm{v}_{1}=\bm{x}+\bm{v}_{1}\sim_{\mathcal{Q}_{1}}\bm{y}+\bm{v}_{1}.$

If $(\bm{u}_{1},\bm{v}_{1})=(\bm{u},\bm{v})$ then this contradicts
$(\bm{x}+\bm{u},\bm{y}+\bm{v})=(\bm{s},\bm{t})\notin\mathcal{Q}_{1}$. If
$(\bm{u}_{1},\bm{v}_{1})<(\bm{u},\bm{v})$ then
$(\bm{s},\bm{t})=(\bm{x}+\bm{u}_{1},\bm{y}+\bm{v}_{1})+(\bm{u}-\bm{u}_{1},\bm{v}-\bm{v}_{1})$
contradicts the minimality of $(\bm{u},\bm{v})$.

If $(\mathcal{Q}_{i})_{i\leq\ell}$ is a $(g,n)$-controlled chain of
congruences in $\mathbb{N}^{d}$ then by Lemma 4.6,
$(U(\mathcal{Q}_{i}))_{i\leq\ell}$ is a $(g,n)$-controlled chain of upwards
closed subsets of $\mathbb{N}^{4d}$ and thus has length at most
$1+g^{\omega^{4d}}(4dn)$. Hence, the same bound applies to
$(\mathcal{Q}_{i})_{i\leq\ell}$.

######  Lemma 4.8.

Any $(g,n)$-controlled chain of congruences in $\mathbb{N}^{d}$ has length
$\leq 1+g^{\omega^{4d}}(4dn)$.

Putting together Theorem 4.4 and Lemma 4.8 we can conclude that Algorithm 1
terminates after $H^{\omega^{4d+3}}(e(n))$ iterations for some elementary
function $e(n)$.

######  Proposition 4.9.

Reachability in bidirected pushdown VAS is in ${\small\mathsf{ACKERMANN}}$,
and in ${\small\mathsf{F}}_{4d+3}$ if the dimension $d$ is fixed.

The detailed complexity analysis can be found in Appendix A. The result above
also holds for bidirected pushdown VASS (Theorem 1.1) by simulating the state
in two additional counters. Hence the complexity for dimension $d$ increases
from ${\small\mathsf{F}}_{4d+3}$ to ${\small\mathsf{F}}_{4d+11}$.

##  5 One-dimensional pushdown VASS

In this section we prove that reachability is in polynomial space for
bidirected 1-PVASS (Theorem 1.2). For the rest of this section consider a
1-PVASS $\mathcal{P}=(Q,\Gamma,T)$ of $|Q|=n$ states. To simplify our bounds,
we assume $|\Gamma|=2$. This can be achieved with a simple encoding: To
simulate stack letters $a_{1},\ldots,a_{k}$, we can encode each $a_{i}$ by the
string $ab^{i}ab^{k-i}a$.

#### Preliminaries

We extend the usual component-wise ordering $\leq$ to tuples
$(\mathbb{Z}\cup\\{-\infty,\omega\\})^{k}$. Given two functions $f,g\colon
X\to(\mathbb{Z}\cup\\{-\infty,\omega\\})^{k}$, we write $f\leq g$ to denote
that $f(x)\leq g(x)$ for each $x\in X$. We define the one-step $\mathbb{Z}$
relation $\hookrightarrow$ for $\mathcal{P}$ similarly to the one-step
relation $\xrightarrow{}$ but with a $\mathbb{Z}$-counter, i.e., we do not
require the counter to remain non-negative. A _path from $p$ to $q$_ consists
of the initial state $p$ and a sequence of transitions of $\mathcal{P}$, such
that it induces a run
$(p_{1},x_{1},w_{1})\hookrightarrow(p_{2},x_{2},w_{2})\hookrightarrow\dots\hookrightarrow(p_{j},x_{j},w_{j})$,
with the requirement that $p_{1}=p$, $x_{1}=0$ and $w_{1}=w_{j}=\varepsilon$.
Given such a path $P$, we let

  * •

$\mathit{MaxSH}(P)=\max_{i}|w_{i}|$ be the maximum stack height along $P$,

  * •

$w(P)=x_{j}$ be the value of the counter at the end of $P$, and

  * •

$\mathit{m}(P)=\min_{i}x_{i}$ be the minimum value of the counter along $P$.
Note that $\mathit{m}(P)\leq 0$, as the counter is $0$ at the beginning of
$P$.

We also write $\overline{P}$ for the reverse of $P$. We denote by
$\\{p\rightsquigarrow q\\}$ the set of paths from $p$ to $q$, and let
$\\{p\rightsquigarrow q\\}_{k}=\\{P\in\\{p\rightsquigarrow
q\\}\colon\mathit{MaxSH}(P)\leq k\\}$ be the set of such paths with stack
height at most $k$. Given two paths $P_{1}$ and $P_{2}$, we write $P_{1}\leq
P_{2}$ to denote that
$(\mathit{m}(P_{1}),w(P_{1}))\leq(\mathit{m}(P_{2}),w(P_{2}))$.

We say that a state $q$ is reachable from a state $p$ if
$(p,\bm{0},\varepsilon)\xrightarrow{*}(q,\bm{0},\varepsilon)$. We say that $q$
is _$\mathbb{Z}$ -reachable_ from $p$ if there is a path
$P\in\\{p\rightsquigarrow q\\}$ with $w(P)=0$ (hence state reachability
implies $\mathbb{Z}$-reachability). Given additionally a natural number
$i\in\mathbb{N}$, we say that $p$ covers $(q,i)$ if
$(p,0,\varepsilon)\xrightarrow{*}(q,i+j,\varepsilon)$ for some $j\geq 0$. Thus
reachability implies coverability for $i=0$. The following is a simpler proof
of a reduction observed in [30]: For bidirected $1$-PVASS, reachability
reduces to coverability and $\mathbb{Z}$-reachability.

######  Lemma 5.1.

For any two states $p,q$ of $\mathcal{P}$, we have that $p$ reaches $q$ iff
(i) $p$ covers $(q,0)$, (ii) $q$ covers $(p,0)$, and (iii) $p$
$\mathbb{Z}$-reaches $q$.

######  Proof 5.2.

Clearly if $p$ reaches $q$ then conditions (i)-(iii) hold, so we only need to
argue about the reverse direction. If $p$ does not cover $(q,1)$, since $p$
covers $(q,0)$, we have that $p$ reaches $q$, and we are done. Similarly, if
$q$ does not cover $(p,1)$, we have that $q$ reaches $p$ and thus we are done.
Finally, assume that $p$ covers $(q,1)$ and $q$ covers $(p,1)$, and let
$P_{p}$ and $P_{q}$ be the corresponding paths witnessing coverability. Let
$P$ be a path witnessing that $p$ $\mathbb{Z}$-reaches $q$. We construct the
path $H_{\ell}$ witnessing the reachability of $q$ from $p$ as
$H_{\ell}=(P_{p}\circ P_{q})^{\ell}\circ
P\circ(\overline{P_{p}}\circ\overline{P_{q}})^{\ell}$, where $\ell$ is chosen
such that $w((P_{p}\circ P_{q})^{\ell})\geq-\mathit{m}(P)$.

In light of Lemma 5.1, for Theorem 1.2, it suffices to show that for
bidirected $1$-PVASS, both $\mathbb{Z}$-reachability and coverability can be
decided in ${\small\mathsf{PSPACE}}$. The former is known already:
Reachability in $\mathbb{Z}$-PVASS belongs to ${\small\mathsf{NP}}$ [23]; in
the bidirected case, it is even decidable in ${\small\mathsf{P}}$ [20]. Thus,
the rest of this section is devoted to deciding coverability in
${\small\mathsf{PSPACE}}$.

######  Lemma 5.3.

Coverability in 1-dimensional bidirected pushdown VASS is in
${\small\mathsf{PSPACE}}$.

#### Summary functions

We define a summary function $\gamma_{k}\colon Q\times Q\to(\mathbb{Z}_{\leq
0}\cup\\{-\infty\\})\times(\mathbb{Z}\cup\\{-\infty,\omega\\})$, parametric on
$k\in\mathbb{N}$, as $\gamma_{k}(p,q)=(a,b)$, where $a$ and $b$ are defined as
follows.

$\displaystyle a=\max(\\{\mathit{m}(P)\colon P\in\\{p\rightsquigarrow
q\\}_{k}\\})\qquad b=\sup(\\{w(P)\colon P\in\\{p\rightsquigarrow
q\\}_{k}\text{ and }\mathit{m}(P)=a\\})$

with the convention that $\max(\emptyset)=\sup(\emptyset)=-\infty$. We
occasionally write $\gamma_{k}(p,q)=(a,\\_)$ to denote that
$\gamma_{k}(p,q)=(a,b)$ for some $b$. We further define a summary function
$\delta_{k}\colon V\to(\mathbb{Z}_{\leq 0}\cup\\{-\infty\\})$, parametric on
$k\in\mathbb{N}$, as follows.

$\displaystyle\delta_{k}(p)=\max(\\{\mathit{m}(P)\colon
P\in\\{p\rightsquigarrow p\\}_{k}\text{ and }w(P)>0\\})$

Recall that we use $n=|Q|$ for the number of states in $\mathcal{P}$. It is
well-known that in any pushdown system of $n$ states (and only two stack
letters), a shortest path between two states has length $2^{O(n^{2})}$ (e.g.
this follows by inspecting a proof of the pumping lemma for context-free
languages [27, Lemma 6.1]; a precise bound was obtained in [44]). Since both
the weight and the minima of any path are lower-bounded by minus the length of
the path, if $\\{p\rightsquigarrow q\\}_{k}\neq\emptyset$, then a shortest
path in $\\{p\rightsquigarrow q\\}_{k}$ witnesses $\gamma_{k}(p,q)=(a,b)$
where $a$ and $b$ are at most exponentially negative. This is established in
the following lemma.

######  Lemma 5.4.

Consider any two states $p,q$ and natural number $k$, and let
$\gamma_{k}(p,q)=(a,b)$. If $a>-\infty$ then $a,b\geq-\beta$, for
$\beta=2^{O\left(n^{2}\right)}$.

The bidirectedness of $\mathcal{P}$ also leads to the following lemma.

######  Lemma 5.5.

Consider any two states $p,q$ and natural number $k$, and let
$\gamma_{k}(p,q)=(a,b)$. There exists a constant $\alpha$ independent of
$\mathcal{P}$ and $k$, such that, if $b>2^{\alpha n^{2}}$, then $b=\omega$.

The intuition behind the summary functions $\gamma_{k}$ and $\delta_{k}$ is as
follows. Lemma 5.4 and Lemma 5.5 hint on an algorithm to decide coverability
by saturating $\gamma_{k}$ iteratively for increasing $k$. The lemmas state
that the finite values of $\gamma_{k}$ are exponentially bounded, and thus the
process is guaranteed to reach a fixpoint within exponentially many
iterations. An obstacle to this approach is that $\gamma_{k}$ may fail to
capture paths that are useful in subsequent iterations. In particular,
$\gamma_{k}(p,q)$ misses paths that can reach $q$ with a larger counter at the
cost of a lower minima on the way. The following lemma shows that $\delta_{k}$
captures the effects of all paths missed by $\gamma_{k}$, and allows the two
summaries to be _mutually_ saturated.

######  Lemma 5.6.

For any states $p,q$, let $\gamma_{k}(p,q)=(a,b)$, and assume there exists a
path $P\in\\{p\rightsquigarrow q\\}_{k}$ with $w(P)>b$. Then
$\delta_{k}(p)\geq\mathit{m}(P)$.

Moreover, the values of $\delta_{k}$ are also exponentially bounded, and thus
the mutual saturation can be carried out in polynomial space.

######  Lemma 5.7.

For any state $p$, if $\delta_{k}(p)>-\infty$ then $\delta_{k}(p)\geq-\beta$,
for $\beta=2^{O\left(n^{2}\right)}$.

In the remainder of this section we describe the saturation procedure for
$\gamma_{k}$ and $\delta_{k}$.

#### Finite graphs

We consider weighted finite graphs $G=(V_{G},E_{G},w_{G})$ where $w_{G}\colon
E_{G}\to\mathbb{Z}$. Moreover, we assume that every connected component of $G$
is strongly connected. By a small abuse we extend some of the above notation
on $\mathcal{P}$ to such graphs. Given two nodes $u$, $v$ in $G$, we write
$\\{u\rightsquigarrow v\\}^{G}$ for the set of paths from $u$ to $v$ in $G$.
We similarly extend the summary functions to $\gamma^{G}$ and $\delta^{G}$,
defined by the corresponding paths $P\in\\{u\rightsquigarrow v\\}^{G}$.

######  Lemma 5.8.

Given a graph $G$ as above, the summary functions $\gamma^{G}$ and
$\delta^{G}$ can be computed in polynomial time.

#### Computing $\gamma_{k}$ and $\delta_{k}$.

We now describe a dynamic-programming algorithm for computing $\gamma_{k}$ and
$\delta_{k}$, for increasing values of $k$. We let
$\Gamma_{\bot}=\Gamma\cup\\{\bot\\}$, where $\bot$ is a special symbol, and
assume without loss of generality that every transition in $\mathcal{P}$ that
manipulates the counter does not affect the stack. Afterwards we will argue
that the algorithm terminates within exponentially many iterations.

  1. 1.

We start with $k=0$. We construct a graph $G_{0}$ that consists of nodes
$\langle p,\bot\rangle$ where $p$ is a state of $\mathcal{P}$. Moreover,
$G_{0}$ contains the corresponding transitions of $\mathcal{P}$ that do not
manipulate the stack. In particular, for every transition
$(p,i,\varepsilon,q)\in T$ we have an edge $\langle
p,\bot\rangle\xrightarrow{i}\langle q,\bot\rangle$ in $G_{0}$. We use Lemma
5.8 to compute $\gamma^{G_{0}}$ and $\delta^{G_{0}}$, and report that, for all
states $p$ and $q$, we have $\gamma_{0}(p,q)=\gamma^{G_{0}}(\langle
p,\bot\rangle,\langle q,\bot\rangle)$ and
$\delta_{0}(p)=\delta^{G_{0}}(\langle p,\bot\rangle)$.

  2. 2.

We repeat the following until $\gamma^{G_{k}}$ and $\delta^{G_{k}}$ have
converged. We construct a graph $G_{k}$ as follows. For every state $p$ and
every $\sigma\in\Gamma_{\bot}$, we have a node $\langle p,\sigma\rangle$ in
$G_{k}$. We then do the following.

    1. (a)

Let $\delta^{G_{k-1}}(\langle p,\bot\rangle)=c$. We insert a node $\langle
p^{\prime},\sigma\rangle$, and if $-\infty<c$, we insert two edges
manipulating the counter $\langle p,\sigma\rangle\xrightarrow{c}\langle
p^{\prime},\sigma\rangle$ and $\langle
p^{\prime},\sigma\rangle\xrightarrow{-c+1}\langle p,\sigma\rangle$.

    2. (b)

For every state $q$, let $\gamma^{G_{k-1}}(\langle p,\bot\rangle,\langle
q,\bot\rangle)=(a,b)$. If $-\infty<a$, we insert a node $\langle
p,q,\sigma\rangle$ and two edges manipulating the counter $\langle
p,\sigma\rangle\xrightarrow{a}\langle p,q,\sigma\rangle$ and $\langle
p,q,\sigma\rangle\xrightarrow{-a+b^{\prime}}\langle q,\sigma\rangle$, where
$b^{\prime}=b$ if $b<\omega$ and $b^{\prime}=0$ otherwise.

  3. 3.

Finally, for each stack letter $\sigma\in\Gamma$, we connect nodes of the form
$\langle p,\bot\rangle$ and $\langle q,\sigma\rangle$ using the transitions of
$\mathcal{P}$ that manipulate the stack. That is, for every transition
$(p,0,\sigma,q)\in T$, we insert an edge $\langle
p,\bot\rangle\xrightarrow{}\langle q,\sigma\rangle$, and for every transition
$(p,0,\overline{\sigma},q)\in T$, we insert an edge $\langle
p,\sigma\rangle\xrightarrow{}\langle q,\bot\rangle$.

  4. 4.

We use Lemma 5.8 to compute $\gamma^{G_{k}}$ and $\delta^{G_{k}}$, and report
that, for all states $p$ and $q$, we have
$\gamma_{k}(p,q)=\gamma^{G_{k}}(\langle p,\bot\rangle,\langle q,\bot\rangle)$
and $\delta_{k}(p)=\delta^{G_{k}}(\langle p,\bot\rangle)$.

We first argue that the graphs $G_{k}$ consist of strongly connected
components, and thus Lemma 5.8 is applicable.

######  Lemma 5.9.

For all $k\in\mathbb{N}$, every connected component of $G_{k}$ is strongly
connected.

Given some $\sigma\in\Gamma_{\bot}$ and $k\geq 1$, we denote by
$G_{k}\downharpoonright\sigma$ the subgraph of $G_{k}$ induced by the nodes
whose last element is $\sigma$. It follows directly from the construction of
$G_{k}$ that, for every pair of states $p,q$ of $\mathcal{P}$ and
$\sigma\in\Gamma_{\bot}$, for every path $P$ that goes from $\langle
p,\sigma\rangle$ to $\langle q,\sigma\rangle$ and is contained in
$G_{k}\downharpoonright\sigma$, there is a path $H\in\\{p\rightsquigarrow
q\\}_{k-1}$ with $P\leq H$. In turn, this implies that the summary functions
$\gamma^{G_{k}}$ and $\delta^{G_{k}}$ are always dominated by paths in
$\mathcal{P}$ of stack height at most $k$, i.e., for all states $p$ and $q$,
we have $\gamma^{G_{k}}(\langle p,\bot\rangle,\langle
q,\bot\rangle)\leq\gamma_{k}(p,q)$ and $\delta^{G_{k}}(\langle
p,\bot\rangle)\leq\delta_{k}(p)$ for all $k\in\mathbb{N}$. The following lemma
states that $\gamma^{G_{k}}$ and $\delta^{G_{k}}$ compute $\gamma_{k}$ and
$\delta_{k}$ exactly, by arguing that $\gamma^{G_{k}}$ and $\delta^{G_{k}}$
also dominate all paths of $\mathcal{P}$ with stack height at most $k$. In
turn, this establishes the correctness of the algorithm.

######  Lemma 5.10.

For all $k\in\mathbb{N}$ and states $p,q\in Q$, we have
$\gamma_{k}(p,q)=\gamma^{G_{k}}(\langle p,\bot\rangle,\langle q,\bot\rangle)$
and $\delta_{k}(p)=\delta^{G_{k}}(\langle q,\bot\rangle)$.

Thus, to decide whether $p$ covers $(q,0)$, we saturate $\gamma_{k}$ and
$\delta_{k}$ and check whether $\gamma_{k}(p,q)=(0,\\_)$. The termination and
complexity of the algorithm follows from the boundedness of the finite values
of $\gamma_{k}$ and $\delta_{k}$ (Lemma 5.4, Lemma 5.5 and Lemma 5.7), which
concludes Lemma 5.3.

######  Lemma 5.11.

The above algorithm terminates and uses polynomial space.

Finally, note that if we have a polynomial bound on the stack height, then the
saturation procedure runs in polynomial time, which also leads to reachability
in polynomial time (a closer analysis yields an $O(n^{3})$ bound per
iteration). In particular, the ${\small\mathsf{PSPACE}}$-hardness proof for
1-dimensional directed PVASS from [15] cannot be directly transferred to
bidirected PVASS: The 1-PVASS constructed in [15] has a polynomially bounded
stack height. See also Appendix D for details on how exactly the reduction
fails. Without a bound on the stack height, the saturation might indeed take
exponential time: There are 1-dimensional bidirected PVASS on which shortest
coverability witnesses require an exponential stack height (see Appendix B for
an example).

##  6 Tower lower bound

In this section, we show that reachability in bidirected PVASS is
${\small\mathsf{TOWER}}$-hard with respect to elementary reductions, and
$k$-${\small\mathsf{EXPSPACE}}$-hard in dimension $2k+6$. Recall that
${\small\mathsf{TOWER}}$ is the class of all problems computable by
deterministic Turing machines in time (or space) bounded by a tower of
exponentials of elementary height.

#### Lower bound for directed PVASS

We first recall the ${\small\mathsf{TOWER}}$-hardness proof by Lazić and
Totzke [32] for reachability in directed PVASS. They reduce the
$\exp^{n}(1)$-bounded halting problem for counter programs of size $n$, which
is ${\small\mathsf{TOWER}}$-complete with respect to elementary reductions
(which allow us to replace the parameter $n$ with an arbitrary elementary
function $e(n)$) [19]. A counter program is a finite sequence of commands
which manipulate non-negative counters, initially set to zero. The commands
include increments $x:=x+1$, decrements $x:=x-1$, conditionals if $x=0$ then
goto $L_{1}$ else goto $L_{2}$ (where $L_{1}$ and $L_{2}$ are line numbers),
and ${\bf halt}$. If a counter of value 0 is decremented, the program aborts.
The $\exp^{n}(1)$-bounded halting problem asks whether given a counter program
of size $n$, starting from the first command and all counters set to zero, a
command ${\bf halt}$ can be reached using a run during which all counters are
bounded by $\exp^{n}(1)$ and are all zero at the end.

As in most lower bounds for vector addition systems and their extensions, for
each counter $x$ we store a complement counter $\bar{x}$, maintaining the
invariant $x+\bar{x}=B$ for some (large) bound $B$. This can be achieved by
complementing every in/decrement of $x$ by a de/increment of $\bar{x}$, and
vice versa. Then, a zero test if $x=0$ then goto $L_{1}$ else goto $L_{2}$ can
be replaced by guessing whether $x=0$ and $x\neq 0$: In the former case we add
and subtract $B$ to $x$ and continue with $L_{1}$. In the latter case we add
and subtract $B$ to $\bar{x}$ and continue with $L_{2}$.

The challenge is to implement the addition (and subtraction) with a large
number $B$, here $B=\exp^{n}(1)$, using a polynomially large system. Suppose
we have counters $c_{1},\dots,c_{n}$ with complement counters
$\bar{c}_{1},\dots,\bar{c}_{n}$ satisfying $c_{k}+\bar{c}_{k}=\exp^{k}(1)$ for
all $k$. Lazić and Totzke [32] show how to construct for all $k=1,\dots,n$ a
$\text{poly}(k)$-sized PVASS that adds $\exp^{k}(1)$ to $c_{k}$. It operates
by pushing exactly $\exp^{k-1}(1)$ many zeros to the stack, repeatedly
incrementing the $\exp^{k-1}(1)$-bit binary counter on the stack, while
simultaneously decrementing $c_{k}$, and finally popping exactly
$\exp^{k-1}(1)$ many ones from the stack. Observe that the operations on the
stack can be implemented with the help of $c_{k-1}$ that can be in/decremented
by $\exp^{k-1}(1)$ by induction hypothesis. Before simulating the counter
program, each complement counter $\bar{c}_{k}$ has to be set to $\exp^{k}(1)$,
which can be done in a similar fashion.

#### Simulation by bidirected systems

In the following we will make the above construction outlined by Lazić and
Totzke [32] explicit and show that the simulation is correct even after making
the PVASS bidirected. To this end we need the following argument already found
in Post’s undecidability proof of the word problem for Thue systems [45, Lemma
II]. Consider a deterministic transition system where the final state does not
have any outgoing transitions. To such a system we now add reverse edges to
make it bidirected. Clearly, any original run is present in the bidirected
system. Conversely, consider a run to the final state in the bidirected
system, which may use the new reverse edges. It cannot end on a reverse edge,
since there is no outgoing forward edge from the final state. So as long as
the run contains reverse edges, at least one of these edges must be followed
by one in the forward direction. Let us call them $p\xrightarrow{\bar{a}}q$
and $q\xrightarrow{b}r$. As the original system was deterministic $q$ has
exactly one outgoing edge, and hence
$(q\xrightarrow{b}r)=(q\xrightarrow{a}p)$. Since the effects of $\bar{a}$ and
$b$ cancel out, we can omit both of them from the run. Iterating this argument
eventually yields a run with no reverse edges. It follows that adding reverse
edges to a fully deterministic system does not change its reachability set
(this was originally shown by Mayr and Meyer [42] for their proof of
${\small\mathsf{EXPSPACE}}$-hardness of reachability for bidirected VAS).

The construction of Lazić and Totzke is not fully deterministic. However, it
only uses very restricted nondeterminism that will not impact our simulation
of the counter machine.

#### Gadget construction

Since we also want to show a $k$-${\small\mathsf{EXPSPACE}}$ lower bound for
dimension $2k+6$, we use a slightly more refined analysis: We will assume that
two numbers $k$ and $n$ are given as input and construct a system that
simulates counters bounded by $\exp^{k}(n)$ instead of $\exp^{k}(1)$ as in
Lazić and Totzke.

In the following a gadget $G$ consists of a PVASS and two distinguished
terminal states $s$ and $t$. We consider vectors $\bm{x}\in\mathbb{N}^{2k}$
where the first $k$ components are viewed the values of $k$ counters
$c_{1},\dots,c_{k}$ and the last $k$ components are the values of $k$
complementary counters $\bar{c}_{1},\ldots,\bar{c}_{k}$. Without further
mention, any update on a counter $c$ is always understood with complementary
update on $\bar{c}$ so that the sums $c_{i}+\bar{c}_{i}$ remain constant.

Given two numbers $k,n$ (in unary), we will inductively construct a gadget
$G_{k}$ with stack alphabet $\Gamma_{k}$. This gadget will allow us to add
$\exp^{k}(n)$ to a counter. The gadget’s size will grow exponentially in $k$
(and polynomially in $n$), and later, we improve the construction to grow only
polynomially in $k$. The gadget $G_{1}$ simply increments $c_{1}$ by $2^{n}$.
Assuming $G_{k-1}$ is already constructed, we construct the gadget $G_{k}$.
The gadget $\bar{G}_{k-1}$ is obtained from $G_{k-1}$ by reversing all
transitions, and interchanging its terminal states. Its behavior is inverse to
that of $G_{k-1}$, as it subtracts $\exp^{k-1}(n)$ from $c_{k-1}$. Let
$Z_{k-1}=G_{k-1}\circ\bar{G}_{k-1}$ be the gadget obtained by composing
$G_{k-1}$ with $\bar{G}_{k-1}$, which is a zero test of $c_{k-1}$. We can
naturally view $G_{k-1}$, $\bar{G}_{k-1}$ and $Z_{k-1}$ as gadgets with $2k$
counters, where $c_{k}$ and $\bar{c}_{k}$ are untouched. The gadget $G_{k}$ is
displayed in Figure 1 where 0 and 1 are fresh stack symbols and Inck is a
subprocedure which increments the binary counter on the stack.

To prove correctness of the gadget $G_{k}$ we need a bit of notation. For
brevity we write $[x_{1},\dots,x_{k}]$ for
$(x_{1},\dots,x_{k},\exp^{1}(n)-x_{1},\dots,\exp^{k}(n)-x_{k})$. Our gadgets
will always assume that the “lower” counters $c_{j}$ are set to zero and that
the invariant is satisfied. A counter vector of the form
$[0,\dots,0,x_{i},\dots,x_{k}]$ is called $i$-initialized. Moreover, we call a
run $(s,\bm{u},w)\xrightarrow{*}(t,\bm{v},w^{\prime})$ in a gadget _$i$
-initialized_ if either $\bm{u}$ or $\bm{v}$ is $i$-initialized.

Inck:$p_{0}$$p_{1}$$p_{2}$$p_{3}$$p_{4}$$Z_{k-1}$pt$c_{k-1}+$= 1
$\bar{\texttt{1}}$pt$\bar{\texttt{0}}\texttt{1}$pt$c_{k-1}-$= 1
0$Z_{k-1}$$c_{k}+$= 1

$q_{0}$$q_{1}$$q_{2}$$q_{3}$$q_{4}$$q_{5}$$G_{k-1}$pt$c_{k-1}-$= 1
0$Z_{k-1}$pt$\text{Inc}_{k}$$Z_{k-1}$pt$c_{k-1}+$= 1
$\bar{\texttt{1}}$$c_{k}+$= 1$\bar{G}_{k-1}$

Figure 1: Gadgets Inck and $G_{k}$.

######  Proposition 6.1.

The $k$-initialized runs in $G_{k}$ from $q_{0}$ to $q_{5}$ are precisely the
runs

$(q_{0},[0,\dots,0],w)\xrightarrow{*}_{G_{k}}(q_{5},[0,\dots,0,\exp^{k}(n)],w)\quad\text{for
}w\in\Gamma_{k-1}^{*}.$

Next we will analyse the bidirected version of $G_{k}$. In order to
distinguish the original transitions from the reverse transitions we define
for a PVASS $G$ the relations
$\leftrightarrow_{G}\,=\,\to_{G}\cup\leftarrow_{G}$ and
$\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{G}$, denoting the reflexive
transitive closure of $\leftrightarrow_{G}$. Similarly to the argument by Post
[45, Lemma II], we can prove the following:

######  Proposition 6.2.

Let $\bm{u},\bm{v}\in\mathbb{N}^{2k}$ where $\bm{u}$ or $\bm{v}$ is
$k$-initialized.

  * •

If
$(q_{0},\bm{u},w)\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{G_{k}}(q_{5},\bm{v},w^{\prime})$
then $(q_{0},\bm{u},w)\xrightarrow{*}_{G_{k}}(q_{5},\bm{v},w^{\prime})$.

  * •

If $q\in\\{q_{0},q_{5}\\}$ and
$(q,\bm{u},w)\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{G_{k}}(q,\bm{v},w^{\prime})$
then $\bm{u}=\bm{v}$ and $w=w^{\prime}$.

We need to reduce the size of $G_{k}$ so that it can be constructed in time
polynomial in $k$. Since $G_{k}$ uses ten copies of the subgadget $G_{k-1}$
(each zero test $Z_{k-1}$ uses two copies of $G_{k-1}$), we cannot simply
insert $G_{k-1}$ by copying it, as this would induce exponential growth of the
number of states of our system. Instead, we instantiate each gadget $G_{k-1}$
once. Then, whenever a gadget would be used between two states $p,q$, we push
a fresh stack symbol $t_{p,q}$ and move to $G_{k-1}$. When exiting $G_{k-1}$
we pop $t_{p,q}$ and return to $q$. Since this symbol is unique for every pair
of states, it uniquely determines where we can leave the gadget to, even if
there are multiple incoming and outgoing transitions at the gadget $G_{k-1}$.
Finally, one can verify that Proposition 6.2 still holds for this adapted
version of $G_{k}$.

#### Simulating the counter program

We are ready to finish the lower bound proof. We are given a counter program
of size $n$ with three counters $x_{1},x_{2},x_{3}$ and want to reduce the
$\exp^{k+1}(n)$-bounded halting problem to the reachability problem for
bidirected PVASS using $2k+6$ counters. To this end, we construct the gadget
$G_{k+1}$ three times: Each of these three instances has, instead of $c_{k+1}$
(and its complement), a counter $x_{i}$ (and its complement) for some
$i\in\\{1,2,3\\}$. However, the three instances of $G_{k+1}$ share the
counters $c_{1},\ldots,c_{k}$ (and their complements). Thus, in total, we have
$2\cdot k+2\cdot 3=2k+6$ counters. If $k$ is fixed, this yields our
$k$-${\small\mathsf{EXPSPACE}}$ lower bound ([19]). If $k$ is part of the
input, the problem becomes ${\small\mathsf{TOWER}}$-complete. We start by
initializing the complement counters $\bar{c}_{1},\dots,\bar{c}_{k}$ in
sequence, using variants of the gadgets $G_{i}$ that (i) operate on the
balance counter $\bar{c}_{i}$ instead of $c_{i}$, (ii) do not decrement
$c_{i}$ when incrementing $\bar{c}_{i}$, and (iii) operate on the lower $i-1$
counters as normal. Similarly we initialize
$\bar{x}_{1},\bar{x}_{2},\bar{x}_{3}$ to $\exp^{k+1}(n)$. Finally, in order to
have an all-zero configuration in the final state, we de-initialize these
counters before entering the final state.

Increments and decrements in the counter program are directly translated into
counter updates in the PVASS. A conditional if $x_{i}=0$ then goto $L_{1}$
else goto $L_{2}$ is replaced by a nondeterministic guess of whether $x_{i}=0$
or $x_{i}\neq 0$, verifying this (in)equality, and jumping to $L_{1}$ or
$L_{2}$. Here we use variants of the zero tests
$Z_{k+1}=G_{k+1}\circ\bar{G}_{k+1}$ which on their highest level operate on
$x$ and $\bar{x}$ (instead of $c_{k+1}$ and $\bar{c}_{k+1}$). The question of
reachability of ${\bf halt}$ is then a reachability instance on the bidirected
version of the PVASS.

If the counter program halts then we can find a corresponding computation in
the PVASS. Conversely, consider a successful run of the bidirected PVASS which
uses a minimal number of reverse transitions. By Proposition 6.2 we can assume
that no gadget $G_{k+1}$ and $\bar{G}_{k+1}$ (and their variants) is entered
and exited through the same terminal state. Furthermore, any subrun passing
through such a gadget can be assumed to use only forward transitions. Hence
the only reverse transitions remaining are from increments or decrements.
Observe that the last occurrence of such a reverse transition $\bar{\tau}$
must be followed by its corresponding forward transition $\tau$. Hence we can
cancel $\tau$ with $\bar{\tau}$, contradiction.

##  7 Conclusion

We have shown that the reachability problem in bidirected pushdown VASS is
decidable, with an Ackermann upper bound and a ${\small\mathsf{TOWER}}$ lower
bound. Moreover, in the one-dimensional case, the problem is in
${\small\mathsf{PSPACE}}$, whereas ${\small\mathsf{P}}$-hardness was shown in
[20]. Thus, the exact complexity, both in the general and the one-dimensional
case, remains open.

Another direction for future research is to study bidirected versions of other
infinite-state models. For example, pushdown VASS are the simplest level in a
hierarchy of infinite-state models for which decidability of the reachability
problem is open [53]. Perhaps the techniques from this paper can be applied to
show decidability of all levels in the bidirected setting.

pages main.pgpages pages0 pages

## References

  * [1] Mohamed Faouzi Atig and Pierre Ganty.  Approximating Petri net reachability along context-free traces.  In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2011, December 12-14, 2011, Mumbai, India, volume 13 of LIPIcs, pages 152–163. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011.  doi:10.4230/LIPIcs.FSTTCS.2011.152.
  * [2] Thomas Becker, Volker Weispfenning, and Heinz Kredel.  Gröbner bases - a computational approach to commutative algebra, volume 141 of Graduate texts in mathematics.  Springer, 1993.
  * [3] Rémi Bonnet.  Theory of well-structured transition systems and extended vector-addition systems.  PhD thesis, ENS Cachan, France, 2013.  Thèse de doctorat.
  * [4] Rémi Bonnet, Alain Finkel, Jérôme Leroux, and Marc Zeitoun.  Model checking vector addition systems with one zero-test.  Log. Methods Comput. Sci., 8(2), 2012.  doi:10.2168/LMCS-8(2:11)2012.
  * [5] Ahmed Bouajjani, Javier Esparza, and Oded Maler.  Reachability analysis of pushdown automata: Application to model-checking.  In CONCUR ’97: Concurrency Theory, 8th International Conference, Warsaw, Poland, July 1-4, 1997, Proceedings, volume 1243 of Lecture Notes in Computer Science, pages 135–150. Springer, 1997.  doi:10.1007/3-540-63141-0\\_10.
  * [6] Zakaria Bouziane and Alain Finkel.  Cyclic Petri net reachability sets are semi-linear effectively constructible.  In Second International Workshop on Verification of Infinite State Systems, Infinity 1997, Bologna, Italy, July 11-12, 1997, volume 9 of Electronic Notes in Theoretical Computer Science, pages 15–24. Elsevier, 1997.  doi:10.1016/S1571-0661(05)80423-2.
  * [7] Bruno Buchberger.  Ein Algorithmus zum Auffinden der Basiselemente des Restklassenrings nach einem nulldimensionalen Polynomideal.  PhD thesis, Universität Innsbruck, 1965.
  * [8] Krishnendu Chatterjee, Bhavya Choudhary, and Andreas Pavlogiannis.  Optimal Dyck Reachability for Data-Dependence and Alias Analysis.  Proc. ACM Program. Lang., 2(POPL), December 2018.  doi:10.1145/3158118.
  * [9] Swarat Chaudhuri.  Subcubic algorithms for recursive state machines.  In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pages 159–169. ACM, 2008.  doi:10.1145/1328438.1328460.
  * [10] David C Cooper.  Theorem proving in arithmetic without multiplication.  Machine intelligence, 7(91-99):300, 1972.
  * [11] Wojciech Czerwiński, Slawomir Lasota, Ranko Lazić, Jérôme Leroux, and Filip Mazowiecki.  The reachability problem for Petri nets is not elementary.  In Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing, STOC 2019, Phoenix, AZ, USA, June 23-26, 2019, pages 24–33. ACM, 2019.  doi:10.1145/3313276.3316369.
  * [12] 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.
  * [13] Thomas W Dubé.  The structure of polynomial ideals and Gröbner bases.  SIAM Journal on Computing, 19(4):750–773, 1990.  doi:10.1137/0219053.
  * [14] Samuel Eilenberg and M. P. Schützenberger.  Rational sets in commutative monoids.  Journal of Algebra, 13(2):173–191, 1969.  doi:10.1016/0021-8693(69)90070-2.
  * [15] Matthias Englert, Piotr Hofman, Slawomir Lasota, Ranko Lazić, Jérôme Leroux, and Juliusz Straszynski.  A lower bound for the coverability problem in acyclic pushdown VAS.  Inf. Process. Lett., 167:106079, 2021.  doi:10.1016/j.ipl.2020.106079.
  * [16] 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.
  * [17] Alain Finkel, Jérôme Leroux, and Grégoire Sutre.  Reachability for two-counter machines with one test and one reset.  In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018, December 11-13, 2018, Ahmedabad, India, volume 122 of LIPIcs, pages 31:1–31:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.  doi:10.4230/LIPIcs.FSTTCS.2018.31.
  * [18] Alain Finkel and Grégoire Sutre.  Decidability of reachability problems for classes of two counters automata.  In STACS 2000, 17th Annual Symposium on Theoretical Aspects of Computer Science, Lille, France, February 2000, Proceedings, volume 1770 of Lecture Notes in Computer Science, pages 346–357. Springer, 2000.  doi:10.1007/3-540-46541-3\\_29.
  * [19] Patrick C. Fischer, Albert R. Meyer, and Arnold L. Rosenberg.  Counter machines and counter languages.  Mathematical systems theory, 1968.  doi:10.1007/BF01694011.
  * [20] Moses Ganardi, Rupak Majumdar, and Georg Zetzsche.  The complexity of bidirected reachability in valence systems.  To appear in Proc. of the Thirty-Seventh Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2022).
  * [21] Jan Grabowski.  An algorithm to identify slices, with applications to vector replacement systems.  In International Conference on Fundamentals of Computation Theory (FCT 1981), pages 425–432. Springer, 1981.  doi:10.1007/3-540-10854-8_46.
  * [22] Christoph Haase.  A survival guide to Presburger arithmetic.  ACM SIGLOG News, 5(3):67–82, 2018.  doi:10.1145/3242953.3242964.
  * [23] Matthew Hague and Anthony Widjaja Lin.  Model checking recursive programs with numeric data types.  In Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 743–759. Springer, 2011.  doi:10.1007/978-3-642-22110-1\\_60.
  * [24] Tero Harju, Oscar H. Ibarra, Juhani Karhumäki, and Arto Salomaa.  Some decision problems concerning semilinearity and commutation.  J. Comput. Syst. Sci., 65(2):278–294, 2002.  doi:10.1006/jcss.2002.1836.
  * [25] Nevin Heintze and David A. McAllester.  On the cubic bottleneck in subtyping and flow analysis.  In Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science (LICS), Warsaw, Poland, June 29 - July 2, 1997, pages 342–351. IEEE Computer Society, 1997.  doi:10.1109/LICS.1997.614960.
  * [26] Yoram Hirshfeld.  Congruences in commutative semigroups.  LFCS, Department of Computer Science, University of Edinburgh Edinburgh, 1994.
  * [27] John E Hopcroft and Jeffrey D Ullman.  Introduction to Automata Theory, Languages and Computation.  Adison-Wesley, Reading, Mass, 1979.
  * [28] Dung T. Huynh.  A superexponential lower bound for Gröbner bases and Church-Rosser commutative Thue systems.  Inf. Control., 68(1-3):196–206, 1986.  doi:10.1016/S0019-9958(86)80035-3.
  * [29] Jarkko Kari.  Reversible cellular automata: From fundamental classical results to recent developments.  New Gener. Comput., 36(3):145–172, 2018.  doi:10.1007/s00354-018-0034-6.
  * [30] Adam Husted Kjelstrøm and Andreas Pavlogiannis.  The decidability and complexity of interleaved bidirected Dyck reachability.  Proc. ACM Program. Lang., 6(POPL):1–26, 2022.  doi:10.1145/3498673.
  * [31] Ulla Koppenhagen and Ernst W. Mayr.  The complexity of the coverability, the containment, and the equivalence problems for commutative semigroups.  In Fundamentals of Computation Theory, 11th International Symposium, FCT ’97, Kraków, Poland, September 1-3, 1997, Proceedings, volume 1279 of Lecture Notes in Computer Science, pages 257–268. Springer, 1997.  doi:10.1007/BFb0036189.
  * [32] Ranko Lazić and Patrick Totzke.  What Makes Petri Nets Harder to Verify: Stack or Data?, pages 144–161.  Springer International Publishing, 2017.  doi:10.1007/978-3-319-51046-0_8.
  * [33] Jérôme Leroux.  Vector addition system reachability problem: a short self-contained proof.  In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pages 307–316. ACM, 2011.  doi:10.1145/1926385.1926421.
  * [34] 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.
  * [35] Jérôme Leroux.  Distance between mutually reachable Petri net configurations.  In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2019, December 11-13, 2019, Bombay, India, volume 150 of LIPIcs, pages 47:1–47:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.  doi:10.4230/LIPIcs.FSTTCS.2019.47.
  * [36] 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.
  * [37] 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.
  * [38] Jérôme Leroux, Grégoire Sutre, and Patrick Totzke.  On the coverability problem for pushdown vector addition systems in one dimension.  In Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, volume 9135 of Lecture Notes in Computer Science, pages 324–336. Springer, 2015.  doi:10.1007/978-3-662-47666-6\\_26.
  * [39] Yuanbo Li, Qirun Zhang, and Thomas W. Reps.  Fast graph simplification for interleaved Dyck-reachability.  In Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020, pages 780–793. ACM, 2020.  doi:10.1145/3385412.3386021.
  * [40] Yuanbo Li, Qirun Zhang, and Thomas W. Reps.  On the complexity of bidirected interleaved Dyck-reachability.  Proc. ACM Program. Lang., 5(POPL):1–28, 2021.  doi:10.1145/3434340.
  * [41] Markus Lohrey and Benjamin Steinberg.  An automata theoretic approach to the generalized word problem in graphs of groups.  Proceedings of the American Mathematical Society, 138(2):445–453, 2010.  doi:10.1090/S0002-9939-09-10126-0.
  * [42] 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.  doi:10.1016/0001-8708(82)90048-2.
  * [43] Derek C. Oppen.  A $2^{2^{2^{pn}}}$ upper bound on the complexity of Presburger arithmetic.  J. Comput. Syst. Sci., 16(3):323–332, 1978.  doi:10.1016/0022-0000(78)90021-1.
  * [44] Laurent Pierre.  Rational indexes of generators of the cone of context-free languages.  Theoretical Computer Science, 95(2):279–305, 1992.  doi:10.1016/0304-3975(92)90269-L.
  * [45] Emil L. Post.  Recursive unsolvability of a problem of Thue.  J. Symb. Log., 12(1):1–11, 1947.  doi:10.2307/2267170.
  * [46] Loïc Pottier.  Minimal solutions of linear Diophantine systems: Bounds and algorithms.  In Rewriting Techniques and Applications, 4th International Conference, RTA-91, Como, Italy, April 10-12, 1991, Proceedings, volume 488 of Lecture Notes in Computer Science, pages 162–173. Springer, 1991.  doi:10.1007/3-540-53904-2\\_94.
  * [47] Klaus Reinhardt.  Reachability in Petri nets with inhibitor arcs.  Electron. Notes Theor. Comput. Sci., 223:239–264, 2008.  doi:10.1016/j.entcs.2008.12.042.
  * [48] Sylvain Schmitz.  Complexity hierarchies beyond elementary.  ACM Trans. Comput. Theory, 8(1):3:1–3:36, 2016.  doi:10.1145/2858784.
  * [49] Sylvain Schmitz.  Algorithmic Complexity of Well-Quasi-Orders. (Complexité algorithmique des beaux pré-ordres).  2017\.  URL: https://tel.archives-ouvertes.fr/tel-01663266.
  * [50] Sylvain Schmitz and Georg Zetzsche.  Coverability is undecidable in one-dimensional pushdown vector addition systems with resets.  In Reachability Problems - 13th International Conference, RP 2019, Brussels, Belgium, September 11-13, 2019, Proceedings, volume 11674 of Lecture Notes in Computer Science, pages 193–201. Springer, 2019.  doi:10.1007/978-3-030-30806-3\\_15.
  * [51] Guoqing Xu, Atanas Rountev, and Manu Sridharan.  Scaling CFL-reachability-based points-to analysis using context-sensitive must-not-alias analysis.  In ECOOP 2009 - Object-Oriented Programming, 23rd European Conference, Genoa, Italy, July 6-10, 2009. Proceedings, volume 5653 of Lecture Notes in Computer Science, pages 98–122. Springer, 2009.  doi:10.1007/978-3-642-03013-0\\_6.
  * [52] Dacong Yan, Guoqing Xu, and Atanas Rountev.  Demand-driven context-sensitive alias analysis for Java.  In Proceedings of the 20th International Symposium on Software Testing and Analysis, ISSTA 2011, Toronto, ON, Canada, July 17-21, 2011, pages 155–165. ACM, 2011.  doi:10.1145/2001420.2001440.
  * [53] Georg Zetzsche.  The emptiness problem for valence automata over graph monoids.  Information and Computation, 277, 2021.  doi:10.1016/j.ic.2020.104583.
  * [54] Qirun Zhang, Michael R. Lyu, Hao Yuan, and Zhendong Su.  Fast algorithms for Dyck-CFL-reachability with applications to alias analysis.  In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, Seattle, WA, USA, June 16-19, 2013, pages 435–446. ACM, 2013.  doi:10.1145/2491956.2462159.
  * [55] Qirun Zhang and Zhendong Su.  Context-sensitive data-dependence analysis via linear conjunctive language reachability.  In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 344–358. ACM, 2017.  doi:10.1145/3009837.3009848.

##  Appendix A Additional material for Section 4

See 4.1

######  Proof A.1.

Let $M\subseteq S$ be the set of minimal nonzero elements of
$S\subseteq\mathbb{N}^{k}$. Clearly $M^{*}\subseteq S$ because $S$ is a
submonoid. For the converse, let $\bm{s}$ be a minimal element in $S\setminus
M^{*}$. Then, there exists $\bm{m}\in M^{*}$ such that $\bm{m}<\bm{s}$. Since
$S$ is subtractive we know that $\bm{s}-\bm{m}\in S$. Moreover, by minimality
of $\bm{s}$ in $S\setminus M^{*}$ we obtain $\bm{s}-\bm{m}\in M^{*}$. But then
$\bm{s}=(\bm{s}-\bm{m})+\bm{m}\in M^{*}$ is a contradiction.

See 4.2

######  Proof A.2.

We may clearly assume that $R$ is symmetric. Let $\mathcal{S}=\langle
V\rangle\cap(\mathbb{N}^{d}\times\mathbb{N}^{d})$ where $V=R\cup E$,
$E=\\{(\bm{e}_{i},\bm{e}_{i})\mid i\in[1,d]\\}$, and $\langle\cdot\rangle$
denotes the generated subgroup. We claim that $\mathcal{S}$ is a congruence on
$\mathbb{N}^{d}$. First, $\mathcal{S}$ is a subtractive submonoid and
therefore $(\bm{x},\bm{y}),(\bm{z},\bm{z})\in\mathcal{S}$ implies
$(\bm{x}+\bm{z},\bm{y}+\bm{z})\in\mathcal{S}$. It is a reflexive and symmetric
relation since $E^{*}\subseteq\mathcal{S}$ and $V$ is symmetric. For
transitivity suppose $(\bm{x},\bm{y}),(\bm{y},\bm{z})\in\mathcal{S}$, and
therefore $(\bm{x}+\bm{y},\bm{y}+\bm{z})\in\mathcal{S}$. Since
$(\bm{y},\bm{y})\in\mathcal{S}$ and $\mathcal{S}$ is subtractive we also have
$(\bm{x},\bm{z})\in\mathcal{S}$.

Next observe that $\mathcal{Q}\subseteq\mathcal{S}$ since $\mathcal{S}$ is a
congruence containing $R$. Furthermore
$\mathcal{Q}_{\bm{b}{\uparrow}}\subseteq\mathcal{S}$ for any $\bm{b}$ since
the subgroup $\langle V\rangle$ is clearly invariant under translation by
$(\bm{b},\bm{b})$. It remains to find a vector $\bm{b}$ such that
$\mathcal{Q}_{\bm{b}{\uparrow}}\supseteq\mathcal{S}$. Let
$A\in\mathbb{Z}^{2d\times 2|V|}$ be the matrix with the $2|V|$ many column
vectors $\\{\bm{v},-\bm{v}\mid\bm{v}\in V\\}$. Then we can write:

$\mathcal{S}=\\{\bm{y}\in\mathbb{N}^{2d}\mid\exists\bm{x}\in\mathbb{N}^{2|V|}\colon
A\bm{x}=\bm{y}\\}.$

The set of all solutions $(\bm{x},\bm{y})\in\mathbb{N}^{2d+2|V|}$ of
$A\bm{x}-\bm{y}=\bm{0}$ forms a submonoid generated by the finite set
$M^{\prime}$ of its minimal nonzero solutions. By [46, Theorem 1] the norm of
each minimal solution in $M^{\prime}$ is bounded by
$\lambda=(1+\|A\|_{1,\infty})^{2d}$ where $\|A\|_{1,\infty}$ is the maximal
1-norm of a column in $A$. By projecting $M^{\prime}$ to the
$\bm{y}$-components we obtain the set $M$ of minimal nonzero solutions of
$\mathcal{S}$, which generates $\mathcal{S}$. Hence, each vector
$(\bm{s},\bm{t})\in M$ can be written as

$(\bm{s},\bm{t})=\sum_{\bm{v}\in
V}\lambda_{\bm{s},\bm{t},\bm{v}}\cdot\bm{v}\quad\text{for some
}\lambda_{\bm{s},\bm{t},\bm{p}}\in\mathbb{Z},\,\bm{v}\in V$ (1)

where the absolute values of the coefficients $\lambda_{\bm{s},\bm{t},\bm{p}}$
are bounded by $\lambda$. Define the vector

$(\bm{b},\bm{b})=\lambda\cdot\sum_{\bm{v}\in V}\bm{v}.$ (2)

By summing (1) and (2), we can write $(\bm{b},\bm{b})+(\bm{s},\bm{t})$ as a
non-negative linear combination of vectors $\bm{p}\in V$. This proves
$(\bm{s},\bm{t})\in\mathcal{Q}_{\bm{b}{\uparrow}}$ and hence also
$\mathcal{S}=M^{*}\subseteq\mathcal{Q}_{\bm{b}{\uparrow}}$.

#### Elimination ideals and ideal quotients

Let $I\subseteq\mathbb{Z}[\bm{x}]$ is be an ideal, given by a basis $B$, and
$\bm{y}$ is a subsequence of $\bm{x}$. To compute a Gröbner basis for the
elimination ideal $I\cap\mathbb{Z}[\bm{y}]$, we first turn $B$ into a Gröbner
basis with respect to a monomial ordering where the variables in $\bm{y}$ are
ordered greater than the variables in $\bm{x}\setminus\bm{y}$. Then
$B\cap\mathbb{Z}[\bm{y}]$ is a Gröbner basis for $I\cap\mathbb{Z}[\bm{y}]$ [2,
Proposition 6.15].

Next we explain how to compute a Gröbner basis for the ideal quotient
$I:\bm{x}^{\bm{b}}$ for a given vector $\bm{b}\in\mathbb{N}^{d}$. Observe that
$I:\bm{x}^{\bm{b}}$ is a projection of the set of all solutions
$(p_{0},\bm{q})\in\mathbb{Z}[\bm{x}]^{1+|B|}$ of the polynomial equation
$p\bm{x}^{\bm{b}}+\sum_{f\in B}q_{f}f=0$. In general, if
$\bm{f}=(f_{1},\ldots,f_{n})\in\mathbb{Z}[\bm{x}]^{n}$ is a tuple of
polynomials, then the solutions
$(q_{1},\dots,q_{n})\in\mathbb{Z}[\bm{x}]^{n}$, called syzygies, to the
polynomial equation $q_{1}f_{1}+\dots+q_{n}f_{n}=0$ form a submodule of
$\mathbb{Z}[\bm{x}]^{n}$, denoted $\mathrm{Syz}(\bm{f})$. This means,
$\mathrm{Syz}(\bm{f})$ is closed under componentwise addition in
$\mathbb{Z}[\bm{x}]^{n}$ and is closed under scalar multiplication by
$\mathbb{Z}[\bm{x}]$-polynomials. Given $\bm{f}\in\mathbb{Z}[\bm{x}]^{n}$, one
can compute a generating set for $\mathrm{Syz}(\bm{f})$ in elementary time [2,
Section 6.1], i.e. tuples
$\bm{g}_{1},\dots,\bm{g}_{m}\in\mathbb{Z}[\bm{x}]^{n}$ such that
$\mathrm{Syz}(\bm{f})=\\{\sum_{i=1}^{m}h_{i}\bm{g}_{i}\mid
h_{1},\dots,h_{m}\in\mathbb{Z}[\bm{x}]\\}$.

See 4.3

######  Proof A.3.

Let $L=\bm{b}+P^{*}$ be the region. We can treat the cases
$L=\bm{b}{\uparrow}$ and $L=P^{*}$ separately since
$\mathcal{Q}_{L}=(\mathcal{Q}_{\bm{b}{\uparrow}})_{P^{*}}$. For
$L=\bm{b}{\uparrow}$ we compute the reduced Gröbner basis $B_{\bm{b}}$ for the
ideal quotient $I:\bm{x}^{\bm{b}}$ and turn the basis back into a finite
congruence basis
$R_{\bm{b}}=\\{(\bm{s},\bm{t})\mid\bm{x}^{\bm{s}}-\bm{x}^{\bm{t}}\in
B_{\bm{b}}\\}$. For $L=P^{*}$ we compute the reduced Gröbner basis
$B_{\bm{y}}$ for the elimination ideal $I\cap\mathbb{Z}[\bm{y}]$ where
$\bm{y}$ contains the variables in $\bm{x}$ that do not correspond to a unit
vector in $P$. Then we turn the basis $B_{\bm{y}}$ back into a finite
congruence basis
$R_{\bm{y}}=\\{(\bm{s},\bm{t})\mid\bm{x}^{\bm{s}}-\bm{x}^{\bm{t}}\in
B_{\bm{y}}\\}$.

See 4.4

######  Proof A.4.

As described before we can assume that $R$ is finite by replacing each linear
set $\bm{b}+\\{\bm{p}_{1},\dots,\bm{p}_{n}\\}^{*}$ by the vectors
$\bm{b},\bm{b}+\bm{p}_{1},\dots,\bm{b}+\bm{p}_{n}$. We proceed by induction
over $d$. It suffices to give a reduction from an instance in dimension $d$ to
instances in dimension $d-1$ whose running time is bounded by an elementary
function independent from $d$.

First, we compute a vector $\bm{b}\in\mathbb{N}^{d}$ and a finite set
$M\subseteq\mathbb{N}^{2d}$ of vectors of elementary norm such that
$\mathcal{Q}_{\bm{b}{\uparrow}}=M^{*}$ by Lemma 4.2. This yields a
representation for $\mathcal{Q}\cap L_{0}^{2}=(\bm{b},\bm{b})+M^{*}$ on the
region $L_{0}=\bm{b}{\uparrow}$. The complement
$\mathbb{N}^{d}\setminus(\bm{b}{\uparrow})$ can be decomposed into at most
$d\cdot\|\bm{b}\|$ many regions of dimension $d-1$: Let
$i_{1},i_{2},\dots,i_{n}\in[1,d]$ be arbitrary such that
$\bm{b}=\bm{e}_{i_{1}}+\dots+\bm{e}_{i_{n}}$ where $n\leq d\cdot\|\bm{b}\|$.
Then $\mathbb{N}^{d}\setminus(\bm{b}{\uparrow})=\bigcup_{j=1}^{n}L_{j}$ where
the region $L_{j}=\bm{b}_{j}+P_{j}^{*}$ is defined by
$\bm{b}_{j}=\bm{e}_{i_{1}}+\dots+\bm{e}_{i_{j-1}}$ and
$P_{j}=\\{\bm{e}_{k}\mid k\neq i_{j}\\}^{*}$. Using Lemma 4.3 we compute bases
for the congruences $\mathcal{Q}_{L_{j}}$ on the submonoids $P_{j}^{*}$. By
projecting away some zero-component we can compute a semilinear representation
for $\mathcal{Q}_{L_{j}}$ by induction hypothesis, and thus also for
$\mathcal{Q}\cap L_{j}^{2}=(\bm{b}_{j},\bm{b}_{j})+\mathcal{Q}_{L_{j}}$.

Finally, given a decomposition $\mathbb{N}^{d}=\bigcup_{j=0}^{n}L_{j}$ into
regions and semilinear representations for the restrictions
$Q_{j}=\mathcal{Q}\cap L_{j}^{2}$, we can define the entire congruence
$\mathcal{Q}$ in Presburger arithmetic. Suppose that
$\bm{s}\sim_{\mathcal{Q}}\bm{t}$ and consider a minimal length sequence
$\bm{w}_{1},\dots,\bm{w}_{\ell}\in\mathbb{N}^{d}$ where $\bm{s}=\bm{w}_{1}$,
$\bm{w}_{\ell}=\bm{t}$, and for each $i\in[1,\ell-1]$, either there exists
$(\bm{u},\bm{v})\in R$ with $\bm{w}_{i}-\bm{u}\geq\bm{0}$ and
$\bm{w}_{i+1}=\bm{w}_{i}-\bm{u}+\bm{v}$, or $(\bm{w}_{i},\bm{w}_{i+1})\in
Q_{k}$ for some $k\in[0,n]$. Then for each region $L_{k}$ the derivation
contains at most 2 elements $\bm{w}_{i}$ belonging to $L_{k}$ since we could
otherwise replace a subsequence $\bm{w}_{i},\bm{w}_{i+1},\dots,\bm{w}_{j}$
where $\bm{w}_{i},\bm{w}_{j}\in L_{k}$ by the pair $\bm{w}_{i},\bm{w}_{j}$
related in $Q_{k}$. Therefore, we can express $\bm{u}\sim_{\mathcal{Q}}\bm{v}$
in Presburger arithmetic by quantifying over sequences of length at most
$2(n+1)$ where adjacent elements are related by an $R$-step or in some
relation $Q_{k}$. This concludes the proof.

See 4.9

######  Proof A.5.

Let us bound the length of the chain $R_{1}\subsetneq
R_{2}\subsetneq\dots\subsetneq R_{\ell}$ computed by Algorithm 1. Let $n$ be
the size of the PVAS. Then $\|R_{i}\|\leq\exp^{c_{2}d}(\|R_{i-1}\|)$ for all
$i\in[1,\ell]$ where $c_{2}$ is an absolute constant. This follows from
Theorem 4.4 and the fact that the update in line 7 takes elementary time.
Hence, we can bound $\|R_{i}\|\leq\exp^{c_{2}id}(n)$ for all $i\in[1,\ell]$.
This in turn implies that the chain $R_{1},R_{2},\dots$ is $(g,n)$-controlled
where $g(n)=\exp^{c_{3}d}(n)$ for some absolute constant $c_{3}$. Here we use
the fact that the set difference $S_{2}\setminus S_{1}$ of two semilinear sets
contains a vector of elementary norm in $\|S_{1}\|+\|S_{2}\|$, if it is empty.
It is easy to verify that $\exp(x)=2^{x}\leq
2^{x+1}(x+1)-1=H^{\omega^{2}}(x)$. Since the Hardy functions satisfy
$(h^{\alpha})^{\beta}(x)=h^{\alpha\cdot\beta}(x)$ (under specific conditions
on $\alpha\cdot\beta$, see [48, Eq. (3.12)]) the chain is indeed
$(H^{\omega^{2}c_{3}d},n)$-controlled. By Lemma 4.8 its length $\ell$ is
bounded by

$\displaystyle 1+(H^{\omega^{2}c_{3}d})^{\omega^{4d}}(4dn)$ $\displaystyle\leq
1+(H^{\omega^{2}c_{3}d})^{\omega^{4d}}(4dnc_{3})$ $\displaystyle\leq
1+(H^{\omega^{3}})^{\omega^{4d}}(4dnc_{3})$
$\displaystyle=1+H^{\omega^{4d+3}}(4dnc_{3}).$

It remains to argue that the running time is basically determined by $\ell$.
Iteration $i$ in Algorithm 1 takes $\exp^{O(d)}(\|R_{i-1}\|)$ time, where
$\|R_{i-1}\|$ can be bounded by $\exp^{O(\ell d)}(n)$. Hence the total running
time of the algorithm is $\ell\cdot\exp^{O(\ell d)}(n)$. By [48, Lemma 4.6] we
obtain the complexity bounds ${\small\mathsf{F}}_{4d+3}$ in fixed dimension
$d$ and ${\small\mathsf{F}}_{\omega}$ in arbitrary dimension.

##  Appendix B Additional material for Section 5

######  Lemma B.1.

Consider any two states $p,q$ and natural number $k\in\mathbb{N}$, and let
$\gamma_{k}(p,q)=(a,b)$ and $\delta_{k}(p)=c$, with $-\infty<a$. Either $a>c$,
or $a=c$ and $b=\omega$.

######  Proof B.2.

Since $-\infty<a$, there is a path $P\in\\{p\rightsquigarrow q\\}_{k}$. Assume
that $a\leq c$, and let $C\in\\{p\rightsquigarrow p\\}_{k}$ be a path with
$w(C)>0$. Then for any natural number $\ell\in\mathbb{N}$, we can construct a
path $H_{\ell}$ with $\mathit{m}(H_{\ell})=c$ and $w(H_{\ell})\geq\ell$ by
traversing $C$ sufficiently many times and then following $P$ to $q$. The
sequence of paths $(H_{\ell})_{\ell}$ witnesses that $a=c$ and $b=\omega$, as
desired.

######  Proof B.3 (Proof of Lemma 5.5).

Since $b>-\infty$, we have $\\{p\rightsquigarrow q\\}_{k}\neq\emptyset$. Since
$\mathcal{P}$ is bidirected, we also have $\\{q\rightsquigarrow
p\\}_{k}\neq\emptyset$, and thus there exists a path
$P^{\prime}\in\\{q\rightsquigarrow p\\}_{k}$. It is known that shortest paths
in pushdown systems of $n$ states have length upper bounded by $2^{O(n^{2})}$
(this follows from the pumping lemma for context-free languages [27, Lemma
6.1]), hence $|P^{\prime}|\leq 2^{\alpha n^{2}}$, for some constant $\alpha$.
Now assume that $b>|P^{\prime}|$, and thus we have a path
$P\in\\{p\rightsquigarrow q\\}_{k}$ with $\mathit{m}(P)=a$ and
$w(P)>|P^{\prime}|$. We construct a cycle $C\in\\{p\rightsquigarrow p\\}_{k}$
as $C=P\circ P^{\prime}$. We have $w(C)=w(P)+w(P^{\prime})\geq
w(P)-|P^{\prime}|>0$ and
$\mathit{m}(C)\geq\min(\mathit{m}(P),w(P)-|P^{\prime}|)=a$. Thus, there exists
a cycle starting in $p$ whose minimal counter value is $\geq a$ and which has
positive effect. Therefore, if we set $c=\delta_{k}(p)$, then we have shown
$a\leq c$. By Lemma B.1 we have $a=c$ and $b=\omega$.

######  Proof B.4 (Proof of Lemma 5.6).

By the definition of $\gamma_{k}$, we have that $\mathit{m}(P)<a$. Let $H$ be
a path that witnesses $\gamma_{k}(p,q)$, and $C=P\circ\overline{H}$, and
notice that $C\in\\{p\rightsquigarrow p\\}_{k}$. Moreover,
$w(C)=w(P)+w(\overline{H})=w(P)-b>0$, while
$\mathit{m}(C)=\min(\mathit{m}(P),w(P)+\mathit{m}(\overline{H}))$. Note that
$\mathit{m}(\overline{H})=a-b$, and thus $w(P)+\mathit{m}(\overline{H})>a$,
concluding that $\mathit{m}(C)=\mathit{m}(P)$. Thus
$\delta_{k}(p)\geq\mathit{m}(P)$, as desired.

######  Proof B.5 (Proof of Lemma 5.7).

Consider a shortest path $P\in\\{p\rightsquigarrow p\\}_{k}$ with $w(P)>0$,
and we first argue that $\mathit{MaxSH}(P)\leq 2n^{2}$. Indeed, if
$\mathit{MaxSH}(P)>2n^{2}$, then there is a pair of states $(q,r)$ that
appears three times in $P$, $(q_{i},r_{i})_{1\leq i\leq 3}$, such that, for
each $i\in\\{1,2\\}$, $P$ has subpaths $P^{q}_{i}\colon q_{i}\rightsquigarrow
q_{i+1}$ and $P^{r}_{i}\colon r_{i+1}\rightsquigarrow r_{i}$ such that
removing $P^{q}_{i}$ and $P^{r}_{i}$ yields another path
$P^{\prime}_{i}\in\\{p\rightsquigarrow p\\}_{<k}$. Moreover, let
$P^{\prime}_{1,2}\in\\{p\rightsquigarrow p\\}_{<k}$ be the path obtained by
removing $P^{q}_{i}$ and $P^{r}_{i}$ for both $i=1$ and $i=2$. Then each of
the three paths $P^{\prime}_{1},P^{\prime}_{2},P^{\prime}_{1,2}$ is strictly
shorter than $P$ and therefore
$w(P^{\prime}_{1})=w(P^{\prime}_{2})=w(P^{\prime}_{1,2})=0$: If one of these
paths had non-zero effect, then this path or its reverse would be a shorter
cycle on $p$ than $P$ with positive effect. However, observe that

$w(P)=w(P^{\prime}_{1,2})\leavevmode\nobreak\ +\leavevmode\nobreak\
\underbrace{(w(P^{\prime}_{1})-w(P^{\prime}_{1,2}))}_{\text{effect of
$P^{q}_{1}$ and $P^{r}_{1}$}}\leavevmode\nobreak\ +\leavevmode\nobreak\
\underbrace{(w(P^{\prime}_{2})-w(P^{\prime}_{1,2}))}_{\text{effect of
$P^{q}_{2}$ and $P^{r}_{2}$}},$

and since the right-hand side vanishes, we have $w(P)=0$, a contradiction.
Thus $\mathit{MaxSH}(P)\leq 2n^{2}$.

Next, we argue that $|P|\leq 2n|\Gamma|^{2n^{2}}$. Indeed, if this is not the
case, then $P$ traverses two cycles in the configuration space, i.e., it
contains two subpaths $H_{s}\in\\{s\rightsquigarrow s\\}$ and
$H_{t}\in\\{t\rightsquigarrow t\\}$ such that, removing either or both of
them, results in another path in $\\{p\rightsquigarrow p\\}_{k^{\prime}}$,
where $k^{\prime}=\mathit{MaxSH}(P)$. An analogous argument to the above
concludes that we can remove one or both of them, to obtain a shorter positive
cycle from $p$ to itself.

Since $|\Gamma|=2$, this means $|P|=2^{O(n^{2})}$, which implies the statement
of the lemma (witnessed by the worst case where $P$ decrements the counter in
each step).

######  Proof B.6 (Proof of Lemma 5.9).

Since $\mathcal{P}$ is bidirected, it suffices to argue that for every two
states $p,q$, and $\sigma\in\Gamma_{\bot}$, if we have a path $\langle
p,\sigma\rangle\xrightarrow{}\langle p,v,\sigma\rangle\xrightarrow{}\langle
q,\sigma\rangle$ then we also have a path $\langle
q,\sigma\rangle\xrightarrow{}\langle q,u,\sigma\rangle\xrightarrow{}\langle
p,\sigma\rangle$. Observe that the condition for having the former path is
that $\gamma_{k-1}(u,v)=(a,\\_)$, for some $-\infty<a$, i.e., we have
$\\{u\rightsquigarrow v\\}_{k-1}\neq\emptyset$. Since $\mathcal{P}$ is
bidirected, we also have $\\{v\rightsquigarrow u\\}_{k-1}\neq\emptyset$, and
thus the latter path is also present in $G_{k}$.

######  Proof B.7 (Proof of Lemma 5.10).

The statement holds clearly for $k=0$. Now we argue that the statement also
holds for arbitrary $k$, given that it holds for $k-1$. In turn, it suffices
to show that, for every two states $p,q$, for every path
$P\in\\{p\rightsquigarrow q\\}_{k-1}$ and $\sigma\in\Gamma_{\bot}$, we have a
path $P^{\prime}\in\\{\langle p,\sigma\rangle\rightsquigarrow\langle
q,\sigma\rangle\\}^{G_{k}}$ that is contained in
$G_{k}\downharpoonright\sigma$ and such that $P\leq P^{\prime}$. This is
sufficient because for any paths $P_{1}$, $P_{2}$, $P_{1}^{\prime}$,
$P^{\prime}_{2}$ with $P_{1}\leq P^{\prime}_{1}$ and $P_{2}\leq
P^{\prime}_{2}$, we have $P_{1}\circ P_{2}\leq P^{\prime}_{1}\circ
P^{\prime}_{2}$.

Let $\gamma_{k-1}(p,q)=(a,b)$ and $\delta_{k-1}(p)=c$, and by the induction
hypothesis we have $(a,b)=\gamma^{G_{k-1}}(\langle p,\bot\rangle,\langle
q,\bot\rangle)$ and $c=\delta^{G_{k-1}}(\langle p,\bot\rangle)$. In
particular, this implies that $\mathit{m}(P)\leq a$. We distinguish the
following cases.

  * •

$b=\omega$. Due to Lemma B.1, we have $c=a$. We construct $P^{\prime}$ by
traversing the loop $\langle p,\sigma\rangle\xrightarrow{c}\langle
p^{\prime},\sigma\rangle\xrightarrow{-c+1}\langle p,\sigma\rangle$
sufficiently many times, and then taking the edges $\langle
p,\sigma\rangle\xrightarrow{a}\langle p,q,\sigma\rangle\xrightarrow{-a}\langle
q,\sigma\rangle$, to obtain $P\leq P^{\prime}$.

  * •

$b<\omega$ and $w(P)\leq b$. We construct $P^{\prime}$ by traversing the edges
$\langle p,\sigma\rangle\xrightarrow{a}\langle
p,q,\sigma\rangle\xrightarrow{-a+b}\langle q,\sigma\rangle$, to obtain $P\leq
P^{\prime}$.

  * •

$b<\omega$ and $w(P)>b$. Due to Lemma 5.6, we have that $\mathit{m}(P)<c$. We
construct $P^{\prime}$ by traversing the loop $\langle
p,\sigma\rangle\xrightarrow{c}\langle
p^{\prime},\sigma\rangle\xrightarrow{-c+1}\langle p,\sigma\rangle$
sufficiently many times, and then taking the edges $\langle
p,\sigma\rangle\xrightarrow{a}\langle
p,q,\sigma\rangle\xrightarrow{-a+b}\langle q,\sigma\rangle$, to obtain $P\leq
P^{\prime}$.

######  Proof B.8 (Proof of Lemma 5.11).

Due to Lemma 5.4, Lemma 5.5 and Lemma 5.7, all elements of the summary
functions $\gamma_{k}$ and $\delta_{k}$ that are finite are bounded in
absolute value by $2^{O(n^{2})}$, and thus each iteration takes polynomial
space. Since for every $k>0$, the algorithm proceeds in the next iteration iff
$\gamma_{k-1}<\gamma_{k}$ or $\delta_{k-1}<\delta_{k}$, we conclude that the
algorithm terminates within $2^{O(n^{2})}$ iterations.

#### Computing $\gamma^{G}$ and $\delta^{G}$.

Here we present an algorithm behind Lemma 5.8.

Let $n=|V|$ be the number of nodes in $G$. Given a simple cycle $C$ of $G$
with $w(C)>0$, we call a node $x$ in $C$ critical if the path $C_{x}$ obtained
by traversing $C$ starting from $x$ is such that $\mathit{m}(C_{x})=0$. Note
that every positive simple cycle has at least one critical node. We assume
without loss of generality that $G$ consists of a single (strongly) connected
component, as otherwise we can repeat the computation on each component of $G$
independently. Given a pair of values $(a,b)\in(\mathbb{Z}_{\leq
0}\cup\\{-\infty\\})\times(\mathbb{Z}\cup\\{-\infty\\})$ and an integer
$c\in\mathbb{Z}$, we define the extend operation $\odot$ as

$(a,b)\odot c=(\min(a,b+c),b+c).$

The extend operation is monotonic, i.e. $(a,b)\leq(a^{\prime},b^{\prime})$
implies $(a,b)\odot c\leq(a^{\prime},b^{\prime})\odot c$. The algorithm
manipulates a graph data structure $G^{\prime}$, initially identical to $G$,
as follows.

  1. 1.

We perform a standard Bellman-Ford computation on $G^{\prime}$, and detect
whether there exists a positive cycle $C$. If so, we identify a critical node
$x$ of $C$. We remove the edges outgoing $x$ from $G^{\prime}$, and repeat
this step.

  2. 2.

Let $X$ be the set of critical nodes identified in the previous step, and
$G^{\prime}=(V^{\prime},E^{\prime},w^{\prime})$ the graph data structure at
the end of that step (note that $V^{\prime}=V$). For every node $u$, we
compute $\delta^{G}(u)$ and $\gamma^{G}(u,v)$ for all nodes $v\in V^{\prime}$,
as follows.

    1. (a)

We initialize a map data structure $\mathit{DS}\colon V\to(\mathbb{Z}_{\leq
0}\cup\\{-\infty\\})\times(\mathbb{Z}\cup\\{-\infty\\})$ with
$\mathit{DS}(u)=(0,0)$ and $\mathit{DS}(v)=(-\infty,-\infty)$ for all nodes
$v\neq u$. We then perform $n-1$ relaxation steps as follows. In each step, we
iterate over all edges $(y,v)\in E^{\prime}$, and let
$(a^{\prime},b^{\prime})=\mathit{DS}(y)\odot w^{\prime}(y,v)$. If
$\mathit{DS}(v)<(a^{\prime},b^{\prime})$, we update $\mathit{DS}(v)$ with
$(a^{\prime},b^{\prime})$.

    2. (b)

We compute $c=\min(\\{a\colon x\in X\text{ and }\mathit{DS}(x)=(a,\\_)\\})$,
and report that $\delta^{G}(u)=c$. Given a node $v$, let
$\mathit{DS}(v)=(a_{v},b_{v})$ at the end of the previous step. If $a_{v}\leq
c$, we report that $\gamma^{G}(u,v)=(c,\omega)$. Otherwise, we report that
$\gamma^{G}(u,v)=\mathit{DS}(v)$.

The algorithm clearly operates in polynomial time in the size of $G$, thus it
remains to argue about the correctness. We start with a straightforward lemma.

######  Lemma B.9.

At the end of Item 2a above, for every node $v$ we have
$\mathit{DS}(v)=\gamma^{G^{\prime}}(u,v)$.

######  Proof B.10.

For a natural number $i\in\mathbb{N}$, we let $\\{u\rightsquigarrow
v\\}^{G^{\prime}}_{i}$ be the paths in $\\{u\rightsquigarrow
v\\}^{G^{\prime}}$ of length $\leq i$. and similarly denote by
$\gamma^{G^{\prime}}_{i}$ the corresponding summary function restricted to
paths in $\\{u\rightsquigarrow v\\}^{G^{\prime}}_{i}$. We argue that the
following assertions hold for all nodes $v$.

  1. 1.

At all times, we have $\mathit{DS}(v)\leq\gamma^{G^{\prime}}(u,v)$.

  2. 2.

For all $i\in\\{0,\dots,n-1\\}$, at the end of iteration $i$, we have
$\gamma^{G^{\prime}}_{i}(u,v)\leq\mathit{DS}(v)$.

Note that since $G^{\prime}$ does not have positive cycles, Item 2 implies
that, in fact, $\gamma^{G^{\prime}}(u,v)\leq\mathit{DS}(v)$, and hence the two
items imply that $\gamma^{G^{\prime}}_{i}(u,v)=\mathit{DS}(v)$. We argue about
each item separately.

  1. 1.

The statement clearly holds after the initialization of $\mathit{DS}$ with
$\mathit{DS}(u)=0$ and $\mathit{DS}(v)=-\infty$ for all nodes $v\neq u$. Now
consider a point in which $\mathit{DS}(v)$ is updated with
$\mathit{DS}(y)\odot w^{\prime}(y,v)$, and assume that the statement holds for
$\mathit{DS}(y)$. Thus we have a path $P\in\\{u\rightsquigarrow
y\\}^{G^{\prime}}$ with $\mathit{DS}(y)\leq(\mathit{m}(P),w(P))$. We obtain a
path $H\in\\{u\rightsquigarrow v\\}^{G^{\prime}}$ by extending $P$ with the
edge $(y,v)$. Observe that
$\mathit{m}(H)=\min(\mathit{m}(P),w(P)+w^{\prime}(y,v))$ and
$w(H)=w(P)+w^{\prime}(y,v)$. Hence
$(\mathit{m}(H),w(H))=(\mathit{m}(P),w(P))\odot w^{\prime}(y,v)$, and thus
after the update we have $\mathit{DS}(v)\leq\gamma^{G^{\prime}}(u,v)$ by
monotonicity of $\odot$.

  2. 2.

The statement clearly holds after the initialization of $\mathit{DS}$, i.e.,
in iteration $0$. Now assume it holds for some iteration $i-1$, for $i>0$, and
we argue that it holds for iteration $i$. Let $P$ be a path witnessing
$\gamma^{G^{\prime}}_{i}(u,v)$. If $|P|<i$, the statement holds by the
induction hypothesis and the fact that $\mathit{DS}(v)$ can only increase over
the course of the algorithm. Otherwise we have $|P|=i$, and $P$ occurs by
extending a path $H$, having $|H|=i-1$, with an edge $(y,v)$. By the induction
hypothesis, we have $(\mathit{m}(H),w(H))\leq\mathit{DS}(y)$. After the
algorithm has processed the edge $(y,v)$, we have $(\mathit{m}(H),w(H))\odot
w^{\prime}(y,v)\leq\mathit{DS}(v)$, and thus
$(\mathit{m}(P),w(P))\leq\mathit{DS}(v)$.

The desired result follows.

The following lemma yields the correctness of the algorithm.

######  Lemma B.11.

Consider two nodes $u,v$ and let $\gamma^{G}(u,v)=(a,b)$ and
$\delta^{G}(u)=c$. The following assertions hold.

  1. 1.

$c=\min(\\{a^{\prime}\colon x\in X\text{ and
}\gamma^{G^{\prime}}(u,x)=(a^{\prime},\\_)\\})$.

  2. 2.

Either $a=c$ and $b=\omega$ or $a>c$ and $\gamma^{G^{\prime}}(u,v)=(a,b)$.

######  Proof B.12.

We argue about each item separately.

  1. 1.

Since $G^{\prime}$ is a subgraph of $G$, we clearly have
$c\geq\min(\\{a^{\prime}\colon x\in X\text{ and
}\gamma^{G^{\prime}}(u,x)=(a^{\prime},\\_)\\})$, witnessed by a path that
reaches such a node $x$, traverses a positive cycle on which $x$ is critical
sufficiently many times, and then returns to $u$. We now argue that
$c\leq\min(\\{a^{\prime}\colon x\in X\text{ and
}\gamma^{G^{\prime}}(u,x)=(a^{\prime},\\_)\\})$. Indeed, let $P$ be a path
witnessing $\delta^{G}(u)$, and thus $\mathit{m}(P)=c$ and $w(P)>0$. Since $P$
traverses a positive cycle and there are no positive cycles in $G^{\prime}$,
$P$ must contain a node $x\in X$, thus
$\mathit{m}(P)\leq\min(\\{a^{\prime}\colon x\in X\text{ and
}\gamma^{G^{\prime}}(u,x)=(a^{\prime},\\_)\\})$, and hence
$c\leq\min(\\{a^{\prime}\colon x\in X\text{ and
}\gamma^{G^{\prime}}(u,x)=(a^{\prime},\\_)\\})$, as desired.

  2. 2.

Due to Lemma B.1 and the previous item, either $a=c$ and $b=\omega$, or $a>c$.
In the latter case there is a path $P$ witnessing $\gamma^{G}(u,v)=(a,b)$
which does not contain any node in $X$. Hence $P$ is a path in $G^{\prime}$,
and thus $\gamma^{G^{\prime}}(u,v)=(a,b)$.

#### Exponential stack height

We remark that even in 1 dimension, runs that witness reachability might
require an exponential height on the stack. As a simple example, consider a
PVASS $\mathcal{P}$ with transitions (i) $p\xrightarrow{\sigma}p^{\prime}$,
(ii) $p^{\prime}\xrightarrow{1}p$ (iii) $q\xrightarrow{\sigma}q^{\prime}$,
(iv) $q^{\prime}\xrightarrow{1}q$, as well as their bidirected variants (we
use $\sigma$ to denote pushing on the stack). Moreover, $p$ can reach $q$ via
an exponentially long path (that only uses polynomial stack height) which
decreases the counter in almost every step in the first half of the path, and
increases the counter in almost every step in the second half. This effect can
be easily generated by serially connecting two similar gadgets: each gadget
uses the stack as a binary counter, which, before it ticks, it decrements (for
the first gadget) and increments (for the second gadget) the PVASS counter (we
may simply make the two gadgets use different stack symbols to easily discard
paths that might alternate between the two due to bidirectedness). Note that
$q$ is reachable from $p$, but any witness run requires to initially traverse
the $p\xrightarrow{\sigma}p^{\prime}\xrightarrow{1}p$ cycle exponentially many
times in order to cross the exponentially deep valley generated by the two
gadgets. In effect, this results in increasing the stack height by an
exponential amount.

##  Appendix C Additional material for Section 6

See 6.1

######  Proof C.1.

We say that a gadget $G$ is $i$-neutral if
$(s,\bm{u},w)\xrightarrow{*}_{G}(t,\bm{v},w^{\prime})$ implies that $\bm{u}$
is $i$-initialized if and only if $\bm{v}$ is $i$-initialized. Observe that
the statement implies that $G_{k}$ is $k$-neutral since both $[0,\dots,0]$ and
$[0,\dots,0,\exp^{k}(n)]$ are $k$-initialized.

We proceed by induction over $k$ where the case $k=1$ is clear and we assume
$k>1$. It is easy to verify the existence of the runs
$(q_{0},[0,\dots,0],w)\xrightarrow{*}_{G_{k}}(q_{5},[0,\dots,0,\exp^{k}(n)],w)$,
which traverses the gadget Inck exactly $\exp^{k}(n)-1$ times. It remains to
verify that these are the only $k$-initialized runs from $q_{0}$ to $q_{5}$.
To this end, we decompose such a run into subruns, along the several
subgadgets it traverses. By arguing that all subgadgets are $(k-1)$-neutral we
can conclude that all subruns must be $(k-1)$-initialized so that we can apply
the induction hypothesis to the subruns.

First consider the gadgets $Z_{k-1}$ and Inck. The only $(k-1)$-initialized
runs in $Z_{k-1}$ between its terminal states, say $s$ and $t$, are the runs
of the form

$(s,[0,\dots,0],w)\xrightarrow{*}_{Z_{k-1}}(t,[0,\dots,0],w)\quad\text{for
}w\in\Gamma_{k-1}^{*},$

since $G_{k-1}$ satisfies the induction hypothesis and is $(k-1)$-neutral.
Moreover, we claim that the only $(k-1)$-initialized runs in Inck from $p_{0}$
to $p_{4}$ are the runs of the form

$(p_{0},[0,\dots,0,x_{k}],w\texttt{0}\texttt{1}^{\ell})\xrightarrow{*}_{\text{Inc}_{k}}(p_{4},[0,\dots,0,x_{k}+1],w\texttt{1}\texttt{0}^{\ell})$
(3)

for $w\in\Gamma_{k-1}^{*}$ and $\ell\leq\exp^{k-1}(n)$. This follows from the
previous statement for $Z_{k-1}$, the fact that the stack determines how often
the $p_{1}$-loop is executed and the fact that the $p_{2}$-loop must be
repeated until $c_{k-1}=0$.

Now consider a $k$-initialized run in $G_{k}$ from $q_{0}$ to $q_{5}$. It can
be decomposed into subruns which traverse the gadgets $G_{k-1}$,
$\bar{G}_{k-1}$ and $Z_{k-1}$, and subruns that do not manipulate the counters
$c_{j},\bar{c}_{j}$ with $j<k-1$. In particular, all these subruns are
$(k-1)$-initialized, which allows us to apply the uniqueness properties for
$G_{k-1}$ and $Z_{k-1}$: The $Z_{k-1}$-runs must start and end with a vector
$[0,\dots,0,x_{k}]$ whereas the $G_{k-1}$-runs must start with a vector
$[0,\dots,0,x_{k}]$ and end with $[0,\dots,\exp^{k-1}(n),x_{k}]$. This in turn
implies that the loops on $q_{1}$ and $q_{3}$ must be executed exactly
$\exp^{k-1}(n)$ times. The gadget Inck must be executed exactly
$\exp^{k}(n)-1$ times, considering that the binary counter on the stack must
be incremented from $\texttt{0}^{\exp^{k-1}(n)}$ to
$\texttt{1}^{\exp^{k-1}(n)}$ according to (3).

See 6.2

######  Proof C.2.

Again we proceed by induction over $k$ where $k=1$ is clear. For $k>1$
consider a $\leftrightarrow_{G_{k}}$-derivation witnessing
$(s,\bm{u},w)\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{G_{k}}(t,\bm{v},w^{\prime})$,
with the minimal number of $\leftarrow_{G_{k}}$-steps. Whenever the derivation
passes through a subgadget $G_{k-1}$ or $\bar{G}_{k-1}$, this part can be
replaced by a forward derivation by induction hypothesis. Moreover, the
$\leftrightarrow_{G_{k}}$-derivation cannot contain subruns which enter and
exit a subgadget $G_{k-1}$ or $\bar{G}_{k-1}$ through the same terminal state
since, again by induction hypothesis, such a subrun could be cut out, reducing
the number of reverse transitions. Hence, the
$\leftrightarrow_{G_{k}}$-derivation can only contain reverse transitions
which are not contained in a subgadget $G_{k-1}$ or $\bar{G}_{k-1}$. Consider
the first occurrence of a reverse transition $\bar{\tau}$. By a case
distinction, one can argue that $\bar{\tau}$ must always be preceded by
$\tau$, and hence we can cancel $\tau$ and $\bar{\tau}$. If $\tau$ is the loop
on $q_{1}$ then the occurrence of $\bar{\tau}$ must be preceded by either
$\tau$ itself, in which case $\tau$ and $\bar{\tau}$ can be cancelled, or a
run through $G_{k-1}$. However, after executing $G_{k-1}$ the counter
$\bar{c}_{k-1}$ must be zero and $\bar{\tau}$ cannot decrement
$\bar{c}_{k-1}$. Similar arguments hold for the loops on $q_{3}$ and $p_{1}$,
and the transitions $p_{3}\to p_{4}$ and $q_{3}\to q_{4}$. If $\tau$ is the
loop on $p_{2}$ then $\bar{\tau}$ is either preceded by $\tau$ or by the
transition $p_{1}\to p_{2}$. However, since the transition $p_{1}\to p_{2}$
pushes 1 the symbol 0 cannot be popped by $\bar{\tau}$.

In a very similar fashion we can prove the second statement, by considering a
$\leftrightarrow_{G_{k}}$-cycle with the minimal number of backward
transitions. Using the induction hypothesis we can cut out cycles on the
gadgets $G_{k-1}$ and $\bar{G}_{k-1}$, and replace bidirected derivations
passing through $G_{k-1}$ or $\bar{G}_{k-1}$ by forward derivations. It
remains to deal with backward transitions, which can be done with the same
arguments as above.

##  Appendix D Failure of a ${\small\mathsf{PSPACE}}$ lower bound technique

The paper [15] presents a ${\small\mathsf{PSPACE}}$-hardness proof for the
coverability problem in $1$-PVASS that could be considered a candidate to show
${\small\mathsf{PSPACE}}$-hardness of coverability (or just reachability) in
bidirected $1$-PVASS. However, it fails for non-obvious reasons. Here, we will
briefly outline why it fails. More specifically, we argue that simply making
the $1$-PVASS from that proof bidirected (by adding backwards edges) will not
yield a correct reduction. We assume familiarity with the construction from
[15].

The reduction in [15] reduces from the alternating subset sum problem. Here,
we are given numbers $a_{1},a^{\prime}_{1},\ldots,a_{k},a^{\prime}_{k}$,
$e_{1},e^{\prime}_{1},\ldots,e_{k},e^{\prime}_{k}$, and $s$ in $\mathbb{N}$
(in binary) and we want to decide whether

$\forall x_{1}\in\\{a_{1},a^{\prime}_{1}\\}\leavevmode\nobreak\ \exists
y_{1}\in\\{e_{1},e^{\prime}_{1}\\}\cdots\forall
x_{k}\in\\{a_{k},a^{\prime}_{k}\\}\leavevmode\nobreak\ \exists
y_{k}\in\\{e_{k},e^{\prime}_{k}\\}\colon\leavevmode\nobreak\
x_{1}+y_{1}+\cdots+x_{k}+y_{k}=s.$

This can be seen as a two-player game with a universal player that picks each
$x_{i}\in\\{a_{i},a^{\prime}_{i}\\}$ and an existential player that picks each
$y_{i}\in\\{e_{i},e^{\prime}_{i}\\}$. The instance is positive if the
existential player has a winning strategy, which means that it ensures
$x_{1}+y_{1}+\cdots+x_{k}+y_{k}=s$.

We say that a sequence of transitions in a PVASS is a _pseudo-run_ if the
counter is allowed to go below zero. The 1-PVASS constructed in [15] has the
property that each pseudo-run $(q_{0},\varepsilon,0)\to(q_{f},\varepsilon,m)$
corresponds to a strategy for the existential player. Moreover, it is a run if
it is indeed a winning strategy for the existential player.

Now suppose that (i) every play will overshoot $s$, i.e.
$x_{1}+y_{1}+\cdots+x_{k}+y_{k}>s$ (in particular, there is no winning
strategy), but (ii) there are two strategies for $E$ that will, with the same
moves by $A$, overshoot in distinct ways. Specifically, there are
$x_{i}\in\\{a_{i},a^{\prime}_{i}\\}$ for $i\in[1,k]$ and
$y_{i}\in\\{e_{i},e^{\prime}_{i}\\}$ for $i\in[1,k-1]$ such that

$\displaystyle x_{1}+y_{1}+\cdots+x_{k}+e_{k}$ $\displaystyle>s$
$\displaystyle x_{1}+y_{1}+\cdots+x_{k}+e^{\prime}_{k}$ $\displaystyle>s$

and $e_{k}\neq e^{\prime}_{k}$. Then there are two runs in the constructed
$1$-PVASS of the form

$\displaystyle(q_{0},\varepsilon,0)\xrightarrow{*}(p,w,m)\xrightarrow{*}(q,w,m-\delta_{1})\leavevmode\nobreak\
\text{and}\leavevmode\nobreak\ (p,w,m)\xrightarrow{*}(q,w,m-\delta_{2}),$ (4)

where $\delta_{1}\neq\delta_{2}$. This is because at the top of the stack
(which then has the form $wv$ for some $v$), it is checked that each sum is at
least $s$. However, if the sum is more than $s$, this only leads to issues all
the way at the end of the run, because going above $s$ will remove too many
tokens to sustain a run to $(q_{f},\varepsilon,0)$. Therefore, in the
$1$-PVASS, there is no run in this case.

However, if we add backwards edges, the two runs in (4) allow us to create an
arbitrary supply of tokens: Suppose $\delta_{1}<\delta_{2}$ and set
$\delta=\delta_{2}-\delta_{1}>0$. Then we can execute:

$\displaystyle(p,w,m)\xrightarrow{*}(q,w,m-\delta_{1})\xrightarrow{*}(p,w,m-\delta_{1}+\delta_{2})=(p,w,m+\delta).$
(5)

And thus $(p,w,m)\xrightarrow{*}(p,w,m+\ell\delta)$ for every
$\ell\in\mathbb{N}$. However, in the constructed $1$-PVASS, it is easy to see
that for every reachable configuration $(r,v,n)$, there exists some
$n^{\prime}$ such that from $(r,v,n^{\prime})$, we can cover
$(q_{f},\varepsilon,0)$, this shows that we can cover $(q_{f},\varepsilon,0)$
even if there is no winning strategy.

pagestotal main.pgtpagestotal pagestotal0 pagestotal