Abstract
To produce a program guaranteed to satisfy a given specification one can synthesize it from a formal constructive proof that a computation satisfying that specification exists. This process is particularly effective if the specifications are written in a high-level language that makes it easy for designers to specify their goals. We consider a high-level specification language that results from adding knowledge to a fragment of Nuprl specifically tailored for specifying distributed protocols, called event theory. We then show how high-level knowledge-based programs can be synthesized from the knowledge-based specifications using a proof development system such as Nuprl. Methods of Halpern and Zuck [15] then apply to convert these knowledge-based protocols to ordinary protocols. These methods can be expressed as heuristic transformation tactics in Nuprl.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aho, A.V., Ullman, J.D., Wyner, A.D., Yannakakis, M.: Bounds on the size and transmission rate of communication protocols. Computers and Mathematics with Applications 8(3), 205–214 (1982), This is a later version of [2]
Aho, A.V., Ullman, J.D., Yannakakis, M.: Modeling communication protocols by automata. In: Proc. 20th IEEE Symp. on Foundations of Computer Science, pp. 267–273 (1979)
Bartlett, K.A., Scantlebury, R.A., Wilkinson, P.T.: A note on reliable fullduplex transmission over half-duplex links. Communications of the ACM 12, 260–261 (1969)
Bates, J.L., Constable, R.L.: Proofs as programs. ACM Transactions on Programming Languages and Systems 7(1), 53–71 (1985)
Bickford, M., Constable, R.L.: A logic of events. Technical Report TR2003-1893, Cornell University (2003)
Bickford, M., Kreitz, C., van Renesse, R., Liu, X.: Proving hybrid protocols correct. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 105–120. Springer, Heidelberg (2001)
Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Reading (1988)
Constable, R.L.: Naïve computational type theory. In: Schwichtenberg, H., Steinbrüggen, R. (eds.) Proof and System-Reliability, Proceedings of International Summer School Marktoberdorf, Amsterdam, July 24 - August 5, 2001. NATO Science Series III, vol. 62, pp. 213–260. Kluwer Academic Publishers, Dordrecht (2002)
Constable, R.L., et al.: Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs (1986)
Dwork, C., Moses, Y.: Knowledge and common knowledge in a Byzantine environment: crash failures. Information and Computation 88(2), 156–186 (1990)
Engelhardt, K., van der Meyden, R., Moses, Y.: A program refinement framework supporting reasoning about knowledge and time. In: Tiuryn, J. (ed.) FOSSACS 2000. LNCS, vol. 1784, pp. 114–129. Springer, Heidelberg (2000)
Engelhardt, K., van der Meyden, R., Moses, Y.: A refinement theory that supports reasoning about knowledge and time for synchronous agents. In: Proc. Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning, pp. 125–141. Springer, Berlin (2001)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press, Cambridge (1995)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Knowledge-based programs. Distributed Computing 10(4), 199–225 (1997)
Halpern, J.Y., Zuck, L.D.: A little knowledge goes a long way: knowledge-based derivations and correctness proofs for a family of protocols. Journal of the ACM 39(3), 449–478 (1992)
Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Communications of the ACM 21(7), 558–565 (1978)
Lynch, N., Tuttle, M.: An introduction to Input/Output automata. Centrum voor Wiskunde en Informatica 2(3), 219–246 (1989)
Panangaden, P., Taylor, S.: Concurrent common knowledge: defining agreement for asynchronous systems. Distributed Computing 6(2), 73–93 (1992)
Sanders, B.: A predicate transformer approach to knowledge and knowledge-based protocols. In: Proc. 10th ACM Symp. on Principles of Distributed Computing, pp. 217–230 (1991); A revised report appears as ETH Informatik Technical Report 181 (1992)
Stenning, M.V.: A data transfer protocol. Comput. Networks 1, 99–110 (1976)
Stulp, F., Verbrugge, R.: A knowledge-based algorithm for the Internet protocol (TCP). Bulletin of Economic Research 54(1), 69–94 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bickford, M., Constable, R.C., Halpern, J.Y., Petride, S. (2005). Knowledge-Based Synthesis of Distributed Systems Using Event Structures. In: Baader, F., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2005. Lecture Notes in Computer Science(), vol 3452. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-32275-7_30
Download citation
DOI: https://doi.org/10.1007/978-3-540-32275-7_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25236-8
Online ISBN: 978-3-540-32275-7
eBook Packages: Computer ScienceComputer Science (R0)