SAT-based Bounded Model Checking for SE-LTL

For concurrent software systems state/event linear temporal logic SE-LTL is a specification language with high expressive power and the ability to reason about both states and events. Until now, SE-LTL model checking algorithm is still explicit. We introduce a bounded model checking procedure for SE-LTL which reduces model checking to propositional satisfiability. This new technique avoids the space blow up of BDDs, generates counterexamples much faster, and sometimes speeds up the verification. For SE-LTL-_x we further show how to integrate the procedure and stuttering equivalent technique. The experiment result shows that the integration can reduce the verification time very much.