1733 LABEL:LastPageOct. 30, 2020Jul. 20, 2021

# The Complexity of Reachability in
Affine Vector Addition Systems with States

Michael Blondin  Université de Sherbrooke, Canada
<EMAIL_ADDRESS>and  Mikhail Raskin  Technische Universität
München, Germany<EMAIL_ADDRESS>
###### Abstract.

Vector addition systems with states (VASS) are widely used for the formal
verification of concurrent systems. Given their tremendous computational
complexity, practical approaches have relied on techniques such as
reachability relaxations, e.g., allowing for negative intermediate counter
values. It is natural to question their feasibility for VASS enriched with
primitives that typically translate into undecidability. Spurred by this
concern, we pinpoint the complexity of integer relaxations with respect to
arbitrary classes of affine operations.

More specifically, we provide a trichotomy on the complexity of integer
reachability in VASS extended with affine operations (affine VASS). Namely, we
show that it is -complete for VASS with resets, -complete for VASS with
(pseudo-)transfers and VASS with (pseudo-)copies, and undecidable for any
other class. We further present a dichotomy for standard reachability in
affine VASS: it is decidable for VASS with permutations, and undecidable for
any other class. This yields a complete and unified complexity landscape of
reachability in affine VASS. We also consider the reachability problem
parameterized by a fixed affine VASS, rather than a class, and we show that
the complexity landscape is arbitrary in this setting.

###### Key words and phrases:

vector addition system, affine transformation, reachability, computational
complexity

M. Blondin was supported by the Fonds de recherche du Québec – Nature et
technologies (FRQNT) and by a Discovery Grant from the Natural Sciences and
Engineering Research Council of Canada (NSERC)

M. Raskin was upported by the European Research Council (ERC) under the
European Union’s Horizon 2020 research and innovation programme under grant
agreement No 787367 (PaVeS)

##  1\. Introduction

_Vector addition systems with states (VASS)_ , which can equivalently be seen
as Petri nets, form a widespread general model of infinite-state systems with
countless applications ranging from the verification of concurrent programs to
the modeling of biological, chemical and business processes (see, e.g., [GS92,
KKW14, EGLM17, HGD08, van98]). They comprise a finite-state controller with
counters ranging over $\mathbb{N}$ and updated via instructions of the form
$x\leftarrow x+c$ which are executable if $x+c\geq 0$. The central decision
problem concerning VASS is the _reachability problem_ : given configurations
$x$ and $y$, is it possible to reach $y$ starting from $x$? Such queries
allow, e.g., to verify whether unsafe states can be reached in concurrent
programs. The notorious difficulty of the reachability problem led to many
proofs of its decidability over the last decades [ST77, May81, Kos82, Lam92,
Ler10, Ler11, Ler12]. While the problem has been known to be -hard since 1976
[Lip76], its computational complexity has remained unknown until very
recently, where it was shown to be -hard [CLL+19] and solvable in Ackermannian
time [LS15, LS19].

Given the potential applications on the one hand, and the tremendously high
complexity on the other hand, researchers have investigated relaxations of
VASS in search of a tradeoff between expressiveness and algorithmic
complexity. Two such relaxations consist in permitting either:

  1. (1)

transitions to be executed fractionally, and consequently counters to range
over $\mathbb{Q}_{\geq 0}$ (_continuous reachability_); or

  2. (2)

counters to range over $\mathbb{Z}$ (_integer reachability_).

In both cases, the complexity drops drastically: continuous reachability is
¶-complete and -complete for Petri nets and VASS respectively [FH15, BH17],
while integer reachability is -complete for both models [HH14, CHH18].
Moreover, these two types of reachability have been used successfully to prove
safety of real-world instances like multithreaded program skeletons, e.g., see
[ELM+14, ALW16, BFHH17].

Although VASS are versatile, they are sometimes too limited to model common
primitives. Consequently, their modeling power has been extended with various
operations. For example, _(multi-)transfers_ , i.e., operations of the form

$x\leftarrow x+\sum_{i=1}^{n}y_{i};\ y_{1}\leftarrow 0;\ y_{2}\leftarrow 0;\
\cdots;\ y_{n}\leftarrow 0,$

allow, e.g., for the verification of multi-threaded C and Java program
skeletons with communication primitives [KKW14, DRV02]. Another example is the
case of _resets_ , i.e., operations of the form $x\leftarrow 0$, which allow,
e.g., for the validation of some business processes [WvdAtHE09], and the
generation of program loop invariants [SK19]. Many such extensions fall under
the generic family of _affine VASS_ , i.e., VASS with instructions of the form
$\bm{x}\leftarrow\mathbf{A}\cdot\bm{x}+\bm{b}$. As a general rule of thumb,
reachability is undecidable for essentially any class of affine VASS
introduced in the literature; in particular, for transfers and resets [AK76,
DFPS98].

Given the success of relaxations for the practical analysis of (standard)
VASS, it is tempting to employ the same approach for affine VASS.
Unfortunately, continuous reachability becomes undecidable for mild affine
extensions such as resets and transfers. However, _integer reachability_ was
recently shown decidable for affine operations such as resets (-complete) and
transfers (-complete) [HH14, BHM18]. While such complexity results do not
translate immediately into practical procedures, they arguably guide the
design of algorithmic verification strategies.

Contribution. Thus, these recent results raise two natural questions: for
_what classes_ of affine VASS is integer reachability decidable? And, whenever
it is decidable, what is its _exact_ computational complexity? We fully answer
these questions in this paper by giving a precise trichotomy: integer
reachability is -complete for VASS with resets, -complete for VASS with
(pseudo-)transfers and VASS with (pseudo-)copies, and undecidable for _any_
other class. In particular, this answers a question left open in [BHM18]:
integer reachability is undecidable for _any_ class of affine VASS with
_infinite_ matrix monoid.

This clear complexity landscape is obtained by formalizing classes of affine
VASS and by carefully analyzing the structure of arbitrary affine
transformations; which could be of independent interest. In particular, it
enables us to prove a dichotomy on _(standard) reachability_ for affine VASS:
it is decidable for VASS with permutations, and undecidable for _any_ other
class. To the best of our knowledge, this is the first proof of the folkore
rule of thumb stating that “reachability is undecidable for essentially any
class of affine VASS”.

We further complement these trichotomy and dichotomy by showing that the
(integer or standard) reachability problem has an arbitrary complexity when it
is parameterized by a fixed affine VASS rather than a fixed class.

Related work. Our work is related to [BHM18] which shows that integer
reachability is decidable for affine VASS whose matrix monoid is finite
(refined to by [BHK+20]); and more particularly -complete in general for VASS
with transfers and VASS with copies. While it is also recalled in [BHM18] that
integer reachability is undecidable in general for affine VASS, the authors do
not provide any necessary condition for undecidability to hold. Moreover, the
complexity landscape for affine VASS with finite monoids is left blurred,
e.g., it does not give necessary conditions for -hardness results to hold, and
the complexity remains unknown for monoids with negative coefficients. This
paper completes the work initiated in [BHM18] by providing a unified
framework, which includes the notion of _matrix class_ , that allows us to
precisely characterize the complexity of integer reachability for _any_ class
of affine VASS.

Our work is also loosely related to a broader line of research on (variants
of) affine VASS dealing with, e.g., modeling power [Val78], accelerability
[FL02], formal languages [CFM12], coverability [BFP12], and the complexity of
integer reachability for restricted counters [FGH13] and structures [IS16].

Structure of the paper. Section 2 introduces general notation and affine VASS.
In Section 3, we prove our main result, namely the complexity trichotomy for
integer reachability in affine VASS. In Section 4, we show a dichotomy on
(standard) reachability in affine VASS. In Section 5, we show that the
complexity of reachability can be arbitrary when fixing an affine VASS.
Finally, we conclude in Section 6. To avoid cluttering the presentation with
too many technical details, some of them are deffered to an appendix.

##  2\. Preliminaries

Notation. Let $\mathbb{Z}$, $\mathbb{N}$, $[a,b]$ and $[k]$ denote
respectively the sets $\\{\ldots,-1,0,1,\ldots\\}$, $\\{0,1,2,\ldots\\}$,
$\\{a,a+1,\ldots,b\\}$ and $[1,k]$. For every vectors
$\bm{u},\bm{v}\in\mathbb{Z}^{k}$, let $\bm{u}+\bm{v}$ be the vector
$\bm{w}\in\mathbb{Z}^{k}$ such that $\bm{w}(i)\coloneqq\bm{u}(i)+\bm{v}(i)$
for every $i\in[k]$. Let $\bm{e}_{i}$ be the unit vector such that
$\bm{e}_{i}(i)=1$ and $\bm{e}_{i}(j)=0$ for every $j\neq i$. We do not specify
the arity of $\bm{e}_{i}$ as we will use it without ambiguity in various
dimensions. For every square matrix $\mathbf{A}\in\mathbb{Z}^{k\times k}$, let
$\dim{\mathbf{A}}\coloneqq k$ and let

$\lVert\mathbf{A}\rVert\coloneqq\max\\{|\mathbf{A}_{i,j}|:i,j\in[k]\\}.$

We naturally extend the latter notation to any set $X$ of matrices, i.e.,
$\lVert X\rVert\coloneqq\sup\\{\lVert\mathbf{A}\rVert:\mathbf{A}\in X\\}$.
Throughout the paper, we will often refer to matrix and vector indices as
_counters_. We will also often describe permutations in cycle notation, where
elements are separated by semicolons for readability, e.g., $(i;j)$ denotes
the permutation that swaps $i$ and $j$.

Affine VASS. An _affine vector addition system with states (affine VASS)_ is a
tuple $\mathcal{V}=(d,Q,T)$ where:

  * •

$d\geq 1$ is the _number of counters_ of $\mathcal{V}$;

  * •

$Q$ is a finite set of elements called _control-states_ ;

  * •

$T\subseteq Q\times\mathbb{Z}^{d\times d}\times\mathbb{Z}^{d}\times Q$ is a
finite set of elements called _transitions_.

For every transition $t=(p,\mathbf{A},\bm{b},q)$, let
$\mathrm{src}(t)\coloneqq p$, $M(t)\coloneqq\mathbf{A}$,
$\Delta(t)\coloneqq\bm{b}$ and $\mathrm{tgt}(t)\coloneqq q$. A _configuration_
is a pair $(q,\bm{v})\in Q\times\mathbb{Z}^{d}$ written $q(\bm{v})$. For all
$t\in T$ and $\mathbb{D}\in\\{\mathbb{Z},\mathbb{N}\\}$, we write

$p(\bm{u})\xrightarrow{t}_{\mathbb{D}}q(\bm{v})$

if $\bm{u},\bm{v}\in\mathbb{D}^{d}$, $\mathrm{src}(t)=p$, $\mathrm{tgt}(t)=q$,
and $\bm{v}=M(t)\cdot\bm{u}+\Delta(t)$. The relation
$\xrightarrow{}_{\mathbb{D}}$ is naturally extended to sequences of
transitions, i.e., for every $w\in T^{k}$ we let

$\xrightarrow{w}_{\mathbb{D}}\ \coloneqq\
\xrightarrow{w_{k}}_{\mathbb{D}}\circ\cdots\circ\xrightarrow{w_{2}}_{\mathbb{D}}\circ\xrightarrow{w_{1}}_{\mathbb{D}}.$

Moreover, we write

$\displaystyle p(\bm{u})\xrightarrow{}_{\mathbb{D}}q(\bm{v})\ $ if
$p(\bm{u})\xrightarrow{\mathmakebox[8pt][c]{t}}_{\mathbb{D}}q(\bm{v})$ for
some $t\in T$, and $\displaystyle
p(\bm{u})\xrightarrow{*}_{\mathbb{D}}q(\bm{v})\ $ $\displaystyle\text{ if
$p(\bm{u})\xrightarrow{\mathmakebox[8pt][c]{w}}_{\mathbb{D}}q(\bm{v})$ for
some $w\in T^{*}$}.$

As an example, let us consider the affine VASS of Figure 1, i.e., where $d=2$,
$Q=\\{p,q,r\\}$ and $T$ is as depicted graphically. We have:

$p(3,1)\xrightarrow{s}_{\mathbb{Z}}q(1,0)\xrightarrow{t}_{\mathbb{Z}}r(1,0)\xrightarrow{u}_{\mathbb{Z}}q(1,1)\xrightarrow{t}_{\mathbb{Z}}r(2,0)\xrightarrow{u}_{\mathbb{Z}}q(2,2)\xrightarrow{t}_{\mathbb{Z}}r(4,0).$

More generally, $p(x,1)\xrightarrow{*}_{\mathbb{Z}}r(2^{k},0)$ for all
$x\in\mathbb{Z}$ and $k\in\mathbb{N}_{>0}$. However,
$p(3,0)\xrightarrow{s}_{\mathbb{N}}q(1,-1)$ does _not_ hold as counters are
not allowed to become negative under this semantics.

$p$$q$$r$$s\colon\begin{pmatrix}0&0\\\ 0&1\end{pmatrix},\begin{pmatrix}1\\\
-1\end{pmatrix}$ $t\colon\begin{pmatrix}1&1\\\
0&0\end{pmatrix},\begin{pmatrix}0\\\ 0\end{pmatrix}$
$u\colon\begin{pmatrix}1&0\\\ 1&0\end{pmatrix},\begin{pmatrix}0\\\
0\end{pmatrix}$ Figure 1. Example of an affine VASS.

Classes of matrices. Let us formalize the informal notion of _classes_ of
affine VASS, such as “VASS with resets”, “VASS with transfers”, “VASS with
doubling”, etc., used throughout the literature.

Such classes depend on the extra operations they provide, i.e., by their
affine transformations, and more precisely by their linear part (matrices)
rather than their additive part (vectors). Affine VASS extend standard VASS
since they always include the identity matrix, which amounts to not applying
any extra operation. Moreover, as transformations can be composed along
sequences of transitions, their matrices are closed under multiplication,
i.e., if matrices $M(s)$ and $M(t)$ are allowed on transitions $s$ and $t$ of
two affine VASS of a given class, then $M(s)\cdot M(t)$ is typically also
allowed in an affine VASS of the class as it is understood that $s$ and $t$
can be composed. In other words, matrices form a _monoid_. In addition,
classes of affine VASS typically considered do not pose restrictions on the
number of counters that can be used, or on the subset of counters on which
operations can be applied. In other words, their affine transformations can be
extended to _arbitrary dimensions_ and can be applied on _any subset of
counters_ , e.g., general “VASS with resets” allow to reset any counter, not
just say the first one.

We formalize these observations as follows. For every $k\geq 1$, let
$\mathbf{I}_{k}$ be the $k\times k$ identity matrix and let $\mathcal{S}_{k}$
denote the set of permutations over $[k]$. Let
$\mathbf{P}_{\sigma}\in{\\{0,1\\}}^{k\times k}$ be the permutation matrix of
$\sigma\in\mathcal{S}_{k}$. For every matrix $\mathbf{A}\in\mathbb{Z}^{k\times
k}$, every permutation $\sigma\in\mathcal{S}_{k}$ and every $n\geq 1$, let

$\sigma({\mathbf{A}})\coloneqq\mathbf{P}_{\sigma}\cdot\mathbf{A}\cdot\mathbf{P}_{\sigma^{-1}},$

and let ${\mathbf{A}}\\!\\!\restriction_{n}\in\mathbb{Z}^{(k+n)\times(k+n)}$
be the matrix such that:

${\mathbf{A}}\\!\\!\restriction_{n}\coloneqq\begin{pmatrix}\mathbf{A}&\mathbf{0}_{\phantom{n}}\\\
\mathbf{0}&\mathbf{I}_{n}\end{pmatrix}.$

A _class (of matrices)_ is a set of matrices
$\mathcal{C}\subseteq\bigcup_{k\geq 1}\mathbb{Z}^{k\times k}$ that satisfies
$\\{\sigma({\mathbf{A}}),{\mathbf{A}}\\!\\!\restriction_{n},\allowbreak\mathbf{I}_{n},\mathbf{A}\cdot\mathbf{B}\\}\subseteq\mathcal{C}$
for every $\mathbf{A},\mathbf{B}\in\mathcal{C}$, every
$\sigma\in\mathcal{S}_{\dim{\mathbf{A}}}$ and every $n\geq 1$. In other words,
$\mathcal{C}$ is closed under counter renaming; each matrix of $\mathcal{C}$
can be extended to larger dimensions; and $\mathcal{C}\cap\mathbb{Z}^{k\times
k}$ is a monoid under matrix multiplication for every $k\geq 1$.

Note that “counter renaming” amounts to choosing a set of counters on which to
apply a given transformation, i.e., it renames the counters, applies the
transformation, and renames the counters back to their original names. Let us
illustrate this. Consider the classical case of transfer VASS, i.e., where the
contents of a counter can be transferred onto another counter with operations
of the form “$x\leftarrow x+y;\ y\leftarrow 0$”. In matrix notation, this
amounts to:

$\mathbf{O}\coloneqq\begin{pmatrix}1&1\\\ 0&0\end{pmatrix}.$

Now, consider a system with three counters $c_{1}$, $c_{2}$ and $c_{3}$. This
system should be able to compute “$c_{1}\leftarrow c_{1}+c_{2}+c_{3};\
c_{2}\leftarrow 0;\ c_{3}\leftarrow 0$”, but matrix $\mathbf{O}$ cannot
achieve this on its own. However, it can be done with the following matrix:

$\mathbf{O}^{\prime}\coloneqq\begin{pmatrix}1&1&\textit{0}\\\
0&0&\textit{0}\\\
\textit{0}&\textit{0}&\textit{1}\end{pmatrix}\cdot\begin{pmatrix}1&\textit{0}&1\\\
\textit{0}&\textit{1}&\textit{0}\\\
0&\textit{0}&0\end{pmatrix}=\begin{pmatrix}1&1&1\\\ 0&0&0\\\
0&0&0\end{pmatrix}.$

