Profile Trees for Buchi Word Automata, with Application to Determinization
========================================================

The determinization of Buchi automata is a celebrated problem, with applications in realms such as
synthesis, probabilistic verification, and module checking.  Since the 1960s, there has been a
steady progress of constructions: from McNaughton, Safra, Piterman, and Schewe, among others.
All of these constructions are difficult, however, and lack a crisp mathematical description. These
constructions employ trees as states, and transitions between trees are defined operationally,
rather than declaratively.

In 2008, Kahler and Wilke attempted to unify Buchi determinization with complementation and
disambiguation. Unfortunately, the determinization construction deviated significantly from the
common ground of the other two constructions. In 2010, we refined their approach to complementation, and demonstrated how to provide a complementation construction that was deterministic in the limit.
We here extend the approach to full determinization. The resulting construction can be defined as a
subset construction, augmented with two preorders over states and a labeling. We define both Rabin and parity variants of the construction, matching the best known lower bounds.