A probabilistic framework for fairness notions

Fairness is a convenient and popular tool when modelling and specifying concurrent systems, many fairness notions exist in the literature. However, there was no fully satisfactory abstract characterisation of fairness. In order to show fairness definitions are reasonable, a probabilistic framework for fairness notions was proposed, where concurrent systems were modelled inductively in the theorem prover Isabelle/HOL, and a general fairness notion was defined. It was shown that the set of fair infinite executions of concurrent systems has probability 1. Finally, the usage of this framework was argued. All formalisations and proofs have been carried out with Isabelle/HOL/Isar.