Fairness in Temporal Logic

Overview

In this chapter a different pattern of reasoning is introduced, known as temporal-reasoning. It uses a notation which is directly interpreted on infinite sequences (or trees) which, in turn, can be used to represent the evolution in time of the program state. An important distinguished characteristic of this approach (as presented here) is its being endogenous, i.e. it considers the set of complete computation sequences (or trees) as given, and reasons directly about the behavior of the whole program.

Thus, given a program, the reasoning is factored as follows:

• a) define the set of all its computation histories,

• b) prove any required property in terms of these histories, independently of the program.

This may be contrasted with the exogenous approach of the proof rules in previous chapters, where the rules related properties of the whole program to properties of its parts.

One consequence of this distinction is that the temporal approach is more suitable for dealing with programs presented as transition systems in contrast to the exogenous systems, that fit nicely in dealing with well-structured programs. Recently several attempts were made to provide temporal semantics in a more structured, compositional way.

Another observation is that the temporal approach is rather more powerful for general liveness properties, of which termination is just a special case. Hence, in dealing with fair termination of GC programs, one does not take full advantage of the whole power of the system.