检查 VASS 快速终止的高效算法

带状态向量加法系统（Vector Addition Systems with States, VASS）由一个有限状态空间组成，该空间配备 d 个计数器，其中在每个转换中，每个计数器都会递增、递减或保持不变。VASS 为并发过程和参数化系统的分析提供了基础模型，也被用作程序界限分析的抽象模型。虽然终止性是询问给定模型是否总是终止这一质性问题的基本活性属性，但更一般的量化问题则询问终止所需的步数界限。在量化界限领域，一个基本问题是获得终止时间的渐近界限。诸如指数级或更高的巨大渐近界限通常表明建模中存在某些错误，或者该模型在实践中无用。因此，我们专注于 VASS 的多项式渐近界限。虽然一些知名方法（例如词典序排序函数）对于多项式界限既不完全也不可靠，但其他方法仅提出了用于上界的可靠方法。在本工作中，我们的主要贡献如下：首先，针对线性渐近界限，我们提出了一种针对 VASS 的可靠且完备的方法，此外，我们的算法在多项式时间内运行。其次，我们根据循环向量的法线对 VASS 进行分类。我们表明，法线中的奇点是导致 VASS 出现指数级和非初等渐近界限的关键原因。在没有奇点的情况下，我们证明渐近复杂度界限总是多项式的，形式为 ${\Theta}(n^k)$，其中 k $\leq$ d。我们提出了一种算法，其时间复杂度在 VASS 规模上为多项式，在维度 d 上为指数级，用于计算最优的 k。