From LTL to symbolically represented deterministic automata

Abstract

Temporal logics like LTL are frequently used for the specification and verification of reactive systems. For verification, LTL formulas are typically translated to generalized nondeterministic Büchi automata so that the verification problem is reduced to checking the emptiness of automata. While this can be done symbolically for nondeterministic automata, other applications require deterministic automata, so that a subsequent determinization step is required. Unfortunately, currently known determinization procedures for Büchi automata like Safra's procedure are not amenable to a symbolic implementation. It is well-known that ω-automata that stem from LTL formulas have special properties. In this paper, we exploit such a property in a new determinization procedure for these automata. Our procedure avoids the use of complicated tree structures as used in Safra's procedure and it generates symbolic descriptions of equivalent deterministic parity automata which was so far not possible for full LTL. © 2008 Springer-Verlag Berlin Heidelberg.