Minimal Coverability Set for Petri Nets: Karp and Miller Algorithm with Pruning

• Autorzy: Reynier P-A. , Servais F.
• Języki publikacji: EN

Abstrakty

EN

This paper presents the Monotone-Pruning algorithm (MP) for computing the minimal coverability set of Petri nets. The original Karp and Miller algorithm (K&M) unfolds the reachability graph of a Petri net and uses acceleration on branches to ensure termination. The MP algorithm improves the K&M algorithm by adding pruning between branches of the K&M tree. This idea was first introduced in the Minimal Coverability Tree algorithm (MCT), however it was recently shown to be incomplete. The MP algorithm can be viewed as the MCT algorithm with a slightly more aggressive pruning strategy which ensures completeness. Experimental results show that this algorithm is a strong improvement over the K&M algorithm as it dramatically reduces the exploration tree.

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2013
• Tom: Vol. 122, nr 1-2
• Strony: 1--30
• Opis fizyczny: Bibliogr. 10 poz., tab., wykr.

Twórcy

autor

Reynier P-A.

• Aix-Marseille Universite, CNRS, LIF, UMR 7279, Marseille, France

autor

Servais F.

• Hasselt University and Transnational University of Limburg, Belgium

Bibliografia

• [1] A. Finkel. A generalization of the procedure of Karp and Miller to well structured transition system. In Proc.ICALP’87, volume 267 of LNCS, pages 499–508. Springer, 1987.
• [2] A. Finkel. The minimal coverability graph for Petri nets. In Proc. ICATPN’91, volume 674 of LNCS, pages210–243. Springer, 1993.
• [3] A. Finkel and J. Goubault-Larrecq. Forward analysis for WSTS, part I: Completions. In Proc. STACS’09,volume 3 of LIPIcs, pages 433–444. Leibniz-Zentrum für Informatik, 2009.
• [4] A. Finkel and J. Goubault-Larrecq. Forward analysis for WSTS, part II: Complete WSTS. In Proc. ICALP’09,volume 5556 of LNCS, pages 188–199. Springer, 2009.
• [5] A. Finkel, J.-F. Raskin, M. Samuelides, and L. V. Begin. Monotonic extensions of Petri nets: Forward and backward search revisited. Electr. Notes Theor. Comput. Sci., 68(6), 2002.
• [6] G. Geeraerts. Coverability and Expressiveness Properties of Well-structured Transitions Systems. Thse dedoctorat, Universit Libre de Bruxelles, Belgique, 2007.
• [7] G. Geeraerts, J.-F. Raskin, and L. Van Begin. On the efficient computation of the coverability set for petri nets. International Journal of Foundations of Computer Science, 21(2):135–165, 2010.
• [8] R.M. Karp and R. E. Miller. Parallel program schemata. Journal of Computer and System Sciences, 3(2):147–195, 1969.
• [9] K. Lüttge. Zustandsgraphen von Petri-Netzen. Master’s thesis, Humboldt-Universität, 1995.
• [10] K. Schmidt. Model-checking with coverability graphs. Form. Methods Syst. Des., 15(3):239–254, 1999