Joseph Y. Halpern
Skip Abstract Section
Abstract
A high-level, knowledge-based approach for deriving a family of protocols for the sequence transmission problem is presented. The protocols of Aho et al. [2, 3], the Alternating Bit protocol [5], and Stenning's protocol [44] are all instances of one knowledge-based protocol that is derived. The derivation in this paper leads to transparent and uniform correctness proofs for all these protocols.
- 1 AFEK, Y., AND GAFNI, E. End-to-end communication in unrehable networks. In Proceedings of the 7th A CM Symposium on Prmciples of Distributed Computing (Toronto, Ont. Canada, Aug. 15-17). ACM, New York, 1988, pp. 131 - 148. Google Scholar
- 2 AHO, A. V., ULLMAN, J. D., WYNER, A. D., AND YANNAKAKIS, M. Bounds on the size and transmission rate of communication protocols. Comput. Math. Appl. 8, 3 (1982), 205-214. (This is a later version of {3} )Google Scholar
- 3 AHO, A. V., ULLMAN, J. D., AND YANNAKAKIS, M. Modeling commumcatlon protocols by automata. In Proceedings of the 20th IEEE Symposium on Foundations of Computer Science. IEEE, New York, 1979, pp. 267-273.Google Scholar
- 4 ATTIYA, C., FISCHER, M.J., WANG, D., AND ZUCK, L. D. Reliable communication usmg unreliable channels. Unpubhshed manuscript, 1988.Google Scholar
- 5 BARTLETT, K. A., SC~NTLEBURY, R. A, AND WmK~NSON, P T. A note on reliable full-duplex transmission over half-duplex links. Commun. ACM, I2, 5 (May 1969), 260-261. Google Scholar
- 6 BOCHMANN, G. V., AND GECSe*, J. A unified method for the specification and verification of protocols. In B. Gilchrlst, ed., Information Processing 77, North-Holland, Amsterdam, The Netherlands, 1977, pp 229-234.Google Scholar
- 7 BOCHMANN, G. V., AND SUNSHINE, C.A. Formal methods is communication protocol design IEEE Trans. Commun. COM-28 (1980) 624-631.Google Scholar
- 8 CHANDY, K. M., AND MISRA, J. HOW processes learn. Distr. Comput. l, 1 (1986), 40-52. Google Scholar
- 9 CLARK, D. D., LAMBERT, m. t., AND ZHANG, L. NETBLT: A high throughput transport protocol, in SigComm 87 Workshop. 1987, pp. 353-359 (Proceedings published in Comput. Commun. Rev. 17, 5.) Google Scholar
- 10 CLARKE, E. M., EMERSON, E. A., AND SISTLA, A. P. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8, 2 (Apr. 1986), 244-263. (An early version appeared in Proceedings of the lOth ACM Symposium on Principles of Programming Languages (Austin, Tex., Jan. 24-26). ACM, New York, 1983, pp. 117-126.) Google Scholar
- 11 DWORK, C., AND MOSES, Y. Knowledge and common knowledge in a Byzantine environment: Crash failures. Inf. Comput. 88, 2 (1990), 156-186. Google Scholar
- 12 FAGIN, R., HALPERN, J. Y., AND VARDI, M. Y. What can machines know? On the epistemic properties of machines. J. ACM 39, 2 (Apr. 1992), 382-428. Google Scholar
- 13 FISCHER, M. J., AND IMMERMAN, N. Foundations of knowledge for distributed systems. In J. Y. Halpern, ed., Theoretical Aspects of Reasoning about Knowledge: Proceedings of the 1986 Conference. Morgan-Kaufmann, San Mateo, Cahf., 1986, pp. 171-186. Google Scholar
- 14 FITTING, M. Modal logic should say more than it does. In J.-L. Lassez and G. Plotkin, ed, Computational Logic, Essays in Honor of Alan Robinson. MIT Press, Cambridge, Mass., 1991, pp. 113-135.Google Scholar
- 15 GAFNI, E. Perspectives on distributed network protocols: A case for building blocks. In Proceedings of IEEE MILCOM'86. IEEE, New York, 1986, pp. 1.1.1-1.1.3.Google Scholar
- 16 GLIGOR, V. D., AND SHATTUCK, S. H. On deadlock detection in distributed systems. IEEE Trans. Softw. Eng. SE-6, 5 (1980), 435-440.Google Scholar
- 17 GOUDA, M. On "A simple protocol whose proof isn't". IEEE Trans. Commun. COM-33, 4 (1985), 382-384.Google Scholar
- 18 GROVE, A., AND HALPERN, J.Y. Naming and identity in a multi-agent epistemic logic. In J. A. Allen, R. Fike, and E. Sandewall, ed., Principles of Knowledge Representation and Reasoning: Proceedings of the 2nd International Conference. Morgan-Kaufmann, San Mateo, Calif., 1991. pp. 301-312.Google Scholar
- 19 HADZILACOS, V. A knowledge-theoretic analysis of atomic commitment protocols. In Proceedings of the 6th A CM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (San Diego, Calif., Mar. 23-25). ACM, New York, 1987, pp. 129-134. (A revised version has been submitted for publication.) Google Scholar
- 20 HAILPERN, B. T. A simple protocol whose proof isn't. IEEE Trans. Commun. COM-33, 4 (1985), 330-337.Google Scholar
- 21 HAILPERN, B. T., AND OWI~~, S.S. Modular verificatlon of communication protocols. IEEE Trans. Commun. COM-31, 1 (1983) 56-68.Google Scholar
- 22 HALPERN, J.Y. Using reasoning about knowledge to analyze distributed systems. In J. F. Traub, B. J. Grosz, B. W. Lampson, and N. J. Nilsson, ed., Annual Review of Computer Science, vol. 2. Annual Reviews, inc., Palo Alto. Calif., 1987, pp. 37-68.Google Scholar
- 23 HALPERN, J. Y., AND FAGIN, R. A formal model of knowledge, action, and communication in distributed systems. In Proceedings of the 4th A CM Symposium on Principles of Distributed Computing. (Minaki, Ont., Canada, Aug. 5-7). ACM, New York, 1985, pp. 224-236. Google Scholar
- 24 HALPERN, J. Y., AND FAGIN, R. Modeling knowledge and action in distributed systems. Dist. Computing 3, 4 (1989), 159-179.Google Scholar
- 25 HALPERN, J. Y., AND Moses, Y. Knowledge and common knowledge in a distributed environment. J. ACM 37, 3 (July 1990), 549-587. (A preliminary version appeared in Proceedings of the 3rd ACM Symposium on Principles of Distributed Computing. ACM, New York, 1984.) Google Scholar
- 26 HALPERN, J. Y., MOSES, Y., AND TUTTLE, M.R. A knowledge-based analysis of zero knowledge. In Proceedings of the 20th A CM Symposium on Theory of Computing (Chicago, Ill., May 2-4). ACM, New York, 1988, pp. 132-147. Google Scholar
- 27 HALPERN, J. Y., MosEs, Y., AND WAARTS, O. A characterization of eventual Byzantine agreement. In Proceedings of the 9th A CM Symposium on Principles of Distributed Computing. (Quebec City, Que., Canada, Aug. 22-24). ACM. New York, 1990, pp. 333-346. Google Scholar
- 28 HALPERN, J. Y., AND VARD~, M.Y. The complexity of reasoning about knowledge and time. i: Lower Bounds. J. Comput. Syst. Sci. 38, 1 (1988), 195-237. Google Scholar
- 29 LADNER, R., AND REIF, J. The logic of distributed protocols (preliminary report). In J. Y. Halpern, ed., Theoretical Aspects of Reasoning about Knowledge: Proceedings of the 1986 Conference. Morgan-Kaufmann, San Mateo, Calif., 1986, pp. 207-222. Google Scholar
- 30 LYNCH, N. A., MANSOUR, Y., AND FEKETE, A. Data link layer: Two impossibility results. In Proceedings of the 7th A CM Symposium on Principles of Distributed Computing (Toronto, Ont., Canada, Aug. 15-17). ACM, New York, 1988, pp. 149-170. Google Scholar
- 31 LYNCH, N. A., AND TUTTLE, M.R. Hierarchical correctness proofs for distributed algorithms. Tech. Rep. MIT/LCS/TR-387. MIT, Cambridge, Mass., 1987. Google Scholar
- 32 MAZER, M. S. A knowledge theoretic account of recovery in distributed systems: The case of negotiated commitment. In M. Y. Vardi. ed., Proceedings of the 2nd Conference on Theoretical Aspects of Reasoning about Knowledge. Morgan-Kaufmann, San Mateo, Calif., 1988, pp. 309-324. Google Scholar
- 33 MAZER, M.S. A hnk between knowledge and communication in faulty distrlbuted systems. In R. Parikh, ed., Proceedings of the 3rd Conference on Theoretical Aspects of Reasoning about Knowledge. Morgan-Kaufmann, San Mateo, Calif., 1990, pp. 289-304 Google Scholar
- 34 MERHN, P.M. A methodology for the design and implementation of communication protocols. IEEE Trans. Commun. COM-24, 4 (1976), 614-621.Google Scholar
- 35 Moses, Y. Knowledge in a distributed environment. Ph D dissertation, Stanford University, Stanford, Calif., 1986. Google Scholar
- 36 MOSES, Y., AND TUTTLE, M.R. Programming sxmultaneous actions using common knowledge. Algorithmica, 3 (1988), 121-169.Google Scholar
- 37 NEIGER, G., ~ND TOUEG, S Substituting for real txme and common knowledge in asynchronous distributed systems. In Proceedings of the 6th Annual A CM Symposlum of Principles of Distributed Computing, (Vancouver, B.C., Canada, Aug. 10-12). ACM, New York, 1987, pp 281-293. Google Scholar
- 38 OWlCKI, S., AND LAMPORT, L. Proving liveness properties of concurrent programs. A CM Trans. Frog. Lang. Syst. 4, 3 (July 1982), 455-495. Google Scholar
- 39 PAR~KH, R., AND RAMANUJAM, R, Distributed processing and the logm of knowledge In R. Parikh, ed., Proceedings of the Workshop on Logics of Programs. Springer-Verlag, New York, 1985, pp. 256-268. Google Scholar
- 40 PNUF~LT, A. The temporal logic of programs. In Proceedings of the 18th {EEE Symposmm on Foundations of Conwuter Science. IEEE, New York, 1977, pp 46-57Google Scholar
- 41 QUEILLE, J. P., AND SIFAKIS, J. Specification and verification of concurrent systems m CESAR. In Proceedings of the 5th International Symposium on Programming. Lecture Notes in Computer Science, rot 157. Sprmger-Verlag, Berlin/New York, 1982, pp. 337-351 Google Scholar
- 42 SCHWARTZ, R. L., AND MELLIAR-SMITH, P. M. From state machines to temporal logic. Specification methods for protocol standards. IEEE Trans. Comrnun. COM-30, 12 (1982), 2486-2496.Google Scholar
- 43 SOLOWA~, S R, ~ND HUMB~ F.T, P. A On distributed network protocols for changing topologies. Tech. Rep. LIDS-P-I564. MIT, Cambridge, Mass, 1986.Google Scholar
- 44 STF, NN~NG, M.V. A data transfer protocol. Comput. Netw. 1 (1976), 99-110.Google Scholar
- 45 SUNSHINE, C.A. Formal techniques for protocol ~pecificat~on and verification. IEEE Comput. 12 (1979), 20-27.Google Scholar
Index Terms
- A little knowledge goes a long way: knowledge-based derivations and correctness proofs for a family of protocols
Recommendations
Optimal Eventual Byzantine Agreement Protocols with Omission Failures
PODC '23: Proceedings of the 2023 ACM Symposium on Principles of Distributed ComputingWork on optimal protocols for Eventual Byzantine Agreement (EBA)---protocols that, in a precise sense, decide as soon as possible in every run and guarantee that all nonfaulty agents decide on the same value---has focused on full-information protocols ...
Reviews
Richard John Botting
In this research paper, the authors design programs by assuming that the programs can test statements like “I know that the other program knows that it has received message number 5.” The authors refine two such conceptual designs into algorithms that use implementable conditions like “I just received message number 6 from the other program.” In this way, they derive and prove the correctness of two well-known protocols for solving the sequence transmission problem. They proceed to use the same approach to derive a new protocol for solving the same problem. Researchers in protocol design and formal methods should study this paper in detail. They need to know that a superfluous negation and “K” appear in the first condition in Figure 1. The definition of what it means for a program to have knowledge is deep, so the body of the paper is not for the general reader. The conclusions on pages 475 and 476 have a wider application than protocol design, however: high-level designs should focus on ideas, not efficiency; and creating and verifying a design remains a time-consuming art.
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments