Stubborn versus structural reductions for Petri nets

Frederik M. Bønneland, Jakob Dyhr, Peter G. Jensen, Mads Johannsen, Jiří Srba

Research output: Contribution to journalJournal articleResearchpeer-review

9 Citations (Scopus)
52 Downloads (Pure)

Abstract

Partial order and structural reduction techniques are some of the most beneficial
methods for state space reduction in reachability analysis of Petri nets. This
is among others documented by the fact that these techniques are used by the
leading tools in the annual Model Checking Contest (MCC) of Petri net tools.
We suggest improved versions of a partial order reduction based on stubborn
sets and of a structural reduction with additional new reduction rules, and we
extend both methods for the application on Petri nets with weighted arcs and
weighted inhibitor arcs. All algorithms are implemented in the open-source
verification tool TAPAAL and evaluated on a large benchmark of Petri net
models from MCC’17, including a comparison with the tool LoLA (the last
year winner of the competition). The experiments document that both methods
provide significant state space reductions and, even more importantly, that their
combination is indeed beneficial as a further nontrivial state space reduction can
be achieved.
Original languageEnglish
JournalJournal of Logic and Algebraic Programming
Volume102
Pages (from-to)46-63
Number of pages18
ISSN2352-2208
DOIs
Publication statusPublished - 2019

Fingerprint

Dive into the research topics of 'Stubborn versus structural reductions for Petri nets'. Together they form a unique fingerprint.

Cite this