Greedy Model Checking

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.