Efficient ω-regular language containment

Abstract

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; one involves computing the transitive closure of the product machine, and the other is an application of a method due to Emerson-Lei ([Eme86]). We have implemented both methods and extended them. We introduce a few generalpurpose operators on graphs and use them to construct efficient algorithms for the above task. Fast special checks are applied to find bad cycles early on. Initial experimental results are encouraging and are presented here.