Tighter Bounds for the Determinisation of Biichi Automata

摘要

The introduction of an efficient determinisation technique for Biichi automata by Safra has been a milestone in automata theory. To name only a few applications, efficient determinisation techniques for ω-word automata are the basis for several manipulations of ω-tree automata (most prominently the nondeterminisation of alternating tree automata) as well as for satisfiability checking and model synthesis for branching- and alternating-time logics. This paper proposes a determinisation technique that is simpler than the constructions of Safra, Piterman, and Muller and Schupp, because it separates the principle acceptance mechanism from the concrete acceptance condition. The principle mechanism intuitively uses a Rabin condition on the transitions; we show how to obtain an equivalent Rabin transition automaton with approximately (1.65 n)~n states from a nondeterministic Biichi automaton with n states. Having established this mechanism, it is simple to develop translations to automata with standard acceptance conditions. We can construct standard Rabin automata whose state-space is bilinear in the size of the input alphabet and the state-space of the Rabin transition automaton, or, for large input alphabets, contains approximately (2.66 n)~n states, respectively. We also provide a flexible translation to parity automata with O(n!~2) states and 2n priorities based on a later introduction record, and hence connect the transformation of the acceptance condition to other record based transformations known from the literature.