Symbolic Model Checking Sample Clauses

Symbolic Model Checking. The model-checking procedure described so far relies on the assumption that the transition system has an explicit representation by the predecessor and successor lists per state. Such an enumerative representation is not adequate for very large transition systems. To counter the state explosion problem, the model-checking procedure can be reformulated in a sym- bolic way where sets of states and sets of transitions are represented rather than single states and transitions [111, 29]. More generally, we can call this approach to deal with the state explosion problem the method of using packed state spaces [139]. There are several possibilities to realize model checking algorithms in a packed state space stetting. The most prominent ones rely on a binary encoding of the states, which per- mits identifying subsets of the state space and the transition relation with switching functions. To obtain compact representations of switching functions, special data structures have been developed, such as ordered binary decision diagrams (OBDD) [111, 50, 29]. In this method, the state set, the transition relation over the set of states and the labeling function which assigns proposition sets onto states, all are encoded by OBDD models. Then the verifica- tion algorithms and tools have to be modified to work on the packed state spaces instead of ordinary ones. The efficiency and usefulness of the symbolic representation of the state space using OBDD models and their suitable verification algorithms are crucially dependent on the se- lected ordering over the set of boolean variables, which is fixed before constructing the OBDD models. It can be shown that for some switching function, using two different variable orderings produces OBDD structures whose sizes differ exponentially [29]. Since for many switching functions the OBDD sizes for different variable ordering can vary enormously, the efficiency of OBDD-based computations crucially relies on the use of techniques that im- prove a given variable ordering. However, the problem to find an optimal variable ordering is known to be computationally NP-hard [34]. Thus, the main problem with the symbolic model checking method is to find the best variable ordering.