Affine Extensions of Integer Vector Addition Systems with States
Michael Blondin Christoph Haase Filip Mazowiecki Mikhail Raskin

Affine Extensions of Integer Vector Addition Systems with States]Affine Extensions of 

  Integer Vector Addition Systems with States
*A preliminary version of this paper appeared in the proceedings of the 29^th International Conference on Concurrency Theory (CONCUR), 2018 <cit.>.


M. Blondin]Michael Blondin
Université de Sherbrooke, Canada
michael.blondin@usherbrooke.ca
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)

C. Haase]Christoph Haase
University of Oxford, United Kingdom
christoph.haase@cs.ox.ac.uk

F. Mazowiecki]Filip Mazowiecki
Max Planck Institute for Software Systems, Germany
filipm@mpi-sws.org
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]Mikhail Raskin
Technische Universität München, Germany
raskin@in.tum.de
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)



  We study the reachability problem for affine -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 -VASS with the finite-monoid property
  (afmp--VASS). The latter have the property that the monoid
  generated by the matrices appearing in their affine transformations
  is finite. The class of afmp--VASS encompasses classical
  operations of counter machines such as resets, permutations,
  transfers and copies. We show that reachability in an afmp--VASS
  reduces to reachability in a -VASS whose control-states grow
  linearly in the size of the matrix monoid. Our construction shows
  that reachability relations of afmp--VASS are semilinear, and in
  particular enables us to show that reachability in -VASS with
  transfers and -VASS with copies is PSPACE-complete. We then
  focus on the reachability problem for affine -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 -VASS with infinite matrix monoids we raised in a
  preliminary version of this paper. We complement this result by
  presenting an affine -VASS with monogenic matrix monoid
  and undecidable reachability relation.



[
    [
    December 30, 2023
=====================






§ 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 <cit.>. Those properties make VASS
and their extensions a prime choice for reasoning about and modelling
concurrent, distributed and parametrised systems, see  the recent
surveys by Abdulla and Delzanno <cit.>.

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 <cit.>, all
important decision problems for VASS with two counters which can
arbitrarily be tested for zero are undecidable <cit.>. 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 <cit.> yet decidable coverability
problem <cit.>. Nevertheless, the computational costs for those
extensions are high: while coverability is EXPSPACE-complete for
VASS <cit.>, it becomes Ackermann-complete in the presence of
resets and transfers <cit.>. 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 <cit.>. It was already observed
in <cit.> 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 ( A, b⃗), where A is a
d× d matrix over the integers and b⃗∈^d is an
integer vector. A transition switches the control-state while updating
the configuration of the counters v⃗∈^d to A·v⃗ + b⃗, provided that A·v⃗ + b⃗≥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 <cit.>.

Due to the symbolic state-explosion problem and Ackermann-hardness of
coverability, standard decision procedures for transfer VASS such as
the backward algorithm <cit.> 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,
, <cit.>). 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 -VASS,
see  <cit.>. 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, , affine VASS in which a configuration of the counters
is a point in ^d, and in which all transitions are
non-blocking. Subsequently, we refer to such VASS as affine
  -VASS.

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

In more detail, we show that reachability in an afmp--VASS can be
reduced to reachability in a -VASS whose size is polynomial in the
size of the original afmp--VASS and in the norm of the finite
monoid  generated by the matrices occurring along
transitions, denoted by . For a vast number of classes
of affine transformations considered in the literature,
 is bounded exponentially in the dimension of the
matrices. This enables us to deduce a general PSPACE upper bound for
extensions of -VASS such as transfer -VASS and copy
-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 -VASS <cit.>. We also show
that a PSPACE lower bound of the reachability problem already holds
for the extension of -VASS that only use permutation matrices in
their transition updates. This in turn gives PSPACE-completeness of
interesting classes such as transfer -VASS and copy -VASS.

Finally, we show that an affine -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,
 classes of monoids with a single generator. We show that although
reachability can still be undecidable for an affine -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 <ref>, 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 <cit.>, Iosif and Sangnier <cit.>, Haase
and Halfon <cit.>, and Cadilhac, Finkel and
McKenzie <cit.>. In <cit.>, Finkel and
Leroux consider a model more general than affine -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 σ, Finkel and
Leroux show that the reachability set obtained from repeatedly
iterating σ, , the acceleration of σ, 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 <cit.> do not work over  since transitions are
non-blocking. Iosif and Sangnier <cit.> 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 <cit.>
studied the complexity of the reachability, coverability and inclusion
problems for -VASS and reset -VASS, two submodels of the
affine -VASS that we study in this paper.  In
 <cit.>, 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 <cit.>.
  
Structure of the paper. We introduce general notations and
affine -VASS in Section <ref>. In
Section <ref>, we give the reduction from
afmp--VASS to -VASS. Subsequently, in
Section <ref> we show that afmp--VASS have
semilinear reachability relations and discuss semilinearity of affine
-VASS in general. In Section <ref>, we show
PSPACE and NP upper bounds of the reachability problem for some
classes of afmp--VASS; and in Section <ref> we
show PSPACE-hardness and undecidability results for some classes of
affine -VASS. In Section <ref>, we show that
reachability is undecidable for monogenic affine -VASS and remains
decidable for a specific class of infinite monoids. Some concluding
remarks will be made in Section <ref>.






§ PRELIMINARIES



General notation. For n ∈, we write [n] for the set
{1, 2, …, n}. For every x⃗ = (x_1, x_2, …, x_d)
∈^d and every i ∈ [d], we define x⃗(i)  x_i. We
denote the identity matrix and the zero-vector by I and
0⃗ in every dimension, as there will be no ambiguity. For 
x⃗∈^d and A∈^d × d, we define the
max-norm of x⃗ and A as x⃗max{|x⃗(i)| : i ∈ [d]} and Amax{A_i : i ∈ [d]} where A_i denotes the
i^th column of A. We naturally extend this notation
to finite sets,  Gmax{A : A∈ G} for every G ⊆_fin^d × 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 -VASS) is a tuple = (d, Q, T)
where d ∈, Q is a finite set and T ⊆ Q ×^d
  × d×^d × Q is finite. Let us fix such a
. We call d the dimension of  and the elements of Q
and T respectively control-states and transitions. For
every transition t = (p, A, b⃗, q), we define t
p, t q, [t] A and [t] b⃗, and let f_t ^d →^d be the affine
transformation defined by f_t(x⃗) = A·x⃗ +
b⃗. The size of , denoted ||, 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
||  d + |Q| + (d^2 + d) · |T| ·max(1, ⌈log(T + 1) ⌉) where 
    Tmax(max{[t] : t ∈ T }, max{[t] : t ∈
    T }).


