Efficient forward model checking algorithm for omega-regular properties
We present a symbolic language emptiness check algorithm based on forward state traversal. A verification property is given by a set of error traces written in omega-regular expression and is manipulated explicitly as a non-deterministic state transition graph. State space of the design model is implicitly traversed along the explicit graph. This method has a large amount of flexibility for controlling state traversal on the property space. It should become a good framework of incremental or approximate verification of omega-regular properties.
forward model checking language emptiness check omega-regular expression symbolic model checking formal verification