向量加法系统可达性的三步证明
计算机科学中的逻辑
2020-05-28 v3
摘要
本笔记是对向量加法系统带状态（VASS）可达性问题的可判定性著名证明的梳理，该证明最初由 Mayr 于 1981 年建立，随后由 Kosaraju 于 1982 年简化。本笔记既非严格形式化也非完备；其旨在对证明中所用主要概念给出直观但足够精确的描述。粗略而言，总体思想是给出一个关于 VASS 的可判定条件 Theta，使得 Theta 蕴含可达性，而其否定蕴含 VASS 的规模可被约简。凭借这两个性质，输入的规模可逐步减小直至问题变得平凡。我们分三步进行：首先为朴素 VASS 表述条件 Theta，然后将其适配到具有无约束坐标的更一般 VASS，最后适配到 Kosaraju 的广义 VASS。
引用
@article{arxiv.1812.11966,
title = {VASS reachability in three steps},
author = {Sławomir Lasota},
journal= {arXiv preprint arXiv:1812.11966},
year = {2020}
}