A Probabilistic Model for Parametric Fairness in Isabelle/HOL ?

In paper (1), a liveness proof method suitable for inductive protocol verication is proposed. The utility of this method has been conrmed by several machine checked formal verications(2{4). One re- maining question about (1) is the meaning of Parametric Fairness, a new fairness notion adapted from Pnueli's Extreme Fairness(5) to suit the set- ting of higher-order logic. This paper tries to answer this question. As a standard practice in establishing a fairness notion, this paper constructs a probabilistic model for parametric fairness in Isabelle/HOL. Using this model, it is shown that most innite executions of a concurrent system are parametrically fair. Therefore the denition of parametric fairness in paper (1) is reasonable. This work gives a rmer basis for existing and forthcoming formal verications based on the method of paper (1).