Old and New Algorithms for Minimal Coverability Sets

摘要

Many algorithms for computing minimal coverability sets for Petri nets prune futures. That is, if a new marking strictly covers an old one, then not just the old marking but also some subset of its subsequent markings is discarded from search. In this publication, a simpler algorithm that lacks future pruning is presented and proven correct. Then 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. If the minimal coverability set is constructed in depth-first or most tokens first order, and if so-called history merging is applied, then most of the advantage of future pruning is automatic. Some implementation aspects of minimal coverability set construction are also discussed.