Simplification of CTL Formulae for Efficient Model Checking of Petri Nets

Result code in 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>
Result on the web
<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>

Result language
angličtina
Original language name
Simplification of CTL Formulae for Efficient Model Checking of Petri Nets
Original language description
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.
Czech name
—
Czech description
—

Project
—
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

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

Article name in the collection
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
—
Number of pages
21
Pages from-to
143-163
Publisher name
Springer-Verlag
Place of publication
Holland
Event location
Bratislava, Slovak Republic
Event date
Jan 1, 2018
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—

Similar results(10)