Symbolic search solves state space problems consisting of an initial state, a set of goal states, and a set of actions using a succinct representation for state sets. The approach lessens the costs associated with the exponential memory requirements for the state sets involved as problem sizes get bigger. Symbolic search has been associated with the term planning via model checking (Giunchiglia and Traverso 1999). While initially applied to model check hardware verification problems (McMillan 1993), symbolic search features many modern action planning systems (Ghallab et al. 2000). Symbolic search algorithms explore the underlying problem graph by using functional expressions to represent sets of states and actions. Compared with the space requirements induced by standard explicit-state search algorithms, symbolic representations additionally save space by sharing parts of the state vector. Algorithm designs change, as not all search algorithms adapt to the exploration of state sets.
A methodology for hardware verification using compositional model checking
