Relating omega-Regular Languages Defined By Various Automata.

Let LAMBDA and GAMMA be any of a variety of automata which define the omega-regular languages, such as the classical Buchi, Muller and Rabin automata. We show that a test for language containment L ( LAMBDA ) subset L ( GAMMA ) can be performed in time polynomial in the size of LAMBDA and GAMMA in most cases, when GAMMA is strongly deterministic.