Simplification of CTL Formulae for Efficient Model Checking of Petri Nets

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

2 Citationer (Scopus)

Resumé

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% 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.
OriginalsprogEngelsk
TitelPETRI NETS 2018: Application and Theory of Petri Nets and Concurrency
Udgivelses sted978-3-319-91267-7
ForlagSpringer Publishing Company
Publikationsdato8 mar. 2018
Sider143-163
ISBN (Elektronisk)978-3-319-91268-4
DOI
StatusUdgivet - 8 mar. 2018
BegivenhedInternational Conference on Applications and Theory of Petri Nets and Concurrency - Bratislava, Slovenien
Varighed: 24 jun. 201829 jun. 2018

Konference

KonferenceInternational Conference on Applications and Theory of Petri Nets and Concurrency
LandSlovenien
By Bratislava
Periode24/06/201829/06/2018
NavnLecture Notes in Computer Science
Vol/bind10877
ISSN0302-9743

Fingerprint

Model checking
Petri nets
Explosions

Citer dette

Bønneland, F. M., Dyhr, J., Jensen, P. G., Johannsen, M., & Srba, J. (2018). Simplification of CTL Formulae for Efficient Model Checking of Petri Nets. I PETRI NETS 2018: Application and Theory of Petri Nets and Concurrency (s. 143-163). 978-3-319-91267-7: Springer Publishing Company. Lecture Notes in Computer Science, Bind. 10877 https://doi.org/10.1007/978-3-319-91268-4_8
Bønneland, Fredrik Meyer ; Dyhr, Jakob ; Jensen, Peter Gjøl ; Johannsen, Mads ; Srba, Jiri. / Simplification of CTL Formulae for Efficient Model Checking of Petri Nets. PETRI NETS 2018: Application and Theory of Petri Nets and Concurrency . 978-3-319-91267-7 : Springer Publishing Company, 2018. s. 143-163 (Lecture Notes in Computer Science, Bind 10877).
@inproceedings{17ebc33a7d764a2b983cb18eda891fb6,
title = "Simplification of CTL Formulae for Efficient Model Checking of Petri Nets",
abstract = "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{\%} 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.",
author = "B{\o}nneland, {Fredrik Meyer} and Jakob Dyhr and Jensen, {Peter Gj{\o}l} and Mads Johannsen and Jiri Srba",
year = "2018",
month = "3",
day = "8",
doi = "10.1007/978-3-319-91268-4_8",
language = "English",
series = "Lecture Notes in Computer Science",
publisher = "Springer Publishing Company",
pages = "143--163",
booktitle = "PETRI NETS 2018: Application and Theory of Petri Nets and Concurrency",
address = "United States",

}

Bønneland, FM, Dyhr, J, Jensen, PG, Johannsen, M & Srba, J 2018, Simplification of CTL Formulae for Efficient Model Checking of Petri Nets. i PETRI NETS 2018: Application and Theory of Petri Nets and Concurrency . Springer Publishing Company, 978-3-319-91267-7, Lecture Notes in Computer Science, bind 10877, s. 143-163, Bratislava, Slovenien, 24/06/2018. https://doi.org/10.1007/978-3-319-91268-4_8

Simplification of CTL Formulae for Efficient Model Checking of Petri Nets. / Bønneland, Fredrik Meyer; Dyhr, Jakob; Jensen, Peter Gjøl; Johannsen, Mads; Srba, Jiri.

PETRI NETS 2018: Application and Theory of Petri Nets and Concurrency . 978-3-319-91267-7 : Springer Publishing Company, 2018. s. 143-163 (Lecture Notes in Computer Science, Bind 10877).

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

TY - GEN

T1 - Simplification of CTL Formulae for Efficient Model Checking of Petri Nets

AU - Bønneland, Fredrik Meyer

AU - Dyhr, Jakob

AU - Jensen, Peter Gjøl

AU - Johannsen, Mads

AU - Srba, Jiri

PY - 2018/3/8

Y1 - 2018/3/8

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

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

U2 - 10.1007/978-3-319-91268-4_8

DO - 10.1007/978-3-319-91268-4_8

M3 - Article in proceeding

T3 - Lecture Notes in Computer Science

SP - 143

EP - 163

BT - PETRI NETS 2018: Application and Theory of Petri Nets and Concurrency

PB - Springer Publishing Company

CY - 978-3-319-91267-7

ER -

Bønneland FM, Dyhr J, Jensen PG, Johannsen M, Srba J. Simplification of CTL Formulae for Efficient Model Checking of Petri Nets. I PETRI NETS 2018: Application and Theory of Petri Nets and Concurrency . 978-3-319-91267-7: Springer Publishing Company. 2018. s. 143-163. (Lecture Notes in Computer Science, Bind 10877). https://doi.org/10.1007/978-3-319-91268-4_8