Constructing Minimal Coverability Sets
Research output: Contribution to journal › Article › Scientific › peer-review
|Number of pages||22|
|Publication status||Published - 4 Mar 2016|
|Publication type||A1 Journal article-refereed|
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.
ASJC Scopus subject areas
- antichain data structure, coverability set, Tarjan's algorithm