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

Issue title: Applications and Theory of Petri Nets and Other Models of Concurrency, 2011

Article type: Research Article

Authors: Reynier, Pierre-Alain | Servais, Frédéric

Affiliations: Aix-Marseille Université, CNRS, LIF, UMR 7279, Marseille, France. [email protected] | Hasselt University and Transnational University of Limburg, Belgium. [email protected]

Note: [] This work has been partly supported by the project ECSPER funded by the french agency for research (ANR-09-JCJC-0069). Address for correspondence: Pierre-Alain Reynier, LIF, 163 avenue de Luminy - Case 901, 13288 Marseille Cedex 9, France.

Abstract: 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.

DOI: 10.3233/FI-2013-781

Journal: Fundamenta Informaticae, vol. 122, no. 1-2, pp. 1-30, 2013