Acceleration for Petri Nets
Acceleration for Petri Nets
复制标题
Petri 网的加速
DOI：
10.1007/978-3-319-02444-8_1
复制
发表时间：
2013
影响因子：
0.4
通讯作者：
Jérôme Leroux
中科院分区：
文献类型：
--
作者：
Jérôme Leroux
Petri网的可达性问题是网理论的核心问题。这个问题被认为是可判定的归纳不变量中定义的Presburger算法。当可达集在Presburger算法中是可定义的，这样的归纳不变量的存在是立即的。然而，在这种情况下，表示可达集的Presburger公式的计算是一个开放的问题。最近，这个问题得到关闭，通过证明，如果可达集的Petri网是可定义的Presburger算法，那么Petri网是平坦的，即它的可达集可以得到运行标记的字在一个有界的语言。作为一个直接的后果，经典算法的基础上加速技术有效地计算公式的Presburger算术表示的可达性集。
The reachability problem for Petri nets is a central problem of net theory. The problem is known to be decidable by inductive invariants definable in the Presburger arithmetic. When the reachability set is definable in the Presburger arithmetic, the existence of such an inductive invariant is immediate. However, in this case, the computation of a Presburger formula denoting the reachability set is an open problem. Recently this problem got closed by proving that if the reachability set of a Petri net is definable in the Presburger arithmetic, then the Petri net is flat, i.e. its reachability set can be obtained by runs labeled by words in a bounded language. As a direct consequence, classical algorithms based on acceleration techniques effectively compute a formula in the Presburger arithmetic denoting the reachability set.