TY - GEN
T1 - On the relationship between LTL normal forms and Büchi automata
AU - Li, Jianwen
AU - Pu, Geguang
AU - Zhang, Lijun
AU - Wang, Zheng
AU - He, Jifeng
AU - Guldstrand Larsen, Kim
PY - 2013
Y1 - 2013
N2 - In this paper, we revisit the problem of translating LTL formulas to Bü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ü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.
AB - In this paper, we revisit the problem of translating LTL formulas to Bü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ü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.
UR - https://www.scopus.com/pages/publications/84883246757
U2 - 10.1007/978-3-642-39698-4_16
DO - 10.1007/978-3-642-39698-4_16
M3 - 会议稿件
AN - SCOPUS:84883246757
SN - 9783642396977
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 256
EP - 270
BT - Theories of Programming and Formal Methods
T2 - Theories of Programming and Formal Methods: Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday
Y2 - 1 September 2013 through 3 September 2013
ER -