# Hardware Model Checking Algorithms and Techniques
## 2 Background and Notation
### Temporal Logics
#### 2.9.2 Computation Tree Logic  
Computation Tree Logic (CTL) was introduced by [PERSON] et al. [35] to overcome the semantics limitation of LTL. In CTL, two kinds of formulas are distinguished: _state formulas_ and _path formulas_. CTL also introduces two new temporal operators, called _path quantifiers_ to allow the specification of properties for some or all the paths starting from a state. These quantifiers are **A** (\"for all paths\") and **E** (\"there exists a path\"). CTL formulas are interpreted in terms of trees of paths, i.e., possible alternative paths of a transition system. Their semantics is also extended to states and whole transition systems. **Definition 50** (Syntax of CTL Formulas). : _Given a set of propositional variables \(AP\), the syntax of CTL state formulas is defined inductively as follows._  
* _Boolean constants_ \(\top\) _and_ \(\bot\) _are CTL state formulas._
* _Each_ \(a\in AP\) _is a CTL state formula._
* _Given_ \(\psi\)_, a CTL state formula_ \(\
eg\psi\) _is a CTL state formula._
* _Given_ \(\psi_{1}\) _and_ \(\psi_{2}\)_, CTL state formula_ \(\psi_{1}\wedge\psi_{2}\) _is a CTL state formula._
* _Given_ \(\psi_{1}\) _and_ \(\psi_{2}\)_, CTL state formula_ \(\psi_{1}\vee\psi_{2}\) _is a CTL state formula._
* _Given_ \(\varphi\)_, a CTL path formula_ \(\textbf{A}\varphi\) _is a CTL state formula._
* _Given_ \(\varphi\)_, a CTL path formula_ \(\textbf{E}\varphi\) _is a CTL state formula._  
_The syntax of CTL path formulas is defined inductively as follows:_  
* _Given_ \(\psi\)_, a CTL state formula_ \(\textbf{X}\psi\) _is a CTL path formula._
* _Given_ \(\psi\)_, a CTL state formula_ \(\textbf{F}\psi\) _is a CTL path formula._
* _Given_ \(\psi\)_, a CTL state formula_ \(\textbf{G}\psi\) _is a CTL path formula._
* _Given_ \(\psi_{1}\) _and_ \(\psi_{2}\)_, CTL state formula_ \(\psi_{1}\textbf{U}\psi_{2}\) _is a CTL path formula._  
Note that Definition 50 can be restricted to exclude \(\top\), \(\lor\), **F** and **G**, without losing expressiveness in the same way as Definition 46. Syntax can also be expanded to other common Boolean operators as usual. **Example 4**. : _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 CTL logic:_  
\[\psi=\
eg\textbf{E}(a_{0}\wedge a_{1}) \tag{19}\]  
Intuitively, state formulas describe properties of states, whereas path formulas describe properties of (infinite) paths. Path formulas can be transformed into state formulas by prefixing them with a path quantifier. Note that path quantifiers must immediately precede temporal operators in order for the resulting state formula to be well formed. Intuitively, the semantics of path quantifiers is the following: \(\textbf{A}\varphi\) holds at the current state if \(\varphi\) holdsfor all paths starting at the current state; \(\mathbf{E}\varphi\) holds at the current state if \(\varphi\) holds for some paths starting at the current state. Formally, the semantics of CTL formulas is defined with respect to paths, states and transition systems, by means of two satisfaction relations: one for state formulas and the other for path formulas. **Definition 51** (Semantics of CTL Path Formulas with Respect to Paths). : _Given a transition system \(\mathcal{TS}\stackrel{{\mathit{\mathit{\mathit{\mathit{\mathit{\mathit{ \mathit{\mathit{\mathit{\mathit{\mathit{\mathit{\mathit{\mathit{\mathit{\mathit{\mathit{\mathitmathitmathitmathitmathitmathitmathitmathitmathitmathitmathit{ \mathit{ \mathit{ \mathit{ \mathit{ }}}}  
**Definition 57** (Invariant Properties).