Paper Info
Title
The Complexity of Reachability in Affine Vector Addition Systems with States
Abstract
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 for negative intermediate counter values. It is natural to question their feasibility for VASS enriched with primitives that typically translate into undecidability. Spurred by this concern, we pinpoint the complexity of integer relaxations w.r.t. arbitrary classes of affine operations. More specifically, we provide a trichotomy on the complexity of integer reachability in VASS extended with affine operations (affine VASS). Namely, we show that it is NP-complete for VASS with resets, PSPACE-complete for VASS with (pseudo-)transfers and VASS with (pseudo-)copies, and undecidable for any other class. We further present a dichotomy for standard reachability in affine VASS: it is decidable for VASS with permutations, and undecidable for any other class. This yields a complete and unified complexity landscape of reachability in affine VASS.
Year
DOI
Venue
2020
10.1145/3373718.3394741
LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science Saarbrücken Germany July, 2020
Keywords
DocType
ISSN
vector addition system, affine transformation, reachability, computational complexity
Conference
1043-6871
ISBN
Citations 
PageRank 
978-1-4503-7104-9
0
0.34
References 
Authors
0
2
Name
Order
Citations
PageRank
Michael Blondin1279.06
Raskin Mikhail200.34