C.5 Symbolic Model Checking 567
As another example let us check the formula AFgreen. Initially s
1
is assigned to
the variable NextStates, but at the first iteration pre-img-af returns the empty set,
then the loop terminates and the algorithm returns False.
C.5 Symbolic Model Checking
Most often, realistic models of systems need huge numbers of states. For exam-
ple, an interlocking system may have something like 10
200
states. Symbolic model
checking [99] has been devised to deal with large state spaces. It is a form of
model checking in which propositional formulas are used for the compact rep-
resentation of finite-state models, and transformations over propositional formulas
provide a basis for efficient exploration of the state space. Most often, the ...