On Refinement of Büchi Automata for Explicit Model Checking

Investor logo

Warning

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

BLAHOUDEK František DURET-LUTZ Alexandre RUJBR Vojtěch STREJČEK Jan

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

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-319-23404-5_6
Field Informatics
Keywords linear temporal logic; Büchi automata; explicit model checking; specification refinement
Description In explicit model checking, systems are typically described in an implicit and compact way. Some valid information about the system can be easily derived directly from this description, for example that some atomic propositions cannot be valid at the same time. The paper shows several ways to apply this information to improve the Büchi automaton built from an LTL specification. As a result, we get smaller automata with shorter edge labels that are easier to understand and, more importantly, for which the explicit model checking process performs better.
Related projects:

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