Fair termination of communicating processes

Fairness has become one of the main issues in the theory of non-determinism and concurrency. Recently, the problem of proof rules for fair termination of programs (and some of its variants) has attracted considerable attention (AO83, APS82, GFK83, GFMR81, LPS81, P83). However, though the main interest and motivation for the consideration of fair termination stems from concurrency, almost all of the recent results are formulated in terms of nondeterministic programs. The main reason for this is the elegance of formalisms for structured nondeterminism, such as Guarded Commands DIJ76, and their convenience for syntax directed proofs. Other attempts use transition-systems as the program model, and temporal logic as the underlying reasoning formalism (QS82, P83), thereby giving up the structured, syntax-directed, approach.