向量加法系统可达性揭秘
计算机科学中的逻辑
2015-08-11 v2
摘要
在向量加法系统（VAS）提出三十多年后，其可达性可判定性证明仍笼罩在诸多神秘之中。这些证明关键依赖于由 Mayr、Kosaraju 和 Lambert 逐步精炼的运行分解，该分解看似相当神奇，且已知无复杂度上界。我们首先为这一分解技术提供合理性证明，表明它利用运行间自然嵌入关系以及拟序，计算了运行集合的理想分解。在第二部分，我们应用近期关于终止复杂度的结果（得益于良拟序与良序）得到了分解算法的三次 Ackermann 上界，从而给出了通用 VAS 可达性的首个已知上界。
引用
@article{arxiv.1503.00745,
title = {Demystifying Reachability in Vector Addition Systems},
author = {Jérôme Leroux and Sylvain Schmitz},
journal= {arXiv preprint arXiv:1503.00745},
year = {2015}
}
备注
To appear in the Proceedings of LICS 2015