1731 LABEL:LastPageSep. 30, 2019Jul. 20, 2021 *A preliminary version of this
paper appeared in the proceedings of the $29^{\text{th}}$ International
Conference on Concurrency Theory (CONCUR), 2018 [BHM18].

# Affine Extensions of
Integer Vector Addition Systems with States

Michael Blondin  Université de Sherbrooke, Canada
<EMAIL_ADDRESS>,  Christoph Haase  University of Oxford,
United Kingdom<EMAIL_ADDRESS>,  Filip Mazowiecki  Max Planck
Institute for Software Systems, Germany<EMAIL_ADDRESS>and  Mikhail
Raskin  Technische Universität München, Germany<EMAIL_ADDRESS>
###### Abstract.

We study the reachability problem for affine $\mathbb{Z}$-VASS, which are
integer vector addition systems with states in which transitions perform
affine transformations on the counters. This problem is easily seen to be
undecidable in general, and we therefore restrict ourselves to affine
$\mathbb{Z}$-VASS with the finite-monoid property (afmp-$\mathbb{Z}$-VASS).
The latter have the property that the monoid generated by the matrices
appearing in their affine transformations is finite. The class of
afmp-$\mathbb{Z}$-VASS encompasses classical operations of counter machines
such as resets, permutations, transfers and copies. We show that reachability
in an afmp-$\mathbb{Z}$-VASS reduces to reachability in a $\mathbb{Z}$-VASS
whose control-states grow linearly in the size of the matrix monoid. Our
construction shows that reachability relations of afmp-$\mathbb{Z}$-VASS are
semilinear, and in particular enables us to show that reachability in
$\mathbb{Z}$-VASS with transfers and $\mathbb{Z}$-VASS with copies is PSPACE-
complete. We then focus on the reachability problem for affine
$\mathbb{Z}$-VASS with monogenic monoids: (possibly infinite) matrix monoids
generated by a single matrix. We show that, in a particular case, the
reachability problem is decidable for this class, disproving a conjecture
about affine $\mathbb{Z}$-VASS with infinite matrix monoids we raised in a
preliminary version of this paper. We complement this result by presenting an
affine $\mathbb{Z}$-VASS with monogenic matrix monoid and undecidable
reachability relation.

M. Blondin was supported by a Discovery Grant from the Natural Sciences and
Engineering Research Council of Canada (NSERC), and by a Quebec–Bavaria
project and a start-up grant funded by the Fonds de recherche du Québec –
Nature et technologies (FRQNT)

F. Mazowiecki’s research has been carried out with financial support from the
French State, managed by the French National Research Agency (ANR) in the
frame of the “Investments for the future” Programme IdEx Bordeaux
(ANR-10-IDEX-03-02).

M. Raskin was supported by funding from 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)_ are a fundamental model of
computation comprising a finite-state controller with a finite number of
counters ranging over the natural numbers. When a transition is taken, a
counter can be incremented or decremented provided that the resulting counter
value is greater than or equal to zero. Since the counters of a VASS are
unbounded, a VASS gives rise to an infinite transition system. One of the
biggest advantages of VASS is that most of the standard decision problems such
as configuration reachability and coverability are decidable [KM69, May84,
Kos82, Ler12]. Those properties make VASS and their extensions a prime choice
for reasoning about and modelling concurrent, distributed and parametrised
systems, see e.g. the recent surveys by Abdulla and Delzanno [AD16, Del16].

In order to increase their modelling power, numerous extensions of plain VASS
have been proposed and studied in the literature over the last 25 years. Due
to the infinite-state nature of VASS, even minor extensions often cross the
undecidability frontier. For example, while in the extension of VASS with
hierarchical zero-tests on counters both reachability and coverability remain
decidable [Rei08, Bon13], all important decision problems for VASS with two
counters which can arbitrarily be tested for zero are undecidable [Min67].
Another example is the extension of VASS with reset and transfer operations.
In a _reset VASS_ , transitions may set a counter to zero, whereas _transfer
VASS_ generalize reset VASS and allow transitions to move the contents of a
counter onto another. While it was initially widely believed that any
extension of VASS either renders both reachability and coverability
undecidable, reset and transfer VASS have provided an example of an extension
which leads to an undecidable reachability [AK76] yet decidable coverability
problem [DFPS98]. Nevertheless, the computational costs for those extensions
are high: while coverability is EXPSPACE-complete for VASS [Lip76, Rac78], it
becomes Ackermann-complete in the presence of resets and transfers [Sch10,
FFSPS11]. For practical purposes, the extension of VASS with transfers is
particularly useful since transfer VASS allow for reasoning about broadcast
protocols and multithreaded non-recursive C programs [EN98, KKW14]. It was
already observed in [EN98] that transfer VASS can be viewed as an instance of
so-called _affine VASS_. An affine VASS is a generalization of VASS with
transitions labelled by pairs $(\mathbf{A},\bm{b})$, where $\mathbf{A}$ is a
$d\times d$ matrix over the integers and $\bm{b}\in\mathbb{Z}^{d}$ is an
integer vector. A transition switches the control-state while updating the
configuration of the counters $\bm{v}\in\mathbb{N}^{d}$ to
$\mathbf{A}\cdot\bm{v}+\bm{b}$, provided that
$\mathbf{A}\cdot\bm{v}+\bm{b}\geq\bm{0}$; otherwise, the transition is
blocked. Transfer VASS can be viewed as affine VASS in which the columns of
all matrices are $d$-dimensional unit vectors [EN98].

Due to the symbolic state-explosion problem and Ackermann-hardness of
coverability, standard decision procedures for transfer VASS such as the
backward algorithm [ACJT96] do not _per se_ scale to real-world instances. In
recent years, numerous authors have proposed the use of over-approximations in
order to attenuate the symbolic state-explosion problem for VASS and some of
their extensions (see, e.g., [ELM+14, ALW16, BH17]). Most commonly, the basic
idea is to relax the integrality or non-negativity condition on the counters
and to allow them to take values from the non-negative rational numbers or the
integers. The latter class is usually referred to as $\mathbb{Z}$-VASS, see
e.g. [HH14]. It is easily seen that if a configuration is not reachable under
the relaxed semantics, then the configuration is also not reachable under the
standard semantics. Hence, those state-space over-approximations can, for
instance, be used to prune search spaces and empirically drastically speedup
classical algorithms for VASS such as the backward-algorithm. In this paper,
we investigate reachability in _integer over-approximations_ of affine VASS,
i.e., affine VASS in which a configuration of the counters is a point in
$\mathbb{Z}^{d}$, and in which all transitions are non-blocking. Subsequently,
we refer to such VASS as _affine $\mathbb{Z}$-VASS_.

Main contributions. We focus on affine $\mathbb{Z}$-VASS with the _finite-
monoid property_ (afmp-$\mathbb{Z}$-VASS), i.e. where the matrix monoid
generated by all matrices occurring along transitions in the affine
$\mathbb{Z}$-VASS is finite. By a reduction to reachability in
$\mathbb{Z}$-VASS, we obtain decidability of reachability for the whole class
of afmp-$\mathbb{Z}$-VASS and semilinearity of their reachability relations.

In more detail, we show that reachability in an afmp-$\mathbb{Z}$-VASS can be
reduced to reachability in a $\mathbb{Z}$-VASS whose size is polynomial in the
size of the original afmp-$\mathbb{Z}$-VASS and in the norm of the finite
monoid $\mathcal{M}$ generated by the matrices occurring along transitions,
denoted by $\lVert\mathcal{M}\rVert$. For a vast number of classes of affine
transformations considered in the literature, $\lVert\mathcal{M}\rVert$ is
bounded exponentially in the dimension of the matrices. This enables us to
deduce a general PSPACE upper bound for extensions of $\mathbb{Z}$-VASS such
as transfer $\mathbb{Z}$-VASS and copy $\mathbb{Z}$-VASS. By a slightly more
elaborated analysis of this construction, we are also able to provide a short
proof of the already known NP upper bound for reset $\mathbb{Z}$-VASS [HH14].
We also show that a PSPACE lower bound of the reachability problem already
holds for the extension of $\mathbb{Z}$-VASS that only use permutation
matrices in their transition updates. This in turn gives PSPACE-completeness
of interesting classes such as transfer $\mathbb{Z}$-VASS and copy
$\mathbb{Z}$-VASS.

Finally, we show that an affine $\mathbb{Z}$-VASS that has both transfers and
copies may not have the finite-monoid property, and that the reachability
problem for this class becomes undecidable. We complement this result by
investigating the case of monogenic classes, i.e. classes of monoids with a
single generator. We show that although reachability can still be undecidable
for an affine $\mathbb{Z}$-VASS with a monogenic matrix monoid, there exists a
monogenic class without the finite-monoid property for which reachability is
decidable.

All complexity results obtained in this paper are summarized in Figure 1,
except for the undecidability of general monogenic classes as it is a family
of classes rather than one class.

Related work. Our work is primarily related to the work of Finkel and Leroux
[FL02], Iosif and Sangnier [IS16], Haase and Halfon [HH14], and Cadilhac,
Finkel and McKenzie [CFM12, CFM13]. In [FL02], Finkel and Leroux consider a
model more general than affine $\mathbb{Z}$-VASS in which transitions are
additionally equipped with guards which are Presburger formulas defining
admissible sets of vectors in which a transition does not block. Given a
sequence of transitions $\sigma$, Finkel and Leroux show that the reachability
set obtained from repeatedly iterating $\sigma$, i.e., the _acceleration_ of
$\sigma$, is definable in Presburger arithmetic. Note that the model of Finkel
and Leroux does not allow for control-states and the usual tricks of encoding
each control-state by a counter or all control-states into three counters
[HP79] do not work over $\mathbb{Z}$ since transitions are non-blocking. Iosif
and Sangnier [IS16] investigated the complexity of model checking problems for
a variant of the model of Finkel and Leroux with guards defined by convex
polyhedra and with control-states over a flat structure. Haase and Halfon
[HH14] studied the complexity of the reachability, coverability and inclusion
problems for $\mathbb{Z}$-VASS and reset $\mathbb{Z}$-VASS, two submodels of
the affine $\mathbb{Z}$-VASS that we study in this paper. In [CFM12, CFM13],
Cadilhac, Finkel and McKenzie consider an extension of Parikh automata to
affine Parikh automata with the finite-monoid restriction like in our paper.
These are automata recognizing boolean languages, but the finite-monoid
restriction was exploited in a similar way to obtain some decidability results
in that context. We finally remark that our models capture variants of cost
register automata that have only one $+$ operation [AR13, AFR14].

Structure of the paper. We introduce general notations and affine
$\mathbb{Z}$-VASS in Section 2. In Section 3, we give the reduction from
afmp-$\mathbb{Z}$-VASS to $\mathbb{Z}$-VASS. Subsequently, in Section 4 we
show that afmp-$\mathbb{Z}$-VASS have semilinear reachability relations and
discuss semilinearity of affine $\mathbb{Z}$-VASS in general. In Section 5, we
show PSPACE and NP upper bounds of the reachability problem for some classes
of afmp-$\mathbb{Z}$-VASS; and in Section 6 we show PSPACE-hardness and
undecidability results for some classes of affine $\mathbb{Z}$-VASS. In
Section 7, we show that reachability is undecidable for monogenic affine
$\mathbb{Z}$-VASS and remains decidable for a specific class of infinite
monoids. Some concluding remarks will be made in Section 8.

pt$\mathbb{Z}$-VASSReset $\mathbb{Z}$-VASSPermutation
$\mathbb{Z}$-VASSTransfer $\mathbb{Z}$-VASSCopy $\mathbb{Z}$-VASSTransfer +
copy $\mathbb{Z}$-VASSAffine
$\mathbb{Z}$-VASS$\mathcal{C}_{\mathbf{J}}$-$\mathbb{Z}$-VASSNP-
completePSPACE-completeFinite monoidsInfinite
monoidsDecidableUndecidableptptptptptpt Figure 1. Classification of the
complexity of reachability in affine $\mathbb{Z}$-VASS in terms of classes of
matrices. The rectangular regions below and above the horizontal dashed line
correspond to classes of matrices with finite and infinite monoids
respectively. The rectangular green dotted region and the elliptical red
striped region correspond to the classes where reachability is decidable and
undecidable, respectively. The elliptical blue region and the orange
elliptical region correspond to the classes where reachability is NP-complete
and PSPACE-complete respectively. The term
“$\mathcal{C}_{\mathbf{J}}$-$\mathbb{Z}$-VASS” refers to the specific
monogenic class of infinite monoids that will be defined in Section 7.1.

##  2\. Preliminaries

General notation. For $n\in\mathbb{N}$, we write $[n]$ for the set
$\\{1,2,\ldots,n\\}$. For every
$\bm{x}=(x_{1},x_{2},\ldots,x_{d})\in\mathbb{Z}^{d}$ and every $i\in[d]$, we
define $\bm{x}(i)\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}x_{i}$. We denote the identity matrix and the
zero-vector by $\mathbf{I}$ and $\bm{0}$ in every dimension, as there will be
no ambiguity. For $\bm{x}\in\mathbb{Z}^{d}$ and
$\mathbf{A}\in\mathbb{Z}^{d\times d}$, we define the _max-norm_ of $\bm{x}$
and $\mathbf{A}$ as
$\lVert\bm{x}\rVert\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}\max\\{|\bm{x}(i)|:i\in[d]\\}$ and
$\lVert\mathbf{A}\rVert\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}\max\\{\lVert\mathbf{A}_{i}\rVert:i\in[d]\\}$
where $\mathbf{A}_{i}$ denotes the $i^{\text{th}}$ column of $\mathbf{A}$. We
naturally extend this notation to finite sets, i.e. $\lVert
G\rVert\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}\max\\{\lVert\mathbf{A}\rVert:\mathbf{A}\in
G\\}$ for every $G\subseteq_{\text{fin}}\mathbb{Z}^{d\times d}$. We assume
that numbers are represented in binary, hence the entries of vectors and
matrices can be exponential in the size of their encodings.

