一句话：给出了仿射 VASS 整数可达性的复杂度三分律及标准可达性的二分律，形成统一复杂度图景。
向量加法系统（VASS）广泛用于并发系统形式验证，但其复杂度极高，实践常采用允许中间计数值为负等可达性松弛。本文研究在 VASS 上加入通常导致不可判定的仿射操作后，整数松弛可达性是否仍可行。作者针对任意仿射操作类给出复杂度三分律：带 reset 时 NP 完全，带 (pseudo-)transfer 或 (pseudo-)copy 时 PSPACE 完全，其他类不可判定；同时对标准可达性给出二分律：带 permutation 可判定，其他类不可判定。此外，固定仿射 VASS 的参数化复杂度图景可以是任意的。这些结果完整统一了仿射 VASS 可达性的复杂度分类。
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 with respect to 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. We also consider the reachability problem parameterized by a fixed affine VASS, rather than a class, and we show that the complexity landscape is arbitrary in this setting.
@article{paperbot1299,
title = {The Complexity of Reachability in Affine Vector Addition Systems with States},
author = {Michael Blondin and Mikhail Raskin},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 3},
year = {2021},
doi = {10.46298/lmcs-17(3:3)2021}
}