TY - RPRT
T1 - Greedy Model Checking
AU - Williams, Poul Frederick
AU - Rauzy, Antoine
PY - 2000/10
Y1 - 2000/10
N2 - 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.
AB - 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.
M3 - Report
T3 - IT University Technical Report Series
BT - Greedy Model Checking
PB - IT-Universitetet i København
CY - Copenhagen
ER -