Affine Integer VASS. An _affine integer vector addition system with states
(affine $\mathbb{Z}$-VASS)_ is a tuple $\mathcal{V}=(d,Q,T)$ where
$d\in\mathbb{N}$, $Q$ is a finite set and $T\subseteq
Q\times\mathbb{Z}^{d\times d}\times\mathbb{Z}^{d}\times Q$ is finite. Let us
fix such a $\mathcal{V}$. We call $d$ the _dimension_ of $\mathcal{V}$ and the
elements of $Q$ and $T$ respectively _control-states_ and _transitions_. For
every transition $t=(p,\mathbf{A},\bm{b},q)$, we define
$\mathrm{src}(t)\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}p$,
$\mathrm{tgt}(t)\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}q$,
$M(t)\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}\mathbf{A}$ and
$\Delta(t)\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}\bm{b}$, and let
$f_{t}\colon\mathbb{Z}^{d}\to\mathbb{Z}^{d}$ be the affine transformation
defined by $f_{t}(\bm{x})=\mathbf{A}\cdot\bm{x}+\bm{b}$. The _size_ of
$\mathcal{V}$, denoted $|\mathcal{V}|$, is the number of bits used to
represent $d$, $Q$ and $T$ with coefficients written in binary. For our
purposes, we formally define it in a crude way as
$|\mathcal{V}|\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}d+|Q|+(d^{2}+d)\cdot|T|\cdot\max(1,\lceil\log(\lVert
T\rVert+1)\rceil)$ where

$\lVert T\rVert\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}\max(\max\\{\lVert\Delta(t)\rVert:t\in
T\\},\max\\{\lVert M(t)\rVert:t\in T\\}).$

A _configuration_ of $\mathcal{V}$ is a pair $(q,\bm{v})\in
Q\times\mathbb{Z}^{d}$ which we write as $q(\bm{v})$. For every $t\in T$ and
$p(\bm{u}),q(\bm{v})\in Q\times\mathbb{Z}^{d}$, we write
$p(\bm{u})\xrightarrow{t}\mathrel{\vphantom{\to}}q(\bm{v})$ whenever
$p=\mathrm{src}(t)$, $q=\mathrm{tgt}(t)$ and $\bm{v}=f_{t}(\bm{u})$. We
naturally extend $\xrightarrow{}\mathrel{\vphantom{\to}}$ to sequences of
transitions as follows. For every $w=w_{1}\cdots w_{k}\in T^{k}$ and
$p(\bm{u}),q(\bm{v})\in Q\times\mathbb{Z}^{d}$, we write
$p(\bm{u})\xrightarrow{w}\mathrel{\vphantom{\to}}q(\bm{v})$ if either $k=0$
(denoted $w=\varepsilon$) and $p(\bm{u})=q(\bm{v})$, or $k>0$ and there exist
$p_{0}(\bm{u}_{0}),p_{1}(\bm{u}_{1}),\ldots,p_{k}(\bm{u}_{k})\in
Q\times\mathbb{Z}^{d}$ such that

$p(\bm{u})=p_{0}(\bm{u}_{0})\xrightarrow{w_{1}}\mathrel{\vphantom{\to}}p_{1}(\bm{u}_{1})\xrightarrow{w_{2}}\mathrel{\vphantom{\to}}{}\cdots{}\xrightarrow{w_{k}}\mathrel{\vphantom{\to}}p_{k}(\bm{u}_{k})=q(\bm{v}).$

We write $p(\bm{u})\xrightarrow{*}\mathrel{\vphantom{\to}}q(\bm{v})$ if there
exists some $w\in T^{*}$ such that
$p(\bm{u})\xrightarrow{w}\mathrel{\vphantom{\to}}q(\bm{v})$. The relation
$\xrightarrow{*}\mathrel{\vphantom{\to}}$ is called the _reachability
relation_ of $\mathcal{V}$. If
$p(\bm{u})\xrightarrow{w}\mathrel{\vphantom{\to}}q(\bm{v})$, then we say that
$w$ is a _run from $p(\bm{u})$ to $q(\bm{v})$_, or simply a _run_ if the
source and target configurations are irrelevant. We also say that $w$ is a
_path_ from $p$ to $q$, and if $p=q$ then we say that $w$ is a _cycle_.

Let $M(\mathcal{V})\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}\\{M(t):t\in T\\}$ and
$\Delta(\mathcal{V})\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}\\{\Delta(t):t\in T\\}$. If $\mathcal{V}$ is
clear from the context, we sometimes simply write $M$ and $\Delta$. The
_monoid of $\mathcal{V}$_, denoted $\mathcal{M}_{\mathcal{V}}$ or sometimes
simply $\mathcal{M}$, is the monoid generated by $M(\mathcal{V})$, i.e. it is
the smallest set that contains $M(\mathcal{V})$, is closed under matrix
multiplication, and contains the identity matrix. We say that a matrix
$\mathbf{A}\in\mathbb{N}^{d\times d}$ is respectively a (i)  _reset_ , (ii)
_permutation_ , (iii)  _transfer_ , (iv)  _copyless_ , or (v)  _copy_ matrix
if $\mathbf{A}\in\\{0,1\\}^{d\times d}$ and

  1. (1)

$\mathbf{A}$ does not contain any $1$ outside of its diagonal;

  2. (2)

$\mathbf{A}$ has exactly one $1$ in each row and each column;

  3. (3)

$\mathbf{A}$ has exactly one $1$ in each column;

  4. (4)

$\mathbf{A}$ has at most one $1$ in each column;

  5. (5)

$\mathbf{A}$ has exactly one $1$ in each row.

Analogously, we say that $\mathcal{V}$ is respectively a _reset_ ,
_permutation_ , _transfer_ , _copyless_ , or _copy_ $\mathbb{Z}$-VASS if all
matrices of $M(\mathcal{V})$ are reset, permutation, transfer, copyless, or
copy matrices. The monoids of such affine $\mathbb{Z}$-VASS are finite and
respectively of size at most $2^{d}$, $d!$, $d^{d}$, $(d+1)^{d}$ and $d^{d}$.
Copyless $\mathbb{Z}$-VASS correspond to a model of copyless cost-register
automata studied in [AFR14] (see the remark below). If $M(\mathcal{V})$ only
contains the identity matrix, then $\mathcal{V}$ is simply called a
$\mathbb{Z}$-VASS.

A _class of matrices_ $\mathcal{C}$ is a union $\bigcup_{d\geq
1}\mathcal{C}_{d}$ where $\mathcal{C}_{d}$ is a finitely generated, but
possibly infinite, submonoid of $\mathbb{N}^{d\times d}$ for every $d\geq 1$.
We say that $\mathcal{V}$ belongs to a class $\mathcal{C}$ of
$\mathbb{Z}$-VASS if $\mathcal{M}_{\mathcal{V}}\subseteq\mathcal{C}$. If each
$\mathcal{C}_{d}$ is finite, then we say that this class of affine
$\mathbb{Z}$-VASS has the _finite-monoid property_ (afmp-$\mathbb{Z}$-VASS).
For two classes $\mathcal{C}$ and $\mathcal{C}^{\prime}$ we write
$\mathcal{C}+\mathcal{C}^{\prime}$ to denote the smallest set
$\mathcal{D}=\bigcup_{d\geq 1}\mathcal{D}_{d}$ such that $\mathcal{D}_{d}$ is
a monoid that contains both $\mathcal{C}_{d}$ and $\mathcal{C}_{d}^{\prime}$
for every $d\geq 1$. Note that this operation does not preserve finiteness.
For example if $\mathcal{C}$ and $\mathcal{C}^{\prime}$ are the classes of
transfer and copy matrices, respectively, then
$\mathcal{C}+\mathcal{C}^{\prime}$ is infinite (see Figure 2 and Section 6).
We say that a class $\mathcal{C}=\bigcup_{d\geq 1}\mathcal{C}_{d}$ is
_nonnegative_ if $\mathcal{C}_{d}\subseteq\mathbb{N}^{d\times d}$ for every
$d\geq 1$. We say that an affine $\mathbb{Z}$-VASS $\mathcal{V}$ is
_nonnegative_ if $\mathcal{M}_{\mathcal{V}}$ belongs to some nonnegative class
of matrices. Note that the classes of reset, permutation, transfer, copyless
and copy matrices are all nonnegative, respectively.

$p$$q$$\begin{pmatrix}1&0\\\ 1&0\end{pmatrix},\bm{0}$ $\begin{pmatrix}1&1\\\
0&0\end{pmatrix},\bm{0}$ Figure 2. Example of a transfer + copy
$\mathbb{Z}$-VASS $\mathcal{V}$ which does not have the finite-monoid
property.

We discuss the $\mathbb{Z}$-VASS $\mathcal{V}$ in Figure 2 to give some
intuition behind the names transfer and copy $\mathbb{Z}$-VASS. The transition
from $p$ to $q$ is a copy transition and the transition from $q$ to $p$ is a
transfer transition. Notice that for every vector $(x,y)\in\mathbb{Z}^{2}$, we
have $p(x,y)\xrightarrow{}\mathrel{\vphantom{\to}}q(x,x)$, i.e. the value of
the first counter is copied to the second counter. Similarly, for the other
transition we have $q(x,y)\xrightarrow{}\mathrel{\vphantom{\to}}p(x+y,0)$,
that is the value of the second counter is transferred to the first counter
(resetting its own value to $0$). Let $\mathbf{A}$ and $\mathbf{B}$ be the two
matrices used in $\mathcal{V}$. Note that $(\mathbf{A}\cdot\mathbf{B})^{n}$ is
the matrix with all entries equal to $2^{n-1}$, and hence
$\mathcal{M}_{\mathcal{V}}$ is infinite.

######  Remark 1.

The variants of affine $\mathbb{Z}$-VASS that we consider are related to cost
register automata (CRA) with only the $+$ operation [AR13, AFR14] and without
an output function. These are deterministic models with states and registers
that upon reading an input, update their registers in the form $x\leftarrow
y+c$, where $x,y$ are registers and $c$ is an integer. An affine
$\mathbb{Z}$-VASS does not read any input, but is nondeterministic. Thus, one
can identify an affine $\mathbb{Z}$-VASS with a CRA that reads sequences of
transitions as words. In particular, the restrictions imposed on the studied
CRAs correspond to copy $\mathbb{Z}$-VASS [AR13] and copyless
$\mathbb{Z}$-VASS [AFR14].

Decision problems. We consider the _reachability_ and the _coverability_
problems parameterized by classes of matrices $\mathcal{C}$:

$\textsf{Reach}_{\mathcal{C}}$ (reachability problem)
Given: an affine $\mathbb{Z}$-VASS $\mathcal{V}=(d,Q,T)$ and configurations
$p(\bm{u}),q(\bm{v})$ s.t. $\mathcal{M}_{\mathcal{V}}\subseteq\mathcal{C}$.
Decide: whether $p(\bm{u})$.

$\textsf{Cover}_{\mathcal{C}}$ (coverability problem)
Given: an affine $\mathbb{Z}$-VASS $\mathcal{V}=(d,Q,T)$ and configurations
$p(\bm{u}),q(\bm{v})$ s.t. $\mathcal{M}_{\mathcal{V}}\subseteq\mathcal{C}$.
Decide: whether there exists $\bm{v}^{\prime}\in\mathbb{Z}^{d}$ such that
$p(\bm{u})$ and $\bm{v}^{\prime}\geq\bm{v}$.

For standard VASS (where configurations cannot hold negative values), the
coverability problem is much simpler than the reachability problem. However,
for affine $\mathbb{Z}$-VASS, these two problems coincide as observed in
[HH14, Lemma 2]: the two problems are inter-reducible in logarithmic space at
the cost of doubling the number of counters. Therefore we will only study the
reachability problem in this paper.

##  3\. From affine $\mathbb{Z}$-VASS with the finite-monoid property to
$\mathbb{Z}$-VASS

The main result of this section is that every affine $\mathbb{Z}$-VASS
$\mathcal{V}$ with the finite monoid property can be simulated by a
$\mathbb{Z}$-VASS with twice the number of counters whose size is polynomial
in $\lVert\mathcal{M}_{\mathcal{V}}\rVert$ and $|\mathcal{V}|$. More formally,
we show the following:

######  Theorem 2.

For every afmp-$\mathbb{Z}$-VASS $\mathcal{V}=(d,Q,T)$ and $p,q\in Q$ there
exist a $\mathbb{Z}$-VASS
$\mathcal{V}^{\prime}=(d^{\prime},Q^{\prime},T^{\prime})$ and
$p^{\prime},q^{\prime}\in Q^{\prime}$ such that

  * •

$d^{\prime}=2\cdot d$,

  * •

$|Q^{\prime}|\leq 3\cdot|\mathcal{M}_{\mathcal{V}}|\cdot|Q|$,

  * •

$|T^{\prime}|\leq 4d\cdot|\mathcal{M}_{\mathcal{V}}|\cdot(|Q|+|T|)$,

  * •

$\lVert T^{\prime}\rVert\leq\lVert\mathcal{M}_{\mathcal{V}}\rVert\cdot\lVert
T\rVert$,

  * •

$p(\bm{u})$ in $\mathcal{V}$ if and only if $p^{\prime}(\bm{u},\bm{0})$ in
$\mathcal{V}^{\prime}$.

Moreover, $\mathcal{V}^{\prime}$, $p^{\prime}$ and $q^{\prime}$ are
effectively computable from $\mathcal{V}$.

######  Corollary 3.

The reachability problem for afmp-$\mathbb{Z}$-VASS is decidable.

######  Proof 3.3.

By Theorem 2, it suffices to construct, for a given afmp-$\mathbb{Z}$-VASS
$\mathcal{V}$, the $\mathbb{Z}$-VASS $\mathcal{V}^{\prime}$ and to test for
reachability in $\mathcal{V}^{\prime}$. It is known that reachability for
$\mathbb{Z}$-VASS is in NP [HH14]. To effectively compute
$\mathcal{V}^{\prime}$ it suffices to provide a bound for
$\lVert\mathcal{M}_{\mathcal{V}}\rVert$. It is known that if
$|\mathcal{M}_{\mathcal{V}}|$ is finite then it is bounded by a computable
function (see [MS77]), and hence $\lVert\mathcal{M}_{\mathcal{V}}\rVert$ is
also computable.

