Determinization and ambiguity of classical and probabilistic Büchi automata

• Determinisierung und Mehrdeutigkeit von Klassischen und Probabilistischen Büchi-Automaten

Pirogov, Anton; Löding, Christof (Thesis advisor); Ábrahám, Erika (Thesis advisor); Schewe, Sven (Thesis advisor)

Aachen : RWTH Aachen University (2021)
Doktorarbeit

Dissertation, RWTH Aachen University, 2021

Kurzfassung

Büchi-Automaten sind eine natürliche Verallgemeinerung von gewöhnlichen NEA auf unendliche Wörter. Während sie ursprünglich zur Klärung von Entscheidbarkeitsfragen in der Logik eingeführt wurden, entwickelten sie sich zu einem populären Werkzeug in praktischen Anwendungen, z.B. in automatenbasiertem Model Checking und in der Programmsynthese. Als die wohl einfachste und bekannteste Variante von $\omega$-Automaten dienen sie als Zwischenrepräsentation von $\omega$-regulären Spezifikationen von Anforderungen in der Verifikation oder Synthese, die üblicherweise deklarativ in z.B. linearer Temporallogik formuliert werden. Leider sind nichtdeterministische Automaten für einige Anwendungen nicht direkt geeignet, während deterministische Büchi-Automaten weniger ausdrucksstark sind. Dieses Problem wird normalerweise durch die Konstruktion von deterministischen Automaten einer anderen Art gelöst, oder durch Einschränkung ihrer Mehrdeutigkeit, d.h. der größtmöglichen Anzahl von akzeptierenden Läufen auf einem Wort. In beiden Fällen ist die Übersetzung aufwendig und verursacht im schlimmsten Fall ein exponentiell größere Anzahl von Zuständen. Deswegen sind optimierte Konstruktionen und Heuristiken für häufige Spezialfälle von großem Nutzen und Interesse für praktische Anwendungen. In dieser Arbeit werden neue Ergebnisse zu beiden Lösungsansätzen präsentiert. Einerseits wird eine neue generische Konstruktion zur Determinisierung von nichtdeterministischen Büchi- zu deterministischen Paritätsautomaten präsentiert, welche die dominanten Familien der vorhergehenden Ansätze, nämlich die Safra-Konstruktion und Muller-Schupp-Konstruktion, vereinigt. Zusätzlich wird eine Reihe von neuen Heuristiken vorgestellt, von denen einige die Eigenschaften der vorgestellten Konstruktion ausnutzen. Außerdem wird die Mehrdeutigkeit von Büchi-Automaten mittels einer auf einfachen syntaktischen Mustern basierenden Hierarchie charakterisiert sowie eine Konstruktion zur Einschränkung der Mehrdeutigkeit vorgestellt. Abgesehen von klassischen nichtdeterministischen und deterministischen Automatenvarianten ist es naheliegend auch probabilistische Automaten zu untersuchen, welche statt Nichtdeterminismus auf Wahrscheinlichkeitsverteilungen zurückgreifen, um den Nachfolgezustand zu bestimmen. Es ist bekannt, dass solche Automaten im Allgemeinen ausdrucksstärker als klassische Automaten sind. In der Arbeit werden neue Teilklassen von probabilistischen Automaten präsentiert, die bestimmten Klassen der Mehrdeutigkeitshierarchie entsprechen und nicht ausdrucksstärker als klassische Automaten sind, was durch präsentierte Konstruktionen von derartigen probabilistischen zu gewöhnlichen Büchi-Automaten bezeugt wird.

Einrichtungen

• Graduiertenkolleg UnRAVeL [080060]
• Fachgruppe Informatik [120000]
• Lehrstuhl für Informatik 7 (Logik und Theorie diskreter Systeme) [122910]