Expressiveness of LTL, CTL, CTL*

Consider the following examples.

• $\mathbf{GF}p = \mathbf{AGAF}p = \mathbf{AGF} p$
• The existential quantifier is not possible in LTL. E.g., $\mathbf{EF}p$
• $\mathbf{FG}p \neq \mathbf{AFAG}p$, see Fig 1.
• $\mathbf{EFG}p \neq \mathbf{FG}p \neq \mathbf{EFAG} p$
• $\phi \in$ LTL $\Rightarrow \mathbf{A} \phi \in $CTL*
• All CTL formulae are automatically CTL*.

Fig. 1 A Kripke Model $M \models \mathbf{FG}p$ but $M \not \models \mathbf{AFAG}p$

It says

• They can all express some common formulae.
• Some CTL formulae are not covered in LTL.
• Some LTL formulae can not be expressed by CTL.
• Some CTL* formulae are covered neither in CTL nor LTL.
• CTL* subsumes both CTL and LTL.