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.
Nancy A. Lynch, Mark R. Tuttle