Fair termination of communicating processes
Orna Grümberg, Nissim Francez, Shmuel M. Katz · 1984
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.