Simple and Efficient Translation from LTL Formulas to Büchi Automata

We present a collection of simple on-the-fly techniques to generate small Büchi automata from Linear Time Logic formulas. These techniques mainly involve syntactic characterizations of formulas, and yet allow efficient computations. Thus heavily relying on such proof-theoretic issues, we can omit the classical formula pre-simplification step, and also simulation-based post-simplification steps (aka model-theoretic issues).Although closely related to other similar recent works in the same topic, our ideas have led to an implementation that performs significantly better than some of the best available tools, such as Wring or LTL2BA. We compare our tool BAOM (“Büchi Automata Once More”) with others, on formulas commonly found in the literature, and on randomly generated testbenchs.