For the remainder of this section, let us fix some affine $\mathbb{Z}$-VASS
$\mathcal{V}$ such that $\mathcal{M}_{\mathcal{V}}$ is finite. We proceed as
follows to prove Theorem 2. First, we introduce some notations and
intermediary lemmas characterizing reachability in affine $\mathbb{Z}$-VASS.
Next, we give a construction that essentially proves the special case of
Theorem 2 where the initial configuration is of the form $p(\bm{0})$. Finally,
we prove Theorem 2 by extending this construction to the general case.

It is worth noting that proving the general case is not necessary if one is
only interested in deciding reachability. Indeed, an initial configuration
$p(\bm{v})$ can be turned into one of the form $p^{\prime}(\bm{0})$ by adding
a transition that adds $\bm{v}$. The reason for proving the general case is
that it establishes a stronger relation that allows us to prove semilinearity
of afmp-$\mathbb{Z}$-VASS reachability relations in Section 4.

###  3.1. A characterization of reachability

For every $w\in T^{*}$, $t\in T$ and $\bm{u}\in\mathbb{Z}^{d}$, let

$\displaystyle M(\varepsilon)$
$\displaystyle\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}\mathbf{I},$
$\displaystyle\varepsilon(\bm{u})$
$\displaystyle\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}\bm{u},$ $\displaystyle M(wt)$
$\displaystyle\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}M(t)\cdot M(w),$ $\displaystyle wt(\bm{u})$
$\displaystyle\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}M(t)\cdot w(\bm{u})+\Delta(t).$

Intuitively, for any sequence $w\in T^{*}$, $w(\bm{u})$ is the effect of $w$
on $\bm{u}$, regardless of whether $w$ is an actual path of the underlying
graph. A simple induction yields the following characterization:

######  Lemma 4.

For every $w\in T^{*}$ and $p(\bm{u}),q(\bm{v})\in Q\times\mathbb{Z}^{d}$, it
is the case that $p(\bm{u})$ if and only if

  1. (1)

$w$ is a path from $p$ to $q$ in the underlying graph of $\mathcal{V}$, and

  2. (2)

$\bm{v}=w(\bm{u})$.

Testing for reachability with Lemma 4 requires evaluating $w(\bm{u})$. This
value can be evaluated conveniently as follows:

######  Lemma 5.

For every $w=w_{1}w_{2}\cdots w_{k}\in T^{k}$ and $\bm{u}\in\mathbb{Z}^{d}$,
the following holds:

$\displaystyle w(\bm{u})=M(w)\cdot\bm{u}+\sum_{i=1}^{k}M(w_{i+1}w_{i+2}\cdots
w_{k})\cdot\Delta(w_{i}).$ (1)

Moreover, $w(\bm{u})=M(w)\cdot\bm{u}+w(\bm{0})$.

######  Proof 3.5 (Proof of Lemma 5).

We prove (1) by induction on $k$. The base case follows from
$\varepsilon(\bm{u})=\bm{u}=\mathbf{I}\cdot\bm{u}+\bm{0}=M(\varepsilon)\cdot\bm{u}+\bm{0}$.
Assume that $k>0$ and that the claim holds for sequences of length $k-1$. For
simplicity we denote
$\sigma\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}w_{1}\cdots w_{k-1}$. We have:

$\displaystyle w(\bm{u})$ $\displaystyle=\sigma w_{k}(\bm{u})$
$\displaystyle=M(w_{k})\cdot\sigma(\bm{u})+\Delta(w_{k})$ (2)
$\displaystyle=M(w_{k})\cdot\left(M(\sigma)\cdot\bm{u}+\sum_{i=1}^{k-1}M(w_{i+1}w_{i+2}\cdots
w_{k-1})\cdot\Delta(w_{i})\right)+\Delta(w_{k})$ (3)
$\displaystyle=M(w_{k})\cdot
M(\sigma)\cdot\bm{u}+\sum_{i=1}^{k-1}M(w_{k})\cdot M(w_{i+1}w_{i+2}\cdots
w_{k-1})\cdot\Delta(w_{i})+\Delta(w_{k})$ $\displaystyle=M(\sigma
w_{k})\cdot\bm{u}+\sum_{i=1}^{k-1}M(w_{i+1}w_{i+2}\cdots
w_{k})\cdot\Delta(w_{i})+\Delta(w_{k})$ (4)
$\displaystyle=M(w)\cdot\bm{u}+\sum_{i=1}^{k}M(w_{i+1}w_{i+2}\cdots
w_{k})\cdot\Delta(w_{i})$

where (2), (3) and (4) follow respectively by definition of $\sigma
w_{k}(\bm{u})$, by induction hypothesis and by definition of $M(\sigma
w_{k})$.

The last part of the lemma follows from applying (1) to $w(\bm{0})$ and
$w(\bm{u})$, and observing that subtracting them results in
$w(\bm{u})-w(\bm{0})=M(w)\cdot\bm{u}$.

Observe that Lemma 5 is trivial for the particular case of $\mathbb{Z}$-VASS.
Indeed, we obtain $w(\bm{u})=\bm{u}+\sum_{i=1}^{k}\Delta(w_{i})$, which is the
sum of transition vectors as expected for a $\mathbb{Z}$-VASS.

###  3.2. Reachability from the origin

We make use of Lemmas 4 and 5 to construct a $\mathbb{Z}$-VASS
$\mathcal{V}^{\prime}=(d,Q^{\prime},T^{\prime})$ for the special case of
Theorem 2 where the initial configuration is of the form $p(\bm{0})$. The
states and transitions of $\mathcal{V}^{\prime}$ are defined as:

$\displaystyle Q^{\prime}$
$\displaystyle\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}Q\times\mathcal{M},$ $\displaystyle
T^{\prime}$
$\displaystyle\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}\\{((\mathrm{tgt}(t),\mathbf{A}),\mathbf{I},\mathbf{A}\cdot\Delta(t),(\mathrm{src}(t),\mathbf{A}\cdot
M(t))):\mathbf{A}\in\mathcal{M},t\in T\\}.$

The idea behind $\mathcal{V}^{\prime}$ is to simulate a path $w$ of
$\mathcal{V}$ backwards and to evaluate $w(\bm{0})$ as the sum identified in
Lemma 5. More formally, $\mathcal{V}^{\prime}$ and $\mathcal{V}$ are related
as follows:

######  Proposition 6.

  1. (1)

For every $w\in T^{*}$, if $p(\bm{0})$ in $\mathcal{V}$, then
$q^{\prime}(\bm{0})$ in $\mathcal{V}^{\prime}$, where
$q^{\prime}\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}(q,\mathbf{I})$ and
$p^{\prime}\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}(p,M(w))$.

  2. (2)

If $q^{\prime}(\bm{0})$ in $\mathcal{V}^{\prime}$, where
$q^{\prime}\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}(q,\mathbf{I})$ and
$p^{\prime}\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}(p,\mathbf{A})$, then there exists $w\in
T^{*}$ such that $M(w)=\mathbf{A}$ and $p(\bm{0})$ in $\mathcal{V}$.

######  Proof 3.10.

(a) By Lemma 4, $\mathcal{V}$ has a path $w\in T^{*}$ such that
$w(\bm{0})=\bm{v}$. Let
$k\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}|w|$. Let
$\mathbf{A}_{0}\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}\mathbf{I}$, and for every $i\in[k]$ let

$\displaystyle\mathbf{A}_{i}$
$\displaystyle\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}M(w_{k-i+1}\cdots w_{k-1}w_{k}),$
$\displaystyle\bm{b}_{i}$
$\displaystyle\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}\mathbf{A}_{i-1}\cdot\Delta(w_{k-i+1}),$
$\displaystyle w_{i}^{\prime}$
$\displaystyle\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}((\mathrm{tgt}(w_{k-i+1}),\mathbf{A}_{i-1}),\mathbf{I},\bm{b}_{i},(\mathrm{src}(w_{k-i+1}),\mathbf{A}_{i})).$

We claim that
$w^{\prime}\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}w_{1}^{\prime}w_{2}^{\prime}\cdots
w_{k}^{\prime}$ is such that $(q,\mathbf{A}_{0})$ in $\mathcal{V}^{\prime}$.
Note that the validity of the claim completes the proof since
$\mathbf{A}_{0}=\mathbf{I}$ and $\mathbf{A}_{k}=M(w)$.

It follows immediately from the definition of $T^{\prime}$ that
$w_{i}^{\prime}\in T^{\prime}$ for every $i\in[k]$ and hence that $w^{\prime}$
is a path from $(q,\mathbf{A}_{0})$ to $(p,\mathbf{A}_{k})$. By Lemma 4, it
remains to show that $w^{\prime}(\bm{0})=\bm{v}$:

$\displaystyle w^{\prime}(\bm{0})$
$\displaystyle=\sum_{i=1}^{k}M(w_{i+1}^{\prime}w_{i+2}^{\prime}\cdots
w_{k}^{\prime})\cdot\Delta(w_{i}^{\prime})$ (by Lemma 5 applied to
$w^{\prime}(\bm{0})$) $\displaystyle=\sum_{i=1}^{k}\Delta(w_{i}^{\prime})$ (by
$M(w_{i}^{\prime})=\mathbf{I}$ for every $i\in[k]$)
$\displaystyle=\sum_{i=1}^{k}\mathbf{A}_{i-1}\cdot\Delta(w_{k-i+1})$ (by
definition of $\Delta(w_{i}^{\prime})$)
$\displaystyle=\sum_{i=1}^{k}M(w_{k-i+2}w_{k-i+1}\cdots
w_{k})\cdot\Delta(w_{k-i+1})$ (by definition of $\mathbf{A}_{i-1}$)
$\displaystyle=\sum_{i=1}^{k}M(w_{i+1}w_{i+2}\cdots w_{k})\cdot\Delta(w_{i})$
(by inspection of the sum) $\displaystyle=w(\bm{0})$ (by Lemma 5 applied to
$w(\bm{0})$).

(b) Similarly, by Lemma 4, there exists a path $w^{\prime}$ of
$\mathcal{V}^{\prime}$ such that $w^{\prime}(\bm{0})=\bm{v}$, and it suffices
to exhibit a path $w\in T^{*}$ from $p$ to $q$ in $\mathcal{V}$ such that
$w(\bm{0})=\bm{v}$ and $M(w)=\mathbf{A}$. Let
$k\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}|w^{\prime}|$. For every $i\in[k]$, let
$w_{i}^{\prime}=((p_{i},\mathbf{A}_{i}),\mathbf{I},\bm{b}_{i},(q_{i},\mathbf{B}_{i}))$.
By definition of $T^{\prime}$, for every $i\in[k]$, there exists a (possibly
non unique) transition $t_{i}\in T$ such that $\mathrm{tgt}(t)=p_{i}$,
$\mathrm{src}(t)=q_{i}$, $\bm{b}_{i}=\mathbf{A}_{i}\cdot\Delta(t)$ and
$\mathbf{B}_{i}=\mathbf{A}_{i}\cdot M(t)$. We set
$w\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}t_{1}t_{2}\cdots t_{k}$. It is readily seen
that $w$ is a path from $p$ to $q$. To prove $w(\bm{0})=\bm{v}$ and
$M(w)=\mathbf{A}$, Lemma 5 can be applied as in the previous implication.

###  3.3. Reachability from an arbitrary configuration

We now construct the $\mathbb{Z}$-VASS
$\mathcal{V}^{\prime\prime}=(2d,Q^{\prime\prime},T^{\prime\prime})$ of Theorem
2 which is obtained mostly from $\mathcal{V}^{\prime}$. The states of
$\mathcal{V}^{\prime\prime}$ are defined as:

$\displaystyle Q^{\prime\prime}$
$\displaystyle\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}Q\cup Q^{\prime}\cup\overline{Q^{\prime}}$
$\displaystyle\text{where}\quad\overline{Q^{\prime}}\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}\\{(\overline{q},\mathbf{A}):(q,\mathbf{A})\in
Q^{\prime}\\}.$

To simplify notation, given two vectors $\bm{u},\bm{v}\in\mathbb{Z}^{d}$ we
write $(\bm{u},\bm{v})$ for the vector of $\mathbb{Z}^{2d}$ equal to $\bm{u}$
on the first $d$ components and equal to $\bm{v}$ on the last $d$ components.
The set $T^{\prime\prime}$ consists of four disjoint subsets of transitions
$T_{\text{simul}}\cup T_{\text{end}}\cup T_{\text{mult}}\cup T_{\text{final}}$
working in four sequential stages. Intuitively, these transitions allow (1)
$\mathcal{V}^{\prime\prime}$ to simulate a path $w$ of $\mathcal{V}$ backwards
in order to compute $w(\bm{0})$; (2) guess the end of this path; (3) compute
$M(w)\cdot\bm{u}$ by using the fact that $M(w)$ is stored in its control-
state; and (4) guess the end of this matrix multiplication.

The first set of transitions is defined as:

$\displaystyle T_{\text{simul}}$
$\displaystyle\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}\\{(\mathrm{src}(t),\mathbf{I},(\bm{0},\Delta(t)),\mathrm{tgt}(t)):t\in
T^{\prime}\\}.$

Its purpose is to simulate $T^{\prime}$ on the last $d$ counters. The second
set is defined as:

$\displaystyle T_{\text{end}}$
$\displaystyle\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}\\{((q,\mathbf{A}),\mathbf{I},(\bm{0},\bm{0}),(\overline{q},\mathbf{A})):(q,\mathbf{A})\in
Q^{\prime}\\},$

and its purpose is to nondeterministically guess the end of a run in
$\mathcal{V}^{\prime}$ by simply marking $q$. The third set is defined as:

