Automata-Driven Techniques for Partial-Order Reductions and Guided Search of Petri Nets
Term
4. term
Education
Publication year
2021
Submitted on
2021-06-03
Pages
43
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