The Complexity of Reachability in Affine Vector Addition Systems with States

摘要: Vector addition systems with states (VASS) are widely used for the formal verification of concurrent systems. Given their tremendous computational complexity, practical approaches have relied on techniques such as reachability relaxations, e.g., allowing negative intermediate counter values. It is natural to question feasibility VASS enriched primitives that typically translate into undecidability. Spurred by this concern, we pinpoint complexity integer relaxations w.r.t. arbitrary classes affine operations. More specifically, provide a trichotomy in extended operations (affine VASS). Namely, show it NP-complete resets, PSPACE-complete (pseudo-)transfers and (pseudo-)copies, undecidable any other class. We further present dichotomy standard VASS: decidable permutations, This yields complete unified landscape VASS.