A configuration of  is a pair (q, v⃗) ∈ Q ×^d which we write as q(v⃗). For every t ∈ T and
p(u⃗), q(v⃗) ∈ Q ×^d, we write p(u⃗)
t q(v⃗) whenever p = t, q = t and v⃗ =
f_t(u⃗). We naturally extend  to sequences of
transitions as follows. For every w = w_1 ⋯ w_k ∈ T^k and p(u⃗),
q(v⃗) ∈ Q ×^d, we write p(u⃗) w
q(v⃗) if either k = 0 (denoted w = ε) and p(u⃗) = q(v⃗), or
k > 0 and there exist p_0(u⃗_0), p_1(u⃗_1), …,
p_k(u⃗_k) ∈ Q ×^d such that

    p(u⃗) = p_0(u⃗_0) w_1 p_1(u⃗_1) w_2⋯w_k p_k(u⃗_k) = q(v⃗).
 We write p(u⃗) * q(v⃗) if there exists some w ∈
T^* such that p(u⃗) w q(v⃗). The relation
* is called the reachability relation of . If
p(u⃗) w q(v⃗), then we say that w is a run
  from p(u⃗) to q(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 [] {[t] : t ∈ T} and [] {[t] : t ∈ T}. If  is clear from the context, we
sometimes simply write  and . The monoid of ,
denoted [] or sometimes simply , is the monoid
generated by [],  it is the smallest set that contains
[], is closed under matrix multiplication, and contains the
identity matrix. We say that a matrix A∈^d × d is
respectively a (i) reset, (ii) permutation,
(iii) transfer, (iv) copyless, or (v) copy matrix
if A∈{0, 1}^d × d and


  * A does not contain any 1 outside of its diagonal;
  

  * A has exactly one 1 in each row and each column;


  * A has exactly one 1 in each column;


  * A has at most one 1 in each column;


  * A has exactly one 1 in each row.


Analogously, we say that  is respectively a reset,
permutation, transfer, copyless, or copy
-VASS if all matrices of [] are reset, permutation,
transfer, copyless, or copy matrices. The monoids of such affine
-VASS are finite and respectively of size at most 2^d, d!,
d^d, (d+1)^d and d^d. Copyless -VASS correspond to a model
of copyless cost-register automata studied in <cit.> (see the
remark below). If [] only contains the identity matrix, then
 is simply called a -VASS.

A class of matrices  is a union ⋃_d ≥ 1_d where _d is a finitely generated, but possibly
infinite, submonoid of ^d × d for every d ≥ 1. We say
that  belongs to a class  of -VASS if _⊆. If each _d is finite, then we say that this
class of affine -VASS has the finite-monoid property
(afmp--VASS). For two classes  and ' we write
+ ' to denote the smallest set 𝒟 =
⋃_d ≥ 1𝒟_d such that 𝒟_d is a
monoid that contains both _d and _d' for every d ≥
1. Note that this operation does not preserve finiteness. For
example if  and ' are the classes of transfer and copy matrices, respectively,
then + ' is infinite (see
Figure <ref> and Section <ref>). We say
that a class = ⋃_d ≥ 1_d is
nonnegative if _d ⊆^d × d for every
d ≥ 1. We say that an affine -VASS  is nonnegative if
_ belongs to some nonnegative class of matrices. Note that the
classes of reset, permutation, transfer, copyless and copy matrices
are all nonnegative, respectively.



We discuss the -VASS  in Figure <ref> to give some
intuition behind the names transfer and copy -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) ∈^2, we have p(x, y)  q(x, x),  the value of the first
counter is copied to the second counter. Similarly, for the other
transition we have q(x, y)  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 A and B be the two matrices
used in . Note that (A·B)^n is the matrix with
all entries equal to 2^n-1, and hence _ is infinite.


  The variants of affine -VASS that we consider are related to
  cost register automata (CRA) with only the +
  operation <cit.> 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 ← y + c,
  where x, y are registers and c is an integer. An affine
  -VASS does not read any input, but is nondeterministic. Thus,
  one can identify an affine -VASS with a CRA that reads sequences
  of transitions as words. In particular, the restrictions imposed on
  the studied CRAs correspond to copy -VASS <cit.> and
  copyless -VASS <cit.>.


Decision problems. We consider the reachability and the
coverability problems parameterized by classes of matrices
:

  [] (reachability problem) 


  Given:     an affine -VASS = (d, Q, T) and
  configurations p(u⃗), q(v⃗) s.t. []
  ⊆. 

  
  Decide:     whether p(u⃗) * q(v⃗).
 


  [] (coverability problem) 


  Given:     an affine -VASS = (d, Q, T) and
  configurations p(u⃗), q(v⃗) s.t. []
  ⊆. 

  
  Decide:     whether there exists v⃗' ∈^d such
  that p(u⃗) * q(v⃗') and v⃗' ≥v⃗.


For standard VASS (where configurations cannot hold negative values),
the coverability problem is much simpler than the reachability
problem. However, for affine -VASS, these two problems coincide as
observed in <cit.>: 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.




§ FROM AFFINE -VASS WITH THE FINITE-MONOID PROPERTY TO -VASS
 

The main result of this section is that every affine -VASS 
with the finite monoid property can be simulated by a -VASS with twice the number of 
counters whose size is polynomial in [] and
||. More formally, we show the following:


  For every afmp--VASS = (d, Q, T) and p,q ∈ Q there exist a -VASS
  ' = (d', Q', T') and p', q' ∈ Q' such that
  
  
  * d' = 2 · d,

  
  * |Q'| ≤ 3 · |[]| · |Q|,

  
  * |T'| ≤ 4d · |[]| · (|Q| + |T|),

  
  * T'≤[]·T,

  
  * p(u⃗) * q(v⃗) in  if and only if
    p'(u⃗, 0⃗) * q'(0⃗, v⃗) in '.
  
  Moreover, ', p' and q' are effectively computable from .



  The reachability problem for afmp--VASS is decidable.



  By Theorem <ref>, it suffices to construct, for
  a given afmp--VASS , the -VASS ' and to test for
  reachability in '. It is known that reachability for -VASS
  is in NP <cit.>. To effectively compute ' it suffices to
  provide a bound for []. It is known that if
  |_| is finite then it is bounded by a computable function
  (see <cit.>), and hence [] is also
  computable.


