Affiliations: Department of Mathematics, Tampere University of Technology, P.O. Box 553, FI-33101 Tampere, Finland. [email protected], [email protected]
Correspondence:
[*]
Address for correspondence: Department of Mathematics, Tampere University of Technology, P.O. Box 553, FI-33101 Tampere, Finland
Abstract: This publication addresses two bottlenecks in the construction of minimal coverability sets of Petri nets: the detection of situations where the marking of a place can be converted to ω, and the manipulation of the set A of maximal ω-markings that have been found so far. For the former, a technique is presented that consumes very little time in addition to what maintaining A consumes. It is based on Tarjan’s algorithm for detecting maximal strongly connected components of a directed graph. For the latter, a data structure is introduced that resembles BDDs and Covering Sharing Trees, but has additional heuristics designed for the present use. Results from a few experiments are shown. They demonstrate significant savings in running time and varying savings in memory consumption compared to an earlier state-of-the-art technique.
Keywords: coverability set, Tarjan’s algorithm, antichain data structure