$\displaystyle T_{\text{mult}}$
$\displaystyle\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}\ $
$\displaystyle\\{((\overline{q},\mathbf{A}),\mathbf{I},(-\bm{e}_{i},\mathbf{A}\cdot\bm{e}_{i}),(\overline{q},\mathbf{A})):(\overline{q},\mathbf{A})\in\overline{Q^{\prime}},i\in[d]\\}\cup{}$
$\displaystyle\\{((\overline{q},\mathbf{A}),\mathbf{I},(\bm{e}_{i},-\mathbf{A}\cdot\bm{e}_{i}),(\overline{q},\mathbf{A})):(\overline{q},\mathbf{A})\in\overline{Q^{\prime}},i\in[d]\\},$

where $\bm{e}_{i}$ is the $i$-th unit vector such that $\bm{e}_{i}(i)=1$ and
$\bm{e}_{i}(j)=0$ for all $i\neq j$. The purpose of $T_{\text{mult}}$ is to
compute $\mathbf{A}\cdot\bm{u}$ from the $d$ first counters onto the $d$ last
counters. Finally, $T_{\text{final}}$ is defined as:

$\displaystyle T_{\text{final}}$
$\displaystyle\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}\\{((\overline{q},\mathbf{A}),\mathbf{I},(\bm{0},\bm{0}),q):(\overline{q},\mathbf{A})\in\overline{Q^{\prime}}\\},$

and its purpose is to guess the end of the matrix multiplication performed
with $T_{\text{mult}}$.

We may now prove Theorem 2:

######  Proof 3.12 (Proof of Theorem 2).

First, note that we obtain

$\displaystyle|Q^{\prime\prime}|$ $\displaystyle=2\cdot|Q^{\prime}|+|Q|$
$\displaystyle\leq 3\cdot|Q|\cdot|\mathcal{M}|,$
$\displaystyle|T^{\prime\prime}|$
$\displaystyle=|T^{\prime}|+|Q^{\prime}|+2d\cdot|Q^{\prime}|+|Q^{\prime}|$
$\displaystyle=|T^{\prime}|+2(d+1)\cdot|Q^{\prime}|$
$\displaystyle=|T|\cdot|\mathcal{M}|+2(d+1)\cdot|Q|\cdot|\mathcal{M}|$
$\displaystyle\leq 4d\cdot|\mathcal{M}|\cdot(|T|+|Q|).$

Moreover, we have:

$\displaystyle\lVert T^{\prime\prime}\rVert$ $\displaystyle=\max(\lVert
T^{\prime}\rVert,\lVert\mathcal{M}\rVert)$
$\displaystyle\leq\max(\lVert\mathcal{M}\rVert\cdot\lVert
T\rVert,\lVert\mathcal{M}\rVert)$
$\displaystyle=\lVert\mathcal{M}\rVert\cdot\lVert T\rVert.$

We conclude by proving that $p(\bm{u})$ in $\mathcal{V}$ if and only if
$q^{\prime}(\bm{u},\bm{0})$ in $\mathcal{V}^{\prime\prime}$, where
$q^{\prime}\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}(q,\mathbf{I})$.

$\Rightarrow$) By Lemma 4, there exists a path $w$ of $\mathcal{V}$ such that
$w(\bm{u})=\bm{v}$. By definition of $T_{\text{simul}}$ and $T_{\text{end}}$,
and by Proposition 6, it is the case that $q^{\prime}(\bm{u},\bm{0})$ where
$p^{\prime}\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}(p,M(w))$. The transitions of
$T_{\text{mult}}$ allow to transform $(\bm{u},w(\bm{0}))$ into
$(\bm{0},w(\bm{0})+M(w)\cdot\bm{u})$. Thus, using $T_{\text{final}}$, we can
reach the configuration $p(w(\bm{0})+M(w)\cdot\bm{u})$. This concludes the
proof since $w(\bm{u})=w(\bm{0})+M(w)\cdot\bm{u}$ by Lemma 5.

$\Leftarrow$) The converse implication follows the same steps as the previous
one. It suffices to observe that the first part of a run of
$\mathcal{V}^{\prime\prime}$ defines the value $w(\bm{0})$, while the second
part of the run defines $M(w)\cdot\bm{u}$.

##  4\. Semilinearity of affine $\mathbb{Z}$-VASS

A subset of $\mathbb{Z}^{d}$ is called _semilinear_ if it is definable by a
formula of Presburger arithmetic [Pre29], i.e. by a formula of
$\mathsf{FO}(\mathbb{Z},+,<)$, the decidable first-order logic over
$\mathbb{Z}$ with addition and order. Semilinear sets capture precisely finite
unions of sets of the form
$\bm{b}+\mathbb{N}\cdot\bm{p}_{1}+\mathbb{N}\cdot\bm{p}_{2}+\ldots+\mathbb{N}\cdot\bm{p}_{k}$
with each $\bm{p}_{i}\in\mathbb{Z}^{d}$, and are effectively closed under
basic operations such as finite sums, intersection and complement. Those
properties make semilinear sets an important tool in many areas of computer
science and find use whenever infinite subsets of $\mathbb{Z}^{d}$ need to be
manipulated.

The results of Section 3 enable us to show that any affine $\mathbb{Z}$-VASS
with the finite-monoid property has a semilinear reachability relation:

######  Theorem 7.

Given an afmp-$\mathbb{Z}$-VASS $\mathcal{V}=(d,Q,T)$ and $p,q\in Q$, it is
possible to compute an existential Presburger formula
$\varphi_{\mathcal{V},p,q}$ of size at most
$\mathcal{O}(\mathrm{poly}(|\mathcal{V}|,|\mathcal{M}_{\mathcal{V}}|,\log\lVert\mathcal{M}_{\mathcal{V}}\rVert))$
such that $\varphi_{\mathcal{V},p,q}(\bm{u},\bm{v})$ holds if and only if
$p(\bm{u})$ in $\mathcal{V}$.

######  Proof 4.2.

By Theorem 2, there exist an effectively computable $\mathbb{Z}$-VASS
$\mathcal{V}^{\prime}=(d^{\prime},Q^{\prime},T^{\prime})$ and
$p^{\prime},q^{\prime}\in Q^{\prime}$ such that $d^{\prime}=2\cdot d$,
$|Q^{\prime}|\leq 3\cdot|\mathcal{M}|\cdot|Q|$, $|T^{\prime}|\leq
4d\cdot|\mathcal{M}|\cdot(|Q|+|T|)$, $\lVert
T^{\prime}\rVert\leq\lVert\mathcal{M}\rVert\cdot\lVert T\rVert$ and

$\displaystyle p(\bm{u})$ (5)

By [HH14, Sect. 3], we can compute an existential Presburger formula $\psi$ of
linear size in $|\mathcal{V}^{\prime}|$ such that
$\psi(\bm{x},\bm{x}^{\prime},\bm{y},\bm{y}^{\prime})$ holds if and only if
$p^{\prime}(\bm{x},\bm{x}^{\prime})$ in $\mathcal{V}^{\prime}$. By Equation
(LABEL:eq:equiv), the formula
$\varphi_{\mathcal{V},p,q}(\bm{x},\bm{y})\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}\psi(\bm{x},\bm{0},\bm{0},\bm{y})$ satisfies
the theorem.

It was observed in [FL02, Boi98] that the reachability relation of a
$\mathbb{Z}$-VASS $\mathcal{V}=(d,Q,T)$, such that $|Q|=|M(\mathcal{V})|=1$,
is semilinear if and only if $\mathcal{M}_{\mathcal{V}}$ is finite. Theorem 7
shows that if we do not bound the number of states and matrices, i.e. drop the
assumption $|Q|=|M(\mathcal{V})|=1$, then ($\Leftarrow$) remains true. It is
natural to ask whether ($\Rightarrow$) also remains true.

$p$$p$$q$$\begin{pmatrix}1&1\\\ 1&1\end{pmatrix},\bm{0}$
$\mathbf{I},\begin{pmatrix}1\\\ 0\end{pmatrix}$
$\mathbf{I},\begin{pmatrix}0\\\ 1\end{pmatrix}$
$\mathbf{I},\begin{pmatrix}-1\\\ 0\end{pmatrix}$
$\mathbf{I},\begin{pmatrix}0\\\ -1\end{pmatrix}$ $\begin{pmatrix}1&1\\\
1&1\end{pmatrix},\bm{0}$ $\begin{pmatrix}0&0\\\ 0&0\end{pmatrix},\bm{0}$
Figure 3. Examples of affine $\mathbb{Z}$-VASS with infinite monoids and
semilinear reachability relations.

Let $\mathcal{V}_{1}$ and $\mathcal{V}_{2}$ be the affine $\mathbb{Z}$-VASS
illustrated in Figure 3 from left to right respectively. Note that
$\mathcal{M}_{\mathcal{V}_{1}}$ and $\mathcal{M}_{\mathcal{V}_{2}}$ are both
infinite due to the matrix made only of $1$s. Moreover, the reachability
relations of $\mathcal{V}_{1}$ and $\mathcal{V}_{2}$ are semilinear since the
former can reach any target configuration from any initial configuration, and
since the latter can only generate finitely many vectors due to the zero
matrix. Since $\mathcal{V}_{1}$ has a single control-state,
$|M(\mathcal{V}_{1})|=|M(\mathcal{V}_{2})|=2$ and
$\Delta(\mathcal{V}_{2})=\\{\bm{0}\\}$, any simple natural extension of the
characterization of semilinearity in terms of the number of control-states,
matrices and vectors fails.

It is worth noting that an affine $\mathbb{Z}$-VASS with an infinite monoid
may have a non semilinear reachability relation. Indeed, Figure 2 depicts a
transfer + copy $\mathbb{Z}$-VASS with an infinite monoid and such that
$\\{\bm{v}:p(1,1)$, which is known to be non semilinear. Moreover, this proves
that even the reachability set from $p(1,1)$ is not semilinear.

##  5\. Complexity of reachability for afmp-$\mathbb{Z}$-VASS

In this section, we use the results of Section 3 to show that reachability
belongs to PSPACE for a large class of afmp-$\mathbb{Z}$-VASS encompassing all
variants discussed in Section 2. Moreover, we give a novel proof to the known
NP membership of reachability for reset $\mathbb{Z}$-VASS.

For every finite set $G_{d}\subseteq\mathbb{Z}^{d\times d}$, let $\langle
G_{d}\rangle$ be the monoid generated by $G_{d}$. We have:

######  Theorem 8.

Let $\mathcal{C}=\bigcup_{d\geq 1}\mathcal{C}_{d}$ be a class of matrices such
that $\mathcal{C}_{d}$ is finite for every $d\geq 1$. It is the case that
$\textsf{Reach}_{\mathcal{C}}\in\text{PSPACE}$ if there exists a polynomial
$\mathrm{poly}$ such that $|\langle G_{d}\rangle|+\lVert\langle
G_{d}\rangle\rVert\leq 2^{\mathrm{poly}(d+\log\lVert G_{d}\rVert)}$ for every
$d\geq 1$ and every finite set $G_{d}$ such that $\langle
G_{d}\rangle\subseteq\mathcal{C}_{d}$.

######  Proof 5.1.

Let $\mathcal{V}=(d,Q,T)$ be an affine $\mathbb{Z}$-VASS from class
$\mathcal{C}$. Let $\mathcal{V}^{\prime}=(d,Q^{\prime},T^{\prime})$ be the
$\mathbb{Z}$-VASS obtained from $\mathcal{V}$ in Theorem 2. Recall that, by
Theorem 2, $p(\bm{u})$ in $\mathcal{V}$ if and only if
$p^{\prime}(\bm{u},\bm{0})$ in $\mathcal{V}^{\prime}$. Therefore, it suffices
to check the latter for determining reachability in $\mathcal{V}$.

We invoke a result of [BFG+15] on the flattability of $\mathbb{Z}$-VASS. By
[BFG+15, Prop. 3], $p^{\prime}(\bm{x})$ in $\mathcal{V}^{\prime}$ if and only
if there exist $k\leq|T^{\prime}|$,
$\alpha_{0},\beta_{1},\alpha_{1},\ldots,\beta_{k},\alpha_{k}\in(T^{\prime})^{*}$
and $\bm{e}\in\mathbb{N}^{k}$ such that

  1. (1)

$p^{\prime}(\bm{x})$ in $\mathcal{V}^{\prime}$,

  2. (2)

$\beta_{i}$ is a cycle for every $i\in[k]$, and

  3. (3)

$\alpha_{0}\beta_{1}\alpha_{1}\cdots\beta_{k}\alpha_{k}$ is a path from
$p^{\prime}$ to $q^{\prime}$ of length at most
$2\cdot|Q^{\prime}|\cdot|T^{\prime}|$.

For every $w\in(T^{\prime})^{*}$, let
$\Delta(w)\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}\sum_{i=1}^{|w|}\Delta(w_{i})$. By Lemma 5
(see the remark below the proof of Lemma 5), we have
$w(\bm{u})=\bm{u}+\Delta(w)$ for every $\bm{u}\in\mathbb{Z}^{d}$. Thus, by
Lemma 4, checking 1, assuming 3, amounts to testing whether $\bm{e}$ is a
solution of the following system of linear Diophantine equations:

$\displaystyle\bm{x}+\sum_{i=0}^{k}\Delta(\alpha_{i})+\begin{pmatrix}\Delta(\beta_{1})&\Delta(\beta_{2})&\cdots&\Delta(\beta_{k})\end{pmatrix}\cdot\bm{e}$
$\displaystyle=\bm{y}.$ (6)

Let $G_{d}\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}M(\mathcal{V})$. Note that $\lVert
G_{d}\rVert\leq\lVert T\rVert$ and that $\langle
G_{d}\rangle=\mathcal{M}_{\mathcal{V}}$. Let
$m\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}2\cdot|Q^{\prime}|\cdot|T^{\prime}|$. By
Theorem 2, we have $m\leq 48d\cdot|\mathcal{M}|^{2}\cdot|Q|^{2}\cdot|T|$.
Thus, since $\langle G_{d}\rangle$ is a submonoid of $\mathcal{C}_{d}$, and by
assumption on $\mathcal{C}_{d}$, we have

