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)
Dissertation / PhD Thesis

Dissertation, RWTH Aachen University, 2021

Abstract

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.

Institutions

• UnRAVeL Research Training Group [080060]
• Department of Computer Science [120000]
• Chair of Computer Science 7 (Logic and Theory of Discrete Systems) [122910]