We have
$\mathbf{O}^{\prime}={\mathbf{O}}\\!\\!\restriction_{1}\cdot\sigma({{\mathbf{O}}\\!\\!\restriction_{1}})$
where $\sigma\coloneqq(2;3)$. Thus, the operation can be achieved by any class
containing $\mathbf{O}$. The symmetric operation “$c_{3}\leftarrow
c_{1}+c_{2}+c_{3};\ c_{1}\leftarrow 0;\ c_{2}\leftarrow 0$”, e.g., can also be
achieved with appropriate permutations. Hence, this corresponds to the usual
notion of transfers: we are allowed to choose some counters and apply
transfers in either direction.

Note that requiring $\mathbf{P}_{\sigma}\cdot\mathbf{A}\in\mathcal{C}$ for
classes would be too strong as it would allow to permute the contents of
counters even for classes with no permutation matrix, such as resets.

Classes of interest. We say that a matrix $\mathbf{A}\in\mathbb{Z}^{k\times
k}$ is a _pseudo-reset_ , _pseudo-transfer_ or _pseudo-copy_ matrix if
$\mathbf{A}\in{\\{-1,0,1\\}}^{k\times k}$ and if it also satisfies the
following:

  * •

pseudo-reset matrix: $\mathbf{A}$ is a diagonal matrix;

  * •

pseudo-transfer matrix: $\mathbf{A}$ has at most one nonzero entry per column;

  * •

pseudo-copy matrix: $\mathbf{A}$ has at most one nonzero entry per row.

We omit the prefix “pseudo-” if $\mathbf{A}\in{\\{0,1\\}}^{k\times k}$. Note
that the sets of (pseudo-)reset matrices, (pseudo-)transfer matrices, and
(pseudo-)copy matrices all form classes. Moreover, (pseudo-)reset matrices are
both (pseudo-)transfer and (pseudo-)copy matrices.

Note that the terminology of “reset”, “transfer” and “copy” comes from the
fact that such matrices implement operations like “$x\leftarrow 0$”,
“$x\leftarrow x+y;\ y\leftarrow 0$” and “$x\leftarrow x;\ y\leftarrow x$”, as
achieved respectively by the matrices of transitions $s$ (_reset_), $t$
(_transfer_) and $u$ (_copy_) illustrated in Figure 1.

Reachability problems. We say that an affine VASS $\mathcal{V}=(k,Q,T)$
_belongs to_ a class of matrices $\mathcal{C}$ if $\\{M(t):t\in
T\\}\subseteq\mathcal{C}$, i.e., if all matrices appearing on its transitions
belong to $\mathcal{C}$. The _reachability problem_ and _integer reachability
problem_ for a fixed class $\mathcal{C}$ are defined as:

$\textsc{Reach}_{\mathcal{C}}$
---
Input: |  an affine VASS $\mathcal{V}$ that belongs to $\mathcal{C}$, and two configurations $p(\bm{u}),q(\bm{v})$;
Decide: |  $p(\bm{u})\xrightarrow{*}_{\mathbb{N}}q(\bm{v})$ in $\mathcal{V}$?

$\mathbb{Z}\text{-}\textsc{Reach}_{\mathcal{C}}$
---
Input: |  an affine VASS $\mathcal{V}$ that belongs to $\mathcal{C}$, and two configurations $p(\bm{u}),q(\bm{v})$;
Decide: |  $p(\bm{u})\xrightarrow{*}_{\mathbb{Z}}q(\bm{v})$ in $\mathcal{V}$?

##  3\. A complexity trichotomy for integer reachability

This section is devoted to the proof of our main result, namely the trichotomy
on $\mathbb{Z}\text{-}\textsc{Reach}_{\mathcal{C}}$:

######  Theorem 1.

The integer reachability problem
$\mathbb{Z}\text{-}\textsc{Reach}_{\mathcal{C}}$ is:

  1. (1)

-complete if $\mathcal{C}$ only contains reset matrices;

  2. (2)

-complete, otherwise, if either $\mathcal{C}$ only contains pseudo-transfer matrices or $\mathcal{C}$ only contains pseudo-copy matrices;

  3. (3)

Undecidable otherwise.

It is known from [HH14, Cor. 10] that -hardness holds for affine VASS using
only the identity matrix (recall that our definition of reset matrices include
the identity matrix), and that membership holds for any class of reset
matrices. Hence, 1 follows immediately. Thus, the rest of this section is
dedicated to proving 2 and 3.

###  3.1. PSPACE-hardness

For the rest of this subsection, let us fix some class $\mathcal{C}$ that
either only contains pseudo-transfer matrices or only contains pseudo-copy
matrices. We prove -hardness of
$\mathbb{Z}\text{-}\textsc{Reach}_{\mathcal{C}}$ by first proving that
-hardness holds if either:

  * •

$\mathcal{C}$ contains a matrix with an entry equal to $-1$; or

  * •

$\mathcal{C}$ contains a matrix with entries from $\\{0,1\\}$ and a nonzero
entry outside of its diagonal.

For these two cases, we first show that $\mathcal{C}$ can implement operations
$x\leftarrow-x$ or $(x,y)\leftarrow(y,x)$ respectively, i.e., _sign flips_ or
_swaps_. Essentially, each of these operations is sufficient to simulate
linear bounded automata. Before investigating these two cases, let us
carefully formalize what it means to implement an operation:

Let $f\colon\mathbb{Z}^{k}\mapsto\mathbb{Z}^{k}$ and let $\tau\in\\{0,?\\}$.
Given a set of counters $X\subseteq[m]$, let

$V_{X}\coloneqq\left\\{\bm{v}\in\mathbb{Z}^{m}:\bigwedge_{j\not\in
X}\bm{v}(j)=0\right\\}\text{ if }\tau=0,$

and let $V_{X}\coloneqq\mathbb{Z}^{m}$ otherwise. We say that $\mathcal{C}$
_$\tau$ -implements_ $f$ if for every $n\geq k$, there exist counters
$X=\\{x_{1},x_{2},\ldots,x_{n}\\}$, matrices
$\\{\mathbf{F}_{\sigma}:\sigma\in\mathcal{S}_{k}\\}\subseteq\mathcal{C}$ and
$m\geq n$ such that the following holds for every $\sigma\in\mathcal{S}_{k}$
and $\bm{v}\in V_{X}$:

  1. (1)

$\dim{\mathbf{F}_{\sigma}}=m$;

  2. (2)

$(\mathbf{F}_{\sigma}\cdot\bm{v})(x_{\sigma(i)})=f(x_{\sigma(1)},x_{\sigma(2)},\ldots,x_{\sigma(k)})(i)$
for all $i\in[k]$;

  3. (3)

$(\mathbf{F}_{\sigma}\cdot\bm{v})(x_{\sigma(i)})=\bm{v}(x_{\sigma(i)})$ for
every $i\not\in[k]$;

  4. (4)

$\mathbf{F}_{\sigma}\cdot\bm{v}\in V_{X}$.

We further say that $\mathcal{C}$ _implements_ $f$ if it either $0$-implements
or $?$-implements $f$.

Definition 3.1 2 and 3 state that it is possible to obtain arbitrarily many
counters $X$ such that $f$ can be applied on any $k$-subset of $X$, provided
that the counter values belong to $V_{X}$. Moreover, 4 states that vectors
resulting from applying operation $f$ also belong to $V_{X}$, which ensures
that $f$ can be applied arbitrarily many times. Note that 1 allows for extra
auxiliary counters whose values are only restricted by $V_{X}$.

Informally, $?$-implementation means that we use additional counters that can
hold arbitrary values, while $0$-implementation requires the extra counters to
be initialized with zeros but promises to keep them in this state. It turns
out that pseudo-transfer matrix classes $0$-implement the functions we need,
while pseudo-copy matrix classes $?$-implement them.

######  Proposition 2.

If $\mathcal{C}$ contains a matrix with some entry equal to $-1$, then it
implements sign flips, i.e., the operation $f\colon\mathbb{Z}\to\mathbb{Z}$
such that $f(x)\coloneqq-x$.

######  Proof 3.1.

Let $n\geq 1$ and $\mathbf{A}\in\mathcal{C}$ be such that
$\mathbf{A}_{a,b}=-1$ for some counters $a$ and $b$. Let
$d\coloneqq\dim{\mathbf{A}}$. We extend $\mathbf{A}$ with $n+2$ counters
$X^{\prime}\coloneqq X\cup\\{y,z\\}$, where $X\coloneqq\\{x_{i}:i\in[n]\\}$
are the counters for which we wish to implement sign flips, and $\\{y,z\\}$
are auxiliary counters. More formally, let
$\mathbf{A}^{\prime}\coloneqq{\mathbf{A}}\\!\\!\restriction_{n+2}$ where
$X^{\prime}=[d+1,d^{\prime}]$ and $d^{\prime}\coloneqq d+n+2$.

For every $s,t\in X^{\prime}$ such that $s\neq t$, let
$\mathbf{B}_{s,t}\coloneqq\pi_{s,t}(\mathbf{A}^{\prime})$ and let
$\mathbf{C}_{t}\coloneqq\sigma_{t}(\mathbf{A}^{\prime})$ where
$\pi_{s,t}\coloneqq(a;t)(b;s)$ and $\sigma_{t}\coloneqq(a;t)$. For every $x\in
X$, let

$\mathbf{F}_{x}\coloneqq\begin{cases}\mathbf{B}_{z,x}\cdot\mathbf{B}_{y,z}\cdot\mathbf{B}_{x,y}&\text{if
$a\neq b$},\\\ \mathbf{C}_{x}&\text{otherwise}.\end{cases}$

Intuitively, $\mathbf{B}_{s,t}$ (resp. $\mathbf{C}_{t}$) flips the sign from
source counter $s$ (resp. $t$) to target counter $t$. If $a\neq b$, then
matrix $\mathbf{F}_{x}$ implements a sign flip in three steps using auxiliary
counters $y$ and $z$, as illustrated in Figure 2. Otherwise, $\mathbf{F}_{x}$
implements sign flip directly in one step.

$x$$y$$z$$\mathbf{B}_{x,y}$$\mathbf{B}_{y,z}$$\mathbf{B}_{z,x}$

$x$$y$$z$??????$\mathbf{B}_{x,y}$$\mathbf{B}_{y,z}$$\mathbf{B}_{z,x}$

Figure 2. Effect of applying $\mathbf{F}_{x}$ for the case $a\neq b$, where
the left (resp. right) diagram depicts the case where $\mathbf{A}$ is a
pseudo-transfer (resp. pseudo-copy) matrix. A solid or dashed edge from $s$ to
$t$ represents operation $s\leftarrow t$ or $s\leftarrow-t$ respectively.
Filled nodes indicate counters that necessarily hold $0$. Symbol “?” stands
for an integer whose value is irrelevant and depends on $\mathbf{A}$ and the
counter values.

Let us consider the case where $\mathbf{A}$ is a pseudo-transfer matrix. From
the definition of $\mathbf{B}_{s,t}$ and $\mathbf{C}_{t}$, it can be shown
that for every $s,t,u\in X^{\prime}$ such that $s\neq t$ and
$u\not\in\\{s,t\\}$, the following holds:

  1. (1)

$\mathbf{B}_{s,t}\cdot\bm{e}_{s}=\mathbf{C}_{t}\cdot\bm{e}_{t}=-\bm{e}_{t}$,
and

  2. (2)

$\mathbf{B}_{s,t}\cdot\bm{e}_{u}=\mathbf{C}_{t}\cdot\bm{e}_{u}=\bm{e}_{u}$.

Let us show that we $0$-implement sign flips, so let

$V\coloneqq\left\\{\bm{v}\in\mathbb{Z}^{d^{\prime}}:\bigwedge_{j\not\in
X}\bm{v}(j)=0\right\\}.$

Let $\bm{v}\in V$ and $x\in X$. By definition of $V$, $\bm{v}=\sum_{y\in
X}\bm{v}(y)\cdot\bm{e}_{y}$. Let $\bm{v}^{\prime}\coloneqq\sum_{j\in
X\setminus\\{x\\}}\bm{v}(j)\cdot\bm{e}_{j}$. Items 2, 3 and 4 of Definition
3.1 are satisfied since:

$\displaystyle\mathbf{F}_{x}\cdot\bm{v}$
$\displaystyle=\mathbf{F}_{x}\cdot\bm{v}(x)\cdot\bm{e}_{x}+\mathbf{F}_{x}\cdot\bm{v}^{\prime}$
$\displaystyle=\bm{v}(x)\cdot\mathbf{F}_{x}\cdot\bm{e}_{x}+\bm{v}^{\prime}$
(by 2 and def. of $\mathbf{F}_{x}$)
$\displaystyle=\bm{v}(x)\cdot-\bm{e}_{x}+\bm{v}^{\prime}$ (by 1, 2 and def. of
$\mathbf{F}_{x}$) $\displaystyle=-\bm{v}(x)\cdot\bm{e}_{x}+\bm{v}^{\prime}.$

The proof of 1 and 2, and the similar proof for the case where $\mathbf{A}$ is
a pseudo-copy matrix, are analogous (see Appendix A).

######  Proposition 3.

$\mathbb{Z}\text{-}\textsc{Reach}_{\mathcal{C}}$ is -hard if $\mathcal{C}$ has
a matrix with an entry equal to $-1$.

######  Proof 3.2.

We give a reduction, partially inspired by [BHM18, Thm. 10], from the
membership problem for linear bounded automata, which is -complete (e.g., see
[HU79, Sect. 9.3 and 13]).

Let $w\in{\\{0,1\\}}^{k}$ and let
$\mathcal{A}=(P,\Sigma,\delta,p_{\text{init}},p_{\text{acc}})$ be a linear
bounded automaton where:

  * •

$P$ is its finite set of control-states;

  * •

$\Sigma=\\{0,1\\}$ is its input and tape alphabet;

  * •

$\delta\colon P\times\Sigma\to
P\times\Sigma\times\\{\textsc{Left},\textsc{Right}\\}$ is its transition
function; and

  * •

$p_{\text{init}}$ and $p_{\text{acc}}$ are its initial and accepting control-
states, respectively.

We construct an affine VASS $\mathcal{V}=(d,Q,T)$ and configurations
$p(\bm{u})$, $q(\bm{v})$ such that $\mathcal{V}$ belongs to $\mathcal{C}$, and

$p(\bm{u})\xrightarrow{*}_{\mathbb{Z}}q(\bm{v})\iff\text{$\mathcal{A}$ accepts
$w$}.$

For every control-state $p$ and head position $j$ of $\mathcal{A}$, there is a
matching control-state in $\mathcal{V}$, i.e., $Q\coloneqq\\{q_{p,j}:p\in
P,1\leq j\leq k\\}\cup\overline{Q}$, where $\overline{Q}$ will be auxiliary
control-states. We associate two counters to each tape cell of $\mathcal{A}$,
i.e., $d\coloneqq 2\cdot k$. For readability, let us denote these counters
$\\{x_{j},y_{j}:j\in[k]\\}$.

We represent the contents of tape cell $i$ by the sign of counter $y_{j}$,
i.e., $y_{j}>0$ represents $0$, and $y_{j}<0$ represents $1$. We will ensure
that $y_{j}$ is never equal to $0$, which would otherwise be an undefined
representation. Since $\mathcal{V}$ cannot directly test the sign of a
counter, it will be possible for $\mathcal{V}$ to commit errors during the
simulation of $\mathcal{A}$. However, we will construct $\mathcal{V}$ in such
a way that erroneous simulations are detected.

The gadget depicted in Figure 3 simulates a transition of $\mathcal{A}$ in
three steps:

  * •

$x_{i}$ is incremented;

  * •

$y_{i}$ is incremented (resp. decremented) if the letter $a$ to be read is $0$
(resp. $1$);

  * •

the sign of $y_{i}$ is flipped if the letter $b$ to be written differs from
the letter $a$ to be read.

$q_{p,i}$$q_{p^{\prime},i+1}$$x_{i}\leftarrow x_{i}+1$$y_{i}\leftarrow
y_{i}+(-1)^{a}$$y_{i}\leftarrow(-1)^{b-a}\cdot y_{i}$ Figure 3. Gadget of
$\mathcal{V}$ simulating transition
$\delta(p,a)=(p^{\prime},b,\textsc{Right})$ of $\mathcal{A}$. The gadget for
direction Left is the same except for $q_{p^{\prime},i+1}$ which is replaced
by $q_{p^{\prime},i-1}$. Note that $a$ and $b$ are fixed, hence expressions
such as $(-1)^{a}$ are constants; they do not require exponentiation.

Let $\bm{u}\in\mathbb{Z}^{d}$ be the vector such that for every $j\in[k]$:

$\bm{u}(x_{j})\coloneqq 1\text{ and }\bm{u}(y_{j})\coloneqq(-1)^{w_{j}}.$

Provided that $\mathcal{V}$ starts in vector $\bm{u}$, we claim that:

  * •

$\bigwedge_{j=1}^{k}(|x_{j}|\geq|y_{j}|>0)$ is an invariant;

  * •

$\mathcal{V}$ has faithfully simulated $\mathcal{A}$ so far if and only if
$\bigwedge_{j=1}^{k}(|x_{j}|=|y_{j}|)$ holds;

  * •

if $\mathcal{V}$ has faithfully simulated $\mathcal{A}$ so far, then the sign
of $y_{j}$ represents $w_{j}$ for every $j\in[k]$.

