# Hardware Model Checking Algorithms and Techniques
## 4 Temporal Induction  
BMC, introduced in Section 3, is characterized by being an incomplete method: it is capable of finding counterexamples but it is unsuitable to prove correctness. In order to support proofs for unbounded depths, BMC has to be complemented with additional techniques. As an intuition, if exploration is capable of reaching a deep enough bound, such as to have explored all the behavior of the model at hand, such a bound could be considered a so-called completeness threshold. Such a threshold can be used as an upper bound for the length of the counterexamples that have to be considered before stating whether a proof holds. Figure 5: Visualization of states in a transition system \(\mathcal{M}\). States are labeled with their corresponding truth-value assignments to state variables \(V\). In the context of model checking, SAT-based techniques are particularly suitable for performing checks of inductions, i.e., whether the transition system of the model under verification satisfies a given inductive invariant. The underlying question we are posing is whether a given property holds in the initial states and in all the states reachable from states in which the property is satisfied. The main limitation of such reasoning is due to the fact that, if the second condition fails, nothing can be said about the property at hand. On these premises, temporal induction [39], also known as strong induction or \(k-\)induction, represents a widely used technique in unbounded model checking. Such a technique is a generalization of the notion of inductive invariants, which provide a strengthening factor to the base intuition presented above. Given a transition system \(\mathcal{M}=\langle V,\mathcal{I},T\rangle\) and an invariant formula \(\varphi\) over \(V\), that formula is said to be \(k-\)invariant if it is true in the first \(k\) steps of \(\mathcal{M}\). **Definition 84** (\(k\)-invariant formula). : \[\Pi_{0}(k)\to\bigwedge_{i=0}^{k}\varphi(V^{i})\] (52)  
A \(k\)-invariant formula is a \(k\)-inductive invariant if it is \((k-1)\)-invariant and is inductive after \(k\) steps of \(\mathcal{M}\). With respect to simple induction, \(k-\)induction strengthen the hypothesis in the induction step. We have that the property is assumed to hold in the first \(k-1\) steps, starting from \(0\), and is established in step \(k\). Whenever we have a \(k\)-invariant formula \(\varphi\) such that \(\varphi\to P\), we say that \(\varphi\) is a safe \(k-\)inductive invariant with respect to \(\mathcal{M}\). Algorithm 3 reports the top-level procedure for a generic \(k\)-induction model checking scheme. First, the algorithm checks whether the property \(P\) is satisfied by the initial states (lines 3-4). If an initial state fails to satisfy \(P\), the procedure terminates by returning Fail along with a trivial counterexample (lines 5-6). Otherwise, the procedure starts iterating over increasing values of \(k\), checking whether there is at least a path satisfying the induction step formula up to bound \(k\) (line 7), and taking into account only non-looping paths (line 8). If a satisfying path is found, the procedure returns Success (lines 9-10), otherwise the bound \(k\) is increased and the procedure iterates further. ```
0:\(\mathcal{M}=\langle V,\mathcal{I},T\rangle\) a transition system; \(P\) a property over \(V\). 0:\(\langle\mathit{res},\mathit{cex}\rangle\) with \(\mathit{res}\in\{\textsc{Success},\textsc{fail}\}\); \(\mathit{cex}\) a (possibly empty) initial path representing a counterexample.