On the Efficient Computation of the Minimal Coverability Set for Petri Nets
On the Efficient Computation of the Minimal Coverability Set for Petri Nets
复制标题
关于Petri网最小覆盖集的高效计算
DOI：
10.1007/978-3-540-75596-8_9
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
L. V. Begin
中科院分区：
文献类型：
--
作者：
G. Geeraerts;Jean;L. V. Begin
Petri网的极小可覆盖集（MCS）是其可达标记的下闭包的有限表示。最小可覆盖集允许决定几个重要的问题，如可覆盖性，半活性，位置有界性等。计算MCS的经典算法构建了Karp&米勒树[8]。不幸的是，K&M树通常很大，即使对于小网也是如此。该K&M算法的改进是最小覆盖树（MCT）算法[1]，该算法已在15年前引入，并从那时起在Pep [7]等几个工具中实现。不幸的是，我们在本文中表明，MCT是有缺陷的：它可能会计算可达标记的下近似。我们提出了一个新的解决方案的有效计算的MCS的Petri网。实验结果表明，该算法在实际应用中比K&M算法有更好的性能。
Theminimal coverability set(MCS) of a Petri net is a finite representation of the downward-closure of its reachable markings. The minimal coverability set allows to decide several important problems like coverability, semi-liveness, place boundedness, etc. The classical algorithm to compute the MCS constructs the Karp&Miller tree [8]. Unfortunately the K&M tree is often huge, even for small nets. An improvement of this K&M algorithm is the Minimal Coverability Tree (MCT) algorithm [1], which has been introduced 15 years ago, and implemented since then in several tools such as Pep [7]. Unfortunately, we show in this paper that the MCT is flawed: it might compute an under-approximation of the reachable markings. We propose a new solution for the efficient computation of the MCS of Petri nets. Our experimental results show that this new algorithm behaves much better in practice than the K&M algorithm.