Constructing Buechi Automata from Linear Temporal Logic Using Simulation Relations for Alternating Buechi Automata

摘要

We present a new procedure for the translation of propositional linear-time temporal logic (LTL) formulas to equivalent nondeter-ministic Buechi automata. Our procedure is based on simulation relations for alternating Buechi 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 Biichi automaton has already been constructed), our procedure computes simulation relations for alternating Buechi 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.