发表机构
The University of Warsaw（华沙大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文通过引入转移图的坏顶点概念，证明单转移VASS的整数可达性复杂度介于NP与PSPACE之间，坏顶点数决定其精确复杂度。该方法隔离了导致复杂度上升的关键结构特征。
AI 中文摘要
对于带状态的向量加法系统（VASS），整数可达性是NP完全的，但在存在转移操作时变为PSPACE完全。我们通过识别导致复杂度增加的转移的结构特征，细化了单转移VASS的这一复杂度差距。每个系统诱导一个转移图，其顶点为计数器，边表示可能的转移。我们根据其可达子图的分支和循环结构，将顶点分为好顶点和坏顶点。设$b$为坏顶点数。我们证明每个正实例都承认一个大小为$|I|^{O(b+1)}$的多项式可验证证书，其中$|I|$为输入大小。因此，单转移VASS的整数可达性可在非确定性时间$|I|^{O(b+1)}$内判定；特别地，对于任何坏计数器数量有界的类，它属于NP。反之，我们证明坏计数器提供了足够的结构能力来编码空间有界计算。对于每个具有$b$个坏顶点的转移图，我们构造一个单转移VASS，它使用$b^{O(1)}$个磁带单元编码图灵机的接受。这为每个包含线性多个坏顶点的多项式时间可构造转移图族产生PSPACE困难性。我们的结果隔离了导致整数可达性复杂度的转移模式。
英文摘要
Integer reachability is NP-complete for vector addition systems with states (VASS), but becomes PSPACE-complete in the presence of transfer operations. We refine this complexity gap for single-transfer VASS by identifying structural features of transfers responsible for the increase in complexity. Each system induces a transfer graph whose vertices are counters and whose edges represent possible transfers. We classify its vertices as good or bad, according to the branching and cyclic structure of their reachable subgraphs. Let $b$ be the number of bad vertices. We show that every positive instance admits a polynomially verifiable certificate of size $|I|^{O(b+1)}$, where $|I|$ is the input size. Consequently, integer reachability for single-transfer VASS can be decided in nondeterministic time $|I|^{O(b+1)}$; in particular, it belongs to NP for every class with a bounded number of bad counters. Conversely, we show that bad counters provide sufficient structural power to encode space-bounded computation. For every transfer graph with $b$ bad vertices, we construct a single-transfer VASS that encodes the acceptance of a Turing machine using $b^{O(1)}$ tape cells. This yields PSPACE-hardness for every polynomial-time constructible family of transfer graphs containing linearly many bad vertices. Our results isolate the transfer patterns responsible for the complexity of integer reachability.
CommentsFull version of the paper accepted at FSTTCS 2026
