Czasopismo
2013
|
Vol. 122, nr 1-2
|
1--30
Tytuł artykułu
Autorzy
Wybrane pełne teksty z tego czasopisma
Warianty tytułu
Języki publikacji
Abstrakty
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.
Słowa kluczowe
Czasopismo
Rocznik
Tom
Strony
1--30
Opis fizyczny
Bibliogr. 10 poz., tab., wykr.
Twórcy
autor
- Aix-Marseille Universite, CNRS, LIF, UMR 7279, Marseille, France, pierre-alain.reynier@lif.univ-mrs.fr
autor
- Hasselt University and Transnational University of Limburg, Belgium, frederic.servais@uhasselt.be
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
Typ dokumentu
Bibliografia
Identyfikatory
Identyfikator YADDA
bwmeta1.element.baztech-64c26e8c-5f33-4d83-84d8-33dd7b8a562b