# Hardware Model Checking Algorithms and Techniques
## 2 Background and Notation
### Temporal Logics
#### 2.9.1 Linear Temporal Logic  
Linear Temporal Logic (LTL) was introduced by [PERSON] [34] for the specification and verification of reactive systems. Formulas of LTL are constructed from a set of _propositional variables AP_ using the usual _logical connectives_ (negation \(\
eg\), conjunction \(\land\) and disjunction \(\lor\)) and some _temporal operators_**X** (\"next time\"), **F** (\"eventually\"), **G** (\"always\") and **U** (\"until\"). LTL formulas are interpreted in terms of paths, i.e., sequences of states of a transition system. Their semantics is also extended to states and whole transition systems. **Definition 46** (Syntax of LTL Formulas). : _Given a set of propositional variables \(AP\), the syntax of LTL formulas is defined inductively as follows._  
* _Boolean constants_ \(\top\) _and_ \(\bot\) _are LTL formulas._
* _Each_ \(a\in AP\) _is an LTL formula._
* _Given_ \(\psi\)_, an LTL formula_ \(\
eg\psi\) _is an LTL formula._
* _Given_ \(\psi_{1}\) _and_ \(\psi_{2}\)_, LTL formula_ \(\psi_{1}\wedge\psi_{2}\) _is an LTL formula._
* _Given_ \(\psi_{1}\) _and_ \(\psi_{2}\)_, LTL formula_ \(\psi_{1}\vee\psi_{2}\) _is an LTL formula._
* _Given_ \(\psi\)_, an LTL formula_ \(\mathbf{X}\psi\) _is an LTL formula._
* _Given_ \(\psi\)_, an LTL formula_ \(\mathbf{F}\psi\) _is an LTL formula._
* _Given_ \(\psi\)_, an LTL formula_ \(\mathbf{G}\psi\) _is an LTL formula._
* _Given_ \(\psi_{1}\) _and_ \(\psi_{2}\)_, LTL formula_ \(\psi_{1}\mathbf{U}\psi_{2}\) _is an LTL formula._  
Note that \(\bot\) and \(\vee\) can be omitted from Definition 46 without losing expressiveness as they can be easily derived from \(\top\), \(\
eg\) and \(\wedge\). Similarly, \(\mathbf{F}\) and \(\mathbf{G}\) can also be omitted, as they can be derived from \(\mathbf{X}\) and \(\mathbf{U}\) as \(\mathbf{F}\psi\stackrel{{\text{def}}}{{=}}\top\mathbf{U}\psi\) and \(\mathbf{G}\psi\stackrel{{\text{def}}}{{=}}\
eg\mathbf{F}\
eg\psi\). Furthermore, the syntax can be extended to other common Boolean operators by means of their usual definitions in Propositional Logic. **Example 3**. : _Given the hardware design and its transition system described in Example 1, we can model the specification describing how the system will never reach a state in which the output of both flip flops is high as the following property in LTL logic:_  
\[\psi=\
eg\mathbf{F}(a_{0}\wedge a_{1}) \tag{18}\]  
Intuitively, the semantics of the temporal operators of LTL is the following: \(\mathbf{X}\psi\) holds at the current moment if \(\psi\) holds at the next moment; \(\mathbf{F}\psi\) holds at the current moment if there is a future moment at which \(\psi\) holds; \(\mathbf{G}\psi\) holds at the current moment if \(\psi\) holds at the current moment and at every future moment; \(\psi_{1}\mathbf{U}\psi_{2}\) holds at the current moment if there is some future moment at which \(\psi_{2}\) holds and \(\psi_{1}\) holds at each moment until that future moment. Formally, the semantics of LTL formulas is defined with respect to paths, states and transition systems, as follows. **Definition 47** (Semantics of LTL Formulas with Respect to Paths). : _Given a transition system \(\mathcal{TS}\stackrel{{\text{def}}}{{=}}\langle S,S_{0},R,AP,L\rangle\), let \(\boldsymbol{\pi}=(s_{0},s_{1},\dots)\) be an infinite path in \(\mathcal{TS}\) and let \(\psi\) be an LTL formula over \(AP\).