Tampere University of Technology

TUTCRIS Research Portal

Constructing Minimal Coverability Sets

Research output: Contribution to journalArticleScientificpeer-review


Original languageEnglish
Pages (from-to)393-414
Number of pages22
JournalFundamenta Informaticae
Issue number3-4
Publication statusPublished - 4 Mar 2016
Publication typeA1 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.


  • antichain data structure, coverability set, Tarjan's algorithm

Publication forum classification

Field of science, Statistics Finland

Downloads statistics

No data available