$m\leq 48d\cdot\left(2^{\mathrm{poly}(d+\log\lVert
T\rVert)}\right)^{2}\cdot|Q|^{2}\cdot|T|.$

Thus, $m$ is exponential in $|\mathcal{V}|$.

We describe a polynomial-space non deterministic Turing machine $\mathcal{A}$
for testing whether $p^{\prime}(\bm{x})$ in $\mathcal{V}^{\prime}$. The proof
follows from NPSPACE = PSPACE. Machine $\mathcal{A}$ guesses
$k\leq|T^{\prime}|$, a path
$\pi=\alpha_{0}\beta_{1}\alpha_{1}\cdots\beta_{k}\alpha_{k}$ of length at most
$m$ from $p^{\prime}$ to $q^{\prime}$, and $\bm{e}\in\mathbb{N}^{k}$, and
tests whether (6) holds for $\pi$. Note that we are not given
$\mathcal{V}^{\prime}$, but $\mathcal{V}$, so we must be careful for the
machine to work in polynomial space.

Instead of fully constructing $\mathcal{V}^{\prime}$ and fully guessing $\pi$,
we do both on the fly, and also construct
$\Delta(\alpha_{0}),\Delta(\beta_{1}),\ldots,\Delta(\beta_{k}),\Delta(\alpha_{k})$
on the fly as partial sums as we guess $\pi$. Note that to ensure that each
$\beta_{i}$ is a cycle, we do not need to fully store $\beta_{i}$ but only its
starting control-state. Moreover, note that
$\lVert\Delta(\alpha_{i})\rVert,\lVert\Delta(\beta_{i})\rVert\leq m\cdot\lVert
T^{\prime}\rVert$ for every $i$. By Theorem 2 and by assumption on
$\mathcal{C}_{d}$, we have

$\displaystyle\lVert T^{\prime}\rVert$ $\displaystyle\leq\lVert\langle
G_{d}\rangle\rVert\cdot\lVert T\rVert$ $\displaystyle\leq
2^{\mathrm{poly}(d+\log\lVert T\rVert)}\cdot\lVert T\rVert.$

Hence, each $\alpha_{i}$ and $\beta_{i}$ has a binary representation of
polynomial size in $|\mathcal{V}|$.

By [CH16, Prop. 4], (6) has a solution if and only if it has a solution
$\bm{e}\in\mathbb{N}^{k}$ such that

$\lVert\bm{e}\rVert\leq\left((k+1)\cdot\max\\{\lVert\Delta(\beta_{i})\rVert:i\in[k]\\}+\lVert\bm{x}\rVert+\lVert\bm{y}\rVert+\sum_{i=0}^{k}\lVert\Delta(\alpha_{i})\rVert+1\right)^{d^{\prime}}.$

Since $d^{\prime}=2\cdot d$, this means that we can guess a vector
$\bm{e}\in\mathbb{N}^{k}$ whose binary representation is of polynomial size,
and that we can thus evaluate (6) in polynomial time.

######  Corollary 9.

The reachability problem for nonnegative afmp-$\mathbb{Z}$-VASS is in PSPACE,
and hence in particular for reset, permutation, transfer, copy and copyless
$\mathbb{Z}$-VASS.

######  Proof 5.7.

Let $\mathcal{C}=\bigcup_{d\geq 1}\mathcal{C}_{d}$ be a class of nonnegative
matrices. Let $d\geq 1$ and let $G_{d}$ be a finite set of matrices such that
$\langle G_{d}\rangle\subseteq\mathcal{C}_{d}$. By [WS91, Theorem A.2], whose
proof appears in [Web87] written by one of the same authors, we have:

$\displaystyle|\langle G_{d}\rangle|$ $\displaystyle\leq\lVert
G_{d}\rVert^{d^{2}\cdot(d-1)}\cdot 5^{d^{3}/2}\cdot{d^{d^{3}}}\cdot d^{2}$
$\displaystyle=2^{d^{2}\cdot(d-1)\cdot\log\lVert
G_{d}\rVert+(d^{3}/2)\cdot\log 5+d^{3}\cdot\log d+2\cdot\log d},$
$\displaystyle\lVert\langle G_{d}\rangle\rVert$ $\displaystyle\leq\lVert
G_{d}\rVert^{d-1}\cdot 5^{d/2}\cdot d^{d}$
$\displaystyle=2^{(d-1)\cdot\log\lVert G_{d}\rVert+(d/2)\cdot\log 5+d\cdot\log
d}.$

Thus, $\mathcal{C}$ satisfies the requirements of Theorem 8. To complete the
proof, observe that determining whether $\mathcal{M}_{\mathcal{V}}$ is finite
can be done in time $\mathcal{O}(d^{6}\cdot|T|)$, again by [WS91, Theorem A.2]
and [Web87].

Note that this proof applies to reset, permutation, transfer, copy and
copyless classes, respectively, as they are all nonnegative. However, there is
a much simpler argument for these specific classes. Indeed, their matrices all
have a max-norm of a most $1$ and thus their monoids contain at most
$2^{d^{2}}$ matrices.

[[HH14]] The reachability problem for reset $\mathbb{Z}$-VASS belongs to NP.

######  Proof 5.8.

Let $\mathcal{V}=(d,Q,T)$ be a reset $\mathbb{Z}$-VASS. The proof does not
follow immediately from Theorem 2 because $\mathcal{M}_{\mathcal{V}}$ can be
of size up to $2^{d}$. We will analyze the construction used in the proof of
Theorem 2, where reachability in $\mathcal{V}$ is effectively reduced to
reachability in a $\mathbb{Z}$-VASS
$\mathcal{V}^{\prime}=(d^{\prime},Q^{\prime},T^{\prime})$. Recall that
$Q^{\prime}=(Q\times\mathcal{M}_{\mathcal{V}})\cup(\overline{Q}\times\mathcal{M}_{\mathcal{V}})\cup
Q$, and thus that the size of $\mathcal{V}^{\prime}$ depends only on the sizes
of $Q$ and $\mathcal{M}_{\mathcal{V}}$.

It follows from the proof of Theorem 2 and Proposition 6 that for every run
$q^{\prime}(\bm{u},\bm{0})$ in $\mathcal{V}^{\prime}$ where
$q^{\prime}\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}(q,\mathbf{I})$, there is a corresponding run
$p(\bm{u})$ in $\mathcal{V}$ for some $w\in T^{*}$ of length $k\geq 0$.
Moreover, the $i^{\text{th}}$ matrix occuring within the control-states of
this run are is the form $\mathbf{A}_{i}$ where
$\mathbf{A}_{i}=\mathbf{A}_{i-1}\cdot\mathbf{B}$ for some
$\mathbf{B}\in\mathcal{M}_{\mathcal{V}}$. Since $\mathcal{M}_{\mathcal{V}}$
consists of reset matrices, it holds that
$\mathbf{A}_{0},\mathbf{A}_{1},\mathbf{A}_{2},\ldots,\mathbf{A}_{k}$ is
monotonic, i.e. if $\mathbf{A}_{i-1}$ has a $0$ somewhere on its diagonal,
then $\mathbf{A}_{i}$ also contains $0$ in that position. It follows that
$\mathbf{A}_{0},\mathbf{A}_{1},\ldots,\mathbf{A}_{k}$ is made of at most $d+1$
distinct matrices.

To prove the NP upper bound we proceed as follows. We guess at most $d+1$
matrices of $\mathcal{M}_{\mathcal{V}}$ that could appear in sequence
$\mathbf{A}_{0},\mathbf{A}_{1},\ldots,\mathbf{A}_{k}$. We construct the
$\mathbb{Z}$-VASS $\mathcal{V}^{\prime}$ as in Theorem 2, but we discard each
control-state of $Q^{\prime}$ containing a matrix not drawn from the guessed
matrices. Since the constructed $\mathbb{Z}$-VASS is of polynomial size,
reachability can be verified in NP [HH14].

######  Remark 10.

Observe that the proof of Theorem 5.7 holds for any class of affine
$\mathbb{Z}$-VASS with a finite monoid such that every path of its Cayley
graph contains at most polynomially many different vertices. For a reset
$\mathbb{Z}$-VASS of dimension $d$, the number of vertices on every path of
the Cayley graph is bounded by $d+1$.

##  6\. Hardness results for reachability

It is known that the reachability problem for $\mathbb{Z}$-VASS is already NP-
hard [HH14], which means that reachability is NP-hard for all classes of
affine $\mathbb{Z}$-VASS. In this section, we show that PSPACE-hardness holds
for some classes, matching the PSPACE upper bound derived in Section 5.
Moreover, we observe that reachability is undecidable for transfer + copy
$\mathbb{Z}$-VASS.

######  Theorem 11.

The reachability problem for permutation $\mathbb{Z}$-VASS is PSPACE-hard.

######  Proof 6.1.

We give a reduction from the membership problem of linear bounded automata,
which is known to be PSPACE-complete (see, e.g., [HU79, Sect. 9.3 and 13]).
Let
$\mathcal{A}=(P,\Sigma,\Gamma,\delta,q^{\text{ini}},q^{\text{acc}},q^{\text{rej}})$
be a linear bounded automaton, where:

  * •

$P$ is the set of states,

  * •

$\Sigma\subseteq\Gamma$ is the input alphabet,

  * •

$\Gamma$ is the tape alphabet,

  * •

$\delta$ is the transition function, and

  * •

$q^{\text{ini}},q^{\text{acc}},q^{\text{rej}}$ are the initial, accepting and
rejecting states respectively.

The transition function is a mapping $\delta:P\times\Gamma\to
P\times\Gamma\times\\{\textsc{Left},\textsc{Right}\\}$. The intended meaning
of a transition $\delta(p,a)=(q,b,D)$ is that whenever $\mathcal{A}$ is in
state $p$ and holds letter $a$ at the current position of its tape, then
$\mathcal{A}$ overwrites $a$ with $b$ and moves to state $q$ and to the next
tape position in direction $D$.

Let us fix a word $w\in\Sigma^{*}$ of length $n$ that we will check for
membership. We construct a permutation $\mathbb{Z}$-VASS $\mathcal{V}=(d,Q,T)$
and configurations $r(\bm{u})$ and $r^{\prime}(\bm{0})$ such that
$\mathcal{A}$ accepts $w$ if and only if $r(\bm{u})$.

We set $d\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}n\cdot|\Gamma|+1$ and associate a counter to
each position of $w$ and each letter of the tape alphabet $\Gamma$, plus one
additional counter. For readability, we denote these counters respectively as
$x_{i,a}$ and $y$, where $i\in[n]$ and $a\in\Gamma$. The idea is to maintain,
for every $i\in[n]$, a single non zero counter among
$\\{x_{i,a}:a\in\Gamma\\}$ in order to represent the current letter in the
$i^{\text{th}}$ tape cell of $\mathcal{A}$. The initial vector is
$\bm{u}\in\\{0,1\\}^{d}$ such that $\bm{u}(y)=n$ and $\bm{u}(x_{i,a})=1$ if
and only if $w_{i}=a$ for every $i\in[n]$ and $a\in\Gamma$. The invariant that
will be maintained during all runs is $y=\sum_{i,a}x_{i,a}$.

The control-states of $\mathcal{V}$ are defined as:

$\displaystyle Q$
$\displaystyle\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}\\{r_{p,i}:p\in
P,i\in[n]\\}\cup\\{r_{a,i}:a\in\Gamma,i\in[n]\\}\cup\\{r_{\text{acc}}\\}.$

The purpose of each state of the form $r_{p,i}$ is to store the current state
$p$ and head position $i$ of $\mathcal{A}$. States of the form $r_{a,i}$ will
be part of a gadget testing whether $\mathcal{A}$ is simulated faithfully.

We associate a transition to every triple $(p,a,i)\in P\times\Gamma\times[n]$,
which denotes a configuration of $\mathcal{A}$: the automaton is in state $p$
in position $i$, where letter $a$ is stored. Let us fix a transition
$\delta(p,a)=(q,b,D)$; and let
$j\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}i+1$ if $D=\textsc{Right}$, and
$j\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}i-1$ if $D=\textsc{Left}$. For every
$i\in[n]$, if $j\in[n]$, then we add to $T$ the transition

$\displaystyle(r_{p,i},\mathbf{A},\bm{a},r_{q,j})$

where $\mathbf{A}$ is a permutation matrix that swaps the values of $x_{i,a}$
and $x_{i,b}$; and $\bm{a}$ is the vector whose only nonzero components are
$\bm{a}(x_{i,b})=1$ and $\bm{a}(y)=1$. The transition is depicted on the left
of Figure 4 (for $D=\textsc{Right}$). Notice that all transitions maintain the
invariant $y=\sum_{i,a}x_{i,a}$.

The purpose of the swap is to simulate the transition of $\mathcal{A}$, upon
reading $a$ in tape cell $i$ and state $p$, by moving the contents from
$x_{i,a}$ to $x_{i,b}$. Note that this transition may be faulty, i.e. it can
simulate reading letter $a$ even though tape cell $i$ contains another letter.
The purpose of the vector $\bm{a}$ is to detect such faulty behaviour: if the
cell $i$ does not contain $a$, then more than one counter among
$\\{x_{i,a}:a\in\Gamma\\}$ will be a nonzero counter.

$r_{p,i}$$r_{q,i+1}$$r_{a,1}$$r_{b,1}$$r_{a,2}$$r_{b,2}$$r_{a,n}$$r_{b,n}$$r_{\text{acc}}$
swap $x_{i,a}$
---
and $x_{i,b}$
$x_{i,b}\leftarrow x_{i,b}+1$
---
$y\leftarrow y+1$
$x_{1,a}\leftarrow x_{1,a}-1$
---
$y\leftarrow y-1$
$x_{1,b}\leftarrow x_{1,b}-1$
---
$y\leftarrow y-1$
$x_{2,a}\leftarrow x_{2,a}-1$
---
$y\leftarrow y-1$
$x_{2,b}\leftarrow x_{2,b}-1$
---
$y\leftarrow y-1$
$x_{n,a}\leftarrow x_{n,a}-1$
---
$y\leftarrow y-1$
$x_{n,b}\leftarrow x_{n,b}-1$
---
$y\leftarrow y-1$
Figure 4. _Left_ : transitions of $\mathcal{V}$ simulating transition
$\delta(p,a)=(q,b,\textsc{Right})$ of $\mathcal{A}$. _Right_ : gadget
verifying whether the accepting state has been reached with no error during
the simulation. For readability, we assume $\Gamma=\\{a,b\\}$ in the right
gadget.

