Reachability and Related Problems in Vector Addition Systems with Nested Zero Tests

TL;DR

This paper establishes an Ackermannian upper bound for the reachability problem in vector addition systems with nested zero tests, and introduces a unified approach for related problems like semilinearity and separability.

Contribution

It provides the first known Ackermannian complexity bound for VASS with nested zero tests and a unified method to decide related problems.

Findings

Ackermannian upper bound for reachability in VASS with nested zero tests

Unified approach for semilinearity and separability problems

Complexity results for problems previously unknown for plain VASS

Abstract

Vector addition systems with states (VASS), also known as Petri nets, are a popular model of concurrent systems. Many problems from many areas reduce to the reachability problem for VASS, which consists of deciding whether a target configuration of a VASS is reachable from a given initial configuration. In this paper, we obtain an Ackermannian (primitive-recursive in fixed dimension) upper bound for the reachability problem in VASS with nested zero tests. Furthermore, we provide a uniform approach which also allows to decide most related problems, for example semilinearity and separability, in the same complexity. For some of these problems like semilinearity the complexity was unknown even for plain VASS.