Reachability Property

A reachability property states that some particular situation can be reached. A typical CTL expression would be EF$ \phi$ with $ \phi \in L_{PROP}$.

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



Gerd Doeben-Henisch 2010-03-03