Stubborn versus structural reductions for Petri nets

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

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

Resumé

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.
OriginalsprogEngelsk
TidsskriftJournal of Logical and Algebraic Methods in Programming
Vol/bind102
Sider (fra-til)46-63
Antal sider18
ISSN2352-2208
DOI
StatusUdgivet - 2019

Emneord

  • Partial order reduction
  • Stubborn sets
  • Structural reductions
  • Reachability analysis
  • Petri nets

Citer dette

@article{b197c103d5cf46d2976a0d79ac5913c3,
title = "Stubborn versus structural reductions for Petri nets",
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.",
keywords = "Partial order reduction, Stubborn sets, Structural reductions, Reachability analysis, Petri nets",
author = "B{\o}nneland, {Frederik M.} and Jakob Dyhr and Jensen, {Peter G.} and Mads Johannsen and Jiř{\'i} Srba",
year = "2019",
doi = "10.1016/j.jlamp.2018.09.002",
language = "English",
volume = "102",
pages = "46--63",
journal = "Journal of Logical and Algebraic Methods in Programming",
issn = "2352-2208",
publisher = "Elsevier",

}

Stubborn versus structural reductions for Petri nets. / Bønneland, Frederik M.; Dyhr, Jakob; Jensen, Peter G.; Johannsen, Mads; Srba, Jiří.

I: Journal of Logical and Algebraic Methods in Programming, Bind 102, 2019, s. 46-63.

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

TY - JOUR

T1 - Stubborn versus structural reductions for Petri nets

AU - Bønneland, Frederik M.

AU - Dyhr, Jakob

AU - Jensen, Peter G.

AU - Johannsen, Mads

AU - Srba, Jiří

PY - 2019

Y1 - 2019

N2 - 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.

AB - 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.

KW - Partial order reduction

KW - Stubborn sets

KW - Structural reductions

KW - Reachability analysis

KW - Petri nets

U2 - 10.1016/j.jlamp.2018.09.002

DO - 10.1016/j.jlamp.2018.09.002

M3 - Journal article

VL - 102

SP - 46

EP - 63

JO - Journal of Logical and Algebraic Methods in Programming

JF - Journal of Logical and Algebraic Methods in Programming

SN - 2352-2208

ER -