For the remainder of this section, let us fix some affine -VASS
 such that [] is finite. We proceed as follows to prove
Theorem <ref>. First, we introduce some notations
and intermediary lemmas characterizing reachability in affine
-VASS. Next, we give a construction that essentially proves the
special case of Theorem <ref> where the initial
configuration is of the form p(0⃗). Finally, we prove
Theorem <ref> 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(v⃗) can be turned into one of the form
p'(0⃗) by adding a transition that adds v⃗. The reason
for proving the general case is that it establishes a stronger
relation that allows us to prove semilinearity of afmp--VASS
reachability relations in Section <ref>.



 §.§ A characterization of reachability

  
For every w ∈ T^*, t ∈ T and u⃗∈^d, let

    [ε]    I,
         ε(u⃗)    u⃗,
      
    [w t]    [t] ·[w],
          w t(u⃗)    [t] · w(u⃗) + [t].

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

 
  For every w ∈ T^* and p(u⃗), q(v⃗) ∈ Q ×^d, it is the case that p(u⃗) w q(v⃗) if and
  only if
  
  
  * w is a path from p to q in the underlying graph of
    , and 
  
  * v⃗ = w(u⃗).
  


Testing for reachability with Lemma <ref> requires
evaluating w(u⃗). This value can be evaluated conveniently as
follows:

 
  For every w=w_1w_2⋯ w_k ∈ T^k and u⃗∈^d, the
  following holds:
  
    w(u⃗) = [w] ·u⃗ + ∑_i=1^k(w_i+1
        w_i+2⋯ w_k) ·[w_i].

  Moreover, w(u⃗) = [w] ·u⃗ + w(0⃗).



  We prove (<ref>) by induction on k. The base
  case follows from ε(u⃗) = u⃗ = I·u⃗ + 0⃗ = [ε] ·u⃗ +
  0⃗. Assume that k > 0 and that the claim holds for sequences
  of length k - 1. For simplicity we denote σ w_1
  ⋯ w_k-1. We have:
  
    w(u⃗)
           = σ w_k(u⃗) 
       = [w_k] ·σ (u⃗) + [w_k] 
       = [w_k] ·([σ] ·u⃗ +
        ∑_i=1^k-1(w_i+1 w_i+2⋯ w_k-1) ·[w_i]) + [w_k] 
       = [w_k] ·[σ] ·u⃗ + ∑_i=1^k-1[w_k] ·(w_i+1 w_i+2⋯ w_k-1) ·[w_i] + [w_k] 
       = [σ w_k] ·u⃗ + ∑_i=1^k-1(w_i+1 w_i+2⋯ w_k) ·[w_i] + [w_k]
        
       = [w] ·u⃗ + ∑_i=1^k(w_i+1 w_i+2⋯ w_k) ·[w_i]

  where (<ref>), (<ref>) and (<ref>)
  follow respectively by definition of σ w_k(u⃗), by
  induction hypothesis and by definition of M(σ w_k).
  
  The last part of the lemma follows from
  applying (<ref>) to w(0⃗) and
  w(u⃗), and observing that subtracting them results in
  w(u⃗) - w(0⃗) = [w] ·u⃗.


Observe that Lemma <ref> is trivial for the
particular case of -VASS. Indeed, we obtain w(u⃗) = u⃗
+ ∑_i=1^k[w_i], which is the sum of transition vectors
as expected for a -VASS.



 §.§ Reachability from the origin


We make use of Lemmas <ref>
and <ref> to construct a -VASS ' = (d, Q',
T') for the special case of Theorem <ref> where
the initial configuration is of the form p(0⃗). The states and
transitions of ' are defined as:

    Q'     Q ×, 
    
      T'    {((t, A), I, A·[t],
      (t, A·[t])) : A∈, t ∈ T}.


