Simplification of CTL Formulae for Efficient Model Checking of
Petri Nets

D 2018

Simplification of CTL Formulae for Efficient Model Checking of Petri Nets

BOENNELAND, F.M., J. DYHR, P.G. JENSEN, M. JOHANNSEN, Jiří SRBA et. al.

Basic information

Original name

Simplification of CTL Formulae for Efficient Model Checking of Petri Nets

Authors

BOENNELAND, F.M. (208 Denmark), J. DYHR (208 Denmark), P.G. JENSEN (208 Denmark), M. JOHANNSEN (208 Denmark) and Jiří SRBA (203 Czech Republic, guarantor, belonging to the institution)

Edition

Holland, Proceedings of the 39th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets'18), p. 143-163, 21 pp. 2018

Publisher

Springer-Verlag

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10200 1.2 Computer and information sciences

Country of publisher

Netherlands

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

printed version "print"

References:

URL

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/18:00105977

Organization unit

Faculty of Informatics

ISBN

978-3-319-91267-7

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-91268-4_8

Keywords in English

CTL model checking; Petri nets; on-the-fly algorithms

Abstract

V originále

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.

Citovat

BOENNELAND, F.M., J. DYHR, P.G. JENSEN, M. JOHANNSEN and Jiří SRBA. Simplification of CTL Formulae for Efficient Model Checking of Petri Nets. In Proceedings of the 39th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets'18). Holland: Springer-Verlag, 2018, p. 143-163. ISBN 978-3-319-91267-7. Available from: https://dx.doi.org/10.1007/978-3-319-91268-4_8.

@inproceedings{1492177,
   author = {Boenneland, F.M. and Dyhr, J. and Jensen, P.G. and Johannsen, M. and Srba, Jiří},
   address = {Holland},
   booktitle = {Proceedings of the 39th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets'18)},
   doi = {http://dx.doi.org/10.1007/978-3-319-91268-4_8},
   keywords = {CTL model checking; Petri nets; on-the-fly algorithms},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Holland},
   isbn = {978-3-319-91267-7},
   pages = {143-163},
   publisher = {Springer-Verlag},
   title = {Simplification of CTL Formulae for Efficient Model Checking of Petri Nets},
   url = {https://link.springer.com/chapter/10.1007/978-3-319-91268-4_8},
   year = {2018}
}

TY  - JOUR
ID  - 1492177
AU  - Boenneland, F.M. - Dyhr, J. - Jensen, P.G. - Johannsen, M. - Srba, Jiří
PY  - 2018
TI  - Simplification of CTL Formulae for Efficient Model Checking of Petri Nets
PB  - Springer-Verlag
CY  - Holland
SN  - 9783319912677
KW  - CTL model checking
KW  - Petri nets
KW  - on-the-fly algorithms
UR  - https://link.springer.com/chapter/10.1007/978-3-319-91268-4_8
L2  - https://link.springer.com/chapter/10.1007/978-3-319-91268-4_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 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.
ER  -

BOENNELAND, F.M., J. DYHR, P.G. JENSEN, M. JOHANNSEN and Jiří SRBA. Simplification of CTL Formulae for Efficient Model Checking of Petri Nets. In \textit{Proceedings of the 39th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets'18)}. Holland: Springer-Verlag, 2018, p.~143-163. ISBN~978-3-319-91267-7. Available from: https://dx.doi.org/10.1007/978-3-319-91268-4\_{}8.

Detailed Information on Publication Record