An Improved Lower Bound for the Complementation of Rabin Automata

Automata on infinite words (omega-automata) have wide applications in formal language theory as well as in modeling and verifying reactive systems. Complementation of omega-automata is a crucial instrument in many these applications, and hence there have been great interests in determining the state complexity of the complementation problem. However, obtaining nontrivial lower bounds has been difficult. For the complementation of Rabin automata, a significant gap exists between the state-of-the-art lower bound 2^Omega(NlgN) and upper bound 2^O(kNlgN), where k, the number of Rabin pairs, can be as large as 2^N. In this paper we introduce multidimensional rankings to the full automata technique. Using the improved technique we establish an almost tight lower bound for the complementation of Rabin automata. We also show that the same lower bound holds for the determinization of Rabin automata.