Old and New Algorithms for Minimal Coverability Sets

• Autorzy: Valmari A. , Hansen H.

Identyfikatory

DOI

10.3233/FI-2014-1002

• Języki publikacji: EN

Abstrakty

EN

Many algorithms for computing minimal coverability sets for Petri nets prune futures. That is, if a newmarking strictly covers an old one, then not just the old marking but also some subset of its successor markings is discarded from search. In this publication, a simpler algorithm that lacks future pruning is presented and proven correct. Its performance is compared with future pruning. It is demonstrated, using examples, that neither approach is systematically better than the other. However, the simple algorithm has some attractive features. It never needs to re-construct pruned parts of the minimal coverability set. It automatically gives most of the advantage of future pruning, if the minimal coverability set is constructed in depth-first or most tokens first order, and if so-called history merging is applied. Some implementation aspects of minimal coverability set construction are also discussed. Some measurements are given to demonstrate the effect of construction order and other implementation aspects.

Słowa kluczowe

EN

computer algorithms; set theory; Petri nets; search engines; mathematical proofs

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2014
• Tom: Vol. 131, nr 1
• Strony: 1--25
• Opis fizyczny: Bibliogr. 12 poz., rys., tab.

Twórcy

autor

Valmari A.

• Department of Mathematics, Tampere University of Technology, PO Box 553, FI-33101 Tampere, Finland

autor

Hansen H.

• Temasek Laboratories, National University of Singapore, Singapore

Bibliografia

• [1] Delzanno, G., Raskin, J.-F., Van Begin, L.: Covering sharing trees: a compact data structure for parameterized verification, International Journal on Software Tools for Technology Transfer, 5(2-3), 2004, 268–297.
• [2] Finkel, A.: A generalization of the procedure of Karp and Miller to well structured transition systems, in: ICALP 1987, vol. 267 of LNCS, Springer, 1987, 499–508.
• [3] Finkel, A.: The minimal coverability graph for Petri nets, in: Advances in Petri Nets 1993 (G. Rozenberg, Ed.), vol. 674 of LNCS, Springer, 1993, 210–243.
• [4] Finkel, A., Geeraerts, G., Raskin, J.-F., Van Begin, L.: A counter-example to the minimal coverability tree algorithm, Technical Report 535, Universite Libre de Bruxelles, 2005.
• [5] Finkel, A., Goubault-Larrecq, J.: Forward analysis for WSTS, part II: Complete WSTS, in: ICALP 2009, vol. 5556 of LNCS, Springer, 2009, 188–199.
• [6] Finkel, A., Goubault-Larrecq, J., et al.: Forward analysis for WSTS, Part I: Completions, 26th International Symposium on Theoretical Aspects of Computer Science-STACS 2009, 2009.
• [7] Geeraerts, G., Raskin, J.-F., van Begin, L.: On the efficient computation of the minimal coverability set of Petri nets, International Journal of Foundations of Computer Science, 21(2), 2010, 135–165.
• [8] Karp, R., Miller, R.: Parallel program schemata, Journal of Computer and System Sciences, 3(2), 1969, 147–195.
• [9] König, B., Koziura, V.: Incremental construction of coverability graphs, Information Processing Letters, 103(5), 2007, 203–209.
• [10] Piipponen, A., Valmari, A.: Constructing Minimal Coverability Sets, in: Reachability Problems, vol. 8169 of LNCS, Springer, 2013, 183–195.
• [11] Reynier, P.-A., Servais, F.: Minimal Coverability Set for Petri Nets: Karp andMiller Algorithmwith Pruning, in: Petri Nets 2011, vol. 6709 of LNCS, Springer, 2011, 69–88.
• [12] Valmari, A., Hansen, H.: Old and new algorithms for minimal coverability sets, in: Petri Nets 2012, vol. 7347 of LNCS, Springer, 2012, 208–227.