Extension and Generalizations of Fairness

Overview

The aim of this chapter is to introduce extensions and generalizations of the previously studied concepts of fairness, in order to understand better both the scope of applicability and limitations of the proof methods for fair termination introduced. For these extensions and generalizations it is assumed that states may be augmented by auxiliary variables (and auxiliary assignments to them), by means of which it is possible to express properties of any prefix of the computation up to any given intermediate state occurrence.

We first study the property of equifair termination, a strengthening of fair termination imposing stronger restrictions on infinite computations, requiring infinitely many equalizations among sets of directions along infinite computations. In particular, we present proof rules for equifair termination for GC and prove their soundness and semantic completeness with respect to the semantics of computation trees. This is an attempt towards understanding properties of programs executed under a variety of restrictions on infinite behavior, a variety richer than the previously discussed fairness assumption, by means of a representative concept. The material in these sections is based on [GF 82] and [GFK 83]. Then we introduce the abstract notion of generalized fairness, relative to an arbitrary finite set of pairs of state conditions, and study termination under it, thereby generalizing both fairness and equifairness, as well of a whole family of related concepts. All these concepts have in common the property that they require similar proof methods for proving termination, and share a similar construction for completeness proofs. This section is based on [FK 83].

Then, we introduce the concept of extreme fairness, which requires yet stronger properties of the scheduler. Its main merit is its constituting a better approximation to probabilistic termination (termination with probability 1 when selection probabilities are attributed to directions). We present a proof rule for Extremely Fair Termination; however, it is not known whether this rule is complete for the strong version. The exposition is an adaptation of [PN 83] to our context and terminology.

Finally, we consider another modification of the fairness concept, whereby the focus is shifted from fair selection of directions to fair reachability of predicates, following [QS 83].