Greedy Model Checking
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
PostScript(gzip'ed),
PostScript,
PDF, and
BibTeX.