向量加法系统的可达性在固定维下为原始递归
计算机科学中的逻辑
2019-08-20 v1
摘要
向量加法系统中的可达性问题是核心问题，不仅对于这些系统的静态验证，也对于各领域中出现的许多可相互归约的决策问题。该问题目前已知的最佳上界并非原始递归的，即便考虑固定维系统亦然。我们对 Mayr、Kosaraju 与 Lambert 的经典分解算法及其终止性证明给出了显著改进，从而在一般情形下得到 ACKERMANN 上界，在固定维下得到原始递归上界。虽然这不与当前已知的可达性 TOWER 下界匹配，但对于相关问题而言是最优的。
引用
@article{arxiv.1903.08575,
title = {Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension},
author = {Jérôme Leroux and Sylvain Schmitz},
journal= {arXiv preprint arXiv:1903.08575},
year = {2019}
}