Definition. Guarantee properties [ltp-0005]

A guarantee (or cosafety) property is the complement of a safety property. A guarantee property says that a good thing happens eventually. As with safety properties, the "good thing" is some finite, observable event. In other words, guarantee properties are those properties whose satisfaction can be established by examining only a finite prefix of the behaviour.

For example, the guarantee property "The state \mathtt {a} is eventually reached" is satisfied by any finite prefix containing the state \mathtt {a}.

Leslie Lamport originally called these liveness properties, but we use the more popular definition of that term from Alpern and Schneider.