Anzeige
Erschienen in:
2008 | OriginalPaper | Buchkapitel
From LTL to Symbolically Represented Deterministic Automata
verfasst von : Andreas Morgenstern, Klaus Schneider
Erschienen in: Verification, Model Checking, and Abstract Interpretation
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.