Let us see why this claim holds. Let $i\in[k]$. Initially, we have
$|x_{i}|=|y_{i}|$ and the sign of $y_{i}$ set correctly. Assume we execute the
gadget of Figure 3, resulting in new values $x_{i}^{\prime}$ and
$y_{i}^{\prime}$. Let $\lambda\geq 0$ be such that $|x_{i}|=|y_{i}|+\lambda$.
Let $c\in\\{0,1\\}$ be the letter represented by $y_{i}$. If $c=a$, then
$|x_{i}^{\prime}|=|y_{i}^{\prime}|+\lambda$ and the sign of $y_{i}^{\prime}$
represents $b$ as desired. If $c\neq a$, then
$|x_{i}^{\prime}|=|y_{i}^{\prime}|+(\lambda+1)$. Thus, we have
$|x_{i}^{\prime}|=|y_{i}^{\prime}|$ if and only if no error was made before
and during the execution of the gadget.

From the above observations, we conclude that $\mathcal{A}$ accepts $w$ if and
only if there exist $i\in[k]$ and $\bm{v}\in\mathbb{Z}^{d}$ such that

$q_{p_{\text{init}},1}(\bm{u})\xrightarrow{*}_{\mathbb{Z}}q_{p_{\text{acc}},i}(\bm{v})$

and $|\bm{v}(x_{j})|=|\bm{v}(y_{j})|$ for every $j\in[k]$. This can be tested
using the gadget depicted in Figure 4, which:

  * •

detects nondeterministically that some control-state of the form
$q_{p_{\text{acc}},i}$ has been reached;

  * •

attempts to set $y_{j}$ to its absolute value for every $j\in[k]$;

  * •

decrements $x_{j}$ and $y_{j}$ simultaneously for every $j\in[k]$.

$r$$q_{p_{\text{acc}},i}$$q_{p_{\text{acc}},1}$$q_{p_{\text{acc}},k}$$y_{1}\leftarrow-
y_{1}$ $x_{1}\leftarrow x_{1}-1$
---
$y_{1}\leftarrow y_{1}-1$
$y_{k}\leftarrow-y_{k}$ $x_{k}\leftarrow x_{k}-1$
---
$y_{k}\leftarrow y_{k}-1$
Figure 4. Gadget of $\mathcal{V}$ for tesing whether $\mathcal{A}$ was
faithfully simulated and has accepted $w$.

Due to the above observations, it is _only_ possible to reach $r(\bm{0})$ if
$|x_{j}|=|y_{j}|$ for every $j\in[k]$ before entering the gadget of Figure 4.
Thus, we are done proving the reduction since $\mathcal{A}$ accepts $w$ if and
only if

$q_{p_{\text{init}},1}(\bm{u})\xrightarrow{*}_{\mathbb{Z}}r(\bm{0}).$

Sign flips. The above construction considers sign flips as a “native”
operation. However, this is not necessarily the case, and instead relies on
the fact that class $\mathcal{C}$ either $0$-implements or $?$-implements sign
flips, by Proposition 2. Thus, the reachability question must be changed to

$q_{p_{\text{init}},1}(\bm{u},\bm{0})\xrightarrow{*}_{\mathbb{Z}}r(\bm{0},\bm{0})$

to take auxiliary counters into account. Moreover, if $\mathcal{C}$
$?$-implements sign flips, then extra transitions
$(r,\mathbf{I},\bm{e}_{j},r)$ and $(r,\mathbf{I},-\bm{e}_{j},r)$ must be added
to $T$, for every auxiliary counter $j$, to allow counter $j$ to be set back
to $0$. Note that control-state $r$ can only be reached _after_ the simulation
of $\mathcal{A}$, hence it plays no role in the emulation of sign flips.
Moreover, if there is an error during the simulation of $\mathcal{A}$ and the
extra transitions set the auxiliary counters to zero, we will stil detect it
as the configuration will be of the form $r(\bm{w},\bm{0})$ where
$\bm{w}\neq\bm{0}$.

In the two forthcoming propositions, we prove -hardness of the remaining case.

######  Proposition 4.

If $\mathcal{C}$ contains a matrix with entries from $\\{0,1\\}$ and a nonzero
entry outside of its main diagonal, then it implements swaps, i.e., the
operation $f\colon\mathbb{Z}^{2}\to\mathbb{Z}^{2}$ such that
$f(x,y)\coloneqq(y,x)$.

######  Proof 3.3.

Let $n\geq 2$ and let $\mathbf{A}\in\mathcal{C}$ be a matrix with entries from
$\\{0,1\\}$ and a nonzero entry outside of its main diagonal. Let
$d\coloneqq\dim{\mathbf{A}}$. There exist $a,b\in[d]$ such that
$\mathbf{A}_{a,b}=1$ and $a\neq b$. Let us extend $\mathbf{A}$ with $n+1$
counters $X^{\prime}\coloneqq X\cup\\{z\\}$ where
$X\coloneqq\\{x_{i}:i\in[n]\\}$. More formally, let
$\mathbf{A}^{\prime}\coloneqq{\mathbf{A}}\\!\\!\restriction_{n+1}$,
$X^{\prime}=[d+1,d^{\prime}]$ and $d^{\prime}\coloneqq d+n+1$.

For all $s,t\in X^{\prime}$ such that $s\neq t$, let
$\mathbf{B}_{s,t}\coloneqq\pi_{s,t}(\mathbf{A}^{\prime})$ where
$\pi_{s,t}\coloneqq(b;s)(a;t)$. For every distinct counters $x,y\in X$, let

$\mathbf{F}_{x,y}\coloneqq\mathbf{B}_{z,x}\cdot\mathbf{B}_{x,y}\cdot\mathbf{B}_{y,z}.$

$x$$y$$z$$\mathbf{B}_{y,z}$$\mathbf{B}_{x,y}$$\mathbf{B}_{z,x}$

$x$$y$$z$???$\mathbf{B}_{y,z}$$\mathbf{B}_{x,y}$$\mathbf{B}_{z,x}$

Figure 5. Effect of applying $\mathbf{F}_{x,y}$, where the left (resp. right)
diagram depicts the case where $\mathbf{A}$ is a transfer (resp. copy) matrix.
An edge from counter $s$ to counter $t$ represents operation $s\leftarrow t$.
Filled nodes indicate counters that necessarily hold $0$. Symbol “?” stands
for an integer whose value is irrelevant and depends on $\mathbf{A}$ and the
counter values.

Intuitively, $\mathbf{B}_{s,t}$ moves the contents from some source counter
$s$ to some target counter $t$, and $\mathbf{F}_{x,y}$ implements a swap in
three steps using an auxiliary counter $z$ as depicted in Figure 5. In the
case where $\mathbf{A}$ is a transfer matrix, $\mathbf{B}_{s,t}$ resets $s$,
provided that $t$ held value $0$.

Let us consider the case where $\mathbf{A}$ is a transfer matrix. From the
definition of $\mathbf{B}_{s,t}$, it can be shown that for every $s,t,u\in
X^{\prime}$ such that $s\neq t$ and $u\not\in\\{s,t\\}$, the following holds:

  1. (1)

$\mathbf{B}_{s,t}\cdot\bm{e}_{s}=\bm{e}_{t}$, and

  2. (2)

$\mathbf{B}_{s,t}\cdot\bm{e}_{u}=\bm{e}_{u}$.

Let us show that we $0$-implement swaps, so let

$V_{X}\coloneqq\left\\{\bm{v}\in\mathbb{Z}^{d^{\prime}}:\bigwedge_{j\not\in
X}\bm{v}(j)=0\right\\}.$

Let $\bm{v}\in V_{X}$ and let $x,y\in X$ be such that $x\neq y$. By definition
of $V_{X}$, $\bm{v}=\sum_{j\in X}\bm{v}(j)\cdot\bm{e}_{j}$. Let

$\bm{v}^{\prime}\coloneqq\sum_{j\in
X\setminus\\{x,y\\}}\bm{v}(j)\cdot\bm{e}_{j}.$

Items 2, 3 and 4 of Definition 3.1 are satisfied since we obtain the following
by applications of 1 and 2:

$\displaystyle\mathbf{F}_{x,y}\cdot\bm{v}$
$\displaystyle=\mathbf{F}_{x,y}\cdot\left(\bm{v}(x)\cdot\bm{e}_{x}+\bm{v}(y)\cdot\bm{e}_{y}\right)+\mathbf{F}_{x,y}\cdot\bm{v}^{\prime}$
(by def. of $\bm{v}^{\prime}$)
$\displaystyle=\mathbf{F}_{x,y}\cdot\left(\bm{v}(x)\cdot\bm{e}_{x}+\bm{v}(y)\cdot\bm{e}_{y}\right)+\bm{v}^{\prime}$
(by 2 and def. of $\mathbf{F}_{x,y}$)
$\displaystyle=\mathbf{B}_{z,x}\cdot\mathbf{B}_{x,y}\cdot\mathbf{B}_{y,z}\cdot(\bm{v}(x)\cdot\bm{e}_{x}+\bm{v}(y)\cdot\bm{e}_{y})+\bm{v}^{\prime}$
(by def. of $\mathbf{F}_{x,y}$)
$\displaystyle=\mathbf{B}_{z,x}\cdot\mathbf{B}_{x,y}\cdot(\bm{v}(x)\cdot\bm{e}_{x}+\bm{v}(y)\cdot\bm{e}_{z})+\bm{v}^{\prime}$
(by 2 and 1)
$\displaystyle=\mathbf{B}_{z,x}\cdot(\bm{v}(x)\cdot\bm{e}_{y}+\bm{v}(y)\cdot\bm{e}_{z})+\bm{v}^{\prime}$
(by 1 and 2)
$\displaystyle=\bm{v}(x)\cdot\bm{e}_{y}+\bm{v}(y)\cdot\bm{e}_{x}+\bm{v}^{\prime}$
$\displaystyle\text{(by~{}\ref{itm:other} and~{}\ref{itm:src:tgt})}.$

The proof of 1 and 2, and the similar proof for the case where $\mathbf{A}$ is
a copy matrix, are analogous (see Appendix A).

######  Proposition 5.

$\mathbb{Z}\text{-}\textsc{Reach}_{\mathcal{C}}$ is -hard if $\mathcal{C}$
contains a matrix with entries from $\\{0,1\\}$ and a nonzero entry outside of
its main diagonal.

######  Proof 3.4.

It is shown in [BHMR19] that $\mathbb{Z}$-reachability is -hard for affine
VASS with swaps, using a reduction from the membership problem for linear
bounded automata.

Here, we may not have swaps as a “native” operation. However, by Proposition
4, class $\mathcal{C}$ implements swaps. Thus, as in the proof of Proposition
3, if the reachability question is of the form

$p(\bm{u})\xrightarrow{*}_{\mathbb{Z}}q(\bm{v}),$

then it must be changed to

$p(\bm{u},\bm{0})\xrightarrow{*}_{\mathbb{Z}}q(\bm{v},\bm{0}).$

Moreover, if the class $\mathcal{C}$ $?$-implements swaps, then new
transitions must be introduced to allow auxiliary counters to be set back to
$0$. Recall that under $?$-implementation, there is no requirement on the
value of the auxiliary counters, hence these new transitions do not interfere
with the emulation of swaps.

We now proceed to prove the main result of this subsection, namely Theorem 1
2:

######  Proof 3.5 (Proof of Theorem 1 2).

Let $\mathcal{M}_{k}\coloneqq\mathcal{C}\cap\mathbb{Z}^{k\times k}$ for every
$k\geq 1$. Theorem 7 of [BHM18] shows that
$\mathbb{Z}\text{-}\textsc{Reach}_{\mathcal{C}}$ belongs to if each
$\mathcal{M}_{k}$ is a finite monoid of at most exponential norm and size in
$k$. Let us show that this is the case. First, since $\mathcal{C}$ is a class
that contains only pseudo-transfer (reps. pseudo-copy) matrices, and since the
product of two such matrices remains so, $\mathcal{M}_{k}$ is a monoid which
is finite as $\mathcal{M}_{k}\subseteq\\{-1,0,1\\}^{k\times k}$. Moreover, by
definitions of pseudo-transfer and pseudo-copy matrices, each such matrix can
be described by cutting it into $k$ lines and specifying for each line either
the position of the unique nonzero entry (which is $-1$ or $1$), or the lack
of such entry. Therefore, for every $k\geq 1$, it is the case that
$\lVert\mathcal{M}_{k}\rVert\leq 1$ and

$\displaystyle|\mathcal{M}_{k}|$
$\displaystyle\leq(2k+1)^{k}\leq(4k)^{k}=2^{2k+k\log k}\leq
2^{\mathrm{poly}(k)}.$

It remains to show -hardness. By assumption, $\mathcal{C}$ contains a nonreset
matrix $\mathbf{A}$. Since $\lVert\mathcal{C}\rVert\leq 1$, we have
$\lVert\mathbf{A}\rVert=1$ as no class can be such that
$\lVert\mathcal{C}\rVert=0$. If $\mathbf{A}$ contains an entry equal to $-1$,
then we are done by Proposition 3. Otherwise, $\mathbf{A}$ only has entries
from $\\{0,1\\}$, and hence we are done by Proposition 5.

###  3.2. Undecidability

In this subsection, we first show that any class $\mathcal{C}$, that does not
satisfy the requirements for
$\mathbb{Z}\text{-}\textsc{Reach}_{\mathcal{C}}\in\\{\text{\NP-
complete},\allowbreak\text{\PSPACE-complete}\\}$, must be such that
$\lVert\mathcal{C}\rVert\geq 2$. We then show that this is sufficient to mimic
doubling, i.e., the operation $x\mapsto 2x$, even if $\mathcal{C}$ does not
contain a doubling matrix. In more details, we will (a) construct a matrix
$\mathbf{C}$ that provides a sufficiently fast growth; which will (b) allow us
to derive undecidability by revisiting a reduction from the Post
correspondence problem which depends on doubling.

######  Proposition 6.

Let $\mathcal{C}$ be a class that contains some matrices $\mathbf{A}$ and
$\mathbf{B}$ which are respectively not pseudo-copy and pseudo-transfer
matrices. It is the case that $\lVert\mathcal{C}\rVert\geq 2$.

######  Proof 3.6.

By assumption, $\mathbf{A}$ and $\mathbf{B}$ respectively have a row and a
column with at least two nonzero entries. We make use of the following lemma
shown in Appendix A:

> if $\mathcal{C}$ contains a matrix which has a row (resp. column) with at
> least two nonzero entries, then $\mathcal{C}$ also contains a matrix which
> has a row (resp. column) with at least two nonzero entries with the _same
> sign_.

Since $\mathcal{C}$ is a class, we can assume that
$\dim{\mathbf{A}}=\dim{\mathbf{B}}=d$ for some $d\geq 2$, as otherwise the
smallest matrix can be enlarged. Thus, there exist $i,i^{\prime},j,k\in[d]$
and $a,b,a^{\prime},b^{\prime}\neq 0$ such that:

  * •

$j\neq k$;

  * •

$\mathbf{A}_{i,j}=a$ and $\mathbf{A}_{i,k}=b$;

  * •

$\mathbf{B}_{j,i^{\prime}}=a^{\prime}$ and
$\mathbf{B}_{k,i^{\prime}}=b^{\prime}$; and

  * •

$a>0\iff b>0$ and $a^{\prime}>0\iff b^{\prime}>0$.

Note that the reason we can assume $\mathbf{A}$ and $\mathbf{B}$ to share
counters $j$ and $k$ is due to $\mathcal{C}$ being closed under counter
renaming.

We wish to obtain a matrix with entry

$\mathbf{A}_{i,j}\cdot\mathbf{B}_{j,i^{\prime}}+\mathbf{A}_{i,k}\cdot\mathbf{B}_{k,i^{\prime}}=a\cdot
a^{\prime}+b\cdot b^{\prime}.$

We cannot simply pick $\mathbf{A}\cdot\mathbf{B}$ as
$(\mathbf{A}\cdot\mathbf{B})_{i,i^{\prime}}$ may differ from this value due to
other nonzero entries. Hence, we rename all counters of $\mathbf{B}$, except
for $j$ and $k$, with fresh counters. This way, we avoid possible overlaps and
we can select precisely the four desired entries. More formally, let
$\mathbf{A}^{\prime}\coloneqq{\mathbf{A}}\\!\\!\restriction_{d}$,
$\mathbf{B}^{\prime}\coloneqq{\mathbf{B}}\\!\\!\restriction_{d}$ and
$\mathbf{C}\coloneqq\mathbf{A}^{\prime}\cdot\sigma({\mathbf{B}^{\prime}})$,
where $\sigma\colon[2d]\to[2d]$ is the permutation:

$\sigma\coloneqq\prod_{\ell\in[d]\setminus\\{j,k\\}}(\ell;\ell+d).$

Let $i^{\prime\prime}\coloneqq i^{\prime}+d$ if $i^{\prime}\not\in\\{j,k\\}$
and $i^{\prime\prime}\coloneqq i^{\prime}$ otherwise. We have:

$\displaystyle\mathbf{C}_{i,i^{\prime\prime}}$
$\displaystyle=\sum_{\ell\in[2d]}\mathbf{A}^{\prime}_{i,\ell}\cdot\mathbf{B}^{\prime}_{\sigma(\ell),i^{\prime}}$
(by def. of $\mathbf{C}$ and by $\sigma(i^{\prime\prime})=i^{\prime}$)
$\displaystyle=\sum_{\ell\in[d]\text{ s.t.
}\sigma(\ell)\in[d]}\mathbf{A}^{\prime}_{i,\ell}\cdot\mathbf{B}^{\prime}_{\sigma(\ell),i^{\prime}}$
(by def. of $\mathbf{A}^{\prime}$ and $\mathbf{B}^{\prime}$, and by
$i,i^{\prime}\in[d]$)
$\displaystyle=\mathbf{A}^{\prime}_{i,j}\cdot\mathbf{B}^{\prime}_{j,i^{\prime}}+\mathbf{A}^{\prime}_{i,k}\cdot\mathbf{B}^{\prime}_{k,i^{\prime}}$
$\displaystyle=a\cdot a^{\prime}+b\cdot b^{\prime}.$

