Demystifying Reachability in Vector Addition Systems
Demystifying Reachability in Vector Addition Systems
复制标题
揭秘矢量加法系统的可达性
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
S. Schmitz
中科院分区：
文献类型：
--
作者：
Jérôme Leroux;S. Schmitz
在其成立30多年后，向量加法系统（VAS）中可达能力的可判定性证明仍然保留着许多神秘之处。这些证明依赖于一个关键的分解运行先后完善迈尔，Kjuaju，和兰伯特，这似乎是相当神奇的，并没有复杂性上限是已知的。我们首先提供了一个理由，这种分解技术，通过显示，它计算的理想分解的运行集，使用运行之间的自然嵌入关系以及准序。在第二部分中，我们应用最近的结果终止的复杂性，以及准订单和订单，以获得一个三次阿克曼上界的分解算法，从而提供了第一个已知的上界一般VAS达到能力。
More than 30 years after their inception, the decidability proofs for reach ability in vector addition systems (VAS) still retain much of their mystery. These proofs rely crucially on a decomposition of runs successively refined by Mayr, Kosaraju, and Lambert, which appears rather magical, and for which no complexity upper bound is known. We first offer a justification for this decomposition technique, by showing that it computes the ideal decomposition of the set of runs, using the natural embedding relation between runs as well quasi ordering. In a second part, we apply recent results on the complexity of termination thanks to well quasi orders and well orders to obtain a cubic Ackermann upper bound for the decomposition algorithms, thus providing the first known upper bounds for general VAS reach ability.