Recall that $y=\sum_{i,a}x_{i,a}$. We conclude that $\mathcal{A}$ accepts $w$
if and only if there exist $j\in[n]$, $\bm{u}^{\prime}\in\mathbb{N}^{d}$ and
$a_{1},a_{2},\ldots,a_{n}\in\Gamma$ such that

$r_{q^{\text{ini}},1}(\bm{u})$

To test whether such index $j$, vector $\bm{u}^{\prime}$ and letters
$a_{1},a_{2},\ldots,a_{n}$ exist, we add some transitions to $T$ as
illustrated on the right of Figure 4. For every $i\in[n]$ and every
$a\in\Gamma$, we add to $T$ the transitions
$(r_{q^{\text{acc}},i},\mathbf{I},\bm{0},r_{a,1})$. For every $i\in[n]$ and
$a\in\Gamma$, we add to $T$ the transitions
$(r_{a,i},\mathbf{I},\bm{b},r_{a,i})$ where $\bm{b}$ is the vector whose only
non zero components are $\bm{b}(x_{i,a})=\bm{b}(y)=-1$. Moreover, if $i<n$,
then for every $a,b\in\Gamma$ we also add transitions
$(r_{a,i},\mathbf{I},\bm{0},r_{b,i+1})$. Finally, for all $a\in\Gamma$, we
also add transitions $(r_{a,n},\mathbf{I},\bm{0},r_{\text{acc}})$. The purpose
of these transitions is to guess for each $i$ some letter $a_{i}$ and
simultaneously decrease $x_{i,a_{i}}$ and $y$. We do this for each $i$
starting from $1$ to $n$ and in the end we move to the state $r_{\text{acc}}$.
We conclude that $\mathcal{A}$ accepts $w$ if and only if
$r_{q^{\text{ini}},1}(\bm{u})$ in $\mathcal{V}$.

######  Corollary 12.

The reachability problem is PSPACE-complete for permutation $\mathbb{Z}$-VASS,
transfer $\mathbb{Z}$-VASS and copy $\mathbb{Z}$-VASS.

######  Proof 6.5.

PSPACE-hardness for permutation $\mathbb{Z}$-VASS was shown in Theorem 11, and
the upper bound for transfer $\mathbb{Z}$-VASS and copy $\mathbb{Z}$-VASS
follows from Theorem 8. It remains to observe that permutation matrices are
also transfer and copy matrices.

######  Proposition 13.

The reachability problem for transfer + copy $\mathbb{Z}$-VASS is undecidable,
even when restricted to three counters.

######  Proof 6.6.

Reichert [Rei15] gives a reduction from the Post correspondence problem over
the alphabet $\\{0,1\\}$ to reachability in affine $\mathbb{Z}$-VASS with two
counters.

$p$$q$$p$$q$$\mathbf{D_{1}},\begin{pmatrix}b_{1}\\\
b_{2}\end{pmatrix}$$\begin{pmatrix}1&0&0\\\ 0&1&0\\\ 1&0&0\end{pmatrix}$,
$\bm{0}$$\begin{pmatrix}1&0&1\\\ 0&1&0\\\ 0&0&0\end{pmatrix}$,
$\begin{pmatrix}b_{1}\\\ b_{2}\\\ 0\end{pmatrix}$ Figure 5. Gadget (on the
right) made of copy and transfer transitions simulating the doubling
transition on the left.

The trick of the reduction is to represent two binary sequences as the natural
numbers the sequences encode, one in each counter. If we add an artificial $1$
at the beginning of the two binary sequences, then these sequences are
uniquely determined by their numerical values. We only need to be able to
double the counter values, which corresponds to shifting the sequences. This
can be achieved using the following matrices:

$\displaystyle\mathbf{D_{1}}$
$\displaystyle\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}\begin{pmatrix}2&0\\\ 0&1\end{pmatrix}\text{
and }\mathbf{D_{2}}\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}\begin{pmatrix}1&0\\\ 0&2\end{pmatrix}.$

The only matrices used in the construction of Reichert are $\mathbf{I}$,
$\mathbf{D_{1}}$ and $\mathbf{D_{2}}$. The last two matrices can be simulated
by a gadget made of copy and transfer matrices and by introducing a third
counter. This gadget is depicted in Figure 5 for the case of matrix
$\mathbf{D_{1}}$. The other gadget is symmetric. Note that if a run enters
control-state $p$ of the gadget with vector $(x,y,0)$, then it leaves control-
state $q$ in vector $(2x+b_{1},y+b_{2},0)$ as required.

######  Remark 14.

The coverability problem for nonnegative affine VASS is known to be decidable
in Ackermann time [FFSPS11]. Recall that coverability and reachability are
inter-reducible for affine $\mathbb{Z}$-VASS. Thus, Proposition 13 gives an
example of a decision problem, namely coverability, which is more difficult
for affine $\mathbb{Z}$-VASS than for affine VASS.

##  7\. Reachability beyond finite monoids

Thus far, we have shown, on the one hand, that reachability is decidable for
affine $\mathbb{Z}$-VASS with the finite-monoid property, and, on the other
hand, that reachability is undecidable for arbitrary affine $\mathbb{Z}$-VASS.
This raises the question of whether there is a decidability dichotomy between
classes of finite and infinite monoids, i.e. whether reachability is
undecidable for _every_ class of infinite monoids. In this section, we show
that this is not the case: we exhibit a non-trivial class of infinite monoids
for which affine $\mathbb{Z}$-VASS reachability is _decidable_. In other
words, the top rectangular region of Figure 1 is _not_ equal to the red
ellipse, which answers a question we left open in [BHM18]. The class of affine
$\mathbb{Z}$-VASS will have a particular shape, namely, the matrix monoids
have a single generator. More formally, we say that a class of matrices
$C=\bigcup_{d\geq 1}\mathcal{C}_{d}$ is _monogenic_ if each monoid
$\mathcal{C}_{d}$ is generated by a single matrix. In the second part of this
section we prove that reachability is in general undecidable for monogenic
classes.

###  7.1. Decidability for a class of affine $\mathbb{Z}$-VASS with infinite
monoids

Let $\mathcal{C}_{d}$ be the monoid generated by the (nonnegative) matrix
$\mathbf{J}_{d}\in\mathbb{N}^{d\times d}$ whose entries are all equal to $1$.
Clearly, $\mathcal{C}_{d}$ is infinite for every $d\geq 2$ since
$(\mathbf{J}_{d})^{n}$ is the matrix whose entries are all equal to $d^{n}$.
Let $\mathcal{C}_{\mathbf{J}}=\bigcup_{d\geq 1}\mathcal{C}_{d}$. The rest of
this section is devoted to proving the following theorem:

######  Theorem 15.

The reachability problem $\textsf{Reach}_{\mathcal{C}_{\mathbf{J}}}$ is
decidable.

Let $\mathcal{V}=(d,Q,T)$ be an affine $\mathbb{Z}$-VASS belonging to
$\mathcal{C}_{\mathbf{J}}$. We will simply write $\mathbf{J}$ instead of
$\mathbf{J}_{d}$ as $d$ is implicit from the dimension of $\mathcal{V}$.
Observe that we can assume w.l.o.g. that for every transition
$(p,\mathbf{A},\bm{b},q)\in T$ either $\mathbf{A}=\mathbf{I}$ or
$\bm{b}=\bm{0}$, i.e. each transition either performs a transformation of the
form $\bm{x}\leftarrow\bm{x}+\bm{b}$ or
$\bm{x}\leftarrow\mathbf{A}\cdot\bm{x}$. Indeed, by adding an extra state $r$,
we can always split such a transition into two transitions
$(p,\mathbf{A},\bm{0},r)$ and $(r,\mathbf{I},\bm{b},q)$. We can further assume
w.l.o.g. that $\mathbf{I}$ and $\mathbf{J}$ are the only matrices occurring in
$\mathcal{V}$. Indeed, if $T$ contains a transition
$t=(p,\mathbf{A},\bm{b},q)$ where
$\mathbf{A}\not\in\\{\mathbf{I},\mathbf{J}\\}$, then
$\mathbf{A}=\mathbf{J}^{n}$ for some $n\geq 2$ and $\bm{b}=\bm{0}$. Thus, we
can simply replace $t$ by a sequence of transitions $t_{1},t_{2},\ldots,t_{n}$
leading from $p$ to $q$ and such that $M(t_{i})=\mathbf{J}$ and
$\Delta(t_{i})=\bm{0}$ for every $i\in[n]$.

Let $T_{\mathbf{I}}$ and $T_{\mathbf{J}}$ denote the (maximal) subsets of $T$
of transitions with matrix $\mathbf{I}$ and $\mathbf{J}$ respectively. Note
that $T_{\mathbf{I}}$ and $T_{\mathbf{J}}$ form a partition of $T$. We will
write and to denote respectively the restriction of and to transitions of a
set $S$. We give a simple characterization of reachability in $\mathcal{V}$:

######  Proposition 16.

For all configurations $p(\bm{u})$ and $q(\bm{v})$ of $\mathcal{V}$,
$p(\bm{u})$ if and only if:

  1. (1)

$p(\bm{u})$; or

  2. (2)

$p(\bm{u})$ for some $r,r^{\prime}\in Q$ and $\bm{w}\in\mathbb{Z}^{d}$.

######  Proof 7.10.

$\Leftarrow$) Immediate.

$\Rightarrow$) Assume that $p(\bm{u})$ for some $w\in T^{*}$. If $w$ does not
contain any transition from $T_{\mathbf{J}}$, then (1) holds and we are done.
Thus, suppose that $w$ contains at least one transition from $T_{\mathbf{J}}$.
Let $t\in T_{\mathbf{J}}$ be the last such transition occurring in $w$. Recall
that, by assumption, $M(t)=\mathbf{J}$ and $\Delta(t)=\bm{0}$. Therefore, we
are done since there exist $r,r^{\prime}\in Q$ and $\bm{w}\in\mathbb{Z}^{d}$
such that

$\displaystyle p(\bm{u})$

In order to prove that $\textsf{Reach}_{\mathcal{C}_{\mathbf{J}}}$ is
decidable, it suffices to show that there exist procedures to decide the two
conditions of Proposition 16. Testing condition (1) amounts to
$\mathbb{Z}$-VASS reachability, which belongs to NP [HH14]. Indeed, any run
restricted to $T_{\mathbf{I}}$ is a run of the $\mathbb{Z}$-VASS induced by
$T_{\mathbf{I}}$. Thus, in the rest of the proof, we focus on showing how to
test condition (2).

For this purpose, let us introduce an auxiliary model. An _affine one-counter
$\mathbb{Z}$-net_ is a pair $(P,U)$ where

  * •

$P$ is a finite set of _states_ , and

  * •

$U\subseteq Q\times\\{+,\cdot\\}\times\mathbb{Z}\times Q$ is a finite set of
_transitions_.

Furthermore, for every transition $t=(p,\circledast,c,q)$, we write $p(n)$ if
$m=n\circledast c$. The notions of runs and reachability are defined
accordingly as for affine $\mathbb{Z}$-VASS. These machines are a special case
of one-counter register machines with polynomial updates whose reachability
problem belongs to PSPACE [FGH13], i.e. we only allow the counter to be
multiplied or incremented by constants, whereas the model of [FGH13] allows to
update the counter by a polynomial such as $x^{2}$ or $x^{3}-x+1$.

For every $\bm{v}\in\mathbb{Z}^{d}$, let

$\delta(\bm{v})\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}\sum_{i=1}^{d}\bm{v}(i).$

Consider the transitions $T$ in the affine $\mathbb{Z}$-VASS $\mathcal{V}$.
For every transition $t\in T$, let $\overline{t}$ be defined as:

$\overline{t}\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}\begin{cases}(p,+,\delta(\Delta(t)),q)&\text{if}\
t\in T_{\mathbf{I}},\\\ (p,\cdot,d,q)&\text{if}\ t\in
T_{\mathbf{J}},\end{cases}$

where $p=\mathrm{src}(t)$ and $q=\mathrm{tgt}(t)$.

Let $\mathcal{W}=(Q,\overline{T})$ be the affine one-counter $\mathbb{Z}$-net
obtained from $\mathcal{V}=(d,Q,T)$ by keeping the same states and taking
$\overline{T}\stackrel{{\scriptstyle\operatorname{\scriptscriptstyle
def}}}{{\raisebox{-0.75pt}{$=$}}}\\{\overline{t}:t\in T\\}$. We write
$\overline{w}\in\overline{T}^{*}$ to denote the (unique) sequence of
transitions in $\mathcal{W}$ corresponding to the sequence $w\in T^{*}$ of
$\mathcal{V}$. Let us observe the following correspondence between
$\mathcal{V}$ and $\mathcal{W}$:

######  Lemma 17.

For every $p,q\in Q$, $\bm{u}\in\mathbb{Z}^{d}$, $m\in\mathbb{Z}$ and $w\in
T^{*}$, we have $p(\delta(\bm{u}))$ in $\mathcal{W}$ if and only if
$p(\bm{u})$ in $\mathcal{V}$ for some $\bm{v}\in\mathbb{Z}^{d}$ such that
$\delta(\bm{v})=m$.

######  Proof 7.18.

The claim follows from a simple induction on $|w|$.

We may now prove Theorem 15.

######  Proof 7.19 (Proof of Theorem 15).

Recall that it suffices to show how to decide condition (2) of Proposition 16.
By definition of $\mathbf{J}$, this condition is equivalent to determining
whether there exist $r\in Q$ and $n\in\mathbb{Z}$ such that

