A master thesis from Aalborg University
Automata-Driven Techniques for Partial-Order Reductions and Guided Search of Petri Nets
Author(s)
Term
4. term
Education
Publication year
2021
Submitted on
2021-06-03
Pages
43 pages
Abstract
Automaton-based model checking, in which a system under verification is paired with a Nondeterministic Büchi Automaton (NBA) describing illegal behaviour, is the main method of model checking Linear Temporal Logic (LTL). However, while techniques for optimising the system under verification or the NBA independently are well known, there is less knowledge on techniques using both. We present a stubborn set method and heuristics for guided search, both of which use local information in the NBA to optimise the process of exploring the state space of the system being verified. We implement these techniques as an extension to the open source model checking engine verifypn used by Tapaal and evaluate them using the dataset from the 2020 edition of the Model Checking Contest (MCC). We find that the guided search technique improves performance compared to unguided search, and that the NBA-based stubborn set method performs better than the classic stubborn set method. Additionally, we show that the classic method can be used whenever the novel method does not apply, forming a mixed method that performs even better. We find that the improvements gained from combining stubborn sets and heuristics are almost equal to the sum of the improvements from stubborn sets and heuristics individually. Lastly, we compare our LTL model checker to ITS-LoLA, the winner of LTL category of the 2020 edition of the MCC, finding that our model checker answers 56.8 % of queries that ITS-LoLA did not, corresponding to a 10.8 % increase in the number of answers.
Keywords
Documents
Colophon: This page is part of the AAU Student Projects portal, which is run by Aalborg University. Here, you can find and download publicly available bachelor's theses and master's projects from across the university dating from 2008 onwards. Student projects from before 2008 are available in printed form at Aalborg University Library.
If you have any questions about AAU Student Projects or the research registration, dissemination and analysis at Aalborg University, please feel free to contact the VBN team. You can also find more information in the AAU Student Projects FAQs.