@article{YIN2009, 
author = {Chongyuan YIN and Guiming LUO},
title = {Efficient Translation of LTL to Büchi Automata},
year = {2009},
journal = {Tsinghua Science and Technology},
volume = {14},
number = {1},
pages = {75-82},
keywords = {linear temporal logic, form-filling algorithm, Büchi automata, state-based Büchi automata},
url = {https://www.sciopen.com/article/10.1016/S1007-0214(09)70010-0},
doi = {10.1016/S1007-0214(09)70010-0},
abstract = {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.}
}