The Syntax of

$L_{CTL^{*}}$ assumes some property language $L_{PROP}$ as basis. The exact nature of this property language does not really matter. In many cases a language $L_{PROP}$ is used which has the following format:

$\displaystyle Names$	$\displaystyle \subseteq$	$\displaystyle UPPER \times LOWER^{*}$	(6.1)
$\displaystyle Names$	$\displaystyle \subseteq$	$\displaystyle L_{PROP}$	(6.2)
$\displaystyle f,f' \in L_{PROP}$	$\displaystyle \Longrightarrow$	$\displaystyle (f = f') \in L_{PROP}$	(6.3)
$\displaystyle f,f' \in L_{PROP}$	$\displaystyle \Longrightarrow$	$\displaystyle (f \neq f') \in L_{PROP}$	(6.4)
$\displaystyle f,f' \in L_{PROP}$	$\displaystyle \Longrightarrow$	$\displaystyle (f < f') \in L_{PROP}$	(6.5)
$\displaystyle f,f' \in L_{PROP}$	$\displaystyle \Longrightarrow$	$\displaystyle (f > f') \in L_{PROP}$	(6.6)
$\displaystyle f,f' \in L_{PROP}$	$\displaystyle \Longrightarrow$	$\displaystyle (f \leq f') \in L_{PROP}$	(6.7)
$\displaystyle f,f' \in L_{PROP}$	$\displaystyle \Longrightarrow$	$\displaystyle (f \geq f') \in L_{PROP}$	(6.8)

While the property language only talks about properties the more complex language $L_{CTL^{*}}$ uses additional logical connectors, temporal operators as well as quantifiers:

$\displaystyle L_{PROP}$	$\displaystyle \subseteq$	$\displaystyle L_{CTL^{*}}$	(6.9)
$\displaystyle \hline LOGICAL: \Phi \in L_{CTL^{*}}$	$\displaystyle \Longrightarrow$	$\displaystyle \neg \Phi \in L_{CTL^{*}}$	(6.10)
$\displaystyle \Phi, \Phi' \in L_{CTL^{*}}$	$\displaystyle \Longrightarrow$	$\displaystyle (\Phi \wedge \Phi') \in L_{CTL^{*}}$	(6.11)
$\displaystyle \Phi, \Phi' \in L_{CTL^{*}}$	$\displaystyle \Longrightarrow$	$\displaystyle (\Phi \vee \Phi') \in L_{CTL^{*}}$	(6.12)
$\displaystyle \hline TEMPORAL: \Phi \in L_{CTL^{*}}$	$\displaystyle \Longrightarrow$	$\displaystyle \textbf{X}\Phi \in L_{CTL^{*}}$	(6.13)
$\displaystyle \Phi \in L_{CTL^{*}}$	$\displaystyle \Longrightarrow$	$\displaystyle \textbf{F}\Phi \in L_{CTL^{*}}$	(6.14)
$\displaystyle \Phi \in L_{CTL^{*}}$	$\displaystyle \Longrightarrow$	$\displaystyle \textbf{G}\Phi \in L_{CTL^{*}}$	(6.15)
$\displaystyle \Phi, \Psi \in L_{CTL^{*}}$	$\displaystyle \Longrightarrow$	$\displaystyle (\Phi \textbf{U} \Psi)$	(6.16)
$\displaystyle \hline QUANTIFIER: \Phi \in L_{CTL^{*}}$	$\displaystyle \Longrightarrow$	$\displaystyle \textbf{E}\Phi \in L_{CTL^{*}}$	(6.17)
$\displaystyle \Phi \in L_{CTL^{*}}$	$\displaystyle \Longrightarrow$	$\displaystyle \textbf{A}\Phi \in L_{CTL^{*}}$	(6.18)

$\displaystyle \exists\Phi$	$\displaystyle =$	$\displaystyle \textbf{E}\Phi$	(6.19)
$\displaystyle \forall\Phi$	$\displaystyle =$	$\displaystyle \textbf{A}\Phi$	(6.20)

The set of all possible operators used in practice can be deduced from different kinds of minimal sets of operators. One very often used minimal set of operators is the following one: $\{ \neg, \wedge, \textbf{X}, \textbf{U}, \textbf{E} \}$ . The others can then be inferred from these by the following equivalences: