Directed Model Checking: It addresses the state explosion problem by using guided or heuristic search techniques during state space exploration (Edelkamp, Lluch-Lafuente, and Lee 2004; Edelkamp 2006). It borrows heavily from well-known AI techniques to enable the model checker to better home in on error states while searching just a portion of the state space, and thereby avoid the problem of state space explosion. There are numerousdifferent types of heuristics that may be used during directed model checking as illustrated below:
- Property-Specific Heuristics
- Structural Heuristics
- User-Guided Searches