Generating Deterministic ω-Automata for most LTL Formulas by the Breakpoint Construction

Temporal logics like LTL are frequently used for the specification and verification of reactive systems. To this end, LTL formulas are typically translated to nondeterministic Büchi automata so that the LTL verification problem is reduced to a nonemptiness problem of ω-automata. While nondeterministic automata are sufficient for this purpose, many other applications require deterministic ω-automata. Unfortunately, the known determinization procedures for Büchi automata like Safra’s procedure are extremely difficult to implement, and the currently available implementations are only able to handle very small examples. In this paper, we present a new symbolic translation of a remarkably large fragment of LTL formulas to equivalent deterministic ω-automata. Our method is based on (1) a syntactically defined fragment of the temporal logic LTL together with a linear-time translation procedure to equivalent nondeterministic symbolic ω-automata, and (2) a (semi)-symbolic determinization procedure for this fragment. The fragment that we consider is complete in the sense that every LTL formula is equivalent to a formula in this fragment, and in practice, we found that most formulas occurring in real specifications already belong to this fragment.