Simplification of CTL Formulae for Efficient Model Checking of Petri Nets

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

17 Citations (Scopus)

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.
Original languageEnglish
Title of host publicationPETRI NETS 2018: Application and Theory of Petri Nets and Concurrency
Place of Publication978-3-319-91267-7
PublisherSpringer Publishing Company
Publication date8 Mar 2018
Pages143-163
ISBN (Electronic)978-3-319-91268-4
DOIs
Publication statusPublished - 8 Mar 2018
EventInternational Conference on Applications and Theory of Petri Nets and Concurrency - Bratislava, Slovenia
Duration: 24 Jun 201829 Jun 2018

Conference

ConferenceInternational Conference on Applications and Theory of Petri Nets and Concurrency
Country/TerritorySlovenia
City Bratislava
Period24/06/201829/06/2018
SeriesLecture Notes in Computer Science
Volume10877
ISSN0302-9743

Fingerprint

Dive into the research topics of 'Simplification of CTL Formulae for Efficient Model Checking of Petri Nets'. Together they form a unique fingerprint.

Cite this