There is not a prevailing definition of fairness, but most definitions attempt to ensure that every transition of a system that is enabled sufficiently often is executed sufficiently often. The authors of this paper present a new definition, called constructive fairness.

Their main contribution is that, contrary to Lamport’s definition based on machine closure [1], their definition is closed under both arbitrary union and countable intersection. This is appealing in the context of transition systems for which a unique fairness assumption does not suffice; in such cases, the property satisfied by the whole system is the intersection of the fairness properties satisfied by each transition independently. Thus, unless these individual properties are constructive, the result is likely not to be a fairness property, which is problematic insofar as this may induce additional safety properties, that is, abnormal behaviors.

Researchers interested in this paper should also read Alur and Henzinger’s paper on local fairness [2], since it is closely related. The main difference seems to be that local fairness was defined for finitary properties only, and that Alur and Henzinger use a language-theoretic characterization. Constructive fairness is characterized using game and topology theory, and it is not restricted to finitary properties; however, local fairness is studied in the context of open systems, which is not the case for constructive fairness.