# Hardware Model Checking Algorithms and Techniques
## 2 Background and Notation
### Symbolic Representation of Transition Systems
#### 2.12 Symbolic Invariant Verification
: _Given a transition system \(\mathcal{M}=\langle V,\mathcal{I},T\rangle\), let \(F\) and \(G\) be propositional formulas over \(V\) and let initiation, consecution and relative consecution be the conditions defined as follows:_  
\[\mathcal{I}\to F\] ( _Initiation_ ) \[F\wedge T\to F^{\prime}\] ( _Consection_ ) \[G\wedge F\wedge T\to F^{\prime}\] ( _Relative Consection_ )  
_A formula \(F\) is said to be inductive if it satisfies consecution. A formula \(F\) is said to be an inductive invariant if it satisfies both initiation and consecution. A formula \(F\) is said to be inductive relative to another formula \(G\) if it satisfies relative consecution. A formula \(F\) is said to be an inductive invariant relative to another formula \(G\) if it satisfies both initiation and relative consecution._  
**Definition 80** (Safety). : _Given a transition system \(\mathcal{M}=\langle V,\mathcal{I},T\rangle\) and an invariant property \(P\) over \(V\), a propositional formula \(F\) over \(V\) is said to be safe with respect to \(F\) iff \(F\) is stronger than \(P\), i.e., \(F\to P\)._  
**Lemma 1** (Inductive Invariants as Overapproximations of Reachable States). : _Given a transition system \(\mathcal{M}=\langle V,\mathcal{I},T\rangle\), an inductive invariant \(F\) of \(\mathcal{M}\) is an overapproximation of the set of reachable states of \(\mathcal{M}\), i.e., \(\mathcal{R}(\mathcal{M})\to F\)._  
Intuitively, an inductive invariant expresses a quality of reachable states. Note that \(\mathcal{R}(\mathcal{M})\) can be seen as the strongest inductive invariant of \(\mathcal{M}\). **Definition 81** (Inductive Strengthening). : _Given a transition system \(\mathcal{M}=\langle V,\mathcal{I},T\rangle\) and a property \(P\) over \(V\), an inductive invariant \(F\) of \(\mathcal{M}\) is called an inductive strengthening of \(P\) iff it is safe with respect to \(P\)._  
**Lemma 2** (Invariant Verification as Search of an Inductive Strengthening). : _Given a transition system \(\mathcal{M}=\langle V,\mathcal{I},T\rangle\) and a property \(P\) over \(V\), if an inductive strengthening \(F\) of \(P\) can be found in \(\mathcal{M}\), then \(P\) holds for every reachable state of \(\mathcal{M}\) and \(\mathcal{M}\) is said to be safe._  
Many state-of-the-art model checking algorithms are based on a search for an inductive strengthening. **Definition 82** (Traces). : _Given a transition system \(\mathcal{M}=\langle V,\mathcal{I},T\rangle\), a trace of length \(k\) with respect to \(\mathcal{M}\) is a sequence \(\mathbf{F_{k}}=(F_{0},\ldots,F_{k})\) in which each \(F_{i}\) is a propositional formula over \(V\), called a frame, such that the following conditions hold:_  
\[F_{0}=\mathcal{I}\] ( _Base_ ) \[F_{i}\wedge T\to F_{i+1}^{\prime}\text{ for }0\leq i<k\] ( _Image Approximation_ )  
_A trace \(\mathbf{F_{k}}\) may also satisfy one or both of the following additional conditions, with \(P\) a property over \(V\):_  
\[F_{i}\to F_{i+1}\text{ for }0\leq i<k\] ( _Monotonicity_ ) \[\Pi_{0}(k)=\mathcal{I}(V^{0})\wedge\Pi(0,k) \tag{41}\]0 ( _Safety_ )  
A trace \(\mathbf{F_{k}}\) that satisfies the monotonicity condition is said to be _monotonic_. A trace \(\mathbf{F_{k}}\) that satisfies the safety condition with respect to the transition system \(P\) is said to be _safe_. In order to provide a more clear understanding of the various traces natures, Figure 4 provides a graphical representation as an overview. The following lemmas hold for traces. **Lemma 3** (Overapproximation of Sets of Exactly Reachable States). : _Given a transition system \(\mathcal{M}\) and a trace \(\mathbf{F_{k}}=(F_{0},\ldots,F_{k})\) with respect to \(\mathcal{M}\), each timeframe \(F_{i}\) of \(\mathbf{F_{k}}\), with \(0\leq i<k\), is an over-approximation of the set of states reachable in exactly \(i\) steps in \(\mathcal{M}\), i.e., \(\mathcal{R}_{i}^{E}(\mathcal{M})\to F_{i}\)._  
**Lemma 4** (Overapproximation of Sets of Reachable States).