The idea behind ' is to simulate a path w of  backwards and
to evaluate w(0⃗) as the sum identified in
Lemma <ref>. More formally, ' and  are
related as follows:
  
 
  
  
  * For every w ∈ T^*, if p(0⃗) w q(v⃗) in
    , then q'(0⃗) * p'(v⃗) in ', where q'
     (q, I) and p'  (p, [w]).

  
  * If q'(0⃗) * p'(v⃗) in ', where q'
     (q, I) and p'  (p, A), then there
    exists w ∈ T^* such that [w] = A and p(0⃗)
    w q(v⃗) in .
  



  (a) By Lemma <ref>,  has a
  path w ∈ T^* such that w(0⃗) = v⃗. Let k 
  |w|. Let A_0 I, and for every i ∈ [k] let
  
    A_i    [w_k-i+1⋯ w_k-1 w_k], 
    
        b⃗_i    A_i-1·[w_k-i+1], 
    
        w_i'     ((w_k-i+1, A_i-1), I, b⃗_i,
        (w_k-i+1, A_i)).

  We claim that w'  w_1' w_2' ⋯ w_k' is such that (q,
  A_0) w' (p, A_k) in '. Note that the
  validity of the claim completes the proof since A_0 =
  I and A_k = [w].

  It follows immediately from the definition of T' that w_i' ∈
  T' for every i ∈ [k] and hence that w' is a path from (q,
  A_0) to (p, A_k). By Lemma <ref>, it
  remains to show that w'(0⃗) = v⃗:
  
    w'(0⃗)
        
           = ∑_i=1^k(w_i+1' w_i+2' ⋯ w_k') ·[w_i']
              (by Lemma <ref> applied to
          w'(0⃗))
    
           = ∑_i=1^k[w_i']
              (by [w_i'] = I for every i ∈ [k])
    
           = ∑_i=1^kA_i-1·[w_k-i+1]
              (by definition of [w_i'])
    
           = ∑_i=1^k(w_k-i+2 w_k-i+1⋯ w_k) ·[w_k-i+1]
              (by definition of A_i-1)
    
           = ∑_i=1^k(w_i+1 w_i+2⋯ w_k) ·[w_i]
              (by inspection of the sum)
    
           = w(0⃗)
              (by Lemma <ref> applied to w(0⃗)).

  

  (b) Similarly, by Lemma <ref>, there
  exists a path w' of ' such that w'(0⃗) = v⃗, and
  it suffices to exhibit a path w ∈ T^* from p to q in 
  such that w(0⃗) = v⃗ and [w] = A. Let k
   |w'|. For every i ∈ [k], let w_i' = ((p_i, A_i),
  I, b⃗_i, (q_i, B_i)). By definition of T', for
  every i ∈ [k], there exists a (possibly non unique) transition
  t_i ∈ T such that t = p_i, t = q_i, b⃗_i =
  A_i ·[t] and B_i = A_i ·[t]. We set w  t_1 t_2 ⋯ t_k. It is readily seen
  that w is a path from p to q. To prove w(0⃗) = v⃗
  and [w] = A, Lemma <ref> can be
  applied as in the previous implication.




 §.§ Reachability from an arbitrary configuration


We now construct the -VASS ”= (2d, Q”, T”) of
Theorem <ref> which is obtained mostly from
'. The states of ” are defined as:

    Q”    Q ∪ Q' ∪Q'      where  Q'{(q, A) :
      (q, A) ∈ Q'}.

To simplify notation, given two vectors u⃗, v⃗∈^d we write (u⃗, v⃗) for the vector of ^2d equal
to u⃗ on the first d components and equal to v⃗ on the
last d components. The set T” consists of four disjoint subsets
of transitions T_simul∪ T_end∪ T_mult∪ T_final working in four sequential stages. Intuitively,
these transitions allow (1) ” to simulate a path w of 
backwards in order to compute w(0⃗); (2) guess the end of this
path; (3) compute [w] ·u⃗ by using the fact that
[w] is stored in its control-state; and (4) guess the end of
this matrix multiplication.

The first set of transitions is defined as:

    T_simul   {(t, I, (0⃗, [t]),
      t) : t ∈ T'}.

Its purpose is to simulate T' on the last d counters. The second
set is defined as:

    T_end   {((q, A), I, (0⃗, 0⃗),
      (q, A)) : (q, A) ∈ Q'},

and its purpose is to nondeterministically guess the end of a run in
' by simply marking q. The third set is defined as:

  T_mult
             {((q, A), I, (-e⃗_i,
  A ·e⃗_i), (q, A)) : (q,
  A) ∈Q', i ∈[d]} ∪ 

  
            {((q, A), I, (e⃗_i, -A ·e⃗_i), (q, A)) : (q, A) ∈Q', i ∈[d]},

where e⃗_i is the i-th unit vector such that e⃗_i(i) = 1
and e⃗_i(j)=0 for all i≠ j. The
purpose of T_mult is to compute A·u⃗ from
the d first counters onto the d last counters. Finally,
T_final is defined as:

    T_final   {((q, A), I, (0⃗,
     0⃗), q) : (q, A) ∈Q'},

and its purpose is to guess the end of the matrix multiplication
performed with T_mult.

We may now prove Theorem <ref>:


  First, note that we obtain
  
    |Q”|
        
           = 2 · |Q'| + |Q| 
    
           ≤ 3 · |Q| · ||, 
    
        |T”|
        
           = |T'| + |Q'| + 2d · |Q'| + |Q'| 
    
           = |T'| + 2(d+1) · |Q'| 
    
           = |T| · || + 2(d+1) · |Q| · || 
    
           ≤ 4d · || · (|T| + |Q|).

  Moreover, we have:
  
    T”
           = max(T', ) 
    
           ≤max(·T, ) 
    
           = ·T.


  We conclude by proving that p(u⃗) * q(v⃗) in 
  if and only if q'(u⃗, 0⃗) * p(0⃗, v⃗)
  in ”, where q'  (q, I).

  ⇒) By Lemma <ref>, there exists a path
  w of  such that w(u⃗) = v⃗. By definition of
  T_simul and T_end, and by
  Proposition <ref>, it is the case that
  q'(u⃗, 0⃗) * p'(u⃗, w(0⃗)) where p'
   (p, [w]). The transitions of T_mult allow to
  transform (u⃗, w(0⃗)) into (0⃗, w(0⃗) +
  [w] ·u⃗). Thus, using T_final, we can reach
  the configuration p(w(0⃗) + [w] ·u⃗). This
  concludes the proof since w(u⃗) = w(0⃗) + [w] ·u⃗ by Lemma <ref>.

  ⇐) The converse implication follows the same steps as
  the previous one. It suffices to observe that the first part of a
  run of ” defines the value w(0⃗), while the second part
  of the run defines [w] ·u⃗.





§ SEMILINEARITY OF AFFINE -VASS
 

A subset of ^d is called semilinear if it is definable by a
formula of Presburger arithmetic <cit.>,  by a formula of
𝖥𝖮(, +, <), the decidable first-order logic over 
with addition and order. Semilinear sets capture precisely finite
unions of sets of the form b⃗ + ·p⃗_1 + ·p⃗_2 + … + ·p⃗_k with each p⃗_i∈^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 ^d need to be manipulated.

The results of Section <ref> enable us to show that
any affine -VASS with the finite-monoid property has a semilinear
reachability relation:

 
  Given an afmp--VASS = (d, Q, T) and p, q ∈ Q, it is
  possible to compute an existential Presburger formula φ_,
    p, q of size at most 𝒪(poly(||,
  |[]|, log[])) such that φ_, p,
    q(u⃗, v⃗) holds if and only if p(u⃗) *
  q(v⃗) in .



  By Theorem <ref>, there exist an effectively
  computable -VASS ' = (d', Q', T') and p', q' ∈ Q' such
  that d' = 2 · d, |Q'| ≤ 3 · || · |Q|,
  |T'| ≤ 4d · || · (|Q| + |T|), T'≤·T and
  
    p(u⃗) * q(v⃗)  in  if and only if
       p'(u⃗, 0⃗) * q'(0⃗, v⃗)  in '.

  By <cit.>, we can compute an existential Presburger
  formula ψ of linear size in |'| such that ψ(x⃗,
  x⃗', y⃗, y⃗') holds if and only if p'(x⃗,
  x⃗') * q'(y⃗, y⃗') in
  '. By Equation (<ref>), the formula φ_, p, q(x⃗,
  y⃗) ψ(x⃗, 0⃗, 0⃗, y⃗) satisfies
  the theorem.


It was observed in <cit.> that the reachability relation of
a -VASS = (d, Q, T), such that |Q| = |[]| = 1, is
semilinear if and only if [] is
finite. Theorem <ref> shows that if we do not bound
the number of states and matrices,  drop the assumption |Q| =
|[]| = 1, then (⇐) remains true. It is
natural to ask whether (⇒) also remains true.



Let _1 and _2 be the affine -VASS illustrated in
Figure <ref> from left to right respectively. Note
that [_1] and [_2] are both infinite due to the
matrix made only of 1s. Moreover, the reachability relations of
_1 and _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
_1 has a single control-state, |[_1]| = |[_2]| = 2
and [_2] = {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 -VASS with an infinite monoid
may have a non semilinear reachability relation. Indeed,
Figure <ref> depicts a transfer + copy -VASS with an
infinite monoid and such that {v⃗ : p(1, 1) *
q(v⃗)} = {(2^n, 2^n) : n ∈}, which is known to be non
semilinear. Moreover, this proves that even the reachability set from
p(1, 1) is not semilinear.




§ COMPLEXITY OF REACHABILITY FOR AFMP--VASS
 

In this section, we use the results of Section <ref>
to show that reachability belongs to PSPACE for a large class of
afmp--VASS encompassing all variants discussed in
Section <ref>. Moreover, we give a novel proof to
the known NP membership of reachability for reset -VASS.

For every finite set G_d ⊆^d × d, let ⟨ G_d
⟩ be the monoid generated by G_d. We have:

 
  Let = ⋃_d ≥ 1_d be a class of matrices
  such that _d is finite for every d ≥ 1. It is the case
  that [] ∈PSPACE if there exists a polynomial
  poly such that |⟨ G_d ⟩| + ⟨ G_d
    ⟩≤ 2^poly(d + logG_d) for every d
  ≥ 1 and every finite set G_d such that ⟨ G_d ⟩⊆_d.



  Let = (d, Q, T) be an affine -VASS from class . Let
  ' = (d, Q', T') be the -VASS obtained from  in
  Theorem <ref>. Recall that, by
  Theorem <ref>, p(u⃗) * q(v⃗)
  in  if and only if p'(u⃗, 0⃗) * q'(0⃗,
  v⃗) in '. Therefore, it suffices to check the latter for
  determining reachability in .

  We invoke a result of <cit.> on the flattability of
  -VASS. By <cit.>, p'(x⃗) *
  q'(y⃗) in ' if and only if there exist k ≤ |T'|,
  α_0, β_1, α_1, …, β_k, α_k ∈ (T')^*
  and e⃗∈^k such that
  
  
  * p'(x⃗) α_0 β_1^e⃗(1)α_1 ⋯β_k^e⃗(k) q'(y⃗) in ', 

  
  * β_i is a cycle for every i ∈ [k], and
    
  
  * α_0 β_1 α_1 ⋯β_k α_k is a path
    from p' to q' of length at most 2 · |Q'| ·
    |T'|. 
  

  For every w ∈ (T')^*, let [w] ∑_i = 1^|w|[w_i]. By Lemma <ref> (see the remark below
  the proof of Lemma <ref>), we have w(u⃗) =
  u⃗ + [w] for every u⃗∈^d. Thus, by
  Lemma <ref>, checking <ref>,
  assuming <ref>, amounts to testing whether e⃗
  is a solution of the following system of linear Diophantine
  equations:
  
    x⃗ +
        ∑_i = 0^k [α_i] +
        [ [β_1] [β_2]     ⋯ [β_k] ]·e⃗   = y⃗.

  Let G_d []. Note that G_d≤T and
  that ⟨ G_d ⟩ = []. Let m  2 · |Q'|
  · |T'|. By Theorem <ref>, we have m ≤
  48d · ||^2 · |Q|^2 · |T|. Thus, since ⟨
  G_d ⟩ is a submonoid of _d, and by assumption on
  _d, we have 
    m ≤ 48d ·(2^poly(d + logT))^2 · |Q|^2 ·
      |T|.
 Thus, m is exponential in ||.
  
  We describe a polynomial-space non deterministic Turing machine
  𝒜 for testing whether p'(x⃗) * q'(y⃗)
  in '. The proof follows from NPSPACE = PSPACE. Machine
  𝒜 guesses k ≤ |T'|, a path π = α_0 β_1
  α_1 ⋯β_k α_k of length at most m from p' to
  q', and e⃗∈^k, and tests
  whether (<ref>) holds for π. Note that we are not
  given ', but , so we must be careful for the machine to work
  in polynomial space.

  Instead of fully constructing ' and fully guessing π, we do
  both on the fly, and also construct [α_0],
  [β_1], …, [β_k], [α_k] on the fly
  as partial sums as we guess π. Note that to ensure that each
  β_i is a cycle, we do not need to fully store β_i but
  only its starting control-state. Moreover, note that
  [α_i], [β_i]≤ m ·T' for every i. By Theorem <ref> and
  by assumption on _d, we have
  
    T'   ≤⟨ G_d ⟩·T
       ≤ 2^poly(d + logT)·T.

  Hence, each α_i and β_i has a binary representation of
  polynomial size in ||.

  By <cit.>, (<ref>) has a solution if
  and only if it has a solution e⃗∈^k such
  that 
    e⃗≤((k + 1) ·max{[β_i] : i ∈ [k]} + x⃗ +
      y⃗ + ∑_i=0^k [α_i] +
      1)^d'.
 Since d' = 2 · d, this means that we can
  guess a vector e⃗∈^k whose binary representation is of
  polynomial size, and that we can thus
  evaluate (<ref>) in polynomial time.



  The reachability problem for nonnegative afmp--VASS is in
  PSPACE, and hence in particular for reset, permutation, transfer,
  copy and copyless -VASS.



  Let = ⋃_d ≥ 1_d be a class of nonnegative
  matrices. Let d ≥ 1 and let G_d be a finite set of matrices
  such that ⟨ G_d ⟩⊆_d. By <cit.>, whose proof appears in <cit.> written by one of
  the same authors, we have:
  
    |⟨G_d ⟩|    ≤G_d^d^2 ·(d - 1) ·5^d^3 / 2 ·d^d^3 ·d^2       = 2^d^2 ·(d-1) ·logG_d + (d^3 / 2) ·log5 + d^3 ·logd + 2
      ·logd,  

    ⟨G_d ⟩    ≤G_d^d-1 ·5^d/2
    ·d^d       = 2^(d-1) ·logG_d + (d / 2) ·log5
      + d ·logd.
  
  Thus,  satisfies the requirements of
  Theorem <ref>. To complete the proof, observe that
  determining whether [] is finite can be done in time
  𝒪(d^6 · |T|), again by <cit.>
  and <cit.>.

  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.


[<cit.>]
  The reachability problem for reset -VASS belongs to NP.



  Let = (d, Q, T) be a reset -VASS. The proof does not follow
  immediately from Theorem <ref> because
  [] can be of size up to 2^d. We will analyze the
  construction used in the proof of Theorem <ref>,
  where reachability in  is effectively reduced to reachability in
  a -VASS ' = (d', Q', T'). Recall that Q' = (Q ×[]) ∪ (Q×[]) ∪ Q, and
  thus that the size of ' depends only on the sizes of Q and
  [].

  It follows from the proof of Theorem <ref> and
  Proposition <ref> that for every run
  q'(u⃗,0⃗) * p(0⃗,v⃗) in ' where q'
   (q, I), there is a corresponding run p(u⃗)
  w q(v⃗) in  for some w ∈ T^* of length k ≥
  0. Moreover, the i^th matrix occuring within the
  control-states of this run are is the form A_i where
  A_i = A_i-1·B for some B∈[]. Since [] consists of reset matrices, it
  holds that A_0, A_1, A_2, …, A_k is
  monotonic,  if A_i-1 has a 0 somewhere on its
  diagonal, then A_i also contains 0 in that position. It
  follows that A_0, A_1, …, 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 [] that could appear in sequence
  A_0, A_1, …, A_k. We construct the
  -VASS ' as in Theorem <ref>, but we
  discard each control-state of Q' containing a matrix not drawn
  from the guessed matrices. Since the constructed -VASS is of
  polynomial size, reachability can be verified in NP <cit.>.



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





§ HARDNESS RESULTS FOR REACHABILITY
 

It is known that the reachability problem for -VASS is already
NP-hard <cit.>, which means that reachability is NP-hard for all
classes of affine -VASS. In this section, we show that
PSPACE-hardness holds for some classes, matching the PSPACE upper
bound derived in Section <ref>. Moreover, we observe
that reachability is undecidable for transfer + copy -VASS.

 
  The reachability problem for permutation -VASS is
  PSPACE-hard.



  We give a reduction from the membership problem of linear bounded
  automata, which is known to be PSPACE-complete (see,
  , <cit.>). Let 𝒜 = (P, Σ,
  Γ, δ, q^ini, q^acc, q^rej) be a
  linear bounded automaton, where:
  
  
  * P is the set of states,
  
  * Σ⊆Γ is the input alphabet,
  
  * Γ is the tape alphabet,
  
  * δ is the transition function, and
  
  * q^ini, q^acc,q^rej are the initial,
    accepting and rejecting states respectively.
  

  The transition function is a mapping δ : P ×Γ→ P
  ×Γ×{Left,Right}. The intended
  meaning of a transition δ(p, a) = (q, b, D) is that whenever
  𝒜 is in state p and holds letter a at the current
  position of its tape, then 𝒜 overwrites a with b and
  moves to state q and to the next tape position in direction D.

  Let us fix a word w ∈Σ^* of length n that we will check
  for membership. We construct a permutation -VASS = (d, Q, T)
  and configurations r(u⃗) and r'(0⃗) such that
  𝒜 accepts w if and only if r(u⃗) *
  r'(0⃗).
  
  We set d  n · |Γ| + 1 and associate a counter to
  each position of w and each letter of the tape alphabet Γ,
  plus one additional counter. For readability, we denote these
  counters respectively as x_i, a and y, where i ∈ [n] and
  a ∈Γ. The idea is to maintain, for every i ∈ [n], a
  single non zero counter among {x_i, a : a ∈Γ} in order
  to represent the current letter in the i^th tape cell of
  𝒜. The initial vector is u⃗∈{0, 1}^d such
  that u⃗(y) = n and u⃗(x_i, a) = 1 if and only if
  w_i = a for every i ∈ [n] and a ∈Γ.  The invariant
  that will be maintained during all runs is y = ∑_i,ax_i,a.

  The control-states of  are defined as:
  
    Q    {r_p, i : p ∈ P, i ∈ [n]}∪{r_a,i : a ∈Γ, i ∈ [n]}∪{r_acc}.

  The purpose of each state of the form r_p, i is to store the
  current state p and head position i of 𝒜. States of the
  form r_a, i will be part of a gadget testing whether
  𝒜 is simulated faithfully.

  We associate a transition to every triple (p, a, i) ∈ P ×Γ× [n], which denotes a configuration of 𝒜:
  the automaton is in state p in position i, where letter a is
  stored. Let us fix a transition δ(p, a) = (q, b, D); and let
  j  i + 1 if D = Right, and j  i - 1 if D
  = Left. For every i ∈ [n], if j ∈ [n], then we add
  to T the transition
  
    (r_p, i, A, a⃗, r_q, j)

  where A is a permutation matrix that swaps the values of
  x_i, a and x_i, b; and a⃗ is the vector whose only nonzero
  components are a⃗(x_i,b) = 1 and a⃗(y) = 1.
  The transition is
  depicted on the left of Figure <ref> (for D =
  Right). Notice that all transitions maintain the invariant y = ∑_i,ax_i,a.
  
  The purpose of the swap is to simulate the transition of
  𝒜, 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,  it can simulate reading letter a
  even though tape cell i contains another letter. The purpose of
  the vector 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 ∈Γ} will be a nonzero counter.

  

  Recall that y = ∑_i,ax_i,a. We conclude that 𝒜
  accepts w if and only if there exist j ∈ [n], u⃗' ∈^d and a_1, a_2, …, a_n ∈Γ such that
  
    r_q^ini,1(u⃗) * r_q^acc,j(u⃗')
       and u⃗'(y) = ∑_i ∈ [d]u⃗'(x_i,a_i).

  
  To test whether such index j, vector u⃗' and letters a_1,
  a_2, …, a_n exist, we add some transitions to T as
  illustrated on the right of Figure <ref>.  For every
  i ∈ [n] and every a ∈Γ, we add to T the transitions
  (r_q^acc,i, I, 0⃗, r_a,1). For every i ∈
  [n] and a ∈Γ, we add to T the transitions (r_a,i,
  I, b⃗, r_a,i) where b⃗ is the vector whose only
  non zero components are b⃗(x_i, a) = b⃗(y) =
  -1. Moreover, if i < n, then for every a,b ∈Γ we also
  add transitions (r_a,i, I, 0⃗, r_b,i+1). Finally,
  for all a ∈Γ, we also add transitions (r_a,n, I,
  0⃗, r_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_acc.  We conclude
  that 𝒜 accepts w if and only if r_q^ini,
    1(u⃗) * r_acc(0⃗) in .



  The reachability problem is PSPACE-complete for permutation
  -VASS, transfer -VASS and copy -VASS.



  PSPACE-hardness for permutation -VASS was shown in
  Theorem <ref>, and the upper bound for transfer
  -VASS and copy -VASS follows from
  Theorem <ref>. It remains to observe that
  permutation matrices are also transfer and copy matrices.



  The reachability problem for transfer + copy -VASS is
  undecidable, even when restricted to three counters.



  Reichert <cit.> gives a reduction from the Post correspondence
  problem over the alphabet {0, 1} to reachability in affine
  -VASS with two counters.
  
  
  
  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:
  
    D_1   [ 2 0; 0 1 ] and D_2[ 1 0; 0 2 ].
  

  The only matrices used in the construction of Reichert are
  I, D_1 and 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 <ref> for the case of matrix
  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.



  The coverability problem for nonnegative affine VASS is known to be
  decidable in Ackermann time <cit.>. Recall that coverability
  and reachability are inter-reducible for affine -VASS. Thus,
  Proposition <ref> gives an example of a
  decision problem, namely coverability, which is more difficult for
  affine -VASS than for affine VASS.





§ REACHABILITY BEYOND FINITE MONOIDS



Thus far, we have shown, on the one hand, that reachability is decidable
for affine -VASS with the finite-monoid property, and, on the other
hand, that reachability is undecidable for arbitrary affine
-VASS. This raises the question of whether there is a decidability
dichotomy between classes of finite and infinite monoids,  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 -VASS
reachability is decidable. In other words, the top rectangular
region of Figure <ref> is not equal to the
red ellipse, which answers a question we left open
in <cit.>. The class of affine -VASS will have a
particular shape, namely, the matrix monoids have a single
generator. More formally, we say that a class of matrices C =
⋃_d ≥ 1_d is monogenic if each monoid
_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.



 §.§ Decidability for a class of affine -VASS with infinite monoids


Let _d be the monoid generated by the (nonnegative) matrix
_d ∈^d × d whose entries are all equal to
1. Clearly, _d is infinite for every d ≥ 2 since
(_d)^n is the matrix whose entries are all equal to
d^n. Let = ⋃_d ≥ 1_d. The rest of this
section is devoted to proving the following theorem:


  The reachability problem [] is decidable.


Let = (d, Q, T) be an affine -VASS belonging to
. We will simply write  instead of _d as
d is implicit from the dimension of . Observe that we can assume
w.l.o.g. that for every transition (p, A, b⃗, q) ∈ T
either A = I or b⃗ = 0⃗,  each
transition either performs a transformation of the form x⃗←x⃗ + b⃗ or x⃗←A·x⃗. Indeed, by adding an extra state r, we can always split
such a transition into two transitions (p, A, 0⃗, r) and
(r, I, b⃗, q). We can further assume w.l.o.g. that
I and  are the only matrices occurring in
. Indeed, if T contains a transition t = (p, A, b⃗,
q) where A∉{I, }, then A =
^n for some n ≥ 2 and b⃗ = 0⃗. Thus, we can
simply replace t by a sequence of transitions t_1, t_2, …,
t_n leading from p to q and such that [t_i] = and
[t_i] = 0⃗ for every i ∈ [n].

Let  and  denote the (maximal) subsets of T of
transitions with matrix I and  respectively. Note
that  and  form a partition of T. We
will write S and S^* to denote respectively the
restriction of  and * to transitions of a set
S. We give a simple characterization of reachability in :


  For all configurations p(u⃗) and q(v⃗) of ,
  p(u⃗) * q(v⃗) if and only if:
  
  
  *  p(u⃗) T_I^* q(v⃗); or

  
  *  p(u⃗) * r'(w⃗) 
    r(·w⃗) ^* q(v⃗) for some r,
    r' ∈ Q and w⃗∈^d.
  



  ⇐) Immediate.

  ⇒) Assume that p(u⃗) w q(v⃗) for some
  w ∈ T^*. If w does not contain any transition from ,
  then (<ref>) holds and we are done. Thus, suppose that w
  contains at least one transition from . Let t ∈ be
  the last such transition occurring in w. Recall that, by
  assumption, [t] = and [t] =
  0⃗. Therefore, we are done since there exist r, r' ∈ Q and
  w⃗∈^d such that
  
    p(u⃗) * r'(w⃗) t r(·w⃗)
        ^* q(v⃗).



In order to prove that [] is decidable, it suffices
to show that there exist procedures to decide the two conditions of
Proposition <ref>. Testing condition (<ref>)
amounts to -VASS reachability, which belongs to
NP <cit.>. Indeed, any run restricted to  is a run of the
-VASS induced by . Thus, in the rest of the proof, we focus
on showing how to test condition (<ref>).

For this purpose, let us introduce an auxiliary model. An affine
  one-counter -net is a pair (P, U) where


  * P is a finite set of states, and


  * U ⊆ Q ×{+, ·}×× Q is a
  finite set of transitions.


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

For every v⃗∈^d, let 
    δ(v⃗) ∑_i=1^d v⃗(i).
 

Consider the transitions T in the affine -VASS . For every transition t ∈ T, let t be defined as:

    t
      (p, +, δ([t]), q)    if t ∈, 
    
      (p, ·, d, q)               if t ∈,
 where p = t and q = t.

Let = (Q, T) be the affine one-counter -net
obtained from = (d, Q, T) by keeping the same states and taking
T{t : t ∈ T}. We write
w∈T^* to denote the (unique) sequence of transitions in
 corresponding to the sequence w ∈ T^* of . Let us observe
the following correspondence between  and :


  For every p, q ∈ Q, u⃗∈^d, m ∈ and w ∈
  T^*, we have p(δ(u⃗)) w q(m) in 
  if and only if p(u⃗) w q(v⃗) in  for some
  v⃗∈^d such that δ(v⃗) = m.



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


We may now prove Theorem <ref>.


Recall that it
suffices to show how to decide condition (<ref>) of
Proposition <ref>. By definition of , this
condition is equivalent to determining whether there exist r ∈ Q
and n ∈ such that

    p(u⃗) T^* · r(n, n, …, n) ^*
      q(v⃗).


Let S = {m ∈ : ∃ n ∈ (m = d · n) ⋁_r ∈ Q r(n, n, …, n) ^* q(v⃗)}. As
we mentioned earlier,  can be seen as a standard -VASS when
restricted to . Since the reachability relation of any -VASS
is effectively semilinear <cit.>, the set S is also effectively
semilinear.



By Lemma <ref>, we have p(u⃗) T^* · r(n, n, …, n) if and only if p(δ(u⃗))
T^* · r(d · n). Indeed,
the direction (⇒) is immediate. To prove the implication (⇐) suppose p(δ(u⃗))
T^* · r(d · n).
By Lemma <ref> we have p(u⃗) T^* · r(v⃗) such that δ(v⃗) = d · n. By definition the last transition is r'(w⃗) t r(·w⃗), where v⃗ = ·w⃗.
By definition of : v⃗ = (δ(w⃗), …, δ(w⃗)). Since δ(v⃗) = d · n we get v⃗ = (n, n, …, n).

Thus, it suffices to test whether p(δ(u⃗))
T^* · r(m) in  for some m
= d · n ∈ S. This can be achieved by extending  with a
gadget that non deterministically subtracts some element of S after
executing a transition from . 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 ∪ B + a · where F = {f_1, f_2,
…, f_k} and B = {b_1, b_2, …, b_ℓ} are finite
subsets of . We extend  with the gadget depicted in
Figure <ref>. More precisely, for every transition
t ∈ 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 ·. Note that the gadget is not
“attached” directly to r as we must ensure that r is entered by
a transition of . Hence, testing
whether 
    p(δ(u⃗)) T^* · r(m)  in  for some  m ∈ S

amounts to testing whether p(δ(u⃗)) * r'(0) in the
new net. Since the latter can be done in polynomial
space <cit.>, we are done.




 §.§ Undecidability for monogenic classes


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


  Reachability for monogenic affine -VASS is
  undecidable. Moreover, there exists a fixed monogenic affine
  -VASS for which deciding reachability is undecidable.


We show the first part of Theorem <ref> 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 <ref>
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 ∈ is the encoding of a halting Turing machine∃y⃗ : P(x, y⃗) = 0.
 The forthcoming construction
will yield a monogenic affine -VASS that can test “∃y⃗ : P(x, y⃗) = 0” by nondeterministically guessing
y⃗ and testing P(x, y⃗) = 0. Hence, reachability cannot
be decided for this monogenic affine -VASS as the above language
is undecidable.

Let us show the first part of Theorem <ref>. Let x_1,
x_2, …, x_k be variables of a given polynomial P(x_1, x_2,
…, x_k). We will construct an instance of the reachability
problem, for a monogenic affine -VASS , such that reachability
holds if and only if P(x_1, x_2, …, x_k) = 0 has a solution
over ^k.

The affine -VASS will be described using the syntax of counter
programs; see <cit.>, where a similar
syntax was used to present the VASS model. We will make use of two
instructions: x and loop. The former checks
whether counter x has value 0, and the latter repeats a block
of instructions an arbitrary number of
times. Figure <ref> gives an example of such a program
together with its translation as an affine -VASS.



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


  0.49
    
  
  0.49
    
  
  


We define another macro “□st” for squaring the
contents of a counter. More precisely, it computes s = t^2
and t = 0. This macro is implemented as follows:


  0.98
    
  
  

The above program starts with t and its auxiliary counters set
to 0, and ends with 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 “ss't” for
multiplication. More precisely, it computes t = s·s' and s = s' = 0. Its implementation exploits the
fact that 2mn = (m + n)^2 - m^2 - n^2:


  0.98
    
  
  

The above program starts with t and its auxiliary counters set
to 0, and ends with s, s' and its auxiliary counters
set to 0. Note that a macro “sct” for
multiplying by a constant c can be achieved by a simpler program:


  0.98
    
  
  


Although these programs can be implemented rather straightforwardly by
an affine -VASS, two remarks are in order:


  * Affine -VASS do not have any native operation for testing a
  counter for zero. However, a counter x can be tested
  once via a reachability query, provided that x is left
  untouched after instruction 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 “st” at line <ref> of
  macro “□st” destroys the contents of s
  which is later needed at line <ref>. As for zero-tests, this
  is not an issue provided that some counter holds a copy of
  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 0⃗, which corresponds to having
all counters set to 0 at the start of the program. The target vector
is also 0⃗, which corresponds to performing zero tests on all
counters.

The program starts by performing a sequence of loops that guess a
valuation x⃗ for which P(x⃗) = 0 is to be tested. More
precisely, a value is nondeterministically picked for each variable
x_i and stored in counters x_i^1, x_i^2, …,
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:


  0.98
    
  
  


After the initialization, we compute the value of each monomial
occurring within polynomial P(x_1, x_2, …, x_k). This can be
achieved using counters x_i^j and the multiplication macro. Let
Q(x_1, x_2, …, 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 “sct”. If d = 1, then we can
simply transfer the appropriate counter x_i^j. Otherwise, Q
is a product of two monomials Q' and Q” of smaller degrees. By
induction hypothesis, we can construct three copies of both monomials
Q' and Q”. 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, …, x_k) = 0.

Before arguing correctness of the construction, let us see why the
whole program can be translated as a monogenic affine -VASS ,
 using only the identity matrix and one extra matrix
A. First, note that all macros have internal counters
x, y and z. Every time we use a macro, we use
three fresh counters, increasing the dimension of . Second, note
that the only macro that requires a matrix different from the identity
is “□st”, which doubles y during an
assignment to z at line <ref>. We will construct the matrix
A as follows. Suppose we want to encode one of the squaring
macros. Matrix A will have the same updates for all counters
denoted as 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 z
from this macro will be updated like in line <ref>,
 “z2y + 1”, and all other counters
corresponding to some other z will be updated as
“z2y”.

Correctness. We conclude by proving correctness of the
construction. If P has a solution, then it is straightforward to
extract a run from : (a) each 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,
 does not perform any operation on this counter or performs
“z2y”. But if the values of y and z
are equal to zero, then z will remain equal to zero after such
an update.

Conversely, suppose there is a reachability witness (from 0⃗ to
0⃗). We claim that the initialization of counters 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 z within the squaring macro. Indeed, all other counters
never change their values afterwards. However, counter z is
updated by “z2y”. If y is non zero, then
this will be detected by the zero-test on y. Otherwise, the
update “z2y” never changes the value of z
as required.




§ CONCLUSION
 

We have shown that the reachability problem for afmp--VASS reduces
to the reachability problem for -VASS,  every afmp--VASS
 can be simulated by a -VASS of size polynomial in ||,
|[]| and []. In particular, this allowed
us to establish that the reachability relation of any afmp--VASS
is semilinear.

For all nonnegative classes and consequently for all of the variants
we studied — reset, permutation, transfer, copy and copyless
-VASS — |[]| and [] 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 _
holds for any class of afmp--VASS over ^d × d. We are
aware that an exponential upper bound holds when _ is
generated by a single matrix <cit.>; and when _ is a
group then we have an exponential bound but only on |_|
(see <cit.> 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.


alpha


