# Hardware Model Checking Algorithms and Techniques
## 5 Interpolation-Based Model Checking
### Example of Interpolation-Based Model Checking  
Let \(\mathcal{M}=\langle V,\mathcal{I},T\rangle\) be a transition system described by the following:  
\[V=\{v_{0},v_{1},v_{2}\} \tag{53}\]  
\[\mathcal{I}=-v_{0}\wedge\
eg v_{1}\wedge\
eg v_{2} \tag{54}\]  
\[\begin{array}{l}T=(-v_{0}\wedge\
eg v_{1}\wedge\
eg v_{2}\wedge v^{\prime}_ {0}\wedge\
eg v^{\prime}_{1}\wedge\
eg v^{\prime}_{2})\vee\\ \qquad(v_{0}\wedge\
eg v_{1}\wedge\
eg v_{2}\wedge\
eg v^{\prime}_{0}\wedge \
eg v^{\prime}_{1}\wedge v^{\prime}_{2})\vee\\ \qquad(-v_{0}\wedge\
eg v_{1}\wedge v_{2}\wedge v^{\prime}_{0}\wedge\
eg v^{ \prime}_{1}\wedge v^{\prime}_{2})\vee\\ \qquad(v_{0}\wedge\
eg v_{1}\wedge v_{2}\wedge\
eg v^{\prime}_{0}\wedge \
eg v^{\prime}_{1}\wedge\
eg v^{\prime}_{2})\vee\\ \qquad(-v_{0}\wedge v_{1}\wedge\
eg v_{2}\wedge v^{\prime}_{0}\wedge v^{ \prime}_{1}\wedge\
eg v^{\prime}_{2})\vee\\ \qquad(v_{0}\wedge v_{1}\wedge\
eg v_{2}\wedge v^{\prime}_{0}\wedge v^{ \prime}_{1}\wedge v^{\prime}_{2})\vee\\ \qquad(v_{0}\wedge v_{1}\wedge v_{2}\wedge v^{\prime}_{0}\wedge v^{\prime}_{1 }\wedge v^{\prime}_{2})\vee\\ \qquad(-v_{0}\wedge v_{1}\wedge v_{2}\wedge v^{\prime}_{0}\wedge v^{\prime}_{1 }\wedge v^{\prime}_{2})\end{array} \tag{55}\]  
and \(P\) be an invariant property over \(V\):  
\[P=-v_{0}\vee\
eg v_{1}\vee\
eg v_{2} \tag{56}\]  
Figure 7 illustrates different steps of the procedure reported in Algorithms 4 and 5 over \(\mathcal{M}\). The ItpModelChecking procedure starts by checking whether or not the initial states \(\mathcal{I}\) are safe. In the case of the system at hand, the single initial state 000 satisfies \(P\); therefore, the procedure will continue by invoking ApproxForwardTraversal with \(k=1\). During the first iteration of the traversal procedure, \(R\) is set to the initial states \(\mathcal{I}\), \(A\) represents the image of \(\mathcal{I}\) and \(B\) corresponds to the negation of the property \(\
eg P\). Suppose that the interpolant \(I\) extracted at line 11 of Algorithm 5 is the one described in Figure 7a. \(I\) overapproximates the image of \(R\), comprising both states that are actually reachable from \(\mathcal{I}\), like 001, and states that are not reachable from \(\mathcal{I}\), like 010 and 011. Figure 7b describes the situation after the current set of reachable states \(R\) has been updated by disjoining it with the interpolant \(I\). During the second iteration of the traversal procedure, an intersection between the image of the current set of reachable states \(A\) and the bad states \(B\) will be found (state 111, as indicated by both the solid and the dash-dotted line enclosing it in Figure 7b). The traversal procedure will then halt reporting an Undef result: this is the case in which a spurious counterexample to the property has been found, due to the interpolant \(I\) being too loose an overapproximation of the states actually reachable from \(\mathcal{I}\), thus including a state (011) that is backward reachable from a bad state but not forward reachable from the initial states. The ItpModelChecking procedure will then resume by increasing \(k\) and invoking the traversal procedure once again with an enlarged cone of bad states. Figure 7c describes the situation during the first step of the new traversal, in which \(R\) and \(A\) are left unchanged whereas \(B\) is enlarged to include the pre-image of \(\
eg P\) (states 011 and 110). Suppose that a new interpolant \(I\) is extracted that includes only states 000, 001, 100 and 101; then, after updating the current set of reachable states \(R\) and performing a second traversal step, a fix-point will be reached as illustrated in Figure 7d. The overall model checking procedure will end with a Success result.