简单带状态向量添加系统可达性可判定性的边界
摘要
向量添加系统带状态 (VASS)，等价于铺底网，是一种众所周有的并发模型。VASS中的核心算法挑战是可达性问题：从给定的起始状态和计数器值是否存在一条路径到达给定的目标状态和计数器值？当输入以二进制编码时，可达性计算不可判定：即使在维度为1的情况下，也已知是NP-hard。本文全面刻画了当输入以一元编码时，该问题可判定性的边界。对于我们的主要结果，我们证明即使在结构受到严格限制为简单线性路径方案 (simple linear path scheme) 的情况下，3-VASS的可达性仍然是NP-hard。这一结果不仅改进了Czerwiński 和 Orlikowski (2022) 最近的成果，还涵盖了计数器数量和所考虑模型的表达性，同时解答了Englert, Lazić 和 Totzke (2016) 以及 Leroux (2021) 的开放问题。简单线性路径方案 (SLPS) 的底层图结构仅是一个在每个节点上都有自环的路径。我们也研究了计算能力极其弱的模型，即在计数器更新为{-1,0,+1}的SLPS (SPLS)。在此情况下，我们展示当维度受限于O(α(k)) 时（其中α为反阿克曼函数，k限制SLPS的大小），可达性是NP-hard。我们补充了这一结果，通过提出一个在2-SLPS中当初始配置和目标配置以二进制指定时即可决定可达性的多项式时间算法。为此，我们展示在此类情形下，可达性是良好结构化的：除了可能的最多常数个循环之外，所有循环要么被采纳多次，要么几乎被最大限度地采纳。这一结果扩展了Englert, Lazić 和 Totzke (2016) 表明当初始配置和目标配置以一元编码指定时，该问题在NL中可判定的主要结果。
引用
@article{arxiv.2412.16612,
title = {The Tractability Border of Reachability in Simple Vector Addition Systems with States},
author = {Dmitry Chistikov and Wojciech Czerwiński and Filip Mazowiecki and Łukasz Orlikowski and Henry Sinclair-Banks and Karol Węgrzycki},
journal= {arXiv preprint arXiv:2412.16612},
year = {2024}
}
备注
Full version of FOCS'24 paper. 60 pages, 16 figures