Since $a$ and $b$ (resp. $a^{\prime}$ and $b^{\prime}$) have the same sign,
and since $a,b,a^{\prime},b^{\prime}\neq 0$, we conclude that
$|\mathbf{C}_{i,i^{\prime\prime}}|\geq 2$ and consequently that
$\lVert\mathcal{C}\rVert\geq\lVert\mathbf{C}\rVert\geq 2$.

To avoid cumbersome subscripts, we write $\bm{e}$ for $\bm{e}_{1}$ in the rest
of the section. Moreover, let
$\lambda_{\ell}(\mathbf{C})\coloneqq(\mathbf{C}^{\ell}\cdot\bm{e})(1)$ for
every matrix $\mathbf{C}$ and $\ell\in\mathbb{N}$.

The following technical lemma will be key to mimic doubling. It shows that,
from any class of norm at least $2$, we can extract a matrix with sufficiently
fast growth.

######  Lemma 7.

For every class of matrices $\mathcal{C}$ such that
$\lVert\mathcal{C}\rVert\geq 2$, there exists $\mathbf{C}\in\mathcal{C}$ with
$\lambda_{n+1}(\mathbf{C})\geq 2\cdot\lambda_{n}(\mathbf{C})$ for every
$n\in\mathbb{N}$.

######  Proof 3.7.

Let $\mathbf{A}\in\mathcal{C}$ be a matrix with some entry $c$ such that
$|c|\geq 2$. We can assume that $c\geq 2$. Indeed, if it is negative, then we
can multiply $\mathbf{A}$ by a suitable permutation of itself to obtain an
entry equal to $c\cdot c$. We can further assume that $c$ is the largest
positive coefficient occurring within $\mathbf{A}$, and that it lies on the
first column of $\mathbf{A}$, i.e., $\mathbf{A}_{k,1}=c$ for some $k\in[d]$
where $d\coloneqq\dim{\mathbf{A}}$. We consider the case where $k=1$. The case
where $k\neq 1$ will be discussed later.

For readability, we rename counters $\\{1,2,\ldots,d\\}$ respectively by
$X\coloneqq\\{x_{1},x_{2},\ldots,x_{d}\\}$. Note that
$(\mathbf{A}\cdot\bm{e})(x_{1})=c\geq 2\cdot\bm{e}(x_{1})$ as desired.
However, vector $\mathbf{A}\cdot\bm{e}$ may now hold nonzero values in
counters $x_{2},\ldots,x_{d}$. Therefore, if we multiply this vector by
$\mathbf{A}$, some “noise” will be added to counter $x_{1}$. If this noise is
too large, then it may cancel the growth of $x_{1}$ by $\approx c$. We address
this issue by introducing extra auxiliary counters replacing
$x_{2},\ldots,x_{d}$ at each “iteration”. Of course, we cannot have infinitely
many auxiliary counters. Fortunately, after a sufficiently large number $m$ of
iterations, the auxiliary counters used at the first iteration will contain
sufficiently small noise so that the process can restart from there.

More formally, let
$\mathbf{A}^{\prime}\coloneqq{\mathbf{A}}\\!\\!\restriction_{|Y|}$ where
$Y\coloneqq\\{y_{i,j}:0\leq i<m,j\in[2,d]\\}$ is the set of auxiliary
counters, and $m\geq 1$ is a sufficiently large constant whose value will be
picked later. Let $V$ be the set of vectors $\bm{v}\in\mathbb{Z}^{|X|+|Y|}$
satisfying $\bm{v}(x_{1})>0$ and

$|\bm{v}(y_{i,j})|\leq\left(\frac{3c}{4}\right)^{i}\cdot\frac{\bm{v}(x_{1})}{4d}\text{
for every }y_{i,j}\in Y.$

Let us fix some vector $\bm{v}_{0}\in V$. For every $0\leq i<m$, let
$\mathbf{B}_{i}\coloneqq\sigma_{i}({\mathbf{A}^{\prime}})$ and
$\bm{v}_{i+1}\coloneqq\mathbf{B}_{i}\cdot\bm{v}_{i}$ where $\sigma_{i}$ is the
permutation

$\sigma_{i}\coloneqq\prod_{j\in[2,d]}(x_{j};y_{i,j}).$

We claim that:

$\bm{v}_{m}(x_{1})\geq 2\cdot\bm{v}_{0}(x_{1})\text{ and }\bm{v}_{m}\in V.$

The validity of this claim proves the lemma. Indeed,
$\mathbf{C}\cdot\bm{v}_{0}=\bm{v}_{m}$ where
$\mathbf{C}\coloneqq\mathbf{B}_{m-1}\cdots\mathbf{B}_{1}\cdot\mathbf{B}_{0}$.
Hence, an application of $\mathbf{C}$ yields a vector whose first component
has at least doubled. Since $\bm{e}\in V$ and the resulting vector also belong
to $V$, this can be iterated arbitrarily many times.

Let us first establish the following properties for every $0\leq i<m$ and
$j\in[2,d]$:

  1. (1)

$\bm{v}_{i}(y_{i,j})=\bm{v}_{i-1}(y_{i,j})=\cdots=\bm{v}_{0}(y_{i,j})$ and
$\bm{v}_{i+1}(y_{i,j})=\bm{v}_{i+2}(y_{i,j})=\cdots=\bm{v}_{m}(y_{i,j})$;

  2. (2)

$\bm{v}_{i+1}(x_{1})\in\left[\frac{3c}{4}\cdot\bm{v}_{i}(x_{1}),\frac{5c}{4}\cdot\bm{v}_{i}(x_{1})\right]$;
and

  3. (3)

$|\bm{v}_{i+1}(y_{i,j})|\leq 2c\cdot\bm{v}_{i}(x_{1})$.

Property 1, which follows from the definition of $\mathbf{B}_{i}$, essentially
states that the contents of counter $y_{i,j}$ is only altered from
$\bm{v}_{i}$ to $\bm{v}_{i+1}$. Properties 2 and 3 bound the growth of the
counters in terms of $x_{1}$. Let us prove these two latter properties by
induction on $i$.

By definition of $\bm{v}_{i+1}$, we have
$\bm{v}_{i+1}(x_{1})=c\cdot\bm{v}_{i}+\delta$ where

$\delta\coloneqq\sum_{\begin{subarray}{c}z\neq
x_{1}\end{subarray}}(\mathbf{B}_{i})_{x_{1},z}\cdot\bm{v}_{i}(z).$

Therefore,
$\bm{v}_{i+1}(x_{1})\in[c\cdot\bm{v}_{i}(x_{1})-|\delta|,c\cdot\bm{v}_{i}(x_{1})+|\delta|]$,
and hence property 2 follows from:

$\displaystyle|\delta|$ $\displaystyle\leq\sum_{\begin{subarray}{c}z\in X\cup
Y\\\ z\neq
x_{1}\end{subarray}}|(\mathbf{B}_{i})_{x_{1},z}|\cdot|\bm{v}_{i}(z)|$
$\displaystyle=\sum_{j\in[2,d]}|\mathbf{A}^{\prime}_{x_{1},x_{j}}|\cdot|\bm{v}_{i}(y_{i,j})|$
(by def. of $\mathbf{B}_{i}$ and $\sigma_{i}$)
$\displaystyle=\sum_{j\in[2,d]}|\mathbf{A}^{\prime}_{x_{1},x_{j}}|\cdot|\bm{v}_{0}(y_{i,j})|$
(by 1) $\displaystyle\leq dc\cdot(3c/4)^{i}\cdot\frac{\bm{v}_{0}(x_{1})}{4d}$
(by $\bm{v}_{0}\in V$ and by maximality of $c$) $\displaystyle\leq
dc\cdot\frac{\bm{v}_{i}(x_{1})}{4d}$ (by
$\bm{v}_{i}(x_{1})\geq(3c/4)^{i}\cdot\bm{v}_{0}(x_{1})$ from 2)
$\displaystyle=\frac{c}{4}\cdot\bm{v}_{i}(x_{1}).$

Similarly, property 3 holds since, for every $j\in[2,d]$:

$\displaystyle|\bm{v}_{i+1}(y_{i,j})|$
$\displaystyle\leq|\mathbf{A}^{\prime}_{x_{j},x_{1}}|\cdot\bm{v}_{i}(x_{1})+\sum_{\ell\in[2,d]}|\mathbf{A}^{\prime}_{x_{j},x_{\ell}}|\cdot|\bm{v}_{i}(y_{i,\ell})|$
(by def. of $\mathbf{B}_{i}$ and $\sigma_{i}$) $\displaystyle\leq
c\cdot\bm{v}_{i}(x_{1})+dc\cdot(3c/4)^{i}\cdot\frac{\bm{v}_{0}(x_{1})}{4d}$
(by 1 and $\bm{v}_{0}\in V$) $\displaystyle\leq
c\cdot\bm{v}_{i}(x_{1})+dc\cdot\frac{\bm{v}_{i}(x_{1})}{4d}$ (by 2)
$\displaystyle\leq 2c\cdot\bm{v}_{i}(x_{1}).$

We may now prove the claim. Let $m$ be sufficiently large so that
$(3c/4)^{m}\geq 8cd$. We have
$\bm{v}_{m}(x_{1})\geq(3c/4)^{m}\cdot\bm{v}_{0}(x_{1})\geq
8cd\cdot\bm{v}_{0}(x_{1})$ by 2 and definition of $m$. Hence, since $c\geq 2$
and $d\geq 1$, we have $\bm{v}_{m}(x_{1})\geq 2\cdot\bm{v}_{0}(x_{1})$, which
satisfies the first part of the claim. Moreover, the second part of the claim,
namely $\bm{v}_{m}\in V$, holds since for every $y_{i,j}\in Y$, we have:

$\displaystyle|\bm{v}_{m}(y_{i,j})|$ $\displaystyle=|\bm{v}_{i+1}(y_{i,j})|$
(by 1) $\displaystyle\leq 2c\cdot\bm{v}_{i}(x_{1})$ (by 3) $\displaystyle\leq
2c\cdot\frac{\bm{v}_{m}(x_{1})}{(3c/4)^{m-i}}$ (by
$\bm{v}_{m}(x_{1})\geq(3c/4)^{m-i}\cdot\bm{v}_{i}(x_{1})$ from 2)
$\displaystyle=2c\cdot(3c/4)^{i}\cdot\frac{\bm{v}_{m}(x_{1})}{(3c/4)^{m}}$
$\displaystyle\leq 2c\cdot(3c/4)^{i}\cdot\frac{\bm{v}_{m}(x_{1})}{8cd}$ (by
def. of $m$) $\displaystyle=(3c/4)^{i}\cdot\frac{\bm{v}_{m}(x_{1})}{4d}.$

We are done proving the lemma for the case $\mathbf{A}_{k,1}=c\geq 2$ with
$k=1$. This case is slightly simpler as $c$ lies on the main diagonal of
$\mathbf{A}$ which means that $\bm{v}_{i+1}(x_{1})\approx
c\cdot\bm{v}_{i}(x_{1})$. If $k\neq 1$, then we have
$\bm{v}_{i+1}(x_{k})\approx c\cdot\bm{v}_{i}(x_{1})$ instead, which breaks
composability for the next iteration. However, this is easily fixed by
swapping the names of counters $x_{k}$ and $x_{1}$.

Let us fix a class $\mathcal{C}$ such that $\lVert\mathcal{C}\rVert\geq 2$ and
the matrix $\mathbf{C}$ obtained for $\mathcal{C}$ from Lemma 7. For
simplicity, we will write $\lambda_{\ell}$ instead of
$\lambda_{\ell}(\mathbf{C})$. We prove two intermediary propositions that
essentially show that $\mathbf{C}$ can encode binary strings. Let
$f_{b}(\bm{v})\coloneqq\mathbf{C}\cdot\bm{v}+b\cdot\bm{e}$ for both
$b\in\\{0,1\\}$ and every $\bm{v}\in\mathbb{Z}^{\dim{\mathbf{C}}}$. Let
$f_{\varepsilon}$ be the identity function, and let $f_{x}\coloneqq
f_{x_{n}}\circ\cdots\circ f_{x_{2}}\circ f_{x_{1}}$ for every
$x\in{\\{0,1\\}}^{n}$. Let $\gamma_{x}\coloneqq f_{x}(\bm{e})(1)$ for every
$x\in{\\{0,1\\}}^{*}$. Let $\llbracket\varepsilon\rrbracket\coloneqq\emptyset$
and $\llbracket w\rrbracket\coloneqq\\{i\in[k]:w_{i}=1\\}$ be the “support” of
$w$ for every sequence $w\in\\{0,1\\}^{+}$ of length $k>0$.

######  Proposition 8.

For every $x\in{\\{0,1\\}}^{*}$, the following holds:
$\gamma_{x}=\lambda_{|x|}+\sum_{i\in\llbracket x\rrbracket}\lambda_{|x|-i}$.

######  Proof 3.8.

It suffices to show that
$f_{x}(\bm{e})=\mathbf{C}^{|x|}\cdot\bm{e}+\sum_{i\in\llbracket
x\rrbracket}\mathbf{C}^{|x|-i}\cdot\bm{e}$ for every $x\in{\\{0,1\\}}^{*}$.
Let us prove this by induction on $|x|$. If $|x|=0$, then $x=\varepsilon$, and
hence $f_{x}(\bm{e})=\bm{e}=\mathbf{C}^{0}\cdot\bm{e}$. Assume that $|x|>0$
and that the claim holds for sequences of length $|x|-1$. There exist
$b\in\\{0,1\\}$ and $w\in{\\{0,1\\}}^{*}$ such that $x=wb$. We have:

$\displaystyle f_{x}(\bm{e})$ $\displaystyle=\mathbf{C}\cdot
f_{w}(\bm{e})+b\cdot\bm{e}$
$\displaystyle=\mathbf{C}\cdot\left(\mathbf{C}^{|w|}\cdot\bm{e}+\sum_{i\in\llbracket
w\rrbracket}\mathbf{C}^{|w|-i}\cdot\bm{e}\right)+b\cdot\bm{e}$ (by induction
hypothesis)
$\displaystyle=\left(\mathbf{C}^{|w|+1}\cdot\bm{e}+\sum_{i\in\llbracket
w\rrbracket}\mathbf{C}^{|w|+1-i}\cdot\bm{e}\right)+b\cdot\bm{e}$
$\displaystyle=\left(\mathbf{C}^{|x|}\cdot\bm{e}+\sum_{i\in\llbracket
x\rrbracket\setminus\\{|x|\\}}\mathbf{C}^{|x|-i}\cdot\bm{e}\right)+b\cdot\mathbf{C}^{|x|-|x|}\cdot\bm{e}$
$\displaystyle=\mathbf{C}^{|x|}\cdot\bm{e}+\sum_{i\in\llbracket
x\rrbracket}\mathbf{C}^{|x|-i}\cdot\bm{e}$ (by def. of $\llbracket
x\rrbracket$).

######  Proposition 9.

For every $x,y\in{\\{0,1\\}}^{*}$, it is the case that $x=y$ if and only if
$\gamma_{x}=\gamma_{y}$.

######  Proof 3.9.

Let $<_{\text{lex}}$ denote the lexicographical order over ${\\{0,1\\}}^{*}$.
It is sufficient to show that for every $x,y\in{\\{0,1\\}}^{*}$ the following
holds: if $x<_{\text{lex}}y$, then $\gamma_{x}<\gamma_{y}$. Indeed, if this
claim holds, then for every $x,y\in{\\{0,1\\}}^{*}$ such that $x\neq y$, we
either have $x<_{\text{lex}}y$ or $y<_{\text{lex}}x$, which implies
$\gamma_{x}\neq\gamma_{y}$ in both cases.

Let us prove the claim. Let $x,y\in{\\{0,1\\}}^{*}$ be such that
$x<_{\text{lex}}y$. We either have $|x|<|y|$ or $|x|=|y|$. If the former
holds, then the claim follows from:

$\displaystyle\gamma_{x}$ $\displaystyle=\lambda_{|x|}+\sum_{i\in\llbracket
x\rrbracket}\lambda_{|x|-i}$ (by Proposition 8)
$\displaystyle\leq\lambda_{|x|}+\sum_{i=1}^{|x|}\lambda_{|x|}/2^{i}$ (by Lemma
7) $\displaystyle=\lambda_{|x|}\cdot\left(1+\sum_{i=1}^{|x|}1/2^{i}\right)$
$\displaystyle=\lambda_{|x|}\cdot(2-1/2^{|x|})$
$\displaystyle<2\cdot\lambda_{|x|}$ (since $\lambda_{|x|}>0$)
$\displaystyle\leq\lambda_{|y|}$ (by Lemma 7) $\displaystyle\leq\gamma_{y}$
(by Proposition 8).

It remains to prove the case where $|x|=|y|=k$ for some $k>0$. Since
$x<_{\text{lex}}y$, there exist $u,v,w\in{\\{0,1\\}}^{*}$ such that $x=u0v$
and $y=u1w$. Let $\ell\coloneqq k-|u|-1$. Note that $\ell=|v|=|w|$. The proof
is completed by observing that:

$\displaystyle\gamma_{y}-\gamma_{x}$
$\displaystyle=\lambda_{\ell}+\sum_{i\in\llbracket
w\rrbracket}\lambda_{\ell-i}-\sum_{i\in\llbracket
v\rrbracket}\lambda_{\ell-i}$ (by Proposition 8)
$\displaystyle\geq\lambda_{\ell}-\sum_{i=1}^{|v|}\lambda_{\ell-i}$
$\displaystyle\geq\lambda_{\ell}-\sum_{i=1}^{|v|}\lambda_{\ell}/2^{i}$ (by
$\lambda_{\ell}\geq 2^{i}\cdot\lambda_{\ell-i}$ from Lemma 7)
$\displaystyle=\lambda_{\ell}\cdot\left(1-\sum_{i=1}^{\ell}1/2^{i}\right)$ (by
$|v|=\ell$) $\displaystyle=\lambda_{\ell}/2^{\ell}$ $\displaystyle>0.$