$\displaystyle p(\bm{u})$

Let $S=\\{m\in\mathbb{Z}:\exists n\in\mathbb{Z}\ (m=d\cdot
n)\land\bigvee_{r\in Q}r(n,n,\ldots,n)$. As we mentioned earlier,
$\mathcal{V}$ can be seen as a standard $\mathbb{Z}$-VASS when restricted to
$T_{\mathbf{I}}$. Since the reachability relation of any $\mathbb{Z}$-VASS is
effectively semilinear [HH14], the set $S$ is also effectively semilinear.

$p$$\vdots$$\cdots$$r$$r^{\prime}$$\overline{T_{\mathbf{J}}}$$\overline{T_{\mathbf{J}}}$$\cdot
d$$\cdot d$$-f_{1}$$-f_{2}$$-f_{k}$$-b_{1}$$-b_{2}$$-b_{\ell}$$+0$$-a$ Figure
6. Affine one-counter $\mathbb{Z}$-net $\mathcal{W}$ extended with a gadget
subtracting a number of $S$ from some transition of
$\overline{T_{\mathbf{J}}}$ leading to $r$. The gadget is depicted in colour.
Transitions connecting $\mathcal{W}$ to the gadget are labeled with “$\cdot
d$” as this is the effect of every transition of $\overline{T_{\mathbf{J}}}$.

By Lemma 17, we have $p(\bm{u})$ if and only if $p(\delta(\bm{u}))$. Indeed,
the direction ($\Rightarrow$) is immediate. To prove the implication
($\Leftarrow$) suppose $p(\delta(\bm{u}))$. By Lemma 17 we have $p(\bm{u})$
such that $\delta(\bm{v})=d\cdot n$. By definition the last transition is
$r^{\prime}(\bm{w})$, where $\bm{v}=\mathbf{J}\cdot\bm{w}$. By definition of
$\mathbf{J}$: $\bm{v}=(\delta(\bm{w}),\ldots,\delta(\bm{w}))$. Since
$\delta(\bm{v})=d\cdot n$ we get $\bm{v}=(n,n,\ldots,n)$.

Thus, it suffices to test whether $p(\delta(\bm{u}))$ in $\mathcal{W}$ for
some $m=d\cdot n\in S$. This can be achieved by extending $\mathcal{W}$ with a
gadget that non deterministically subtracts some element of $S$ after
executing a transition from $\overline{T_{\mathbf{J}}}$. More precisely, since
$S$ is an (effectively) semilinear set of integers, it is also (effectively)
ultimately periodic. Thus, it is possible to obtain a description of $S=F\cup
B+a\cdot\mathbb{N}$ where $F=\\{f_{1},f_{2},\ldots,f_{k}\\}$ and
$B=\\{b_{1},b_{2},\ldots,b_{\ell}\\}$ are finite subsets of $\mathbb{Z}$. We
extend $\mathcal{W}$ with the gadget depicted in Figure 6. More precisely, for
every transition $t\in\overline{T_{\mathbf{J}}}$ leading to $r$, we add a new
transition leading to a gadget that either subtracts some number from $F$ or
some number from $B+a\cdot\mathbb{N}$. Note that the gadget is not “attached”
directly to $r$ as we must ensure that $r$ is entered by a transition of
$\overline{T_{\mathbf{J}}}$. Hence, testing whether

$p(\delta(\bm{u}))$

amounts to testing whether $p(\delta(\bm{u}))$ in the new net. Since the
latter can be done in polynomial space [FGH13], we are done.

###  7.2. Undecidability for monogenic classes

In contrast with the previous result, we prove that decidability is
undecidable in general for monogenic classes:

######  Theorem 18.

Reachability for monogenic affine $\mathbb{Z}$-VASS is undecidable. Moreover,
there exists a fixed monogenic affine $\mathbb{Z}$-VASS for which deciding
reachability is undecidable.

We show the first part of Theorem 18 by giving a reduction from the problem of
determining whether a given Diophantine equation has a solution over the
natural numbers, which is well-known to be undecidable. The second part of
Theorem 18 follows as a corollary. Indeed, by Matiyasevich’s theorem,
Diophantine sets correspond to recursively enumerable sets. In particular,
there exists a polynomial $P$ such that

$x\in\mathbb{N}\text{ is the encoding of a halting Turing
machine}\iff\exists\bm{y}:P(x,\bm{y})=0.$

The forthcoming construction will yield a monogenic affine $\mathbb{Z}$-VASS
that can test “$\exists\bm{y}:P(x,\bm{y})=0$” by nondeterministically guessing
$\bm{y}$ and testing $P(x,\bm{y})=0$. Hence, reachability cannot be decided
for this monogenic affine $\mathbb{Z}$-VASS as the above language is
undecidable.

Let us show the first part of Theorem 18. Let $x_{1},x_{2},\ldots,x_{k}$ be
variables of a given polynomial $P(x_{1},x_{2},\ldots,x_{k})$. We will
construct an instance of the reachability problem, for a monogenic affine
$\mathbb{Z}$-VASS $\mathcal{V}$, such that reachability holds if and only if
$P(x_{1},x_{2},\ldots,x_{k})=0$ has a solution over $\mathbb{N}^{k}$.

The affine $\mathbb{Z}$-VASS will be described using the syntax of counter
programs; see [Esp98, CLL+19], where a similar syntax was used to present the
VASS model. We will make use of two instructions: zero($\mathtt{x}$)? and
loop. The former checks whether counter $\mathtt{x}$ has value $0$, and the
latter repeats a block of instructions an arbitrary number of times. Figure 7
gives an example of such a program together with its translation as an affine
$\mathbb{Z}$-VASS.

loop

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

$\mathtt{y}\,\,=\,\mathtt{y}\,+\,4$

loop

$\mathtt{y}\,\,=\,\mathtt{y}\,-\,3\mathtt{x}+1$

zero($\mathtt{y}$)?

$\begin{pmatrix}1&0\\\ 0&1\end{pmatrix}$, $\begin{pmatrix}1\\\
4\end{pmatrix}$$\begin{pmatrix}1&0\\\ -3&1\end{pmatrix}$, $\begin{pmatrix}0\\\
1\end{pmatrix}$$\begin{pmatrix}1&0\\\ 0&1\end{pmatrix}$, $\begin{pmatrix}0\\\
0\end{pmatrix}$

Figure 7. _Left_ : an example program $\mathcal{P}$ using instructions zero?
and loop. _Right_ : an affine $\mathbb{Z}$-VASS $\mathcal{V}$ equivalent to
$\mathcal{P}$, where its first and second components correspond to counters
$\mathtt{x}$ and $\mathtt{y}$ respectively. The program loops are simulated by
loops within the control structure of $\mathcal{V}$. Note that whenever
$\mathcal{P}$ only adds and subtracts constants from counters, the associated
matrix is the identity. Since the only way $\mathcal{V}$ can test whether a
counter equals $0$ is at the end of the program via a reachability query,
instruction zero($\mathtt{y}$)? merely emphasizes that counter $\mathtt{y}$
will never be used again.

Macros. Before describing the reduction, let us introduce helpful macros.
First, we define macros “transfer ${\mathtt{x}}$ onto ${\mathtt{y}}$” and
“remove ${\mathtt{x}}$ from ${\mathtt{y}}$”. The former computes
$\mathtt{y}=\mathtt{y}+\mathtt{x}$ and $\mathtt{x}=0$, and the latter computes
$\mathtt{y}=\mathtt{y}-\mathtt{x}$ and $\mathtt{x}=0$. Both macros work under
the assumption that $\mathtt{x}$ is initially non negative. These macros are
implemented as follows:

transfer ${\mathtt{x}}$ onto ${\mathtt{y}}$: _// pre-cond.: $\mathtt{x}\geq
0$_

loop

$\mathtt{x}\,\,=\,\mathtt{x}\,-\,1$

$\mathtt{y}\,\,=\,\mathtt{y}\,+\,1$

zero($\mathtt{x}$)?

remove ${\mathtt{x}}$ from ${\mathtt{y}}$: _// pre-cond.: $\mathtt{x}\geq 0$_

loop

$\mathtt{x}\,\,=\,\mathtt{x}\,-\,1$

$\mathtt{y}\,\,=\,\mathtt{y}\,-\,1$

zero($\mathtt{x}$)?

We define another macro “$\mathtt{t}$ = square($\mathtt{s}$)” for squaring the
contents of a counter. More precisely, it computes $\mathtt{s}=\mathtt{t}^{2}$
and $\mathtt{t}=0$. This macro is implemented as follows:

1: $\mathtt{t}$ = square($\mathtt{s}$): _// pre-condition:
$\mathtt{t}=\mathtt{x}=\mathtt{y}=\mathtt{z}=0$_

2: transfer ${\mathtt{s}}$ onto ${\mathtt{x}}$

3: loop

4: $\mathtt{x}\,\,=\,\mathtt{x}\,-\,1$

5: $\mathtt{y}\,\,=\,\mathtt{y}\,+\,1$

6: $\mathtt{z}\,\,=\,\mathtt{z}\,+\,2\mathtt{y}+1$

7: zero($\mathtt{x}$)?

8: transfer ${\mathtt{z}}$ onto ${\mathtt{t}}$ _//
$\mathtt{t}=\mathtt{s}^{2}$, $\mathtt{y}=\mathtt{s}$ and
$\mathtt{x}=\mathtt{z}=0$_

9: remove ${\mathtt{s}}$ from ${\mathtt{y}}$

10: zero($\mathtt{y}$)? _// $\mathtt{y}=0$_

The above program starts with $\mathtt{t}$ and its auxiliary counters set to
$0$, and ends with $\mathtt{s}$ and the auxiliary counters set to $0$. Its
correctness follows by observing that $(n+1)^{2}=n^{2}+(2n+1)$.

We introduce one last macro “$\mathtt{t}$ = mult($\mathtt{s}$,
$\mathtt{s^{\prime}}$)” for multiplication. More precisely, it computes
$\mathtt{t}=\mathtt{s}\cdot\mathtt{s}^{\prime}$ and
$\mathtt{s}=\mathtt{s}^{\prime}=0$. Its implementation exploits the fact that
$2mn=(m+n)^{2}-m^{2}-n^{2}$:

$\mathtt{t}$ = mult($\mathtt{s}$, $\mathtt{s}^{\prime}$): _// pre-condition:
$\mathtt{t}=\mathtt{x}=\mathtt{y}=\mathtt{z}=\mathtt{z}^{\prime}=0$_

$\mathtt{x}$ = square($\mathtt{s}$) _// $\mathtt{x}=\mathtt{s}^{2}$_

$\mathtt{y}$ = square($\mathtt{s}^{\prime}$) _//
$\mathtt{y}=(\mathtt{s}^{\prime})^{2}$_

transfer ${\mathtt{s}}$ onto ${\mathtt{z}^{\prime}}$

transfer ${\mathtt{s}^{\prime}}$ onto ${\mathtt{z}^{\prime}}$

$\mathtt{z}$ = square($\mathtt{z}^{\prime}$) _//
$\mathtt{z}=(\mathtt{s}+\mathtt{s}^{\prime})^{2}$, $\mathtt{z}^{\prime}=0$_

remove ${\mathtt{x}}$ from ${\mathtt{z}}$

remove ${\mathtt{y}}$ from ${\mathtt{z}}$ _//
$\mathtt{z}=2\cdot\mathtt{s}\cdot\mathtt{s}^{\prime}$,
$\mathtt{x}=\mathtt{y}=0$_

loop

$\mathtt{z}\,\,=\,\mathtt{z}\,-\,2$

$\mathtt{t}\,\,=\,\mathtt{t}\,+\,1$

zero($\mathtt{z}$)? _// $\mathtt{t}=\mathtt{s}\cdot\mathtt{s}^{\prime}$,
$\mathtt{z}=0$_

The above program starts with $\mathtt{t}$ and its auxiliary counters set to
$0$, and ends with $\mathtt{s}$, $\mathtt{s}^{\prime}$ and its auxiliary
counters set to $0$. Note that a macro “$\mathtt{t}$ = mult($\mathtt{s}$,
$c$)” for multiplying by a constant $c$ can be achieved by a simpler program:

$\mathtt{t}$ = mult($\mathtt{s}$, $c$): _// pre-condition: $\mathtt{t}=0$_

loop

$\mathtt{s}\,\,=\,\mathtt{s}\,-\,1$

$\mathtt{t}\,\,=\,\mathtt{t}\,+\,c$

zero($\mathtt{s}$)?

Although these programs can be implemented rather straightforwardly by an
affine $\mathbb{Z}$-VASS, two remarks are in order:

  * •

Affine $\mathbb{Z}$-VASS do not have any native operation for testing a
counter for zero. However, a counter $\mathtt{x}$ can be tested _once_ via a
reachability query, provided that $\mathtt{x}$ is left untouched after
instruction zero($x$)? has been invoked. Consequently, a _constant_ number of
zero-tests can be performed on a counter, provided its initial contents has
been duplicated;

  * •

Instruction “transfer ${\mathtt{s}}$ onto ${\mathtt{t}}$” at line 2 of macro
“$\mathtt{t}$ = square($\mathtt{s}$)” destroys the contents of $\mathtt{s}$
which is later needed at line 9. As for zero-tests, this is not an issue
provided that some counter holds a copy of $\mathtt{s}$. Thus, only a
_constant_ number of squaring, and hence of multiplications, can be performed
from a given counter.

The construction. Let us now describe the reachability instance. The initial
vector is $\bm{0}$, which corresponds to having all counters set to $0$ at the
start of the program. The target vector is also $\bm{0}$, which corresponds to
performing zero tests on all counters.

The program starts by performing a sequence of loops that guess a valuation
$\bm{x}$ for which $P(\bm{x})=0$ is to be tested. More precisely, a value is
nondeterministically picked for each variable $x_{i}$ and stored in counters
$\mathtt{x}_{i}^{1},\mathtt{x}_{i}^{2},\ldots,\mathtt{x}_{i}^{n_{i}}$. The
reason for having $n_{i}$ copies of the value is to address the two issues
mentioned earlier concerning zero-tests and reusing counters within macros.
The precise number of copies, $n_{i}$, will be determined later. The fragment
of code achieving the initialization is as follows:

loop

$\mathtt{x}_{1}^{1}\,\,=\,\mathtt{x}_{1}^{1}\,+\,1$;
$\mathtt{x}_{1}^{2}\,\,=\,\mathtt{x}_{1}^{2}\,+\,1$; $\cdots$
$\mathtt{x}_{1}^{n_{1}}\,\,=\,\mathtt{x}_{1}^{n_{1}}\,+\,1$

loop

$\mathtt{x}_{2}^{1}\,\,=\,\mathtt{x}_{2}^{1}\,+\,1$;
$\mathtt{x}_{2}^{2}\,\,=\,\mathtt{x}_{2}^{2}\,+\,1$; $\cdots$
$\mathtt{x}_{2}^{n_{2}}\,\,=\,\mathtt{x}_{2}^{n_{2}}\,+\,1$

⋮

loop

$\mathtt{x}_{k}^{1}\,\,=\,\mathtt{x}_{k}^{1}\,+\,1$;
$\mathtt{x}_{k}^{2}\,\,=\,\mathtt{x}_{k}^{2}\,+\,1$; $\cdots$
$\mathtt{x}_{k}^{n_{k}}\,\,=\,\mathtt{x}_{k}^{n_{k}}\,+\,1$

After the initialization, we compute the value of each monomial occurring
within polynomial $P(x_{1},x_{2},\ldots,x_{k})$. This can be achieved using
counters $\mathtt{x}_{i}^{j}$ and the multiplication macro. Let
$Q(x_{1},x_{2},\ldots,x_{k})$ be a monomial of degree $d$. We show how to
proceed by induction on $d$. If $d=0$, then this is trivial. For larger
degrees, we evaluate $Q$ without its coefficient $c$, and then apply macro
“$\mathtt{t}$ = mult($\mathtt{s}$, $c$)”. If $d=1$, then we can simply
transfer the appropriate counter $\mathtt{x}_{i}^{j}$. Otherwise, $Q$ is a
product of two monomials $Q^{\prime}$ and $Q^{\prime\prime}$ of smaller
degrees. By induction hypothesis, we can construct three copies of both
monomials $Q^{\prime}$ and $Q^{\prime\prime}$. Then, using the multiplication
macro, we obtain $Q$. Having evaluated all monomials, we can transfer each of
their values to a common counter using the transfer and remove macros
depending on whether their sign is positive or negative. Finally, we test if
the resulting value equals zero, which corresponds to having a solution to
$P(x_{1},x_{2},\ldots,x_{k})=0$.

Before arguing correctness of the construction, let us see why the whole
program can be translated as a monogenic affine $\mathbb{Z}$-VASS
$\mathcal{V}$, i.e. using only the identity matrix and one extra matrix
$\mathbf{A}$. First, note that all macros have internal counters $\mathtt{x}$,
$\mathtt{y}$ and $\mathtt{z}$. Every time we use a macro, we use three fresh
counters, increasing the dimension of $\mathcal{V}$. Second, note that the
only macro that requires a matrix different from the identity is “$\mathtt{t}$
= square($\mathtt{s}$)”, which doubles $\mathtt{y}$ during an assignment to
$\mathtt{z}$ at line 6. We will construct the matrix $\mathbf{A}$ as follows.
Suppose we want to encode one of the squaring macros. Matrix $\mathbf{A}$ will
have the same updates for all counters denoted as $\mathtt{z}$ in all macros,
but the vector will use constants according to this macro. That is, all
coordinates for counters not occurring in this macro will be $0$. In
particular, counter $\mathtt{z}$ from this macro will be updated like in line
6, i.e. “$\mathtt{z}\,\,=\,\mathtt{z}\,+\,2\mathtt{y}+1$”, and all other
counters corresponding to some other $\mathtt{z}$ will be updated as
“$\mathtt{z}\,\,=\,\mathtt{z}\,+\,2\mathtt{y}$”.

Correctness. We conclude by proving correctness of the construction. If $P$
has a solution, then it is straightforward to extract a run from
$\mathcal{V}$: (a) each $\mathtt{x}_{i}^{j}$ is initialized according to the
solution; and (b) each loop of the program is performed the exact number times
so that each zero-test holds. It remains to observe that after performing a
zero-test on some counter, $\mathcal{V}$ does not perform any operation on
this counter or performs “$\mathtt{z}\,\,=\,\mathtt{z}\,+\,2\mathtt{y}$”. But
if the values of $\mathtt{y}$ and $\mathtt{z}$ are equal to zero, then
$\mathtt{z}$ will remain equal to zero after such an update.

Conversely, suppose there is a reachability witness (from $\bm{0}$ to
$\bm{0}$). We claim that the initialization of counters $\mathtt{x}_{i}^{j}$
provides a solution to $P$. To prove this, it suffices to show that every
zero-test was valid. This is clear for all counters except for the
$\mathtt{z}$ within the squaring macro. Indeed, all other counters never
change their values afterwards. However, counter $\mathtt{z}$ is updated by
“$\mathtt{z}\,\,=\,\mathtt{z}\,+\,2\mathtt{y}$”. If $\mathtt{y}$ is non zero,
then this will be detected by the zero-test on $\mathtt{y}$. Otherwise, the
update “$\mathtt{z}\,\,=\,\mathtt{z}\,+\,2\mathtt{y}$” never changes the value
of $\mathtt{z}$ as required.

##  8\. Conclusion

We have shown that the reachability problem for afmp-$\mathbb{Z}$-VASS reduces
to the reachability problem for $\mathbb{Z}$-VASS, i.e. every
afmp-$\mathbb{Z}$-VASS $\mathcal{V}$ can be simulated by a $\mathbb{Z}$-VASS
of size polynomial in $|\mathcal{V}|$, $|\mathcal{M}_{\mathcal{V}}|$ and
$\lVert\mathcal{M}_{\mathcal{V}}\rVert$. In particular, this allowed us to
establish that the reachability relation of any afmp-$\mathbb{Z}$-VASS is
semilinear.

For all nonnegative classes and consequently for all of the variants we
studied — reset, permutation, transfer, copy and copyless $\mathbb{Z}$-VASS —
$|\mathcal{M}_{\mathcal{V}}|$ and $\lVert\mathcal{M}_{\mathcal{V}}\rVert$ are
of exponential size, thus yielding a PSPACE upper bound on their reachability
problems. Moreover, we have established PSPACE-hardness for all of these
specific classes, except for the reset case which is NP-complete.

We do not know whether an exponential bound on
$\lVert\mathcal{M}_{\mathcal{V}}\rVert$ holds for any class of
afmp-$\mathbb{Z}$-VASS over $\mathbb{Z}^{d\times d}$. We are aware that an
exponential upper bound holds when $\mathcal{M}_{\mathcal{V}}$ is generated by
a single matrix [IS16]; and when $\mathcal{M}_{\mathcal{V}}$ is a group then
we have an exponential bound but only on $|\mathcal{M}_{\mathcal{V}}|$ (see
[KP02] for an exposition on the group case).

Finally, we have shown that there exists a (monogenic) class without the
finite-monoid property for which reachability is decidable. This result was
complemented by showing that reachability is undecidable in general for
monogenic classes.

## Acknowledgments

We are thankful to James Worrell for insightful discussions on transfer VASS.

## References

  * [ACJT96] Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, and Yih-Kuen Tsay.  General decidability theorems for infinite-state systems.  In Proc. $11^{\text{th}}$ Annual IEEE Symposium on Logic in Computer Science (LICS), pages 313–321, 1996.
  * [AD16] Parosh Aziz Abdulla and Giorgio Delzanno.  Parameterized verification.  International Journal on Software Tools for Technology Transfer, 18(5):469–473, 2016.
  * [AFR14] Rajeev Alur, Adam Freilich, and Mukund Raghothaman.  Regular combinators for string transformations.  In Proc. Joint Meeting of the $23^{\text{rd}}$ EACSL Annual Conference on Computer Science Logic (CSL) and the $29^{\text{th}}$ ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 9:1–9:10, 2014\.
  * [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.
  * [AR13] Rajeev Alur and Mukund Raghothaman.  Decision problems for additive regular functions.  In Proc. $40^{\text{th}}$ International Colloquium on Automata, Languages, and Programming (ICALP), pages 37–48, 2013.
  * [BFG+15] Michael Blondin, Alain Finkel, Stefan Göller, Christoph Haase, and Pierre McKenzie.  Reachability in two-dimensional vector addition systems with states is PSPACE-complete.  In Proc. $30^{\text{th}}$ Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 32–43, 2015.
  * [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.
  * [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.
  * [Boi98] Bernard Boigelot.  Symbolic Methods for Exploring Infinite State Spaces.  PhD thesis, Université de Liège, Belgium, 1998.
  * [Bon13] Rémi Bonnet.  Theory of Well-Structured Transition Systems and Extended Vector-Addition Systems.  PhD thesis, École normale supérieure de Cachan, France, 2013\.
  * [CFM12] Michaël Cadilhac, Alain Finkel, and Pierre McKenzie.  Bounded Parikh automata.  International Journal of Foundations of Computer Science, 23(8):1691–1710, 2012.
  * [CFM13] Michaël Cadilhac, Alain Finkel, and Pierre McKenzie.  Unambiguous constrained automata.  International Journal of Foundations of Computer Science, 24(7):1099–1116, 2013.
  * [CH16] Dmitry Chistikov and Christoph Haase.  The taming of the semi-linear set.  In Proc. $43^{\text{rd}}$ International Colloquium on Automata, Languages, and Programming (ICALP), pages 128:1–128:13, 2016.
  * [CLL+19] Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, 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.
  * [Del16] Giorgio Delzanno.  A unified view of parameterized verification of abstract models of broadcast communication.  International Journal on Software Tools for Technology Transfer, 18(5):475–493, 2016.
  * [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.
  * [ELM+14] Javier Esparza, Ruslán Ledesma-Garza, Rupak Majumdar, Philipp J. Meyer, and Filip Niksic.  An SMT-based approach to coverability analysis.  In Proc. $26^{\text{th}}$ International Conference on Computer Aided Verification (CAV), pages 603–619, 2014.
  * [EN98] E. Allen Emerson and Kedar S. Namjoshi.  On model checking for non-deterministic infinite-state systems.  In Proc. $13^{\text{th}}$ Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 70–80, 1998.
  * [Esp98] Javier Esparza.  Decidability and complexity of Petri net problems — an introduction.  In Lectures on Petri Nets I, pages 374–428, 1998.
  * [FFSPS11] Diego Figueira, Santiago Figueira, Sylvain Schmitz, and Philippe Schnoebelen.  Ackermannian and primitive-recursive bounds with Dickson’s lemma.  In Proc. $26^{\text{th}}$ Annual IEEE Symposium on Logic in Computer Science (LICS), pages 269–278, 2011.
  * [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.
  * [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\.
  * [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.
  * [HP79] John E. Hopcroft and Jean-Jacques Pansiot.  On the reachability problem for 5-dimensional vector addition systems.  Theoretical Computer Science, 8:135–159, 1979.
  * [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 Transactions on Programming Languages and Systems, 36(4):14:1–14:29, 2014.
  * [KM69] Richard M. Karp and Raymond E. Miller.  Parallel program schemata.  Journal of Computer and System Sciences, 3(2):147–195, 1969.
  * [Kos82] S. Rao Kosaraju.  Decidability of reachability in vector addition systems (preliminary version).  In Proc. $14^{\text{th}}$ Annual ACM Symposium on Theory of Computing (STOC), pages 267–281, 1982.
  * [KP02] James Kuzmanovich and Andrey Pavlichenkov.  Finite groups of matrices whose entries are integers.  The American Mathematical Monthly, 109(2):173–186, 2002.
  * [Ler12] Jérôme Leroux.  Vector addition systems reachability problem (a simpler solution).  In The Alan Turing Centenary Conference, pages 214–228, 2012.
  * [Lip76] Richard J. Lipton.  The reachability problem requires exponential space.  Technical Report 63, Department of Computer Science, Yale University, 1976\.
  * [May84] Ernst W. Mayr.  An algorithm for the general Petri net reachability problem.  SIAM Journal on Computing, 13(3):441–460, 1984.
  * [Min67] Marvin Lee Minsky.  Computation: Finite and Infinite Machines.  Prentice-Hall, 1967.
  * [MS77] Arnaldo Mandel and Imre Simon.  On finite semigroups of matrices.  Theoretical Computer Science, 5(2):101–111, 1977.
  * [Pre29] Mojżesz Presburger.  Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt.  Comptes Rendus du $\text{I}^{\text{er}}$ Congrès des mathématiciens des pays slaves, pages 192–201, 1929.
  * [Rac78] Charles Rackoff.  The covering and boundedness problems for vector addition systems.  Theoretical Computer Science, 6:223–231, 1978.
  * [Rei08] Klaus Reinhardt.  Reachability in Petri nets with inhibitor arcs.  Electronic Notes in Theoretical Computer Science, 223:239–264, 2008\.
  * [Rei15] Julien Reichert.  Reachability games with counters: decidability and algorithms.  PhD thesis, École normale supérieure de Cachan, France, 2015\.
  * [Sch10] Philippe Schnoebelen.  Revisiting Ackermann-hardness for lossy counter machines and reset Petri nets.  In Proc. $35^{\text{th}}$ International Symposium Mathematical Foundations of Computer Science (MFCS), pages 616–628, 2010.
  * [Web87] Andreas Weber.  Über die Mehrdeutigkeit und Wertigkeit von endlichen Automaten und Transducern.  PhD thesis, Goethe-Universität Frankfurt am Main, 1987.
  * [WS91] Andreas Weber and Helmut Seidl.  On finitely generated monoids of matrices with entries in $\mathbb{N}$.  Informatique Théorique et Applications, 25:19–38, 1991.