Title
A Simple Protocol Whose Proof Isn't
Abstract
Aho, Ullman, and Yannakakis have proposed a set of protocols that ensure reliable transmission of data across an error-prone channel. They have obtained lower bounds on the complexity required of the protocols to assure reliability for different classes of errors. They specify these protocols with finite-state machines. Although the protocol machines have only a small number of states, they are nontrivial to prove correct. In this paper we present proofs of one of these protocols using the finite-state-machine approach and the abstract-program approach. We also show that the abstract-program approach gives special insight into the operation of the protocol.
Year
DOI
Venue
1985
10.1109/TCOM.1985.1096306
Communications, IEEE Transactions  
Keywords
Field
DocType
Communication theory,Protocols
Small number,Computer science,Communication theory,Communication channel,Theoretical computer science,Mathematical proof,Communications protocol,Reliable transmission,Universal composability
Journal
Volume
Issue
ISSN
33
4
0090-6778
Citations 
PageRank 
References 
13
2.18
15
Authors
1
Name
Order
Citations
PageRank
Brent Hailpern1515100.51