@inproceedings{LiPZWHL13,
author = {Jianwen Li and
Geguang Pu and
Lijun Zhang and
Zheng Wang and
Jifeng He and
Kim Guldstrand Larsen},
title = {On the Relationship between {LTL} Normal Forms and B{\"u}chi Automata},
year = {2013},
pages = {256-270},
booktitle = {Theories of Programming and Formal Methods - Essays Dedicated
to Jifeng He on the Occasion of His 70th Birthday},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {8051},
publisher = {Springer},
ee = {http://dx.doi.org/10.1007/978-3-642-39698-4_16},
abstract = {In this paper, we revisit the problem of translating LTL formulas to B\"uchi automata. We first translate the given LTL formula into a special disjuctive-normal form (DNF). The formula will be part of the state, and its DNF normal form specifies the atomic properties that should hold immediately (labels of the transitions) and the formula that should hold afterwards (the corresponding successor state). If the given formula is Until-free or Release-free, the B\"uchi automaton can be obtained directly in this manner. For a general formula, the construction is more involved: an additional component will be needed for each formula that helps us to identify the set of accepting states. Notably, our construction is an on-the-fly construction, which starts with the given formula and explores successor states according to the normal forms. We implement our construction and compare the tool with SPOT [3]. The comparision results are very encouraging and show our construction is quite innovative.}
}