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.