Resumé
| Originalsprog | Engelsk |
|---|---|
| Titel | PETRI NETS 2018: Application and Theory of Petri Nets and Concurrency |
| Udgivelses sted | 978-3-319-91267-7 |
| Forlag | Springer Publishing Company |
| Publikationsdato | 8 mar. 2018 |
| Sider | 143-163 |
| ISBN (Elektronisk) | 978-3-319-91268-4 |
| DOI | |
| Status | Udgivet - 8 mar. 2018 |
| Begivenhed | International Conference on Applications and Theory of Petri Nets and Concurrency - Bratislava, Slovenien Varighed: 24 jun. 2018 → 29 jun. 2018 |
Konference
| Konference | International Conference on Applications and Theory of Petri Nets and Concurrency |
|---|---|
| Land | Slovenien |
| By | Bratislava |
| Periode | 24/06/2018 → 29/06/2018 |
| Navn | Lecture Notes in Computer Science |
|---|---|
| Vol/bind | 10877 |
| ISSN | 0302-9743 |
Fingerprint
Citer dette
}
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 proceeding › Konferenceartikel i proceeding › Forskning › peer 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 -