Determinization and ambiguity of classical and probabilistic Büchi automata

Pirogov, Anton; Schewe, Sven; Löding, Christof; Ábrahám, Erika

doi:HT020872875

Determinization and ambiguity of classical and probabilistic Büchi automata = Determinisierung und Mehrdeutigkeit von Klassischen und Probabilistischen Büchi-Automaten

Pirogov, Anton^RWTH*

2021

Verantwortlichkeitsangabevorgelegt von Anton Pirogov, M.Sc.

ImpressumAachen : RWTH Aachen University 2021

Umfang1 Online-Ressource : Illustrationen, Diagramme

Dissertation, RWTH Aachen University, 2021

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Löding, Christof (Thesis advisor)^RWTH* ; Ábrahám, Erika (Thesis advisor)^RWTH* ; Schewe, Sven (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2021-02-18

Online
DOI: 10.18154/RWTH-2021-02027
URL: https://publications.rwth-aachen.de/record/813936/files/813936.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
ambiguity (frei) ; büchi automata (frei) ; determinization (frei) ; parity automata (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

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.

Büchi automata can be seen as a straight-forward generalization of ordinary NFA, adapted to handle infinite words. While they were originally introduced for applications in decidability of logics, they became a popular tool for practical applications, e.g. in automata-based approaches to model checking and synthesis problems. Being arguably both the simplest and most well-known variant in the zoo of so-called omega-automata that are considered in this setting, they serve as an intermediate representation of omega-regular specifications ofverification or synthesis requirements that are usually expressed in a more declarative fashion, e.g. using linear temporal logic. Unfortunately, nondeterministic automata are not directly suitable for certain applications, whereas deterministic Büchi automata are less expressive. This problem is usually solved by either constructing deterministic automata of a different kind, or by restricting their ambiguity, i.e., the maximal number of accepting runs on some word. In both cases, the transformation is expensive, yielding an exponential blow-up of the state space in the worst case. Therefore, optimized constructions and heuristics for common special cases are useful and in demand for actual practical applications. In this thesis new results concerning both approaches are presented. On one hand, we present a new general construction for determinization from nondeterministic Büchi to deterministic parity automata that unifies the dominant branches of previous approaches based on the Safra construction and the Muller-Schupp construction. Additionally, we provide a set of new heuristics, some of which exploit properties of our unified construction. Furthermore, we characterize the ambiguity of Büchi automata by a hierarchy that is determined by simple syntactical patterns in the automata, and present a new construction that reduces the ambiguity of an automaton. Apart from the classical nondeterministic and deterministic variants of automata, it is natural to consider probabilistic automata, i.e., automata that instead of utilizing nondeterminism use a probability distribution on the states to decide which state to go to next. It is known that in general, such automata are more expressive than classical automata. We show that subclasses of probabilistic automata that correspond to certain classes of the previously mentioned ambiguity hierarchy are not more expressive than classical automata, providing constructions to obtain classical Büchi automata from them.

OpenAccess:
PDF
(additional files)