Integer Vector Addition Systems with States

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.