 The logic LTL is very useful for expressing properties of infinite computations in reactive systems, such as safety, liveness, and fairness, as laid out in  Section 11.1.  For example, the specification “Every time when a message is sent, an acknowledgment of receipt will eventually be returned, and the message will not be marked ‘sent’ before an acknowledgment of receipt is returned” can be formalized in LTL as: