Chasing the Best Büchi Automata for Nested Depth-first Search Based Model Checking

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BLAHOUDEK František

Year of publication 2014
Type Article in Proceedings
Conference 11th Summer School on Modelling and Verification of Parallel Processes (MOVEP'14)
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords LTL, Büchi automata, model checking
Attached files
Description The automata-based model checking uses a translation of formulae in Linear Temporal Logic (LTL) into Büchi automata (BA). The performance of the model checkers can be heavily influenced by the BA used. In this paper we discuss several heuristics commonly used to decide which BA should be used for given verification task, suggest a novel heuristic for this problem and finally evaluate the heuristics using common LTL-to-BA translators, model checker Spin and benchmark of real verification tasks. Our evaluation shows that heuristics based only on number of states of BA or the degree of determinism often give wrong answer or are unable to answer. On a concrete example we further demonstrate our suggestion to exploit some partial knowledge about systems to improve our heuristic.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.