We may finally prove the last part of our trichotomy.

######  Theorem 10.

$\mathbb{Z}\text{-}\textsc{Reach}_{\mathcal{C}}$ is undecidable if
$\lVert\mathcal{C}\rVert\geq 2$.

######  Proof 3.10.

We give a reduction from the Post correspondence problem inspired by [Rei15].
There, counter values can be doubled as a “native” operation. Here, we adapt
the construction with our emulation of doubling. Let us consider an instance
of the Post correspondence problem over alphabet $\\{0,1\\}$:

$\Gamma\coloneqq\left\\{\left[\begin{tabular}[]{cc}\\!\\!\\!{$u_{1}$}\\!\\!\\!\\\
\hline\cr\\!\\!\\!{$v_{1}$}\\!\\!\\!\end{tabular}\right],\left[\begin{tabular}[]{cc}\\!\\!\\!{$u_{2}$}\\!\\!\\!\\\
\hline\cr\\!\\!\\!{$v_{2}$}\\!\\!\\!\end{tabular}\right],\ldots,\left[\begin{tabular}[]{cc}\\!\\!\\!{$u_{\ell}$}\\!\\!\\!\\\
\hline\cr\\!\\!\\!{$v_{\ell}$}\\!\\!\\!\end{tabular}\right]\right\\}.$

We say that $\Gamma$ _has a match_ if there exists $w\in\Gamma^{+}$ such that
the underlying top and bottom sequences of $w$ are equal.

Let $\mathbf{C}$ be the matrix obtained for $\mathcal{C}$ from Lemma 7, let
$d\coloneqq\dim{\mathbf{C}}$, and let $\bm{e}$ be of size $d$. For every
$x\in{\\{0,1\\}}^{*}$, let $g_{x}$ and $h_{x}$ be the linear mappings over
$\mathbb{Z}^{2d}$ defined as $f_{x}$, but operating on counters $1,2,\ldots,d$
and counters $d+1,d+2,\ldots,2d$ respectively.

$p$$q_{1}$$q_{i}$$q_{\ell}$$r$$g_{u_{1}}$$h_{v_{1}}$$g_{u_{\ell}}$$h_{v_{\ell}}$$(-\bm{e},-\bm{e})$$(-\bm{e},-\bm{e})$$g_{u_{i}}$$h_{v_{i}}$
Figure 6. Affine VASS $\mathcal{V}$ for the Post correspondence problem. Arcs
labeled by mappings of the form $g_{x}$ and $h_{x}$ stand for sequences of
$|x|$ transitions implementing $g_{x}$ and $h_{x}$.

Let $\mathcal{V}\coloneqq(2d,Q,T)$ be the affine VASS such that $Q$ and $T$
are as depicted in Figure 6. Note that $\mathcal{V}$ belongs to $\mathcal{C}$.
Indeed, $g_{x}$ and $h_{x}$ can be obtained from matrix
$\mathbf{C}\in\mathcal{C}$ and the fact that $\mathcal{C}$ is a class, and
hence closed under counter renaming and larger dimensions. We claim that

$p(\bm{e},\bm{e})\xrightarrow{*}_{\mathbb{Z}}r(\bm{e},\bm{e})\text{ if and
only if }\Gamma\text{ has a match}.$

Note that any sequence $w\in T^{+}$ from $p$ to $p$ computes $g_{w_{x}}\circ
h_{w_{y}}$ for some word

$\left[\begin{tabular}[]{cc}\\!\\!\\!{$w_{x}$}\\!\\!\\!\\\
\hline\cr\\!\\!\\!{$w_{y}$}\\!\\!\\!\end{tabular}\right]\in\Gamma^{+}.$

Therefore:

$\displaystyle\phantom{{}\iff{}}p(\bm{e},\bm{e})\xrightarrow{*}_{\mathbb{Z}}r(\bm{e},\bm{e})$
$\displaystyle\iff\exists w\in
T^{+},\bm{v}\in\mathbb{Z}^{2d}:p(\bm{e},\bm{e})\xrightarrow{w}_{\mathbb{Z}}p(\bm{v})\xrightarrow{*}_{\mathbb{Z}}r(\bm{e},\bm{e})$
$\displaystyle\iff\exists w\in
T^{+},\bm{v}\in\mathbb{Z}^{2d}:p(\bm{e},\bm{e})\xrightarrow{w}_{\mathbb{Z}}p(\bm{v})\text{
and }\bm{v}(1)=\bm{v}(d+1)$ $\displaystyle\iff\exists w\in
T^{+}:\gamma_{w_{x}}=\gamma_{w_{y}}$ (by def. of $g$, $h$ and $\gamma$)
$\displaystyle\iff\exists w\in T^{+}:w_{x}=w_{y}$ (by Proposition 9)
$\displaystyle\iff\Gamma\text{ has a match.}$

We conclude this section by proving Theorem 1 3 which can be equivalently
formulated as follows:

######  Corollary 11.

$\mathbb{Z}\text{-}\textsc{Reach}_{\mathcal{C}}$ is undecidable if
$\mathcal{C}$ does not only contain pseudo-transfer matrices and does not only
contain pseudo-copy matrices.

######  Proof 3.11.

By Proposition 6, $\lVert\mathcal{C}\rVert\geq 2$, hence undecidability
follows from Theorem 10.

##  4\. A complexity dichotomy for reachability

This section is devoted to the following complexity dichotomy on
$\textsc{Reach}_{\mathcal{C}}$, which is mostly proven by exploiting notions
and results from the previous section:

######  Theorem 12.

The reachability problem $\textsc{Reach}_{\mathcal{C}}$ is equivalent to the
(standard) VASS reachability problem if $\mathcal{C}$ only contains
permutation matrices, and is undecidable otherwise.

###  4.1. Decidability

Note that the (standard) VASS reachability problem is the problem
$\textsc{Reach}_{\mathcal{I}}$ where $\mathcal{I}\coloneqq\bigcup_{n\geq
1}\mathbf{I}_{n}$. Clearly
$\textsc{Reach}_{\mathcal{I}}\leq\textsc{Reach}_{\mathcal{C}}$ for any class
$\mathcal{C}$. Therefore, it suffices to show the following:

######  Proposition 13.

$\textsc{Reach}_{\mathcal{C}}\leq\textsc{Reach}_{\mathcal{I}}$ for every
$\mathcal{C}$ that only contains permutation matrices.

######  Proof 4.1.

Let $\mathcal{V}=(d,Q,T)$ be an affine VASS that belongs to $\mathcal{C}$. We
construct a (standard) VASS $\mathcal{V}^{\prime}=(d,Q^{\prime},T^{\prime})$
that simulates $\mathcal{V}$. Recall that a (standard) VASS is an affine VASS
that only uses the identity matrix. For readability, we omit the identity
matrix on the transitions of $\mathcal{V}^{\prime}$. We assume without loss of
generality that each transition $t\in T$ satisfies either $\Delta(t)=\bm{0}$
or $M(t)=\mathbf{I}$. Indeed, since permutation matrices are nonnegative,
every transition of $T$ can be splitted in two parts: first applying its
matrix, and then its vector.

The control-states and transitions of $\mathcal{V}^{\prime}$ are defined as
$Q^{\prime}\coloneqq\\{q_{\sigma}:q\in Q,\sigma\in\mathcal{S}_{d}\\}$ and
$T^{\prime}\coloneqq S_{\bm{\circlearrowright}}\cup S_{\text{vec}}$, which are
to be defined shortly. Intuitively, each control-state of
$\mathcal{V}^{\prime}$ stores the current control-state of $\mathcal{V}$
together with the current renaming of its counters. Whenever a transition
$t\in T$ such that $\Delta(t)=\bm{0}$ is to be applied, this means that the
counters must be renamed by the permutation $M(t)$. This is achieved by:

$S_{\bm{\circlearrowright}}\coloneqq\\{(p_{\sigma},\bm{0},q_{\pi\circ\sigma}):(p,\mathbf{P}_{\pi},\bm{0},q)\in
T,\sigma\in\mathcal{S}_{d}\\}.$

Similarly, whenever a transition $t\in T$ such that $M(t)=\mathbf{I}$ is to be
applied, this means that $\Delta(t)$ should be added to the counters, but in
accordance to the current renaming of the counters. This is achieved by:

$S_{\text{vec}}\coloneqq\\{(p_{\sigma},\mathbf{P}_{\sigma}\cdot\bm{b},q_{\sigma}):(p,\mathbf{I},\bm{b},q),\sigma\in\mathcal{S}_{d}\\}.$

A routine induction shows that

$p(\bm{u})\xrightarrow{*}_{\mathbb{N}}q(\bm{v})\text{ in $\mathcal{V}$ iff
}p_{\varepsilon}(\bm{u})\xrightarrow{*}_{\mathbb{N}}q_{\sigma}(\mathbf{P}_{\sigma}\cdot\bm{v})\text{
in $\mathcal{V}^{\prime}$},$

where $\varepsilon$ denotes the identity permutation. Since this amounts to
finitely many reachability queries, i.e., $|\mathcal{S}_{d}|=d!$ queries, this
yields a Turing reduction111Although it is not necessary for our needs, the
reduction can be made _many-one_ by weakly computing a matrix multiplication
by $\mathbf{P}_{\sigma^{-1}}$ onto $d$ new counters, from each control-state
$q_{\sigma}$ to a common state $r$..

###  4.2. Undecidability

We show undecidability by considering three types of classes: (1) classes with
matrices with negative entries; (2) nontransfer _and_ noncopy classes; and (3)
transfer _or_ copy classes. In each case, we will argue that an “undecidable
operation” can be simulated, namely: zero-tests, doubling and resets.

######  Proposition 14.

$\textsc{Reach}_{\mathcal{C}}$ is undecidable for every class $\mathcal{C}$
that contains a matrix with some negative entry.

######  Proof 4.2.

Let $\mathbf{A}\in\mathcal{C}$ be a matrix such that $\mathbf{A}_{i,j}<0$ for
some $i,j\in[d]$ where $d\coloneqq\dim{\mathbf{A}}$. We show how a two counter
Minsky machine $\mathcal{M}$ can be simulated by an affine VASS $\mathcal{V}$
belonging to $\mathcal{C}$. Note that we only have to show how to simulate
zero-tests. The affine VASS $\mathcal{V}$ has $2d$ counters: counters $j$ and
$j+d$ which represent the two counters $x$ and $y$ of $\mathcal{M}$; and
$2d-2$ auxiliary counters which will be permanently set to value $0$.

$x\leftarrow x+c$$y\leftarrow
y+c$$x=0$?$y=0$?$(c\cdot\bm{e}_{j},\bm{0})$$(\bm{0},c\cdot\bm{e}_{j})$$\begin{pmatrix}\mathbf{A}&\mathbf{0}\\\
\mathbf{0}&\mathbf{I}\end{pmatrix}$ $\begin{pmatrix}\mathbf{I}&\mathbf{0}\\\
\mathbf{0}&\mathbf{A}\end{pmatrix}$ Figure 7. _Top_ : example of a counter
machine $\mathcal{M}$. _Bottom_ : an affine VASS $\mathcal{V}$ simulating
$\mathcal{M}$.

Observe that for every $\lambda\in\mathbb{N}$, the following holds:

$\mathbf{A}\cdot\lambda\bm{e}_{j}=\begin{cases}\bm{0}&\text{if }\lambda=0,\\\
\lambda\cdot\mathbf{A}_{\star,j}&\text{otherwise}.\end{cases}$

Thus, $\mathbf{A}$ simulates a zero-test as it leaves all counters set to zero
if counter $j$ holds value zero, and it generates a vector with some negative
entry otherwise, which is an invalid configuration under
$\mathbb{N}$-reachability. Figure 7 shows how each transition of $\mathcal{M}$
is replaced in $\mathcal{V}$. We are done since

$\displaystyle(m,n)\xrightarrow{*}_{\mathbb{N}}(m^{\prime},n^{\prime})\text{
in
}\mathcal{M}\iff(m\cdot\bm{e}_{j},n\cdot\bm{e}_{j})\xrightarrow{*}_{\mathbb{N}}(m^{\prime}\cdot\bm{e}_{j},n^{\prime}\cdot\bm{e}_{j})\text{
in }\mathcal{V}.$

######  Proposition 15.

$\textsc{Reach}_{\mathcal{C}}$ is undecidable if $\mathcal{C}$ does not only
contain transfer matrices and does not only contain copy matrices.

######  Proof 4.3.

If $\mathcal{C}$ contains a matrix with some negative entry, then we are done
by Proposition 14. Thus, assume $\mathcal{C}$ only contains nonnegative
matrices. By Proposition 6, we have $\lVert\mathcal{C}\rVert\geq 2$. Let
$\mathbf{C}$ be the matrix obtained for $\mathcal{C}$ from Lemma 7. Since
$\mathbf{C}\geq\mathbf{0}$, we have $\mathbf{C}\cdot\bm{v}\geq\bm{0}$ for
every $\bm{v}\geq\bm{0}$. Hence, multiplication by $\mathbf{C}$ is always
allowed under $\mathbb{N}$-reachability. Thus, the reduction from the Post
correspondence problem given in Theorem 10 holds here under
$\mathbb{N}$-reachability, as the only possibly (relevant) negative values
arose from $\mathbf{C}$.

We may finally prove the last part of our dichotomy:

######  Theorem 16.

$\textsc{Reach}_{\mathcal{C}}$ is undecidable for every class $\mathcal{C}$
with some nonpermutation matrix.

######  Proof 4.4.

Let $\mathbf{A}\in\mathcal{C}$ be a matrix which is not a permutation matrix.
By Propositions 14 and 15, we may assume that $\mathbf{A}$ is either a
transfer or a copy matrix. Hence, $\mathbf{A}$ must have a column or a row
equal to $\bm{0}$, as otherwise it would be a permutation matrix. Thus, we
either have $\mathbf{A}_{\star,i}=\bm{0}$ or $\mathbf{A}_{i,\star}=\bm{0}$ for
some $i\in[d]$ where $d\coloneqq\dim{\mathbf{A}}$.

We show that $\mathcal{C}$ implements resets, i.e., the operation
$f\colon\mathbb{Z}\to\mathbb{Z}$ such that $f(x)~{}\coloneqq~{}0$. This
suffices to complete the proof since reachability for VASS with resets is
undecidable [AK76].

Let $X\coloneqq\\{d+1,d+2,\ldots,d+n\\}$ be the counters for which we wish to
implement resets. Let
$\mathbf{A}^{\prime}\coloneqq{\mathbf{A}}\\!\\!\restriction_{n}$ and let
$\mathbf{B}_{x}\coloneqq\sigma_{x}(\mathbf{A}^{\prime})$ where
$\sigma_{x}\coloneqq(x;i)$. Let $x,y\in X$ be such that $x\neq y$.

Case $\mathbf{A}_{\star,i}=\bm{0}$. We have:
$\mathbf{B}_{x}\cdot\bm{e}_{x}=(\mathbf{B}_{x})_{\star,x}=\mathbf{A}^{\prime}_{\star,i}=\bm{0}$.
Similarly, it can be shown that $\mathbf{B}_{x}\cdot\bm{e}_{y}=\bm{e}_{y}$.
Hence, class $\mathcal{C}$ $0$-implements resets.

Case $\mathbf{A}_{i,\star}=\bm{0}$. The following holds for every
$\bm{v}\in\mathbb{Z}^{d+n}$:

$\displaystyle(\mathbf{B}_{x}\cdot\bm{v})(x)$
$\displaystyle=\sum_{\ell\in[d+n]}\mathbf{B}_{x,\ell}\cdot\bm{v}(\ell)$
$\displaystyle=\sum_{\ell\in[d+n]}\mathbf{A}^{\prime}_{i,\sigma_{x}(\ell)}\cdot\bm{v}(\ell)$
$\displaystyle=0.$

Similarly, $(\mathbf{B}_{x}\cdot\bm{v})(y)=\bm{v}(y)$. Hence, class
$\mathcal{C}$ $?$-implements resets (see Appendix A).

##  5\. Parameterization by a system rather than a class

In this section, we consider the (integer or standard) reachability problem
parameterized by a fixed affine VASS, rather than a matrix class. We show that
in contrast to the case of classes, this parameterization yields an
_arbitrary_ complexity (up to a polynomial). More formally, this section is
devoted to establishing the following theorem:

######  Theorem 17.

Let $\emptyset\subset L\subset\\{0,1\\}^{*}$ be a decidable decision problem
and let $\mathbb{D}\in\\{\mathbb{Z},\mathbb{N}\\}$. There exists an affine
VASS $\mathcal{V}$ such that $L$ and the following problem are interreducible
under polynomial-time many-one reductions:

$\mathbb{D}\text{-}\textsc{Reach}_{\mathcal{V}}$
---
Input: |  two configurations $p(\bm{u}),q(\bm{v})$;
Decide: |  $p(\bm{u})\xrightarrow{*}_{\mathbb{D}}q(\bm{v})$ in $\mathcal{V}$?

In order to show Theorem 17, we will prove the following technical lemma:

######  Lemma 18.

Let $\mathbb{D}\in\\{\mathbb{Z},\mathbb{N}\\}$ and let
$\varphi\colon\mathbb{D}\to\\{0,1\\}$ be a nontrivial computable predicate.
There exists an affine VASS $\mathcal{V}=(d,Q,T)$ and control-states $p,q\in
Q$ such that:

  1. (1)

For every vector $\bm{u}$, it is the case that
$p(x,\bm{u})\xrightarrow{*}_{\mathbb{D}}q(0,\bm{0})$ in $\mathcal{V}$ iff
$\varphi(x)$ holds;

  2. (2)

