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

Abstract:This paper presents the Monotone-Pruning algorithm (MP) for computing the minimal coverability set of Petri nets. The original Karp and Miller algorithm (KM) unfolds the reachability graph of a Petri net and uses acceleration on branches to ensure termination. The MP algorithm improves the KM algorithm by adding pruning between branches of the 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 KM algorithm as it dramatically reduces the exploration tree.

Publication year:2013

Keywords:Petri net, concurrency, Applied mathematics, Computer science/information technology

BOF-keylabel:yes

IOF-keylabel:yes

BOF-publication weight:0.5

CSS-citation score:1

Authors:International

Authors from:Higher Education

Accessibility:Closed

Review status:Peer-reviewed