CIAA2003

START ConferenceManager

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

Carsten Fritz

Presented at Eighth International Conference on Implementation and Application of Automata (CIAA 2003), July 16-18, 2003 Santa Barbara, CA, USA

Abstract

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