Integer Vector Addition Systems with States
Christoph Haase, Simon Halfon

TL;DR
This paper analyzes the computational complexity of reachability, coverability, and inclusion problems in Integer Vector Addition Systems with States (ZVASS), revealing that certain extensions preserve NP-completeness.
Contribution
It provides the first detailed complexity analysis of ZVASS and shows that adding reset operations does not increase complexity to undecidable levels.
Findings
Reachability in ZVASS is NP-complete.
Adding resets to ZVASS retains NP-completeness.
Resets in VASS lead to undecidability, but not in ZVASS.
Abstract
This paper studies reachability, coverability and inclusion problems for Integer Vector Addition Systems with States (ZVASS) and extensions and restrictions thereof. A ZVASS comprises a finite-state controller with a finite number of counters ranging over the integers. Although it is folklore that reachability in ZVASS 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 undecidability and Ackermann-hardness of reachability and coverability, respectively, they can be added to ZVASS while retaining NP-completness of both coverability and reachability.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
