Dr. Hagen Voelzer (IBM Zurich)

Defining Fairness and Fairly Correct Systems

Summary:

Fairness is a convenient and popular tool when modelling and specifying
concurrent systems. A large variety of fairness notions exists in the
literature. However, in contrast to safety and liveness, there was no
fully satisfactory abstract characterisation of fairness.

We give and justify a characterisation of fairness that is in line with
the characterisations of safety and liveness given by Lamport, Alpern
and Schneider. We provide independent characterisations in terms of
language-theory, game theory, and general topology.

Our characterisation of fairness gives rise to a notion of a "fairly
correct" system: a system is fairly correct if there exists a --possibly
strong-- fairness assumption under which it is correct. Many
distributed, especially fault-tolerant, systems are only fairly correct
with respect to their actual specification since often, fully correct
solutions are too expensive or do not exist.

We motivate this relaxation of correctness and compare it with the
probabilistic notion of an "almost correct" system, that is, a system
that is correct with probability 1 for a given probability measure.
While the two notions "fairly correct" and "almost correct" share many
properties, they do not coincide in general.

The comparison of the two notions directly leads to pleasing results for
 the problem of automatically checking whether a finite-state system is
fairly correct.