Any query “$r(\bm{v})\xrightarrow{*}_{\mathbb{D}}r^{\prime}(\bm{v}^{\prime})$”
can be answered in polynomial time if $r\neq p$ or
$r^{\prime}(\bm{v}^{\prime})\neq q(\bm{0})$.

Before proving Lemma 18, let us see why it implies the validity of Theorem 17:

######  Proof 5.1 (Proof of Theorem 17.).

Let $f\colon\\{0,1\\}^{*}\to\mathbb{D}$ be a polynomial-time computable and
invertible bijection.222If $\mathbb{D}=\mathbb{N}$, we can set
$f(w)\coloneqq\mathrm{val}(\texttt{1}w)-1$, i.e., $f=\\{\varepsilon\mapsto
0,\texttt{0}\mapsto 1,\texttt{1}\mapsto 2,\texttt{00}\mapsto 3,\ldots\\}$. If
$\mathbb{D}=\mathbb{Z}$, we can set $f(\varepsilon)\coloneqq 0$ and
$f(w_{1}\cdots
w_{n})\coloneqq-1^{w_{n}}\cdot\mathrm{val}(\texttt{1}w_{1}\cdots w_{n-1})$,
i.e., $f=\\{\varepsilon\to 0,\texttt{0}\mapsto
1,\texttt{1}\mapsto-1,\texttt{00}\mapsto 2,\texttt{01}\mapsto-2,\ldots\\}$.
Let $\varphi\colon\mathbb{D}\to\\{0,1\\}$ be the characteristic function of
$L$ encoded by $f$, i.e., $w\in L$ iff $\varphi(f(w))$ holds. Let
$\mathcal{V}$ be the affine VASS given by Lemma 18 for $\varphi$, and let
$p,q$ be its associated control-states. To reduce $L$ to
$\textsc{Reach}_{\mathcal{V}}$, we construct, on input $w$, the pair
$I_{w}\coloneqq\langle p(f(w),\bm{0}),q(0,\bm{0})\rangle$. We have $w\in L$
iff $\varphi(f(w))$ holds iff $I_{w}\in\textsc{Reach}_{\mathcal{V}}$ by Lemma
18.

The reduction from $\mathbb{D}\text{-}\textsc{Reach}_{\mathcal{V}}$ to $L$ is
as follows. On input $I=\langle r(\bm{v}),r^{\prime}(\bm{v}^{\prime})\rangle$:

  * •

If $r\neq p$ or $r^{\prime}(\bm{v}^{\prime})\neq q(\bm{0})$, then we check
whether $r(\bm{v})\xrightarrow{*}_{\mathbb{D}}r^{\prime}(\bm{v}^{\prime})$ in
polynomial time and return a positive (resp. negative) instance of $L$ if it
holds (resp. does not hold). This is possible by Lemma 18 and by nontriviality
of $L$.

  * •

Otherwise, $I=\langle p(x,\bm{u}),q(0,\bm{0})\rangle$ for some value $x$ and
some vector $\bm{u}$, so it suffices to return $f^{-1}(x)$. Indeed, by Lemma
18, $I\in\mathbb{D}\text{-}\textsc{Reach}_{\mathcal{V}}$ iff $\varphi(x)$
holds iff $f^{-1}(x)\in L$.

In order to prove Lemma 18, we first establish the following proposition.
Informally, it states that although an affine VASS cannot evaluate a
polynomial $P$ with the mere power of affine functions, it can evaluate $P$
“weakly”. Moreover, its structure is simple enough to answer any reachability
query in polynomial time.

######  Proposition 19.

Let $\mathbb{D}\in\\{\mathbb{Z},\mathbb{N}\\}$, and let $P$ be a polynomial
with integer coefficients and $k$ variables over $\mathbb{D}$. There exist an
affine VASS $\mathcal{V}=(d,Q,T)$ and control-states $p,q\in Q$ such that
$P(\bm{x})=0$ iff
$p(\bm{x},\bm{0})\xrightarrow{*}_{\mathbb{D}}q(\bm{x},\bm{0})$ in
$\mathcal{V}$. Moreover, the following properties hold:

  1. (1)

No transition of $\mathcal{V}$ alters its $k$ first counters (corresponding to
$\bm{x}$);

  2. (2)

Any reachability query
“$r(\bm{v})\xrightarrow{*}_{\mathbb{D}}r^{\prime}(\bm{v}^{\prime})$” can be
answered in polynomial time.

######  Proof 5.2.

We adapt and simplify a contruction of the authors which was given in [BHMR19]
for other purposes. Let us first consider the case of a single monomial
$P(y_{1},\ldots,y_{k})=cy_{1}^{d_{1}}\cdots y_{k}^{d_{k}}$ with $c\geq 1$. We
claim that the affine VASS $\mathcal{V}$ depicted in Figure 8 satisfies the
claim. Its counters are $C\coloneqq Y\cup Y^{\prime}\cup A$, where

$\displaystyle Y$ $\displaystyle\coloneqq\\{y_{1},\ldots,y_{k}\\}\text{
corresponds to the input variables;}$ $\displaystyle Y^{\prime}$
$\displaystyle\coloneqq\\{y_{i,j}:i\in[k],j\in[d_{i}]\\}\text{ are auxiliary
counters that allow to copy $Y$; and}$ $\displaystyle A$
$\displaystyle\coloneqq\\{a_{0}\\}\cup\\{a_{i,j}:i\in[k],j\in[d_{i}]\\}\cup\\{a_{\text{out}}\\}\text{
serve as accumulators.}$

$p$$r_{0}$$r_{1,1}$$r_{1,d_{1}}$$r_{k,1}$$r_{k,d_{k}}$$q$$a_{0}\leftarrow c$$y_{1,1}\leftarrow y_{1}$$y_{k,d_{k}}\leftarrow y_{k}$ $a_{\text{out}}$ | $\leftarrow a_{k,d_{k}}$
---|---
$a_{0}$ | $\leftarrow 0$
$a_{i,j}$ |  $\leftarrow 0$ ($\forall i,j$)
$\text{$y_{1,1}$}\scriptstyle\mathrm{--}$
---
$a_{1,1}\mathrel{+}=a_{0}$
$\text{$y_{1,1}$}\scriptstyle\mathrm{++}$
---
$a_{1,1}\mathrel{-}=a_{0}$
$\text{$y_{1,d_{1}}$}\scriptstyle\mathrm{--}$
---
$a_{1,d_{1}}\mathrel{+}=a_{1,d_{1}-1}$
$\text{$y_{1,d_{1}}$}\scriptstyle\mathrm{++}$
---
$a_{1,d_{1}}\mathrel{-}=a_{1,d_{1}-1}$
$\text{$y_{k,1}$}\scriptstyle\mathrm{--}$
---
$a_{k,1}\mathrel{+}=a_{k-1,d_{k-1}}$
$\text{$y_{k,1}$}\scriptstyle\mathrm{++}$
---
$a_{k,1}\mathrel{-}=a_{k-1,d_{k-1}}$
$\text{$y_{k,d_{k}}$}\scriptstyle\mathrm{--}$
---
$a_{k,d_{k}}\mathrel{+}=a_{k,d_{k}-1}$
$\text{$y_{k,d_{k}}$}\scriptstyle\mathrm{++}$
---
$a_{k,d_{k}}\mathrel{-}=a_{k,d_{k}-1}$
$y_{1,d_{1}}\leftarrow y_{1}$$y_{k,1}\leftarrow y_{k}$ Figure 8. Affine VASS
evaluating $cy_{1}^{d_{1}}\cdots y_{k}^{d_{k}}$, where
“$\text{$x$}\scriptstyle\mathrm{++}$”, “$\text{$x$}\scriptstyle\mathrm{--}$”,
“$x\mathrel{+}=x^{\prime}$” and “$x\mathrel{-}=x^{\prime}$” stand respectively
for “$x\leftarrow x+1$”, “$x\leftarrow x-1$”, “$x\leftarrow x+x^{\prime}$” and
“$x\leftarrow x-x^{\prime}$”.

By construction, counters from $Y$ are never altered, merely copied onto
$Y^{\prime}$. Moreover, if counters from $Y^{\prime}\cup A$ initially hold
zero, and if loops are executed so that counters from $Y^{\prime}$ reach zero,
then $a_{\text{out}}$ contains $P(y_{1},\ldots,y_{k})$ when reaching control-
state $q$, and every other auxiliary counter holds zero (due to the final
resets).

It remains to argue that Item 2 holds. Let us consider a query
“$r(\bm{v})\xrightarrow{*}_{\mathbb{D}}r^{\prime}(\bm{v}^{\prime})$”. Observe
that, although $\mathcal{V}$ has nondeterminism in its loops and uses
nonreversible operations (copies and resets), it is still “reversible” since
the inputs $Y$ are never altered and since each counter from $Y^{\prime}$ can
only be altered at a single copy or via the two loops next to it. This
provides enough information to answer the reachability query. Indeed, we can:

  * •

Answer “false” if $\bm{v}$ and $\bm{v}^{\prime}$ disagree on $Y$;

  * •

Pretend the accumulators do not exist and traverse $\mathcal{V}$ backward from
$r^{\prime}(\bm{v}^{\prime})$ to $r$ by undoing the loops (either up only or
down only), ensuring each counter from $Y^{\prime}$ reaches its correct value;
and answer “false” if not possible;

  * •

Traverse $\mathcal{V}$ forward from $r(\bm{v})$ by running through the loops
the number of times identified by the previous traversal; this now allows to
determine the value of the accumulators $A$;

  * •

If the values of $A$ are incorrect in $r^{\prime}(\bm{v}^{\prime})$, or if we
ever drop below zero in the case of $\mathbb{D}=\mathbb{N}$, then we answer
“false”, and otherwise “true”.

Observe that there is no need to execute the loops one step at a time, e.g.,
if $\bm{v}(y_{i})=10\geq 3=\bm{v}^{\prime}(y_{i,j})$, then we can compute $7$
directly rather than in seven steps.

Let us now consider the general case. We can write the polynomial $P$ as

$P(y_{1},\ldots,y_{k})=\sum_{1\leq i\leq
m}Q_{i}(y_{1},\ldots,y_{k})-\sum_{m<i\leq n}Q_{i}(y_{1},\ldots,y_{k}),$

where each $Q_{i}$ is a monomial with positive coefficient. Thus, we can
compose the above construction sequentially with $n$ distinct sets of
auxiliary counters (only $Y$ is shared).

Let $a_{\text{out},i}$ be output counter for $Q_{i}$. We add a last transition
that computes

$\sum_{1\leq i\leq m}a_{\text{out},i}-\sum_{m<i\leq n}a_{\text{out},i}$

into an extra counter and resets $a_{\text{out},1},\ldots,a_{\text{out},n}$.
This preserves all of the above properties. Indeed, each copy variable is
still only affected locally by a single copy and the next two loops. Note that
ordering the monomials only matters for $\mathbb{D}=\mathbb{N}$ as summing,
e.g., $-2+5$ blocks, while $5-2$ does not.

We may now conclude by proving Lemma 18, which we recall:

See 18

######  Proof 5.3.

Since $\varphi$ is decidable, by Matiyasevich’s theorem333There are two
variants of Matiyasevich’s theorem: stated either over $\mathbb{N}$ or
$\mathbb{Z}$. This follows, e.g., from Lagrange’s four-square theorem, i.e.,
any number from $\mathbb{N}$ can be written as $a^{2}+b^{2}+c^{2}+d^{2}$ where
$a,b,c,d\in\mathbb{Z}$. [Mat71], there exists a polynomial $P$, with integer
coefficients and $k$ variables, such that for every $x\in\mathbb{D}$:

$\varphi(x)\text{ holds}\iff\exists\bm{y}\in\mathbb{D}^{k-1}:P(x,\bm{y})=0.$

Let $\mathcal{V}^{\prime}$ be the affine VASS obtained from Proposition 19 for
$P$, and let $p^{\prime}$ and $q^{\prime}$ be its associated control-states.
Let us show that the affine VASS $\mathcal{V}$ depicted in Figure 9 satisfies
the claim. It uses counters $C\coloneqq Y\cup\overline{Y}$ where
$Y\coloneqq\\{y_{1},\ldots,y_{k}\\}$ are the $k$ first counters of
$\mathcal{V}^{\prime}$ corresponding to the variables of $P$; and where
$\overline{Y}$ forms the other auxiliary counters of $\mathcal{V}^{\prime}$.
We let $m\coloneqq|C|$ and sometimes refer to the counters $C$ as
$\\{c_{1},\ldots,c_{m}\\}$. For the rest of the proof, let us write
$\bm{u}_{X}$ to denote the vector obtained by restricting $\bm{u}$ to counters
$X\subseteq C$.

The affine VASS $\mathcal{V}$ is divided into two parts connecting $p$ to $q$:
the _upper gadget_ made of control-states $\\{a,b_{1},\ldots,b_{m}\\}$, and
the _lower gadget_ made of $\mathcal{V}^{\prime}$.

$\mathcal{V}^{\prime}$$p$$p^{\prime}$$q^{\prime}$$q$reset
$\overline{Y}$$\text{$y_{2}$}\scriptstyle\mathrm{++}$$\text{$y_{k}$}\scriptstyle\mathrm{++}$$\text{$y_{2}$}\scriptstyle\mathrm{--}$$\text{$y_{k}$}\scriptstyle\mathrm{--}$reset
$Y$$a$$b_{1}$$\vdots$$b_{m}$$c_{1}\leftarrow 1$$c_{m}\leftarrow
1$$c_{1}\leftarrow-c_{1}$$c_{m}\leftarrow-
c_{m}$$\text{$c_{1}$}\scriptstyle\mathrm{++}$$\text{$c_{m}$}\scriptstyle\mathrm{++}$$\text{$c_{1}$}\scriptstyle\mathrm{++}$$\text{$c_{m}$}\scriptstyle\mathrm{++}$$\text{$c_{1}$}\scriptstyle\mathrm{--}$$\text{$c_{m}$}\scriptstyle\mathrm{--}$
Figure 9. Affine VASS $\mathcal{V}$ of Lemma 18, where
“$\text{$x$}\scriptstyle\mathrm{++}$”, “$\text{$x$}\scriptstyle\mathrm{--}$”
and “reset $\\{x_{1},x_{2},\ldots\\}$” stand respectively for “$x\leftarrow
x+1$”, “$x\leftarrow x-1$” and “$x_{1}\leftarrow 0;x_{2}\leftarrow 0;\cdots$”.

The purpose of the lower gadget is to satisfy Item 1 by checking whether
$\varphi(y_{1})$ holds. This is achieved by (1) guessing an arbitrary
assignment to counters $Y\setminus\\{y_{1}\\}$; (2) resetting auxiliary
counters $\overline{Y}$; (3) evaluating $P(y_{1},\ldots,y_{k})$; and (4)
resetting counters $Y$.

The purpose of the upper gadget is to satisfy Item 2 by simplifying other
queries from $p$ to $q$. More precisely, the upper gadget allows to generate
an arbitrary nonzero vector. This is achieved by (1) setting each counter
$c_{i}\in C$ to an arbitrary value; (2) nondeterministically setting a counter
$c_{j}$ to $1$; (3) setting $c_{j}$ to an arbitrary positive value; (4)
nondeterministically keeping or flipping the sign of $c_{j}$ (the latter only
works if $\mathbb{D}=\mathbb{Z}$). These steps ensure that all counter values
are possible, provided that some counter $c_{j}\neq 0$.

Let us first show Item 1. Suppose
$p(x,\bm{u})\xrightarrow{*}_{\mathbb{D}}q(0,\bm{0})$. Clearly, the target is
not reached through the upper gadget. So, the following holds for some value
$x^{\prime}$ and some vectors $\bm{y},\bm{y}^{\prime}$:

$p(x,\bm{u}_{Y\setminus\\{y_{1}\\}},\bm{u}_{\overline{Y}})\xrightarrow{*}_{\mathbb{D}}p(x,\bm{y},\bm{u}_{\overline{Y}})\xrightarrow{}_{\mathbb{D}}p^{\prime}(x,\bm{y},\bm{0})\xrightarrow{*}_{\mathbb{D}}q^{\prime}(x^{\prime},\bm{y}^{\prime},\bm{0})\xrightarrow{}_{\mathbb{D}}q(0,\bm{0},\bm{0}).$

Since $\mathcal{V}^{\prime}$ does not alter counters $Y$, we have
$(x,\bm{y})=(x^{\prime},\bm{y}^{\prime})$ and consequently:

$p^{\prime}(x,\bm{y},\bm{0})\xrightarrow{*}_{\mathbb{D}}q^{\prime}(x,\bm{y},\bm{0}).$

Hence, $P(x,\bm{y})=0$, which implies that $\varphi(x)$ holds, as desired.
Conversely, if $\varphi(x)$ holds, then $P(x,\bm{y})=0$ holds for some vector
$\bm{y}$. Clearly, we can achieve the following:

$p(x,\bm{u}_{Y\setminus\\{y_{1}\\}},\bm{u}_{\overline{Y}})\xrightarrow{*}_{\mathbb{D}}p(x,\bm{y},\bm{u}_{\overline{Y}})\xrightarrow{}_{\mathbb{D}}\underbrace{p^{\prime}(x,\bm{y},\bm{0})\xrightarrow{*}_{\mathbb{D}}q^{\prime}(x,\bm{y},\bm{0})}_{\text{by
Prop.~{}\ref{prop:poly:eval}}}\xrightarrow{}_{\mathbb{D}}q(0,\bm{0},\bm{0}).$

Let us now show Item 2. Recall that we want to show that queries not covered
by Item 1 can be answered in polynomial time. These are queries of the form
$r(\bm{v})\xrightarrow{*}_{\mathbb{D}}r^{\prime}(\bm{v}^{\prime})$ where
$\neg(r=p\land r^{\prime}(\bm{v}^{\prime})=q(\bm{0}))$, which amounts to
either $r\neq p$ or $r^{\prime}(\bm{v}^{\prime})\neq q(\bm{0})$.

