# Hardware Model Checking Algorithms and Techniques
## 2 Background and Notation
### Transition Systems  
Transition systems are often used in computer science as models to describe the behavior of real-world systems. They can be seen as directed graphs, with nodes representing _states_ and edges representing _transitions_. A state describes some unique configuration of information about a given system at a certain moment of its behavior. Transitions specify how the system can evolve from one state to another. **Definition 36** (Transition System). : _A transition system (also known in the literature as a Kripke structure [33]) is a tuple \(\mathcal{TS}\stackrel{{\mbox{\tiny{\it def}}}}{{=}}\langle S,S_{0},R,AP,L\rangle\), where \(S\) is the set of states, \(S_{0}\subseteq S\) is the set of initial states, \(R\subseteq S\times S\) is the transition relation, \(AP\) is a set of propositional variables representing atomic propositions and \(L:S\to 2^{AP}\) is a labeling function._  
For each state \(s\in S\), the labeling function \(L(s)\) denotes the set of atomic propositions that hold in \(s\). A transition system can be either _finite_ or _infinite_, depending on whether or not it admits an infinite set of states (and consequently transitions). In this paper, we are interested in the model checking of bit-level hardware sequential circuits. Since the behavior of such systems can be modeled using finite transition systems, we restrict the discussion to those models. For this reason, we hereinafter use the term _transition system_ as a shorthand for _finite transition systems_ without risk of ambiguity. **Example 1**. : _The sequential hardware system described in Figure 2(a), representing a 2-bit synchronous counter that counts up to 2, can be modeled as the following transition system:_  
\[\mathcal{TS} =\langle S,S_{0},R,AP,L\rangle \tag{9}\] \[S =\{s_{0},s_{1},s_{2},s_{3}\}\] (10) \[S_{0} =\{s_{0}\} \tag{11}\]\[R=\{(s_{0},s_{1}),(s_{1},s_{2}),(s_{1},s_{0}),(s_{3},s_{2})\} \tag{12}\]  
\[AP=\{a_{0},a_{1}\} \tag{13}\]  
\[L=\{(s_{0},\mathcal{O}),(s_{1},\{a_{0}\}),(s_{2},\{a_{1}\}),(s_{3},\{a_{0},a_{1} \})\} \tag{14}\]  
_States \(S=\{s_{0},s_{1},s_{2},s_{3}\}\) represent the four possible states of the counter, corresponding to the combined digital values of the two flip flops; \(s_{0}\) represent the reset state of the system, in which the output of both flip flops is low, \(R\) indicates how the system will transition between states at each clock cycle and the labeling function \(L\) maps each state to a set of atomic propositions in \(AP=\{a_{0},a_{1}\}\) each indicating that either \(Q_{0}\) or \(Q_{1}\) is high, respectively. The transition system is visualized in Figure 3b. We will use this system and its model as a running example in the rest of the section._  
Let \(\mathcal{TS}=\langle S,S_{0},R,AP,L\rangle\) be a transition system; we provide the following useful definitions. **Definition 37** (Transition). : _A transition in \(\mathcal{TS}\) is a pair of states \((s_{1},s_{2})\) such that \((s_{1},s_{2})\in R\)._  
**Definition 38** (Successor and Predecessor States). : _Given a pair of states \((p,s)\), \(p\) is said to be a predecessor of \(s\) iff \((p,s)\) is a transition in \(\mathcal{TS}\). Vice versa, \(s\) is said to be a successor of \(p\)._  
**Definition 39** (Paths). : _A path in \(\mathcal{TS}\) is any sequence of states \(\boldsymbol{\pi}=(s_{0},s_{1},\dots)\) of arbitrary (event infinite) length \(|\boldsymbol{\pi}|\) such that \((s_{i},s_{i+1})\) is a transition in \(\mathcal{TS}\) for each \(0\leq i<|\boldsymbol{\pi}|\). A path \(\boldsymbol{\pi}\) is said to be finite if \(|\boldsymbol{\pi}|\in\mathbb{N}\); otherwise, it is said to be infinite. We denote by \(\boldsymbol{\pi}_{i}=(s_{i},s_{i+1},\dots)\) the suffix of \(\boldsymbol{\pi}\) starting with the \((i+1)\)-th state of \(\boldsymbol{\pi}\). We also denote by \(\boldsymbol{\pi}[i]\) the \((i+1)\)-th state in \(\boldsymbol{\pi}\)._  
**Definition 40** (Initial Paths).