# Hardware Model Checking Algorithms and Techniques
## 2 Background and Notation
### Model Checking Problem  
Let \(\mathcal{TS}=\langle S,S_{0},R,AP,L\rangle\) be a transition system; the model checking problem can be formalized as follows:  
**Definition 58** (Model Checking Problem). : _Given a transition system \(\mathcal{TS}\) and a temporal property \(\psi\) over \(AP\), the decision problem to check whether \(\mathcal{TS}\models\psi\) is called a model checking problem. In the case \(\mathcal{TS}\
ot\models\psi\), the model checking procedure is required to provide a counterexample._  
**Definition 59** (Counterexample). : _Given a transition system \(\mathcal{TS}\) and a temporal property \(\psi\) over \(AP\) such that \(\mathcal{TS}\
ot\models\psi\), a counterexample to \(\psi\) for \(\mathcal{TS}\) is any initial path \(\pi\) of \(\mathcal{TS}\) such that \(\pi\
ot\models\psi\)._  
Model checking is therefore a decision problem, as defined in Section 2.6, that admits a Yes-answer (\(\psi\) holds for \(\mathcal{TS}\)) or a No-answer (\(\psi\) does not hold for \(\mathcal{TS}\)). **Definition 60** (Model Checking Algorithm). : _A model checking algorithm, or model checker, is any decision procedure able to solve a model checking problem._  
When a model checking algorithm terminates with a No-answer, it must also emit a No-certificate in the form of a counterexample. Model checking algorithms must systematically traverse all behaviors of the system in order to either confirm that the property holds or provide a counterexample. A model checking algorithm may have either or both of the following qualities. **Definition 61** (Completeness and Soundness (of a Model Checking Algorithm)). : _A model checking algorithm is said to be complete iff, given a transition system \(\mathcal{TS}\) and a property \(\psi\), it is able to either provide a counterexample of \(\psi\) for \(\mathcal{TS}\) or detect the absence of counterexamples of any length. A model checking algorithm is said to be sound iff, given a transition system \(\mathcal{TS}\) and a property \(\psi\), it provides a counterexample of \(\psi\) for \(\mathcal{TS}\) only when \(\mathcal{TS}\
ot\models\psi\) and it proves the absence of counterexamples of any length only when \(\mathcal{TS}\models\psi\)._  
Different classes of model checking problems can be distinguished, depending on the category of temporal properties being checked. In this paper, we are interested only in the model checking of invariant properties, also called _invariant verification problems_, which we show can be solved via reachability analysis on the transition system under verification. **Definition 62** (Invariant Verification Problem). : _Given a transition system \(\mathcal{TS}\) and an invariant property \(\psi\) over \(AP\), the invariant verification problem of \(\psi\) for \(\mathcal{TS}\) is the model checking problem to decide \(\mathcal{TS}\models\psi\) or to provide a counterexample._  
**Definition 63** (Invariant). : _Given a transition system \(\mathcal{TS}\) and an invariant property \(\psi\) over \(AP\), if \(\mathcal{TS}\models\psi\), then the invariant condition \(\varphi\) of \(\psi\) is a propositional formula over \(AP\) and is said to be an invariant of \(\mathcal{TS}\)._  
The invariant verification problem can be reduced to a reachability problem over \(\mathcal{TS}\), as follows. **Theorem 2** (Reduction of Invariant Verification to Reachability). : _Given a transition system \(\mathcal{TS}\) and an invariant property \(\psi\) over \(AP\), let \(\varphi\) over \(AP\) be the invariant condition of \(\psi\); then, the invariant verification problem can be reduced to the problem to check whether a state \(s\in S\) such that \(s\models\varphi\) is reachable in \(\mathcal{TS}\). If that is the case, \(\mathcal{TS}\
ot\models\psi\) and any initial path to \(s\) is a counterexample for the invariant verification problem. Otherwise, \(\mathcal{TS}\models\psi\).