Liveness Properties
- Safety Properties are complemented by liveness properties, which require
progress.
- Safety violations can always be demonstrated by a finite trace.
- Liveness properties assert that "something good will eventually happen".
Definition
An LT property \(P_{live}\) over \(\texttt{AP}\) is a liveness property whenever \(\texttt{pref}(P_{live}) = (2^{\texttt{AP}})^\star\).
Thus, a liveness property (over \(\texttt{AP}\)) is an LT property P such that each finite word can be extended to an infinite word that satisfies P. Stated differently, P is a liveness property if and only if for all finite words \(w \in (2^{\texttt{AP}})^\star\) there exists an infinite word \(\sigma \in (2^{\texttt{AP}})^\omega\) satisfying \(w \sigma \in P\).
That is, every finite prefix can be extended into a computation satisfying the property.