Efficient omega-Language Containment

One method for proving properties about a design is by using L-automata (Kur90). The main computation involves building the product machine of the system and specification, and then checking for cycles not contained in any of the cycle sets (these are sets of states specified by the user). In (Tou91) two methods were introduced for performing the above task; by computing the transitive closure of the product machine, and an application of a method due to Emerson-Lei ([Eme86]).