Greedy Model Checking
TR-2000-2, Authors: Poul F. Williams and Antoine Rauzy Poul Frederick Williams
We present a model checking method which greedily explores the state space. Using ideas similar to greedy satisfiability checking, our method tries to fit a path to match a temporal specification. The advantages of this method is that we do not need any quantifications, we do not calculate a reachable (neither forward nor backward) set of states, and the memory requirements are quite small.
Technical report TR-2000-2 in IT University Technical Report Series, October 2000.
Available as PDF.