Vector Addition Systems Reachability Problem (A Simpler Solution)
Vector Addition Systems Reachability Problem (A Simpler Solution)
复制标题
矢量加法系统可达性问题（更简单的解决方案）
DOI：
10.29007/bnx2
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Jérôme Leroux
中科院分区：
文献类型：
--
作者：
Jérôme Leroux
矢量加法系统（VASs）的可达性问题是网络理论的核心问题。一般问题已知可由基于经典kosaraju - lambert - mayer - sacerdote - tenney分解（KLMTS分解）的算法确定。最近，从这个分解中，我们推导出当且仅当存在包含初始位形而不包含最终位形的Presburger归纳不变量时，最终位形不能从初始位形到达。由于我们可以确定Preburger公式是否表示归纳不变量，因此我们从这个结果推导出在Preburger算法中存在不可达性的可检查证明。特别地，存在一种基于两种半算法确定一般VAS可达性问题的简单算法。第一个试图通过列举有限的行为序列来证明可达性第二个试图通过列举普雷斯伯格公式来证明不可达性。在最近的另一篇论文中，我们提供了不基于KLMST分解的VAS可达性问题的第一个证明。该证明基于生产关系的概念，直接证明了Presburger归纳不变量的存在性。在本文中，我们提出了新的中间结果，极大地简化了最后一个证明。
The reachability problem for Vector Addition Systems (VASs) is a central problem of net theory. The general problem is known to be decidable by algorithms based on the classical Kosaraju-Lambert-Mayr-Sacerdote-Tenney decomposition (KLMTS decomposition). Recently from this decomposition, we deduced that a final configuration is not reachable from an initial one if and only if there exists a Presburger inductive invariant that contains the initial configuration but not the final one. Since we can decide if a Preburger formula denotes an inductive invariant, we deduce from this result that there exist checkable certificates of non-reachability in the Presburger arithmetic. In particular, there exists a simple algorithm for deciding the general VAS reachability problem based on two semi-algorithms. A first one that tries to prove the reachability by enumerating finite sequences of actions and a second one that tries to prove the non-reachability by enumerating Presburger formulas. In another recent paper we provided the first proof of the VAS reachability problem that is not based on the KLMST decomposition. The proof is based on the notion of production relations that directly proves the existence of Presburger inductive invariants. In this paper we propose new intermediate results that dramatically simplify this last proof.