Efficient Translation of LTL to Büchi Automata

The construction of Büchi automata from linear temporal logic is a significant step in model checking. This paper presents a depth-first construction algorithm to obtain simple Büchi automata from linear-time temporal logic which significantly reduces the sizes of the state spaces. A form-filling algorithm was used to reduce the size of the generated automata and the algorithms were applied directly to state-based Büchi automata, without transformation into transition-based automata. A form-filling algorithm for the Büchi automata, which is based on the form-filling algorithm for deterministic automata, was developed by redefining parts of the configuration of the Büchi automata as well as the transition function. The correctness of this form-filling algorithm was proven. Tests show that this approach is competitive, especially on LTL formulae in the form of G, F, and U.