# Hardware Model Checking Algorithms and Techniques
## 2 Background and Notation
### Symbolic Representation of Transition Systems
#### 2.11.1 Symbolic Representation of States  
In order to symbolically represent the set of states \(S\) of a transition system \(\mathcal{TS}\), we introduce a set of propositional variables \(V\), called _state variables_, with \(|V|=\lceil log_{2}|S|\rceil\). Given a transition system \(\mathcal{TS}=\langle S,S_{0},R,AP,L\rangle\) and a set of state variables \(V\), we give the following definitions. **Definition 64** (Encoding Function). : _An encoding function \(\phi:S\rightarrow\mathbb{B}^{|V|}\) over \(V\) is an injective function mapping states to complete truth assignments over \(V\)._  
**Definition 65** (Encoding of States). : _A state \(s\in S\) is encoded as a complete truth assignment \(\mu_{s}=\phi(s)\) over \(V\) according to an encoding function \(\phi\). The complete truth assignment \(\mu_{s}\) is called encoding of \(s\) over \(V\)._Note that \(\phi\) is bijective if and only if \(|S|=2^{|V|}\). Otherwise, some pseudo-state representations are introduced in the symbolic representation of \(S\) by encoding. Such pseudo-states can be disregarded and treated as unreachable states of \(\mathcal{TS}\). Propositional formulas over \(V\) are used to represent sets of states. Any propositional formula \(F_{Q}\) over \(V\) represents the set of states \(Q\subseteq S\) such that, for each state \(q\in Q\), its corresponding encoding \(\mu_{q}\) over \(V\) satisfies \(F_{Q}\), i.e., \(\mu_{q}\models F_{Q}\). Given an encoding function \(\phi\) over \(V\), and letting \(q\in S\) be a state of \(\mathcal{TS}\), many logically equivalent propositional formulas over \(V\) can be used to represent \(q\). We define one example of such a formula as follows. **Definition 66** (Characteristic Formula for States). : _The characteristic formula of \(q\) is the propositional formula \(\xi_{q}\) over \(V\) such that_  
\[\xi_{q}\stackrel{{ def}}{{=}}\bigwedge_{v_{i}\in V}l_{i}\;\;\text{ where}\;\; \begin{cases}l_{i}=v_{i},&\text{iff}\;\mu_{q}(v_{i})=\top\\ l_{i}=\
eg v_{i},&\text{iff}\;\mu_{q}(v_{i})=\bot\end{cases}  \tag{22}\]  
_where \(\mu_{q}=\phi(q)\)._  
Note that \(\xi_{q}\) is a cube and it is satisfied only by the complete truth assignment \(\mu_{q}\) encoding \(q\). Let \(Q\subseteq S\) be a set of states; many logically equivalent propositional formulas over \(V\) can be used to represent \(Q\). We define one example of such a formula as follows. **Definition 67** (Characteristic Formula for Set of States). : _The characteristic formula of \(Q\) is the propositional formula \(\xi_{Q}\) over \(V\) such that_  
\[\xi_{Q}\stackrel{{ def}}{{=}}\bigvee_{q\in Q}\xi_{q} \tag{23}\]  
Note that \(\xi_{Q}\) is satisfied only by the complete truth assignments \(\mu_{q}\) encoding states \(q\in Q\). With abuse of notation, hereinafter, we make no distinction among the following concepts:  
* A state \(s\in S\), any propositional formula \(F_{s}\) that is logically equivalent to its characteristic formula \(\xi_{s}\) and the only model for such formula \(\mu_{s}\). * A set of states \(Q\subseteq S\), any propositional formula \(F_{Q}\) that is logically equivalent to its characteristic formula \(\xi_{Q}\) and the set of models for such formula \(\text{Mods}(F_{Q})=\{\mu_{q}\mid q\in Q\}\). Initial states \(S_{0}\subseteq S\) of \(\mathcal{TS}\) can be represented symbolically by a propositional formula \(\mathcal{I}\) such that the encodings \(\mu_{s_{0}}\) over \(V\) of each initial state \(s_{0}\in S_{0}\) satisfy \(\mathcal{I}\). **Example 6**.