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

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

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

Full text

Pdf (1.36 MB)

Source

Annual ACM Symposium on Principles of Distributed Computing archive
Proceedings of the sixth annual ACM Symposium on Principles of distributed computing table of contents

Vancouver, British Columbia, Canada

Pages: 269 - 280

Year of Publication: 1987

ISBN:0-89791-239-4

Author

Joseph Y. Halpern

IBM Almaden Research Center

Sponsors

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory
SIGOPS: ACM Special Interest Group on Operating Systems

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 2, Downloads (12 Months): 12, Citation Count: 18

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/41840.41863 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	AUWY82	A. V. Aho, J. D. Ullman, A. D. Wyner, and M. Yannakakis, Bounds on the si~e and transmission rate of communication protocols, Comp. 8~ Maths. with Appls. 8:3, 1982, pp. 205-214. This is a later version of {AUY79}.
	AUY79	A.V. Aho, J. D. Ullman, and M. Yannakakis, Modeling communication protocols by automata, Proe. 20th IEEE Syrup. on Foundations of Computer Science, 1979, pp. 267-273.
	BS80	G.V. Bochmann and C. A. Sunshine, Formal methods in communication protocol design, IEEE Transactions on Communications COM-28, 1980~ pp. 624-631.
	BSW69	K. A. Bartlett , R. A. Scantlebury , P. T. Wilkinson, A note on reliable full-duplex transmission over half-duplex links, Communications of the ACM, v.12 n.5, p.260-261, May 1969 [doi>10.1145/362946.362970]
	CM86	K. M. Chandy , Jayadev Misra, How processes learn, Distributed Computing, v.1 n.1, p.40-52, Jan. 1986 [doi>10.1007/BF01843569]
	DM86	C Dwork , Y Moses, Knowledge and common knowledge in a Byzantine environment I: crash failures, Proceedings of the 1986 Conference on Theoretical aspects of reasoning about knowledge, p.149-169, March 1986, Monterey, California, United States
	FI86	M Fischer , N Immerman, Foundations of knowledge for distributed systems, Proceedings of the 1986 Conference on Theoretical aspects of reasoning about knowledge, p.171-185, March 1986, Monterey, California, United States
	GA87	E. Gafni and Y. Afek, Communication in unreliable networks, unpublished manuscript, 1987.
	Gaf86	E. Gafni, Perspectives on distributed network protocols: a case for building blocks, MILCOM "86, 1986.
	Gou85	M. Gouda, On "a simple protocol whose proof isn't", IEEE Transactions on Communications COM-33:4, 1985, pp. 382-384.
	GS80	V.D. Gligor and S. H. Shattuck, On deadlock detection in distributed systems, IEEE Transactions on Software Engineering SE-6:5, 1980, pp. 435- 440.
	Had87	V. Hadzilacos, A knowledge-theoretic analysis of atomic commitment protocols, Proceedings of the sixth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.129-134, March 23-25, 1987, San Diego, California, United States [doi>10.1145/28659.28672]
	Hai82	R. T. Hailpern, Verifying Concurrent Processes Using Temporal Logic, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
	Hai85	B.T. Hailpern, A simple protocol whose proof isn't, IEEE Transactions on Communications COM-33:4, 1985, pp. 330-337.
	Hal87a	j.Y. Halpern, Using reasoning about knowledge to analyze distributed systems, Annual Review of Computer Science, Vol. 2, Annual Reviews Inc., 1987.
	Hal87b	J.Y. Halpern, Yet another formalism for reasoning about distributed systems, Technical Report to appear, IBM, 1987.
	HF85	Joseph Y. Halpern , Ronald Fagin, A formal model of knowledge, action, and communication in distributed systems: preliminary report, Proceedings of the fourth annual ACM symposium on Principles of distributed computing, p.224-236, August 1985, Minaki, Ontario, Canada [doi>10.1145/323596.323617]
	HM84	Joseph Y. Halpern , Yoram Moses, Knowledge and common knowledge in a distributed environment, Proceedings of the third annual ACM symposium on Principles of distributed computing, p.50-61, August 27-29, 1984, Vancouver, British Columbia, Canada [doi>10.1145/800222.806735]
	HO83	B.T. Hailpern and S. S. Owicki, Modular verification of communication protocols, IEEE Transactions on Communications COM-31:I, 1983, pp. 56-68.
	HV86	J Y Halpern , M Y Vardi, The complexity of reasoning about knowledge and time, Proceedings of the eighteenth annual ACM symposium on Theory of computing, p.304-315, May 28-30, 1986, Berkeley, California, United States [doi>10.1145/12130.12161]
	LR86	R Ladner , J Reif, The logic of distributed protocols, Proceedings of the 1986 Conference on Theoretical aspects of reasoning about knowledge, p.207-222, March 1986, Monterey, California, United States
	MT86	Y. Moses and M. Tuttle, Programming simultaneous actions using common knowledge, Proc. 27th IEEE Syrup. on Foundations of Computer Science, 1986, pp. 208-221.
	OL82	Susan Owicki , Leslie Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.455-495, July 1982 [doi>10.1145/357172.357178]
	Pnu77	A. Pnueli, The Temporal Logic of programs, Proe. 18th IEEE Syrup. on Foundations of Computer Science, 1977, pp. 46-57.
	PR85	Rohit Parikh , R. Ramanujam, Distributed Processes and the Logic of Knowledge, Proceedings of the Conference on Logic of Programs, p.256-268, June 17-19, 1985
	SH86	S.R. Soloway and P. A. Humblet, On distributed network protocols for changing topologies, Technical Report LIDS- P- 1564, MIT, 1986.
	SM82	R.L. Schwartz and P. M. Melliar- Smith, From state machines to Temporal Logic: specification methods for protocol standards, IEEE Transactions on Communications, 12 1982.
	Ste76	M.V. Stenning, A data transfer protocol, Comput. Networks 1, 1976, pp. 99- 110.
	Sun79	C.A. Sunshine, Formal techniques for protocol specification and verification, IEEE Computer 12, 1979, pp. 20-27.

