Stubborn Versus Structural Reductions for Petri Nets

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F19%3A00113644" target="_blank" >RIV/00216224:14330/19:00113644 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1016/j.jlamp.2018.09.002" target="_blank" >https://doi.org/10.1016/j.jlamp.2018.09.002</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1016/j.jlamp.2018.09.002" target="_blank" >10.1016/j.jlamp.2018.09.002</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Stubborn Versus Structural Reductions for Petri Nets

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Stubborn Versus Structural Reductions for Petri Nets

Popis výsledku anglicky

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.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2019

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

Journal of Logical and Algebraic Methods in Programming

ISSN

2352-2208

e-ISSN

2352-2216

Svazek periodika

102

Číslo periodika v rámci svazku

January 2019

Stát vydavatele periodika

NL - Nizozemsko

Počet stran výsledku

18

Strana od-do

46-63

Kód UT WoS článku

000453499800003

EID výsledku v databázi Scopus

2-s2.0-85064897283