Safety Property

A safety property expresses that, under certain conditions, something will never occur. A typical CTL expression would be AG$\neg\phi$ with $\phi \in L_{PROP}$.

The negation of a safety statement will become a reachability property. Therefore $\neg$AG $\neg\phi \Longleftrightarrow$ EF$\phi$