A Model and Proof Technique for Message-Based Systems
Jerome A. Feldman, Anil Nigam · SIAM Journal on Computing · 1980
Distributed computing with widely separated machines is a subject of growing theoretical and practical interest. This paper attempts to present a framework for the analysis of message-based distributed computations. This is done in the context of the classical critical section problem and the high-level language, PLITS. The proof techniques described are based on the use of finite-state machines which characterize the external behavior of each module in the distributed computation.