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.
Affine Extensions of Integer Vector Addition Systems with States