Minimal Coverability Set of Petri Nets

This page presents the prototype of the implementation of the Monotone-Pruning algorithm, proposed by Frédéric Servais and I, for computing the minimal coverability set of Petri nets. The prototype has been written by Frédéric Servais.

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 KM 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.

Downloads/Links:

• Paper presented at Petri Nets'11.
• Archive containing the code of our prototype (written in Python), with Readme and examples.
• Models considered have been taken from there.

README:
To launch the tests, simply run:
> python tests.py