2011 | OriginalPaper | Buchkapitel
Entscheidungsverfahren für ω-Automaten
verfasst von : Prof. Dr. Martin Hofmann, Prof. Dr. Martin Lange
Erschienen in: Automatentheorie und Logik
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
Automaten sollen den algorithmischen Zugang zu logischen Problemen, insbesondere den Erfüllbarkeitsproblem liefern. In diesem Kapitel widmen wir uns nun den algorithmischen Fragestellungen bzgl. der verschiedenen Typen von Automaten auf unendlichen Wörtern. Wir betrachten im Wesentlichen das Leerheitsproblem (ist
L
(
A
) = ø?) und das Universalitätsproblem (ist
L
(
A
) =
Σ
ω
?). Ersteres z.B. lässt sich dann zusammen mit einer äquivalenzerhaltenden Reduktion von Formeln in Automaten verwenden, um Erfüllbarkeit zu entscheiden. Dies wurde ja auch bereits bei den Entscheidungsverfahren für WMSO und MSO so verwendet. Andere Probleme wie das Wortproblem für endlich repräsentierte
ω
-Wörter etc. lassen sich normalerweise leicht auf diese reduzieren.