4 Integer Vector Addition Systems with States
Christoph Haase, Simon Halfon · 2015
Abstract. This paper studies reachability, coverability and inclusion problems for Integer Vector Addition Systems with States (Z-VASS) and extensions and restrictions thereof. A Z-VASS comprises a finite-state controller with a finite number of counters ranging over the integers. Al-though it is folklore that reachability in Z-VASS is NP-complete, it turns out that despite their naturalness, from a complexity point of view this class has received little attention in the literature. We fill this gap by providing an in-depth analysis of the computational complexity of the aforementioned decision problems. Most interestingly, it turns out that while the addition of reset operations to ordinary VASS leads to undecid-ability and Ackermann-hardness of reachability and coverability, respec-tively, they can be added to Z-VASS while retaining NP-completeness of both coverability and reachability. 1