On "A Simple Protocol Whose Proof Isńt": The State Machine Approach

We discuss how to model a synchronous protocol (due to Aho, Ullman, and Yannakakis) using communicating finite state machines, and present a proof for its safety and liveness properties. Our proof is based on constructing a labeled finite reachability graph for the protocol. This reachability graph can be viewed as a sequential program whose safety and liveness properties can be stated and verified in a straightforward fashion.