(Simple) Liveness Property

A simple liveness property expresses that, under certain conditions, something will ultimetaely occur. Examples of CTL expressions stating the liveness property are as follows:

With $\phi, \psi \in L_{PROP}$:

1. AG( $\phi \Rightarrow \textbf{AF}\psi$)
2. AGEF$\phi$
3. A $\phi \textbf{U} \psi$
4. E $\phi \textbf{U} \psi$