Hierarchical Correctness Proofs for Distributed Algorithms.
Abstract
This thesis introduces a new model for distributed computation in asynchronous networks, the input-output automaton. This simple, powerful model captures in a novel way the game-theoretic interaction between a system and its environment, and allows fundamental properties of distributed computation such as fair computation to be naturally expressed. Futhermore, this model can be used to construct modular, hierarchical correctness proofs of distributed algorithms. This thesis defines the input-output automaton model, and presents an interesting example of how this model can be used to construct such proofs.
Document Details
- Document Type
- Technical Report
- Publication Date
- Apr 03, 1987
- Accession Number
- ADA182177
Entities
People
- Mark S. Tuttle
- Nancy Lynch
Organizations
- Massachusetts Institute of Technology