An Algebraic Approach to Refinement with Fair Choice

In the analysis and design of concurrent systems, it can be useful to assume fairness among processes. Action systems model a process by a set of atomic actions. Typically, actions are combined by nondeterministic choice, which models minimal progress among processes rather than fairness. Here we define an operator for the fair choice among a set of actions. A refinement rule for action systems with fair choice is derived and applied to the development of the alternating bit protocol. The novelty is the algebraic style in which the fair choice operator is defined and in which formal reasoning is carried out; it avoids an appeal to the operational understanding of fairness.