Automata-Driven Techniques for Partial-Order Reductions and Guided Search of Petri Nets
Authors
Ulrik, Nikolaj Jensen ; Virenfeldt, Simon Mejlby
Term
4. term
Education
Publication year
2021
Pages
43
Abstract
Model checking er en metode til automatisk at kontrollere, om et system opfører sig korrekt over tid. I den udbredte automaton-baserede tilgang til Lineær Temporal Logik (LTL) kombineres systemet med en nondeterministisk Büchi-automat (NBA), der beskriver ulovlig adfærd; verificeringen går ud på effektivt at udforske det fælles tilstandsrum for at se, om sådan adfærd kan opstå. Der findes mange optimeringer, som alene udnytter egenskaber ved systemet eller ved automaten, men færre der udnytter begge samtidig. Vi præsenterer en stubborn set-metode og heuristikker til styret søgning, som bruger lokal information fra NBA’en til at beskære og prioritere udforskningen af systemets tilstandsrum. Vi implementerer teknikkerne som en udvidelse af den åbne modelcheck-motor verifypn, der anvendes af Tapaal, og evaluerer dem på datasættet fra Model Checking Contest 2020 (MCC 2020). Resultaterne viser, at den styrede søgning forbedrer ydeevnen i forhold til uspecificeret (blind) søgning, og at vores NBA-baserede stubborn set-metode er bedre end den klassiske stubborn set-metode. Når den nye metode ikke kan anvendes, kan den klassiske bruges som fallback; den kombinerede tilgang giver endnu bedre resultater. Vi finder desuden, at gevinsterne ved at kombinere stubborn sets og heuristikker næsten svarer til summen af gevinsterne ved hver teknik for sig. Endelig sammenligner vi vores LTL-modelchecker med ITS-LoLA, vinderen af LTL-kategorien ved MCC 2020, og finder, at vores værktøj besvarer 56,8 % af de forespørgsler, ITS-LoLA ikke besvarede, svarende til en stigning på 10,8 % i antal svar.
Model checking automatically checks whether a system behaves correctly over time. In the common automaton-based approach to Linear Temporal Logic (LTL), the system is paired with a Nondeterministic Büchi Automaton (NBA) that characterizes illegal behaviour; verification explores their combined state space to see whether such behaviour can occur. Many optimizations target either the system or the automaton alone, but fewer exploit both together. We present a stubborn set method and guided-search heuristics that use local information from the NBA to prune and prioritize the exploration of the system’s state space. We implement these techniques as an extension of the open-source model-checking engine verifypn, used by Tapaal, and evaluate them on the 2020 Model Checking Contest (MCC) dataset. Our results show that guided search improves performance over unguided search, and that our NBA-based stubborn set method outperforms the classic stubborn set method. When the new method does not apply, the classic method can be used as a fallback; this mixed approach performs even better. We also find that the improvements from combining stubborn sets and heuristics are almost equal to the sum of the individual improvements. Finally, compared with ITS-LoLA, the winner of the MCC 2020 LTL category, our LTL model checker answers 56.8% of the queries that ITS-LoLA did not, corresponding to a 10.8% increase in the number of answers.
[This summary has been rewritten with the help of AI based on the project's original abstract]
Keywords
Documents