We assume w.l.o.g. that $r$ can reach $r^{\prime}$ in the underlying graph, as
it can be tested in linear time. Let $Q^{\prime}$ be the control-states of
$\mathcal{V}^{\prime}$. We make a case distinction on $r$ and $r^{\prime}$,
and explain each time how to answer the query.

_Lower part_ :

  * •

_Case $r=r^{\prime}=p$._ Amounts to $\bm{v}^{\prime}(c)=\bm{v}(c)$ for every
$c\in C\setminus\\{y_{2},\ldots y_{k}\\}$.

  * •

_Case $r=p$, $r^{\prime}\in Q^{\prime}$._ Recall that $\mathcal{V}^{\prime}$
does not alter $Y$, that $p$ can generate any values within
$Y\setminus\\{y_{1}\\}$, and that the transition from $p$ to $p^{\prime}$
resets $\overline{Y}$. Hence, we have:

$p(\bm{v})\xrightarrow{*}_{\mathbb{D}}r^{\prime}(\bm{v}^{\prime})\iff\bm{v}(y_{1})=\bm{v}^{\prime}(y_{1})\land
p^{\prime}(\bm{v}^{\prime}_{Y},\bm{0})\xrightarrow{*}_{\mathbb{D}}r^{\prime}(\bm{v}^{\prime}_{Y},\bm{v}^{\prime}_{\overline{Y}}).$

The latter can be answered in polynomial time by Proposition 19.

  * •

_Case $r=p$, $r^{\prime}=q$._ Since $r=p$, we must have
$\bm{v}^{\prime}\neq\bm{0}$ by assumption. Thus, the answer is “true” since
the upper gadget allows to reach any nonzero vector in $q$.

  * •

_Case $r,r^{\prime}\in Q^{\prime}$._ Can be tested in polynomial time by
Proposition 19.

  * •

_Case $r\in Q^{\prime}$, $r^{\prime}=q$._ Recall that $\mathcal{V}^{\prime}$
does not alter $Y$, and that the transition from $q^{\prime}$ to $q$ resets
$Y$, but not $\overline{Y}$. Hence, we have:

$r(\bm{v})\xrightarrow{*}_{\mathbb{D}}q(\bm{v}^{\prime})\iff
r(\bm{v}_{Y},\bm{v}_{\overline{Y}})\xrightarrow{*}_{\mathbb{D}}q^{\prime}(\bm{v}_{Y},\bm{v}^{\prime}_{\overline{Y}}).$

The latter can be answered in polynomial time by Proposition 19.

_Upper part:_

  * •

_Case $r\in\\{p,a\\}$ and $r^{\prime}=a$._ The answer is always “true”.

  * •

_Case $r\in\\{p,a\\}$ and $r^{\prime}=b_{i}$._ Amounts to
$\bm{v}^{\prime}(c_{i})\geq 1$.

  * •

_Case $r=a$, $r^{\prime}=q$._ Amounts to
$\bigvee_{i\in[m]}\bm{v}^{\prime}(c_{i})\neq 0$.

  * •

_Case $r=r^{\prime}=b_{i}$._ Amounts to
$\bm{v}^{\prime}(c_{i})\geq\bm{v}(c_{i})$ and
$\bm{v}^{\prime}(c_{j})=\bm{v}(c_{j})$ for all $j\neq i$.

  * •

_Case $r=b_{i}$, $r^{\prime}=q$._ Amounts to
$|\bm{v}^{\prime}(c_{i})|\geq|\max(\bm{v}(c_{i}),0)|$ and
$\bm{v}^{\prime}(c_{j})=\bm{v}(c_{j})$ for $j\neq i$.

##  6\. Conclusion and further work

Motivated by the use of relaxations to alleviate the tremendous complexity of
reachability in VASS, we have studied the complexity of integer reachability
in affine VASS.

Namely, we have shown a trichotomy on the complexity of integer reachability
for affine VASS: it is -complete for any class of reset matrices; -complete
for any class of pseudo-transfers matrices and any class of pseudo-copies
matrices; and undecidable for _any_ other class. Moreover, the notions and
techniques introduced along the way allowed us to give a complexity dichotomy
for (standard) reachability in affine VASS: it is decidable for any class of
permutation matrices, and undecidable for any other class. This provides a
complete general landscape of the complexity of reachability in affine VASS.

We further complemented these trichotomy and dichotomy by showing that, in
contrast to the case of classes, the (integer or standard) reachability
problem has an arbitrary complexity when it is parameterized by a fixed affine
VASS. A further direction of study is the range of possible complexities for
integer reachability relations for specific matrix monoids, which is entirely
open.

Another direction lies in the related _coverability problem_ which asks
whether $p(\bm{u})\xrightarrow{*}_{\mathbb{D}}q(\bm{v}^{\prime})$ for some
$\bm{v}^{\prime}\geq\bm{v}$ rather than $\bm{v}^{\prime}=\bm{v}$. As shown in
the setting of [HH14, CHH18], this problem is equivalent to the reachability
problem for $\mathbb{D}=\mathbb{Z}$. Indeed, given an affine VASS
$\mathcal{V}$, it is possible to construct an affine VASS
$\mathcal{V}^{\prime}$ such that

$p(\bm{u})\xrightarrow{*}_{\mathbb{Z}}q(\bm{v})\text{ in }\mathcal{V}\iff
p(\bm{u},-\bm{u})\xrightarrow{*}_{\mathbb{Z}}q(\bm{v},-\bm{v})\text{ in
}\mathcal{V}^{\prime}.$ (*)

This can be achieved by replacing each affine transformation
$\mathbf{A}\bm{x}+\bm{b}$ of $\mathcal{V}$ by

$\begin{bmatrix}\mathbf{A}&\mathbf{0}\\\
\mathbf{0}&\mathbf{A}\end{bmatrix}\begin{bmatrix}\bm{x}\\\
\bm{x}^{\prime}\end{bmatrix}+\begin{bmatrix}\bm{b}\\\ -\bm{b}\end{bmatrix}.$

Furthermore, note that classes are closed under this construction, which shows
that integer coverability and integer reachability are equivalent w.r.t.
classes. However, (* ‣ 6) does not hold for $\mathbb{D}=\mathbb{N}$. In this
case, it is well-known, e.g., that the coverability problem is decidable for
VASS with resets or transfers, while the reachability problem is not. Hence, a
precise characterization of the complexity landscape remains unknown in this
case.

## References

  * [AK76] Toshiro Araki and Tadao Kasami.  Some decision problems related to the reachability problem for Petri nets.  Theoretical Computer Science, 3(1):85–104, 1976.
  * [ALW16] Konstantinos Athanasiou, Peizun Liu, and Thomas Wahl.  Unbounded-thread program verification using thread-state equations.  In Proc. $8^{\text{th}}$ International Joint Conference on Automated Reasoning (IJCAR), pages 516–531, 2016.
  * [BFHH17] Michael Blondin, Alain Finkel, Christoph Haase, and Serge Haddad.  The logical view on continuous Petri nets.  ACM Transactions on Computational Logic (TOCL), 18(3):24:1–24:28, 2017.
  * [BFP12] Rémi Bonnet, Alain Finkel, and M. Praveen.  Extending the Rackoff technique to affine nets.  In Proc. $32^{\text{nd}}$ Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), pages 301–312, 2012.
  * [BH17] Michael Blondin and Christoph Haase.  Logics for continuous reachability in Petri nets and vector addition systems with states.  In Proc. $32^{\text{nd}}$ Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–12, 2017.
  * [BHK+20] Georgina Bumpus, Christoph Haase, Stefan Kiefer, Paul-Ioan Stoienescu, and Jonathan Tanner.  On the size of finite rational matrix semigroups.  In Proc. $47^{\text{th}}$ International Colloquium on Automata, Languages, and Programming (ICALP), volume 168, pages 115:1–115:13, 2020.
  * [BHM18] Michael Blondin, Christoph Haase, and Filip Mazowiecki.  Affine extensions of integer vector addition systems with states.  In Proc. $29^{\text{th}}$ International Conference on Concurrency Theory (CONCUR), pages 14:1–14:17, 2018.
  * [BHMR19] Michael Blondin, Christoph Haase, Filip Mazowiecki, and Mikhail A. Raskin.  Affine extensions of integer vector addition systems with states.  CoRR, 2019.  Accepted to Logical Methods in Computer Science (LMCS) in October 2020 with minor revisions.
  * [CFM12] Michaël Cadilhac, Alain Finkel, and Pierre McKenzie.  Affine Parikh automata.  RAIRO – Theoretical Informatics and Applications, 46(4):511–545, 2012.
  * [CHH18] Dmitry Chistikov, Christoph Haase, and Simon Halfon.  Context-free commutative grammars with integer counters and resets.  Theoretical Computer Science, 735:147–161, 2018.
  * [CLL+19] Wojciech Czerwiński, Sławomir Lasota, Ranko Lazić, Jérôme Leroux, and Filip Mazowiecki.  The reachability problem for Petri nets is not elementary.  In Proc. $51^{\text{st}}$ Annual ACM SIGACT Symposium on Theory of Computing (STOC), pages 24–33, 2019.
  * [DFPS98] Catherine Dufourd, Alain Finkel, and Philippe Schnoebelen.  Reset nets between decidability and undecidability.  In Proc. $25^{\text{th}}$ International Colloquium on Automata, Languages and Programming (ICALP), pages 103–115, 1998.
  * [DRV02] Giorgio Delzanno, Jean-François Raskin, and Laurent Van Begin.  Towards the automated verification of multithreaded Java programs.  In Proc. $8^{\text{th}}$ International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 173–187, 2002.
  * [EGLM17] Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar.  Verification of population protocols.  Acta Informatica, 54(2):191–215, 2017.
  * [ELM+14] Javier Esparza, Ruslán Ledesma-Garza, Rupak Majumdar, Philipp J. Meyer, and Filip Nikšić.  An SMT-based approach to coverability analysis.  In Proc. $26^{\text{th}}$ International Conference on Computer Aided Verification (CAV), pages 603–619, 2014.
  * [FGH13] Alain Finkel, Stefan Göller, and Christoph Haase.  Reachability in register machines with polynomial updates.  In Proc. $38^{\text{th}}$ International Symposium on Mathematical Foundations of Computer Science (MFCS), pages 409–420, 2013.
  * [FH15] Estíbaliz Fraca and Serge Haddad.  Complexity analysis of continuous Petri nets.  Fundamenta Informaticae, 137(1):1–28, 2015.
  * [FL02] Alain Finkel and Jérôme Leroux.  How to compose Presburger-accelerations: Applications to broadcast protocols.  In Proc. $22^{\text{nd}}$ Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), pages 145–156, 2002\.
  * [GS92] Steven M. German and A. Prasad Sistla.  Reasoning about systems with many processes.  Journal of the ACM, 39(3):675–735, 1992.
  * [HGD08] Monika Heiner, David R. Gilbert, and Robin Donaldson.  Petri nets for systems and synthetic biology.  In Formal Methods for Computational Systems Biology, pages 215–264, 2008.
  * [HH14] Christoph Haase and Simon Halfon.  Integer vector addition systems with states.  In Proc. $8^{\text{th}}$ International Workshop on Reachability Problems (RP), pages 112–124, 2014.
  * [HU79] John E. Hopcroft and Jeffrey D. Ullman.  Introduction to Automata Theory, Languages and Computation.  Addison-Wesley, 1979.
  * [IS16] Radu Iosif and Arnaud Sangnier.  How hard is it to verify flat affine counter systems with the finite monoid property?  In Proc. $14^{\text{th}}$ International Symposium on Automated Technology for Verification and Analysis (ATVA), pages 89–105, 2016.
  * [KKW14] Alexander Kaiser, Daniel Kroening, and Thomas Wahl.  A widening approach to multithreaded program verification.  ACM Trans. on Prog. Languages and Systems, 36(4):14:1–14:29, 2014.
  * [Kos82] S. Rao Kosaraju.  Decidability of reachability in vector addition systems (preliminary version).  In Proc. $14^{\text{th}}$ Symposium on Theory of Computing (STOC), pages 267–281, 1982.
  * [Lam92] Jean-Luc Lambert.  A structure to decide reachability in Petri nets.  Theoretical Computer Science, 99(1):79–104, 1992.
  * [Ler10] Jérôme Leroux.  The general vector addition system reachability problem by Presburger inductive invariants.  Logical Methods in Computer Science, 6(3), 2010.
  * [Ler11] Jérôme Leroux.  Vector addition system reachability problem: a short self-contained proof.  In Proc. $38^{\text{th}}$ Symposium on Principles of Programming Languages (POPL), pages 307–316, 2011.
  * [Ler12] Jérôme Leroux.  Vector addition systems reachability problem (A simpler solution).  In Turing-100 – The Alan Turing Centenary, pages 214–228, 2012\.
  * [Lip76] Richard J. Lipton.  The reachability problem requires exponential space.  Technical Report 63, Department of Computer Science, Yale University, 1976\.
  * [LS15] Jérôme Leroux and Sylvain Schmitz.  Demystifying reachability in vector addition systems.  In Proc. $30^{\text{th}}$ Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 56–67, 2015.
  * [LS19] Jérôme Leroux and Sylvain Schmitz.  Reachability in vector addition systems is primitive-recursive in fixed dimension.  In Proc. $34^{\text{th}}$ Symposium on Logic in Computer Science (LICS), 2019.
  * [Mat71] Yu. V. Matijasevich.  Diophantine representation of enumerable predicates.  Mathematics of the USSR-Izvestiya, 5(1):1–28, Feb 1971.
  * [May81] Ernst W. Mayr.  An algorithm for the general Petri net reachability problem.  In Proc. $13^{\text{th}}$ Symposium on Theory of Computing (STOC), pages 238–246, 1981.
  * [Rei15] Julien Reichert.  Reachability games with counters: decidability and algorithms.  PhD thesis, École normale supérieure de Cachan, France, 2015\.
  * [SK19] Jake Silverman and Zachary Kincaid.  Loop summarization with rational vector addition systems.  In Proc. $31^{\text{st}}$ International Conference on Computer Aided Verification (CAV), pages 97–115, 2019.
  * [ST77] George S. Sacerdote and Richard L. Tenney.  The decidability of the reachability problem for vector addition systems (preliminary version).  In Proc. $9^{\text{th}}$ Symposium on Theory of Computing (STOC), pages 61–76, 1977.
  * [Val78] Rüdiger Valk.  Self-modifying nets, a natural extension of Petri nets.  In Proc. Fifth Colloquium on Automata, Languages and Programming (ICALP), pages 464–476, 1978.
  * [van98] Wil van der Aalst.  The application of Petri nets to workflow management.  Journal of Circuits, Systems, and Computers, 8(1):21–66, 1998.
  * [WvdAtHE09] Moe Thandar Wynn, Wil M. P. van der Aalst, Arthur H. M. ter Hofstede, and David Edmond.  Synchronization and cancelation in workflows based on reset nets.  International Journal of Cooperative Information Systems, 18(1):63–114, 2009.

##  Appendix A Appendix

###  A.1. Details for the proof of Proposition 2

Pseudo-transfer matrix. Let us first prove properties 1 and 2 stated within
the proof of Proposition 4 for the case where $\mathbf{A}$ is a pseudo-
transfer matrix. The validity of 1 for $\mathbf{B}_{s,t}$ follows from:

$\displaystyle(\mathbf{B}_{s,t}\cdot\bm{e}_{s})(k)$
$\displaystyle=(\mathbf{B}_{s,t})_{k,s}$
$\displaystyle=\mathbf{A}^{\prime}_{\pi_{s,t}(k),b}$ (since $\pi_{s,t}(s)=b$)
$\displaystyle=-1\text{ if }\pi_{s,t}(k)=a\text{ else }0$ (1)
$\displaystyle=-1\text{ if }k=t\text{ else }0$ (since $\pi_{s,t}(t)=a$) where
(1) follows from $\mathbf{A}^{\prime}_{a,b}=-1$ and the fact that
$\mathbf{A}^{\prime}$ is a pseudo-transfer matrix. The validity of 2
$\mathbf{B}_{s,t}$ follows from:
$\displaystyle(\mathbf{B}_{s,t}\cdot\bm{e}_{u})(k)$
$\displaystyle=(\mathbf{B}_{s,t})_{k,u}$
$\displaystyle=\mathbf{A}^{\prime}_{\pi_{s,t}(k),u}=1$ (since $u\in
X^{\prime}\setminus\\{s,t\\}$) $\displaystyle=1\text{ if }\pi_{s,t}(k)=u\text{
else }0$ (by def. of $\mathbf{A}^{\prime}$) $\displaystyle=1\text{ if
}k=u\text{ else }0$ $\displaystyle\text{(since $\pi_{s,t}(u)=u$)}.$

The same proofs apply mutatis mutandis for $\mathbf{C}_{t}$.

Pseudo-copy matrix. Let us now prove Proposition 2 for the case where
$\mathbf{A}$ is a pseudo-copy matrix. For this case, we consider
$?$-implementation and hence $V_{X}=\mathbb{Z}^{d^{\prime}}$. Similarly to the
case of pseudo-transfer matrices, we claim that for every $\bm{v}\in V_{X}$
and every $s,t,u\in X^{\prime}$ such that $s\neq t$ and $u\not\in\\{s,t\\}$,
the following holds:

  1. (1)

$(\mathbf{B}_{s,t}\cdot\bm{v})(t)=(\mathbf{C}_{t}\cdot\bm{v})(t)=-\bm{v}(s)$;

  2. (2)

$(\mathbf{B}_{s,t}\cdot\bm{v})(u)=(\mathbf{C}_{t}\cdot\bm{v})(u)=\bm{v}(u)$.

Indeed, we have:

