A little knowledge goes a long way: Simple knowledge-based derivations and correctness proofs for a family of protocols

Abstract

We use a high-level, knowledge-based approach for deriving a family of protocols for the sequence transmission problem. The protocols of Aho, Ullman, and Yannakakis [AUY79, AUWY82], the Alternating Bit protocol [BSW69], and Stenning's protocol [Ste76] are all instances of one of the knowledge-based protocols that we derive. Our derivation leads to easy and uniform correctness proofs for all these protocols.