A reachability property states that some particular situation can be reached. A typical CTL expression would be EF with .
The negation of a reachability statement will become a safety property. Therefore EF AG