Hierarchical Correctness Proofs for Distributed Algorithms

Abstract: We introduce the input-output automaton, a simple but powerful model of computation in asynchronous distributed networks. With this model we are able to construct modular, hierarchical correctness proofs for distributed algorithms. We de ne this model, and give an interesting example of how it can be used to construct such proofs.

• Type: Conference
• Year: 1987
• Where: PODC
• Authors: Nancy A. Lynch, Mark R. Tuttle
• Keywords: Asynchronous Distributed Networks, Distributed And Parallel Computing, Hierarchical Correctness Proofs, Input-output Automaton, PODC 1987