An automata theoretic approach to temporal logic

Abstract

A syntax directed mapping is presented from Propositional Temporal Logic (PTL) formulae to Müller type finite automata. This is a direct and much more elegant and easier to implement approach than previously described methods. Most of these methods are based on tableau methods for satisfiability checking, and after that a Biichi type of automaton is extracted. Biichi and Müller automata are equally expressive. However, Müller automata have nicer properties than Biichi automata, for instance deterministic Müller automata are expressive as non-deterministic ones, while this is not true for Biichi automata. Also deterministic BUchi automata are not closed under complement. This transformation is the first step in a decision procedure, since the resulting Müller automaton represents the models of the temporal logic formula, and on which further verification and analysis can be performed.