Hierarchical Correctness Proofs for Distributed Algorithms

著者: Nancy A. Lynch, Mark R. Tuttle - Proceedings of the sixth annual ACM Symposium on Principles of distributed computing - PODC '87 1987 被引用: 767

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 aninteresting example of how itcan be used to construct such proofs. 1