# Hardware Model Checking Algorithms and Techniques
## 2 Background and Notation
### Symbolic Representation of Transition Systems
#### 2.12 Symbolic Invariant Verification  
As shown in Section 2.10, the invariant verification problem can be reduced to a problem of reachability in a transition system. Reachability in a transition system (or equally invariant verification) can, in turn, be reduced to reachability in a corresponding symbolic transition system, as follows. **Theorem 3** (Symbolic Invariant Verification). : _Given a transition system \(\mathcal{TS}=\langle S,S_{0},R,AP,L\rangle\) and an invariant property \(\psi\) with invariant condition \(\varphi\) over \(AP\), the reachability problem of \(\
eg\varphi\) in \(\mathcal{TS}\) can be reduced to the reachability problem of \(\
eg P\) in \(\mathcal{M}\) where \(\mathcal{M}=\langle V,\mathcal{I},T\rangle\) is a symbolic transition system encoding \(\mathcal{TS}\) and \(P\) a symbolic invariant property encoding \(\varphi\)._  
In this paper, we are interested in algorithms for symbolic invariant verification. Therefore, with abuse of notation, we hereinafter use the terms \"transition system\", \"reachability\", \"invariant property\" and \"invariant verification\" to denote their symbolic counterparts. **Notation 5** (Target and Bad States). : _Given a transition system \(\mathcal{M}=\langle V,\mathcal{I},T\rangle\) and an invariant property \(P\), with the notion of target we identify set of states corresponding to \(\
eg P\). States (or sets of states) which are part of the target, or may reach the target, are called bad states._  
Given a transition system \(\mathcal{M}=\langle V,\mathcal{I},T\rangle\) and an invariant property \(P\), we provide the following useful definitions for invariant verification algorithms. **Definition 76** (Path Formula). : _A path formula of length \(k=j-i\), starting from timeframe \(i\) and reaching timeframe \(j\), is the propositional formula \(\Pi(i,j)\) over \(V^{i}\cup\cdots\cup V\):_  
\[\Pi(i,j)=\bigwedge_{h=i}^{j-1}T(V^{h},V^{h+1}) \tag{40}\]  
**Definition 77** (Initial Path Formula). : _An initial path formula of length \(k\) is the following propositional formula:_  
\[\Pi_{0}(k)=\mathcal{I}(V^{0})\wedge\Pi(0,k) \tag{41}\]  
Intuitively, a path formula \(\Pi(i,j)\) encodes all paths of length \(k=j-i\) starting at timeframe \(i\) in \(\mathcal{M}\). An initial path formula \(\Pi_{0}(k)\) encodes all paths of length \(k\) starting from the initial states in \(\mathcal{M}\). An initial path formula \(\Pi_{0}(k)\) can thus be used to represent the set of states that can be reached from the initial states in exactly \(k\) steps, in \(\mathcal{M}\). **Definition 78** (Bad Cone). : _A bad cone of length \(k=j-i\) from timeframe \(i\) to timeframe \(j\) is the propositional formula \(\mathit{Cone}(i,j)\) over \(V^{i}\cup\cdots\cup V^{j}\):_  
\[\mathit{Cone}(i,j)=\Pi(i,j)\wedge\bigvee_{h=i}^{j}\
eg P(V^{h}) \tag{42}\]  
A bad cone \(\mathit{Cone}(i,j)\) encodes all paths starting at timeframe \(i\) that can reach the target in at most \(k=j-i\) steps and, thus, it represents the set of bad states that are backward reachable in at most \(k\) steps from the target. Using initial path formulas the reachability problem of \(\
eg P\) in \(\mathcal{M}\) can be reduced to Boolean satisfiability as follows. **Theorem 4** (Reduction of Reachability to Satisfiability). : _Given a transition system \(\mathcal{M}\stackrel{{\text{def}}}{{=}}\langle V,\mathcal{I},T\rangle\) and a property \(P\) over \(V\), the reachability of \(\
eg P\) can be reduced to the problem of finding a bound \(k\geq 0\) such that the propositional formula_  
\[\Pi_{0}(k)\wedge\
eg P(V^{k}) \tag{43}\]  
_is satisfiable._  
**Definition 79** (Induction).