Simplification of CTL Formulae for Efficient Model Checking of Petri Nets

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F18%3A00105977" target="_blank" >RIV/00216224:14330/18:00105977 - isvavai.cz</a>

Výsledek na webu

<a href="https://link.springer.com/chapter/10.1007/978-3-319-91268-4_8" target="_blank" >https://link.springer.com/chapter/10.1007/978-3-319-91268-4_8</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-319-91268-4_8" target="_blank" >10.1007/978-3-319-91268-4_8</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Simplification of CTL Formulae for Efficient Model Checking of Petri Nets

Popis výsledku v původním jazyce

We study techniques to overcome the state space explosion problem in CTL model checking of Petri nets. Classical state space pruning approaches like partial order reductions and structural reductions become less efficient with the growing size of the CTL formula. The reason is that the more places and transitions are used as atomic propositions in a given formula, the more of the behaviour (interleaving) becomes relevant for the validity of the formula. We suggest several methods to reduce the size of CTL formulae, while preserving their validity. By these methods, we significantly increase the benefits of structural and partial order reductions, as the combination of our techniques can achive up to 60 percent average reduction in formulae sizes. The algorithms are implemented in the open-source verification tool TAPAAL and we document the efficiency of our approach on a large benchmark of Petri net models and queries from the Model Checking Contest 2017.

Název v anglickém jazyce

Simplification of CTL Formulae for Efficient Model Checking of Petri Nets

Popis výsledku anglicky

We study techniques to overcome the state space explosion problem in CTL model checking of Petri nets. Classical state space pruning approaches like partial order reductions and structural reductions become less efficient with the growing size of the CTL formula. The reason is that the more places and transitions are used as atomic propositions in a given formula, the more of the behaviour (interleaving) becomes relevant for the validity of the formula. We suggest several methods to reduce the size of CTL formulae, while preserving their validity. By these methods, we significantly increase the benefits of structural and partial order reductions, as the combination of our techniques can achive up to 60 percent average reduction in formulae sizes. The algorithms are implemented in the open-source verification tool TAPAAL and we document the efficiency of our approach on a large benchmark of Petri net models and queries from the Model Checking Contest 2017.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10200 - Computer and information sciences

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2018

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 statě ve sborníku

Proceedings of the 39th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets'18)

ISBN

9783319912677

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

21

Strana od-do

143-163

Název nakladatele

Springer-Verlag

Místo vydání

Holland

Místo konání akce

Bratislava, Slovak Republic

Datum konání akce

1. 1. 2018

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—