• Nikolaj Jensen Ulrik
  • Simon Mejlby Virenfeldt
4. semester, Datalogi, Kandidat (Kandidatuddannelse)
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.
Antal sider43
ID: 413693732