Efficient forward model checking algorithm for omega-regular properties

We present a symbolic language emptiness check algorithm based on forward s tate traversal. A verification property is given by a set of error traces w ritten in omega-regular expression and is manipulated explicitly as a non-d eterministic state transition graph. State space of the design model is imp licitly traversed along the explicit graph. This method has a large amount of flexibility for controlling state traversal on the property space. It sh ould become a good framework of incremental or approximate verification of omega-regular properties.