Stubborn Versus Structural Reductions for Petri Nets

J 2019

Stubborn Versus Structural Reductions for Petri Nets

BOENNELAND, Frederik M.; Jacob DYHR; Peter G. JENSEN; Mads JOHANNSEN; Jiří SRBA et al.

Základní údaje

Originální název

Stubborn Versus Structural Reductions for Petri Nets

Autoři

BOENNELAND, Frederik M.; Jacob DYHR; Peter G. JENSEN; Mads JOHANNSEN a Jiří SRBA

Vydání

Journal of Logical and Algebraic Methods in Programming, 2019, 2352-2208

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Nizozemské království

Utajení

není předmětem státního či obchodního tajemství

Odkazy

URL

Impakt faktor

Impact factor: 0.685

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/19:00113644

Organizační jednotka

Fakulta informatiky

Klíčová slova anglicky

partial order reduction; structural reduction; model checking

Změněno: 6. 5. 2020 17:13, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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.

Citovat

BOENNELAND, Frederik M.; Jacob DYHR; Peter G. JENSEN; Mads JOHANNSEN a Jiří SRBA. Stubborn Versus Structural Reductions for Petri Nets. Journal of Logical and Algebraic Methods in Programming. 2019, roč. 102, January 2019, s. 46-63. ISSN 2352-2208. Dostupné z: https://doi.org/10.1016/j.jlamp.2018.09.002.

@article{1646350,
   author = {Boenneland, Frederik M. and Dyhr, Jacob and Jensen, Peter G. and Johannsen, Mads and Srba, Jiří},
   article_number = {January 2019},
   doi = {https://doi.org/10.1016/j.jlamp.2018.09.002},
   keywords = {partial order reduction; structural reduction; model checking},
   language = {eng},
   issn = {2352-2208},
   journal = {Journal of Logical and Algebraic Methods in Programming},
   title = {Stubborn Versus Structural Reductions for Petri Nets},
   url = {https://doi.org/10.1016/j.jlamp.2018.09.002},
   volume = {102},
   year = {2019}
}

TY  - JOUR
ID  - 1646350
AU  - Boenneland, Frederik M. - Dyhr, Jacob - Jensen, Peter G. - Johannsen, Mads - Srba, Jiří
PY  - 2019
TI  - Stubborn Versus Structural Reductions for Petri Nets
JF  - Journal of Logical and Algebraic Methods in Programming
VL  - 102
IS  - January 2019
SP  - 46-63
EP  - 46-63
SN  - 23522208
KW  - partial order reduction
KW  - structural reduction
KW  - model checking
UR  - https://doi.org/10.1016/j.jlamp.2018.09.002
L2  - https://doi.org/10.1016/j.jlamp.2018.09.002
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.
ER  -

BOENNELAND, Frederik M.; Jacob DYHR; Peter G. JENSEN; Mads JOHANNSEN a Jiří SRBA. Stubborn Versus Structural Reductions for Petri Nets. \textit{Journal of Logical and Algebraic Methods in Programming}. 2019, roč.~102, January 2019, s.~46-63. ISSN~2352-2208. Dostupné z: https://doi.org/10.1016/j.jlamp.2018.09.002.

Přehled o publikaci