带状态的仿射向量加法系统的可达性复杂度
计算机科学中的逻辑
2023-06-22 v5 计算复杂性
形式语言与自动机理论
摘要
带状态的向量加法系统（VASS）被广泛用于并发系统的形式化验证。鉴于其巨大的计算复杂度，实用方法依赖于可达性松弛等技术，例如允许中间计数器取负值。人们自然会质疑，对于增添了通常导致不可判定性的原语的VASS，这些技术的可行性。受此关切推动，我们明确了针对任意仿射运算类的整数松弛的复杂度。更具体地，我们对扩展了仿射运算（仿射VASS）的VASS中整数可达性的复杂度给出了三分法。即，我们表明：对于带复位的VASS为NP完全；对于带（伪）转移和带（伪）拷贝的VASS为PSPACE完全；而对于任何其他类则不可判定。我们进一步给出了仿射VASS中标准可达性的二分法：对于带置换的VASS可判定，而对于任何其他类不可判定。这给出了仿射VASS可达性完整且统一的复杂度图景。我们还考虑了由固定仿射VASS而非一个类参数化的可达性问题，并表明在此设定下复杂度图景是任意的。
引用
@article{arxiv.1909.02579,
title = {The Complexity of Reachability in Affine Vector Addition Systems with States},
author = {Michael Blondin and Mikhail Raskin},
journal= {arXiv preprint arXiv:1909.02579},
year = {2023}
}