t (safety)
violations will always be found first. In other words, check liveness only after the <em>complete</em>
state space has been checked for safety violations.
If unchecked, temporal properties are checked periodically on the <em>incomplete</em>
state graph. Deferring verification of temporal properties is especially useful if it is highly
likely that the model does not violate its temporal properties (e.g. a smaller instance
of the model has successfully been verified for liveness violations).

<h3>F