# Hardware Model Checking Algorithms and Techniques
## 2 Background and Notation
### Symbolic Representation of Transition Systems
#### 2.11.2 Symbolic Representation of Transitions  
In order to symbolically represent transitions (a binary relation on states), we consider two sets of state variables: one to represent the starting state, called _present state_, and another to represent the final state, called _next state_, of a transition. The set \(V\) is used to encode present states while its primed counterpart \(V^{\prime}=\{v^{\prime}\mid v\in V\}\) is used to encode next states. The same primed notation is used to denote the set of next states \(S^{\prime}=\{s^{\prime}\mid s\in S\}\) and any propositional formula \(F^{\prime}=F[V\gets V^{\prime}]\) in which the present state variables have been renamed as the next state variables. Furthermore, we use the superscript notation \(V^{i}\) to denote the set of state variables encoding states at timeframe \(i\). The same superscript notation is used accordingly to denote the sets of states \(S^{i}\) after \(i\) transitions and any propositional formula \(F^{i}=F[V\gets V^{i}]\) referring to timeframe \(i\). We also use the notation \(\mathbf{\pi}^{i,j}\) as a shorthand for a truth assignment over \(V^{i}\cup\cdots\cup V^{\prime}\). **Definition 68** (Next State Encoding Function). : _Given a transition system \(\mathcal{TS}\), a set of present state variables \(V\) and a set of next state variables \(V^{\prime}\), let \(\phi\) be an encoding function over \(S\); we define the next state encoding function \(\phi^{\prime}\) as \(\phi^{\prime}=\phi[V\gets V^{\prime}]\)._  
We give the following definitions. **Definition 69** (Encoding of Transitions). : _A transition \((s,s^{\prime})\in R\) is encoded as a complete truth assignment \(\mu_{s,s^{\prime}}=\phi(s)\cup\phi^{\prime}(s^{\prime})\) over \(V\cup V^{\prime}\). The complete truth assignment \(\mu_{s,s^{\prime}}\) is called an encoding of \((s,s^{\prime})\) over \(V\cup V^{\prime}\)._  
Propositional formulas over \(V\cup V^{\prime}\) are used to represent sets of transitions. Any propositional formula \(F_{Z}\) over \(V\cup V^{\prime}\) represents the set of transitions \(Z\subseteq R\) such that, for each \((z,z^{\prime})\in Z\), its corresponding encoding \(\mu_{z,z^{\prime}}\) over \(V\cup V^{\prime}\) satisfies \(F_{Z}\), i.e., \(\mu_{z,z^{\prime}}\models F_{Z}\). Given the encoding function \(\phi\) and a next state encoding function \(\phi^{\prime}\), and letting \((z,z^{\prime})\in R\) be a transition of \(\mathcal{TS}\), many logically equivalent propositional formulas over \(V\cup V^{\prime}\) can be used to represent \((z,z^{\prime})\). We define one example of such a formula as follows. **Definition 70** (Characteristic Formula for Transitions). : _The characteristic formula of \((z,z^{\prime})\) is the propositional formula \(\tilde{\zeta}_{z,z^{\prime}}\) over \(V\cup V^{\prime}\) such that_  
\[\tilde{\zeta}_{z,z^{\prime}}\overset{def}{=}\bigwedge_{v_{i}\in V\cup V^{ \prime}}l_{i}\;\;\text{where}\;\; \begin{cases}l_{i}=v_{i},&\text{iff}\;\mu_{z,z ^{\prime}}(v_{i})=\top\\ l_{i}=\
eg v_{i},&\text{iff}\;\mu_{z,z^{\prime}}(v_{i})=\bot\end{cases}  \tag{27}\]  
_where \(\mu_{z,z^{\prime}}=\phi(z)\cup\phi^{\prime}(z^{\prime})\)._  
Note that \(\tilde{\zeta}_{z,z^{\prime}}\) is satisfied only by the complete truth assignment \(\mu_{z,z^{\prime}}\) encoding \((z,z^{\prime})\). Let \(Z\subseteq R\) be a set of transitions of \(\mathcal{TS}\). Many logically equivalent propositional formulas over \(V\cup V^{\prime}\) can be used to represent \(Z\). We define one example of such a formula as follows. **Definition 71** (Characteristic Formula for Sets of Transitions). : _The characteristic formula of \(Z\) is the propositional formula \(\xi_{Z}\) over \(V\cup V^{\prime}\) such that_  
\[\xi_{Z}\overset{def}{=}\bigvee_{(z,z^{\prime})\in P}\xi_{z,z^{\prime}} \tag{28}\]  
Note that \(\xi_{Z}\) over \(V\cup V^{\prime}\) is satisfied only by the complete truth assignments \(\mu_{z,z^{\prime}}\) over \(V\cup V^{\prime}\) encoding transitions \((z,z^{\prime})\in Z\).