×

On the efficient computation of the minimal coverability set for Petri nets. (English) Zbl 1141.68507

Namjoshi, Kedar S. (ed.) et al., Automated technology for verification and analysis. 5th international symposium, ATVA 2007 Tokyo, Japan, October 22–25, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-75595-1/pbk). Lecture Notes in Computer Science 4762, 98-113 (2007).
Summary: The minimal 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. 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, which has been introduced 15 years ago, and implemented since then in several tools such as Pep. 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.
For the entire collection see [Zbl 1138.68006].

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Finkel, A.; Rozenberg, G., The minimal coverability graph for Petri nets, Advances in Petri Nets 1993, 210-243 (1993), Heidelberg: Springer, Heidelberg
[2] Finkel, A., Geeraerts, G., Raskin, J.F., Van Begin, L.: A counter-example to the minimal coverability tree algorithm. Technical Report 535, Université Libre de Bruxelles (2005) · Zbl 1272.68302
[3] Geeraerts, G.: Coverability and Expressiveness Properties of Well-structured Transition Systems. PhD thesis, Université Libre de Bruxelles, Belgium (2007)
[4] Geeraerts, G., Raskin, J.F., Van Begin, L.: Well-structured languages. Act. Inf. 44(3-4) · Zbl 1119.68105
[5] Geeraerts, G., Raskin, J.F., Van Begin, L.: On the efficient computation of the minimal coverability set for Petri nets. Technical Report CFV 2007.81 · Zbl 1141.68507
[6] German, S., Sistla, A.: Reasoning about Systems with Many Processes. J. ACM 39(3) (1992) · Zbl 0799.68078
[7] Grahlmann, B.; Grumberg, O., The PEP tool, CAV 1997, 440-443 (1997), Heidelberg: Springer, Heidelberg
[8] Karp, R. M.; Miller, R. E., Parallel Program Schemata, JCSS, 3, 147-195 (1969) · Zbl 0198.32603
[9] Luttge, K.: Zustandsgraphen von Petri-Netzen. Master’s thesis, Humboldt-Universität (1995)
[10] Reisig, W., Petri Nets. An introduction (1986), Heidelberg: Springer, Heidelberg
[11] Starke, P.: Personal communication
[12] Van Begin, L.: Efficient Verification of Counting Abstractions for Parametric systems. PhD thesis, Université Libre de Bruxelles, Belgium (2003)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.