@inbook{1143d1dfb23347c8a13fa5cd76e14aab,
title = "On the relationship between LTL normal forms and B{\"u}chi automata",
abstract = "In this paper, we revisit the problem of translating LTL formulas to B{\"u}chi 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{\"u}chi 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.",
keywords = "Artificial intelligence, Computer science, Automata theory",
author = "Jianwen Li and Geguang Pu and Lijun Zhang and Zheng Wang and Jifeng He and \{Guldstrand Larsen\}, Kim",
year = "2013",
doi = "10.1007/978-3-642-39698-4\_16",
language = "English",
isbn = "978-3-642-39697-7",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "256--270",
booktitle = "Theories of Programming and Formal Methods",
}