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.
翻译:各州( VASS) 的矢量加增系统被广泛用于正式核查并行系统( VASS ) 。 由于其巨大的计算复杂性, 实用的方法依赖了可变性放松等技术, 例如允许负中间反值。 自然地会质疑这些技术对VASS的可行性, 以原始物质浓缩, 通常转化成不可变异性。 受到这一关切的刺激, 我们点出与任意类类的松动操作相关的整变放松的复杂程度。 更具体地说, 我们提供了一个关于VASS 的可完全可达性复杂性的三重体裁法, 并配有折叠式操作( ficine VASS ) 。 也就是说, 我们显示VASS 与 Reset、 PSPACE 和 VASS 完全、 PSPACE 完全和 VASS 具有( 假的) 和 不可变异性( 假的) 。 我们进一步提出在 松动型操作操作中标准可达性区分: VAS 是VASS 的完整和统一复杂度的复杂度, 我们也考虑在级中选择性地展示了一个固定的可达定式的变式变式变式的变式变式的变式的变式的变式的变形变式。