Reachability and Related Problems in Vector Addition Systems with Nested Zero Tests
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.
Keywords
Cite
@article{arxiv.2502.07660,
title = {Reachability and Related Problems in Vector Addition Systems with Nested Zero Tests},
author = {Roland Guttenberg and Wojciech Czerwiński and Sławomir Lasota},
journal= {arXiv preprint arXiv:2502.07660},
year = {2025}
}
Comments
25 pages, 5 figures, full version of paper at LICS 2025