Profile trees for Büchi word automata, with application to determinization (Q897653)

An \textit{\(\omega\)-automaton} is a finite-state machine that reads an infinite word, on a finite alphabet, \textit{accepting} or \textit{rejecting} the word according to some \textit{acceptance condition}. Originally introduced in order to study monadic second-order logic in the 1960s, \(\omega\)-automata have found numerous applications in computer science as a natural model for non-halting computations. A central question in automata theory is whether, and how, one can replace a nondeterministic automaton by a deterministic automaton accepting exactly the same words. This question is quite complex in the case of \(\omega\)-automata, where it has been shown to depend on the type of acceptance condition. For instance, deterministic \(\omega\)-automata with Büchi acceptance conditions (Büchi automata for short) are strictly less powerful that their nondeterministic counterpart. While a nondeterministic Büchi \(\omega\)-automaton can be determinized, this process will, in general, yield a deterministic \(\omega\)-automaton with a more powerful acceptance condition, such as a Rabin acceptance condition. While many approaches to determinize Büchi automata have been developed over the years, these processes are quite complex and involved. The objective of this paper is to develop principles, concepts and data structures to advance the understanding of the theoretical principles underpinning these determinization algorithms. To this aim, the authors extend their \textit{profile-based} approach [the first author et al., Log. Methods Comput. Sci. 9, No. 1, Paper No. 14, 26 p. (2013; Zbl 1274.68158)], based on the history of visits to accepting states. In this paper, they introduce a \textit{profile tree} and show that it allows to develop a new singly exponential Büchi determinization construction. Contrary to previous approaches, this construction uses a declarative rather than an operational definition for the transitions between states of the deterministic automaton.