On Simultaneously Determinizing and Complementing omega-Automata (Extended Abstract)
E. Allen Emerson, Charanjit S. Jutla · Logic in Computer Science · 1989
We give a construction to simultaneously de- terminize and complement a Buchi Automaton on Infinite strings, with an exponential blowup in states, and linear blowup in number of pairs. An exponential lower bound is already known. The previous best construction was do- uble exponential (Safra 88). This permits exponentially improved essentially optimal decision procedures for vari- ous Modal Logics of Programs. The new construction also gives exponentially improved conversions between various kinds of w-automata.