On the temporal analysis of fairness

TLDR

Temporal logic formalism for program reasoning is reviewed. The study analyzes responsiveness and fairness, motivating the introduction of an additional temporal operator, the “until” operator –U. The authors discuss general questions involving the “until” operator. Adding the “until” operator makes the temporal language expressively complete, and the authors prove completeness of two deductive systems, DX and DUX, for the languages without and with the new operator.

Abstract

The use of the temporal logic formalism for program reasoning is reviewed. Several aspects of responsiveness and fairness are analyzed, leading to the need for an additional temporal operator: the 'until' operator -U. Some general questions involving the 'until' operator are then discussed. It is shown that with the addition of this operator the temporal language becomes expressively complete. Then, two deductive systems DX and DUX are proved to be complete for the languages without and with the new operator respectively.