zbMATH — the first resource for mathematics

Efficient Büchi automata form LTL formulae. (English) Zbl 0974.68086
Emerson, E. Allen (ed.) et al., Computer aided verification. 12th international conference, CAV 2000. Chicago, IL, USA, July 15-19, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1855, 248-263 (2000).
Summary: We present an algorithm to generate small Büchi automata for LTL formulae. We describe a heuristic approach consisting of three phases: rewriting of the formula, an optimized translation procedure, and simplification of the resulting automaton. We present a translation procedure that is optimal within a certain class of translation procedures. The simplification algorithm can be used for Büchi automata in general. It reduces the number of states and transitions, as well as the number and size of the accepting sets – possibly reducing the strength of the resulting automaton. This leads to more efficient model checking of linear-time logic formulae. We compare our method to previous work, and show that it is significantly more efficient for both random formulae, and formulae in common use and from the literature.
For the entire collection see [Zbl 0941.00029].

68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)
03D05 Automata and formal grammars in connection with logical questions
PDF BibTeX Cite