Complementation Constructions for Nondeterministic Automata on Infinite Words
=============================================================================

The complementation problem for nondeterministic automata on infinite
words has numerous applications in formal verification.
In particular, the language-containment problem, to which many
verification problems is reduced, involves complementation. 
Traditional optimal complementation constructions are quite complicated
and have not been implemented. Recently, we analyzed runs of
co-Büchi and generalized co-Büchi automata and used the analysis to 
describe simpler optimal complementation constructions for 
Büchi and generalized Büchi automata.
In this work, we extend the analysis to Rabin and Streett
automata, and use the analysis to describe novel, simple, and optimal 
complementation constructions for them.