Greedy Model Checking

TR-2000-2, Authors: Poul F. Williams and Antoine Rauzy

Poul Frederick Williams
Antoine Rauzy

October 2000

Abstract

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.