The General Vector Addition System Reachability Problem by Presburger Inductive Invariants
The General Vector Addition System Reachability Problem by Presburger Inductive Invariants
复制标题
Presburger归纳不变量的一般向量加法系统可达性问题
DOI：
10.2168/lmcs-6(3:22)2010
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Jérôme Leroux
中科院分区：
文献类型：
--
作者：
Jérôme Leroux
矢量加法系统（VASs）的可达性问题是网络理论的核心问题。一般问题已知可由完全基于经典kosaraju - lambert - mayer - sacerdote - tenney分解的算法来决定。本文利用这种分解证明了VASs接受的语言的Parikh象是半伪线性的；一类扩展了半线性集合，即在普雷斯伯格算术中可定义的集合。我们给出了这一结果的一个应用；证明当且仅当存在一个表示包含初始位形而不包含最终位形的前向归纳不变量的Presburger公式时，最终位形不能从初始位形到达。由于我们可以确定Preburger公式是否表示归纳不变量，因此我们推导出存在不可达性的可检查证明。特别地，存在一种基于两种半算法确定一般VAS可达性问题的简单算法。第一个试图通过列举有限的行为序列来证明可达性第二个试图通过列举普雷斯伯格公式来证明不可达性。
The reachability problem for Vector Addition Systems (VASs) is a central problem of net theory. The general problem is known decidable by algorithms exclusively based on the classical Kosaraju-Lambert-Mayr-Sacerdote-Tenney decomposition. This decomposition is used in this paper to prove that the Parikh images of languages accepted by VASs are semi-pseudo-linear; a class that extends the semi-linear sets, a.k.a. the sets definable in the Presburger arithmetic. We provide an application of this result; we prove that a final configuration is not reachable from an initial one if and only if there exists a Presburger formula denoting a forward 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 that there exist checkable certificates of non-reachability. 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.