Definition. Liveness properties [ltp-0006]

A liveness property says that a good thing happens eventually, but unlike guarantee properties, the "good thing" need not be some finite, observable event. Rather, liveness properties are those properties whose violation cannot be established by examining only a finite prefix of the behaviour. In other words, P is a liveness property iff for any finite prefix t \in \Sigma ^\ast , there exists an infinite extension \sigma \in \Sigma ^\omega such that t\sigma is in the property P.

For example, the property "Every \mathtt {r}equest state is eventually followed by an \mathtt {a}nswer state" is a liveness property: No matter how many unanswered \mathtt {r}equests are in a finite prefix, we could always see the \mathtt {a}nswer in the future.