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*.

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