Wednesday, February 6, 2013

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.

No comments:

Post a Comment