CITED BY 18

	Y. Moses , G. Roth, On reliable message diffusion, Proceedings of the eighth annual ACM Symposium on Principles of distributed computing, p.119-127, June 1989, Edmonton, Alberta, Canada
	Joseph Halpern , Yjoram Moses , Mark Tuttle, A knowledge-based analysis of zero knowledge, Proceedings of the twentieth annual ACM symposium on Theory of computing, p.132-147, May 02-04, 1988, Chicago, Illinois, United States
	Michael Merritt , Gadi Taubenfeld, Knowledge in shared memory systems (preliminary version), Proceedings of the tenth annual ACM symposium on Principles of distributed computing, p.189-200, August 19-21, 1991, Montreal, Quebec, Canada
	Joseph Halpern , Vardi, Reasoning about knowledge and time in asynchronous systems, Proceedings of the twentieth annual ACM symposium on Theory of computing, p.53-65, May 02-04, 1988, Chicago, Illinois, United States
	Beverly Sanders, A predicate transformer approach to knowledge and knowledge-based protocols (extended abstract), Proceedings of the tenth annual ACM symposium on Principles of distributed computing, p.217-230, August 19-21, 1991, Montreal, Quebec, Canada
	Da-Wei Wang , L. D. Zuck, Tight bounds for the sequence transmission problem, Proceedings of the eighth annual ACM Symposium on Principles of distributed computing, p.73-83, June 1989, Edmonton, Alberta, Canada
	Ewan Tempero , Richard Ladner, Tight bounds for weakly bounded protocols, Proceedings of the ninth annual ACM symposium on Principles of distributed computing, p.205-218, August 22-24, 1990, Quebec City, Quebec, Canada
	M. J. Fischer , S. Moran , R. Rudich , G. Taubenfeld, The wakeup problem, Proceedings of the twenty-second annual ACM symposium on Theory of computing, p.106-116, May 13-17, 1990, Baltimore, Maryland, United States
	Yehuda Afek , Eli Gafni, Bootstrap network resynchronization (extended abstract), Proceedings of the tenth annual ACM symposium on Principles of distributed computing, p.295-307, August 19-21, 1991, Montreal, Quebec, Canada
	Barbara Dunin-Keplicz , Rineke Verbrugge, Collective intentions, Fundamenta Informaticae, v.51 n.3, p.271-295, July 2002
	Gail E. Kaiser , Brent Hailpern, An object-based programming model for shared data, ACM Transactions on Programming Languages and Systems (TOPLAS), v.14 n.2, p.201-264, April 1992
	Eli Gafni , Yehuda Afek, End-to-end communication in unreliable networks, Proceedings of the seventh annual ACM Symposium on Principles of distributed computing, p.131-148, August 15-17, 1988, Toronto, Ontario, Canada
	Rohit Parikh, Recent issues in reasoning about knowledge, Proceedings of the 3rd conference on Theoretical aspects of reasoning about knowledge, March 04-07, 1990, Pacific Grove, California
	M. van Hulst , J.-J. Ch. Meyer, An epistemic proof system for parallel processes: extended abstract, Proceedings of the 5th conference on Theoretical aspects of reasoning about knowledge, p.243-254, March 13-16, 1994, Pacific Grove, California
	Paul J. Krasucki , R. Ramanujam, Knowledge and the ordering of events in distributed systems: extended abstract, Proceedings of the 5th conference on Theoretical aspects of reasoning about knowledge, p.267-283, March 13-16, 1994, Pacific Grove, California
	Gil Neiger, Knowledge consistency: a useful suspension of disbelief, Proceedings of the 2nd conference on Theoretical aspects of reasoning about knowledge, March 07-09, 1988, Pacific Grove, California
	Yoram Moses, Knowledge and communication: a tutorial, Proceedings of the 4th conference on Theoretical aspects of reasoning about knowledge, p.1-14, March 22-25, 1992, Monterey, California
	Clare Dixon , Mari-Carmen Fernández Gago , Michael Fisher , Wiebe van der Hoek, Temporal Logics of Knowledge and their Applications in Security, Electronic Notes in Theoretical Computer Science (ENTCS), 186, p.27-42, July, 2007