zbMATH — the first resource for mathematics

Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata. (English) Zbl 1279.68152
Ibarra, Oscar H. (ed.) et al., Implementation and application of automata. 8th international conference, CIAA 2003, Santa Barbara, CA, USA, July 16–18, 2003. Proceedings. Berlin: Springer (ISBN 3-540-40561-5/pbk). Lect. Notes Comput. Sci. 2759, 35-48 (2003).
Summary: 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.
For the entire collection see [Zbl 1028.00030].

68Q45 Formal languages and automata
03B44 Temporal logic
03D05 Automata and formal grammars in connection with logical questions
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI