Exponential determinization for ω-automata with strong-fairness acceptance condition

Abstract

In [Saf88] an exponential determinization piocedure for Buchi automata was shown, yielding tight bounds for decision procedures of some logics ([EJ88, Saf88, SV89, KT89]). In [SV89] the complexity of determinization and complementation of w-automata was further investigated, leaving as an open question the complexity of the determinization of a single class of w-automata. For this class of ω-automata with strong fairness as acceptance condition (Streett automata), [SV89] managed to show an exponential complementation procedure, but showed that the blow-up of the translation of these automata to any of the classes known to admit exponential determinization is inherently exponential. This might suggest that the blow-up of the determinization of Streett automata is inherently doubly exponential. Surprisingly, we show an exponential determinization construction for any Streett automaton. In fact, the complexity of our construction is roughly the same as the complexity achieved in [Saf88] for Buchi automata. Moreover, a simple observation extends this upper bound to the complexity of the complementation problem. Since any w-automaton that admits exponential determinization can be easily converted into a Streett automaton, we get one procedure that can be used for all of these conversions. This construction is optimal (up to a constant factor in the exponent) for all of these conversions. Our results imply that Streett automata (with strong fairness as acceptance condition) can be used instead of Buchi automata (with the weaker acceptance condition) without any loss of efficiency.