The Syntax of $L_{CTL}$

The propositional branching-time logic CTL (Computational Temporal Logic) is historically the forerunner of $CTL^{*}$. It has been introduced by Clarke and Emerson (1981) [66]. Only later, when the expressive limits of CTL became more known has $CTL^{*}$ been introduced by Emerson and Halpern (1986) [95] as a possible unifying framework for CTL and PLTL (cf. Emerson (1990) [92], P.1012).

The language $L_{CTL}$ is a proper subset of $L_{CTL^{*}}$:

$$L_{CTL} \subset L_{CTL^{*}}$$ (6.21)

This is caused by some syntactical constraints valid for $L_{CTL}$ (cf. figure 6.1).

$$STATE-STATE: L_{PROP} \subseteq StateFML \subseteq L_{CTL}$$ (6.22)

$$\Phi \in StateFML \Longrightarrow \neg \Phi \in StateFML$$ (6.23)

$$\Phi, \Phi' \in StateFML \Longrightarrow (\Phi \wedge \Phi') \in StateFML$$ (6.24)

$$\Phi, \Phi' \in StateFML \Longrightarrow (\Phi \vee \Phi') \in StateFML$$ (6.25)

$$\hline STATE-PATH: \Phi \in StateFML \Longrightarrow \textbf{X}\Phi \in PathFML$$ (6.26)

$$\Phi \in StateFML \Longrightarrow \textbf{F}\Phi \in PathFML$$ (6.27)

$$\Phi \in StateFML \Longrightarrow \textbf{G}\Phi \in PathFML$$ (6.28)

$$\Phi, \Psi \in StateFML \Longrightarrow (\Phi \textbf{U} \Psi) \in PathFML$$ (6.29)

$$PathFML \subseteq L_{CTL}$$ (6.30)

$$\hline PATH-STATE: \Phi \in PathFML \Longrightarrow \textbf{E}\Phi \in StateFML$$ (6.31)

$$\Phi \in PathFML \Longrightarrow \textbf{A}\Phi \in StateFML$$ (6.32)

Figure 6.1: The 'syntactical states' of CTL formulas

An alternative syntactic definition of CTL can be given as follows ($\Pi$ := Atomic Propositions = $L_{PROP}$, SF := State Formulas, PF := Path Formulas):

1. $\Pi \subseteq SF$
2. If $\Phi,\Psi \in SF$ then $\Phi \wedge \Psi$ and $\Phi \vee \Psi$ in SF as well as $\neg \Phi$
3. If $\Phi,\Psi \in SF$ then $\textbf{X}\Phi, \textbf{F}\Phi,\textbf{G}\Phi, \Phi\textbf{U}\Psi$ in PF
4. If $\Phi\in PF$ then $\textbf{A}\Phi, \textbf{E}\Phi$ in SF
5. $(SF \cup PF) \subseteq L_{CTL}$
6. Only (1) - (5) define the set of $L_{CTL}$

Some other equivalences are the following ones. Having the temporal logical operators $\Box$ (always) and $\Diamond$ (eventually) one can define:

$$EVENTUALLY: \exists\Diamond \Phi = \exists (true \textbf{U} \Phi)$$ (6.33)

$$\forall\Diamond \Phi = \forall (true \textbf{U} \Phi)$$ (6.34)

$$\hline ALWAYS: \exists\Box \Phi = \neg\forall\Diamond\neg \Phi$$ (6.35)

$$\forall\Box \Phi = \neg\exists\Diamond\neg \Phi$$ (6.36)