$\displaystyle(\mathbf{B}_{s,t}\cdot\bm{v})(t)$
$\displaystyle=\sum_{\ell\in[d]\cup
X^{\prime}}(\mathbf{B}_{s,t})_{t,\ell}\cdot\bm{v}(\ell)$
$\displaystyle=\sum_{\ell\in[d]\cup
X^{\prime}}\mathbf{A}^{\prime}_{a,\pi_{s,t}(\ell)}\cdot\bm{v}(\ell)$ (since
$\pi_{s,t}(t)=a$)
$\displaystyle=\mathbf{A}^{\prime}_{a,b}\cdot\bm{v}(s)+\sum_{\begin{subarray}{c}\ell\in[d]\cup
X^{\prime}\\\ \ell\neq
t\end{subarray}}\\!\\!\mathbf{A}^{\prime}_{a,\pi_{s,t}(\ell)}\cdot\bm{v}(\ell)$
(since $\pi_{s,t}(s)=b$) $\displaystyle=-\bm{v}(s)$ $\displaystyle\text{(by
$\mathbf{A}^{\prime}_{a,j}\neq 0\iff j=b$)},$ where the last equality follows
from $\mathbf{A}^{\prime}_{a,b}=-1$ and the fact that $\mathbf{A}^{\prime}$ is
a pseudo-copy matrix. Moreover, we have:
$\displaystyle(\mathbf{B}_{s,t}\cdot\bm{v})(u)$
$\displaystyle=\sum_{\ell\in[d]\cup
X^{\prime}}(\mathbf{B}_{s,t})_{u,\ell}\cdot\bm{v}(\ell)$
$\displaystyle=\mathbf{A}^{\prime}_{u,u}\cdot\bm{v}(u)+\sum_{\begin{subarray}{c}\ell\in[d]\cup
X^{\prime}\\\ \ell\neq
u\end{subarray}}\\!\\!\mathbf{A}^{\prime}_{a,\pi_{s,t}(\ell)}\cdot\bm{v}(\ell)$
(since $\pi_{s,t}(u)=u$) $\displaystyle=\bm{v}(u)$ $\displaystyle\text{(by
$\mathbf{A}^{\prime}_{u,j}\neq 1\iff j=u$)}.$

Again, the same proofs apply mutatis mutandis for $\mathbf{C}_{t}$.

We now prove the proposition. Let $x\in X$ and $\bm{v}\in V_{X}$. We obviously
have $\mathbf{F}_{x}\cdot\bm{v}\in V_{X}$. If $a\neq b$, we have:

$\displaystyle(\mathbf{F}_{x}\cdot\bm{v})(x)$
$\displaystyle=(\mathbf{B}_{z,x}\cdot(\mathbf{B}_{y,z}\cdot\mathbf{B}_{x,y}\cdot\bm{v}))(x_{)}$
(by def. of $\mathbf{F}_{x}$)
$\displaystyle=-(\mathbf{B}_{y,z}\cdot(\mathbf{B}_{x,y}\cdot\bm{v}))(z)$ (by
1) $\displaystyle=(\mathbf{B}_{x,y}\cdot\bm{v})(y)$ (by 1)
$\displaystyle=-\bm{v}(x)$
$\displaystyle\text{(by~{}\ref{itm:src:tgt:flip})},$ and if $a=b$, we have:
$\displaystyle(\mathbf{F}_{x}\cdot\bm{v})(x)$
$\displaystyle=(\mathbf{C}_{x}\cdot\bm{v})(x)$ (by def. of $\mathbf{F}_{x}$)
$\displaystyle=-\bm{v}(x)$
$\displaystyle\text{(by~{}\ref{itm:src:tgt:flip})}.$

Similarly, by applying 2 repeatedly, we derive
$(\mathbf{F}_{x}\cdot\bm{v})(y)=\bm{v}(y)$ for every $y\in X\setminus\\{x\\}$.
∎

###  A.2. Details for the proof of Proposition 4

The details of the proof are similar to those of the proof of Proposition 2.

Transfer matrix. Let us first prove properties 1 and 2 stated within the proof
of Proposition 4 for the case where $\mathbf{A}$ is a transfer matrix. The
validity of 1 follows from:

$\displaystyle(\mathbf{B}_{s,t}\cdot\bm{e}_{s})(k)=1$
$\displaystyle\iff(\mathbf{B}_{s,t})_{k,s}=1$
$\displaystyle\iff\mathbf{A}^{\prime}_{\pi_{s,t}(k),b}=1$ (since
$\pi_{s,t}(s)=b$) $\displaystyle\iff\pi_{s,t}(k)=a$ (since $\mathbf{A}$ is a
transfer matrix) $\displaystyle\iff k=t.$ The validity of 2 follows from:
$\displaystyle(\mathbf{B}_{s,t}\cdot\bm{e}_{u})(k)=1$
$\displaystyle\iff(\mathbf{B}_{s,t})_{k,u}=1$
$\displaystyle\iff\mathbf{A}^{\prime}_{\pi_{s,t}(k),u}=1$ (since $u\in
X^{\prime}\setminus\\{s,t\\}$) $\displaystyle\iff\pi_{s,t}(k)=u$ (by def. of
$\mathbf{A}^{\prime}$) $\displaystyle\iff k=u.$

Copy matrix. Let us now prove Proposition 4 for the case where $\mathbf{A}$ is
a copy matrix. For this case, we consider $?$-implementation and hence
$V_{X}=\mathbb{Z}^{d^{\prime}}$. Similarly to the case of transfer matrices,
we claim that for every $\bm{v}\in V_{X}$ and every $s,t,u\in X^{\prime}$ such
that $s\neq t$ and $u\not\in\\{s,t\\}$, the following holds:

  1. (1)

$(\mathbf{B}_{s,t}\cdot\bm{v})(t)=\bm{v}(s)$;

  2. (2)

$(\mathbf{B}_{s,t}\cdot\bm{v})(u)=\bm{v}(u)$.

Indeed, we have:

$\displaystyle(\mathbf{B}_{s,t}\cdot\bm{v})(t)$
$\displaystyle=\sum_{\ell\in[d]\cup
X^{\prime}}(\mathbf{B}_{s,t})_{t,\ell}\cdot\bm{v}(\ell)$
$\displaystyle=\sum_{\ell\in[d]\cup
X^{\prime}}\mathbf{A}^{\prime}_{a,\pi_{s,t}(\ell)}\cdot\bm{v}(\ell)$ (since
$\pi_{s,t}(t)=a$)
$\displaystyle=\mathbf{A}^{\prime}_{a,b}\cdot\bm{v}(s)+\sum_{\begin{subarray}{c}\ell\in[d]\cup
X^{\prime}\\\ \ell\neq
t\end{subarray}}\\!\\!\mathbf{A}^{\prime}_{a,\pi_{s,t}(\ell)}\cdot\bm{v}(\ell)$
(since $\pi_{s,t}(s)=b$) $\displaystyle=\bm{v}(s)$ $\displaystyle\text{(by
$\mathbf{A}^{\prime}_{a,j}=1\iff j=b$)},$ where the last equality follows from
$\mathbf{A}^{\prime}_{a,b}=1$ and the fact that $\mathbf{A}^{\prime}$ is a
copy matrix. Morever, we have: $\displaystyle(\mathbf{B}_{s,t}\cdot\bm{v})(u)$
$\displaystyle=\sum_{\ell\in[d]\cup
X^{\prime}}(\mathbf{B}_{s,t})_{u,\ell}\cdot\bm{v}(\ell)$
$\displaystyle=\mathbf{A}^{\prime}_{u,u}\cdot\bm{v}(u)+\sum_{\begin{subarray}{c}\ell\in[d]\cup
X^{\prime}\\\ \ell\neq
u\end{subarray}}\\!\\!\mathbf{A}^{\prime}_{a,\pi_{s,t}(\ell)}\cdot\bm{v}(\ell)$
(since $\pi_{s,t}(u)=u$) $\displaystyle=\bm{v}(u)$ $\displaystyle\text{(by
$\mathbf{A}^{\prime}_{u,j}=1\iff j=u$)}.$

We may now prove the proposition. Let $\bm{v}\in V_{X}$ and let $x,y\in X$ be
such that $x\neq y$. We obviously have $\mathbf{F}_{x,y}\cdot\bm{v}\in V_{X}$.
Moreover, we have:

$\displaystyle(\mathbf{F}_{x,y}\cdot\bm{v})(x)$
$\displaystyle=(\mathbf{B}_{z,x}\cdot(\mathbf{B}_{x,y}\cdot\mathbf{B}_{y,z}\cdot\bm{v}))(x)$
(by def. of $\mathbf{F}_{x,y}$)
$\displaystyle=(\mathbf{B}_{x,y}\cdot(\mathbf{B}_{y,z}\cdot\bm{v}))(z)$ (by 1)
$\displaystyle=(\mathbf{B}_{y,z}\cdot\bm{v})(z)$ (by 2)
$\displaystyle=\bm{v}(y)$ $\displaystyle\text{(by~{}\ref{itm:src:tgt:copy})},$

and symmetrically $(\mathbf{F}_{x,y}\cdot\bm{v})(y)=\bm{v}(x)$. Similarly, by
applying 2 three times, we derive $(\mathbf{F}_{x,y}\cdot\bm{v})(u)=\bm{v}(u)$
for every $u\in X\setminus\\{x,y\\}$. ∎

###  A.3. Details for the proof of Proposition 6

Let us prove the technical lemma invoked within the proof of Proposition 6:

######  Lemma 20.

For every class $\mathcal{C}$, if $\mathcal{C}$ contains a matrix which has a
row (resp. column) with at least two nonzero elements, then $\mathcal{C}$ also
contains a matrix which has a row (resp. column) with at least two nonzero
elements with the same sign.

######  Proof A.1.

We first consider the case of rows. Let $\mathbf{A}\in\mathcal{C}$,
$i,j,k\in[d]$ and $a,b\neq 0$ be such that $\mathbf{A}_{i,j}=a$,
$\mathbf{A}_{i,k}=b$ and $j\neq k$. If $a$ and $b$ have the same sign, then we
are done. Thus, assume without loss of generality that $a<0$ and $b>0$.

Let us first give an informal overview of the proof where we see $\mathbf{A}$
as an operation over some counters. We have two counters $x$ and $y$ that we
wish to sum up (with some positive integer coefficients), using a supply of
counters set to zero. We apply $\mathbf{A}$ to $x$ and some zero counters to
produce $a\cdot x$ in some counter (while discarding extra noise into some
other ones), and we then apply $\mathbf{A}$ again to $a\cdot x$, $y$ and some
zero counters in such a way that we get $a^{2}\cdot x+b\cdot y$. The matrix
achieving this procedure will have $a^{2}$ and $b$ on a common row.

More formally, we wish to obtain a matrix $\mathbf{D}$ with positive entries
$a^{2}$ and $b$, and more precisely such that
$\mathbf{D}_{i,j^{\prime}}=a^{2}$ and $\mathbf{D}_{i,k}=b$ for some counter
$j^{\prime}$. Let $\mathbf{B}\coloneqq{\mathbf{A}}\\!\\!\restriction_{d}$,
$\mathbf{C}\coloneqq\sigma({\mathbf{B}})$ and
$\mathbf{D}\coloneqq\mathbf{B}\cdot\mathbf{C}$ where $\sigma\colon[2d]\to[2d]$
is the following permutation:

$\sigma\coloneqq\begin{cases}(j;i;i+d)\cdot\prod_{\ell\in[d]\setminus\\{i,j\\}}(\ell;\ell+d)&\text{if
}j\neq i,\\\ \prod_{\ell\in[d]\setminus\\{i\\}}(\ell;\ell+d)&\text{if
}j=i.\end{cases}$

We claim that $\mathbf{D}$ is as desired. First, observe that:

$\displaystyle\mathbf{D}_{i,k}$
$\displaystyle=\sum_{\ell\in[2d]}\mathbf{B}_{i,\ell}\cdot\mathbf{B}_{\sigma(\ell),k+d}$
(by def. of $\mathbf{D}$ and $\sigma(k)=k+d$)
$\displaystyle=\mathbf{B}_{i,k}\cdot\mathbf{B}_{k+d,k+d}$ (since
$\mathbf{B}_{\sigma(\ell),k+d}\neq 0\iff\sigma(\ell)=k+d$) $\displaystyle=b$
$\displaystyle\text{(since $\mathbf{B}_{k+d,k+d}=1$)}.$

Thus, $\mathbf{D}$ has a positive entry on row $i$. It remains to show that
$\mathbf{D}$ has another positive entry on row $i$. We make a case distinction
on whether $j=i$.

Case $j\neq i$. Note that $k\neq i+d$. Hence, we are done since:

$\displaystyle\mathbf{D}_{i,i+d}$
$\displaystyle=\sum_{\ell\in[2d]}\mathbf{B}_{i,\ell}\cdot\mathbf{B}_{\sigma(\ell),j}$
(by def. of $\mathbf{D}$ and $\sigma(i+d)=j$)
$\displaystyle=\sum_{\ell\,:\,\ell,\sigma(\ell)\in[d]}\mathbf{B}_{i,\ell}\cdot\mathbf{B}_{\sigma(\ell),j}$
(since $\mathbf{B}={\mathbf{A}}\\!\\!\restriction_{d}$ and $i,j\in[d]$)
$\displaystyle=\mathbf{B}_{i,j}\cdot\mathbf{B}_{i,j}$ (by def. of $\sigma$)
$\displaystyle=a^{2}.$

Case $j=i$. Note that $k\neq j=i$. Hence, we are done since:

$\displaystyle\mathbf{D}_{i,i}$
$\displaystyle=\sum_{\ell\in[2d]}\mathbf{B}_{i,\ell}\cdot\mathbf{B}_{\sigma(\ell),i}$
(by def. of $\mathbf{D}$ and $\sigma(i)=i$)
$\displaystyle=\sum_{\ell:\ell,\sigma(\ell)\in[d]}\mathbf{B}_{i,\ell}\cdot\mathbf{B}_{\sigma(\ell),i}$
(since $\mathbf{B}={\mathbf{A}}\\!\\!\restriction_{d}$ and $i\in[d]$)
$\displaystyle=\mathbf{B}_{i,i}\cdot\mathbf{B}_{i,i}$ (by def. of $\sigma$)
$\displaystyle=a^{2}$ $\displaystyle\text{(since $i=j$)}.$

We are done proving the proposition for the case of rows.

For the case of columns, we can instead assume that
$\mathbf{A}^{\mathsf{T}}\in\mathcal{C}$, i.e., the transpose of $\mathbf{A}$
belongs to $\mathcal{C}$. Since $\mathbf{D}^{\mathsf{T}}$ is as desired, we
simply have to show that $\mathbf{D}^{\mathsf{T}}\in\mathcal{C}$. This is the
case since:

$\displaystyle\mathbf{D}^{\mathsf{T}}$
$\displaystyle=(\mathbf{B}\cdot\mathbf{C})^{\mathsf{T}}$
$\displaystyle=\mathbf{C}^{\mathsf{T}}\cdot\mathbf{B}^{\mathsf{T}}$
$\displaystyle=(\mathbf{P}_{\sigma}\cdot\mathbf{B}\cdot\mathbf{P}_{\sigma^{-1}})^{\mathsf{T}}\cdot\mathbf{B}^{\mathsf{T}}$
(since $\mathbf{C}=\sigma({\mathbf{B}})$)
$\displaystyle=(\mathbf{P}_{\sigma}\cdot\mathbf{B}^{\mathsf{T}}\cdot\mathbf{P}_{\sigma^{-1}})\cdot\mathbf{B}^{\mathsf{T}}$
(since $\mathbf{P}_{\pi^{-1}}=\mathbf{P}_{\pi}^{\mathsf{T}}$ for every perm.
$\pi$)
$\displaystyle=\sigma({\mathbf{B}^{\mathsf{T}}})\cdot\mathbf{B}^{\mathsf{T}}$
$\displaystyle=\sigma({({\mathbf{A}}\\!\\!\restriction_{d})^{\mathsf{T}}})\cdot({\mathbf{A}}\\!\\!\restriction_{d})^{\mathsf{T}}$
$\displaystyle=\sigma({(\mathbf{A}^{\mathsf{T}})}\\!\\!\restriction_{d})\cdot{(\mathbf{A}^{\mathsf{T}})}\\!\\!\restriction_{d}$
$\displaystyle\text{(since
$({\mathbf{A}}\\!\\!\restriction_{d})^{\mathsf{T}}={(\mathbf{A}^{\mathsf{T}})}\\!\\!\restriction_{d}$)}.$
$\displaystyle\in\mathcal{C}$ $\displaystyle\text{(since
$\mathbf{A}^{\mathsf{T}}\in\mathcal{C}$)}.$

###  A.4. Details for the proof of Theorem 16

We prove the missing details for both cases:

Case $\mathbf{A}_{\star,i}=\bm{0}$. We have
$\mathbf{B}_{x}\cdot\bm{e}_{y}=\bm{e}_{y}$ since:

$\displaystyle(\mathbf{B}_{x}\cdot\bm{e}_{y})(k)$
$\displaystyle=(\mathbf{B}_{x}){k,y}$
$\displaystyle=\mathbf{A}^{\prime}_{\sigma_{x}(k),y}$ (since $y\neq x$)
$\displaystyle=1\iff k=y$ (by def. of $\mathbf{A}^{\prime}$ and $\sigma_{x}$).
Case $\mathbf{A}_{i,\star}=\bm{0}$. We have:
$\displaystyle(\mathbf{B}_{x}\cdot\bm{v})(y)$
$\displaystyle=\sum_{\ell\in[d+n]}\mathbf{B}_{y,\ell}\cdot\bm{v}(\ell)$
$\displaystyle=\mathbf{A}^{\prime}_{y,y}\cdot\bm{v}(y)$ (by $y\neq x$ and def.
of $\mathbf{A}^{\prime}$ and $\sigma_{x}$) $\displaystyle=\bm{v}(y).$ ∎