We present a new procedure for the translation of propositional linear-time temporal logic (LTL) formulas to equivalent nondeterministic Büchi automata. Our procedure is based on simulation relations for alternating Büchi automata. Whereas most of the procedures that have been described in the past compute simulation relations in the last step of the translation (after a nondeterministic Büchi automaton has already been constructed), our procedure computes simulation relations for alternating Büchi automata in an early stage and uses them in an on-the-fly fashion. This decreases the time and space consumption without sacrificing the potential of simulation relations. We present experimental results that demonstrate the advantages of our approach: Our procedure is faster than TMP but produces, on the average, automata of about the same size; LTL2BA is faster than our procedure but produces larger automata. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Fritz, C. (2003). Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2759, 35–48. https://doi.org/10.1007/3-540-45089-0_5
Mendeley helps you to discover research relevant for your work.