Is there a best Büchi automaton for explicit 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 DURET-LUTZ Alexandre KŘETÍNSKÝ Mojmír STREJČEK Jan

Year of publication 2014
Type Article in Proceedings
Conference 2014 International SPIN Symposium on Model Checking of Software
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1145/2632362.2632377
Field Informatics
Keywords linear temporal logic; Büchi automata; explicit model checking
Attached files
Description LTL to Büchi automata (BA) translators are traditionally optimized to produce automata with a small number of states or a small number of non-deterministic states. In this paper, we search for properties of Büchi automata that really influence the performance of explicit model checkers. We do that by manual analysis of several automata and by experiments with common LTL-to-BA translators and realistic verification tasks. As a result of these experiences, we gain a better insight into the characteristics of automata that work well with Spin.
Related projects:

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