Abstract
We consider the problem of synthesizing protocols in a distributed setting satisfying specifications phrased in the logic of linear time and knowledge. On the one hand, we show that synthesis is already undecidable in environments with just two agents, one of which observes every aspect of the system state and one of which observes nothing of it. This falsifies a conjecture of van der Meyden and Vardi from CONCUR’96. On the other hand, we prove that synthesis is decidable in broadcast environments, verifying a conjecture of van der Meyden and Vardi from the same paper, and we show that for specifications that are positive in the knowledge modalities the synthesis problem can be reduced to the same problem for formulas without knowledge modalities. After adapting Pnueli and Rosner’s decidability result on synthesis for linear temporal logic specifications in hierarchical environments, we obtain that, in our setting, synthesis is decidable for specifications positive in the knowledge modalities when restricted to hierarchical environments. We conclude the decidability in hierarchical systems of a property closely related to nondeducibility on strategies, a notion that has been studied in computer security.
Work supported by a grant from the Australian Research Council. National ICT Australia is funded through the Australian Government’s Backing Australia’s Ability initiative, in part through the Australian Research Council.
A full version of this paper is available at http://www.cse.unsw.edu.au/~meyden/research/unsw-cse-tr-0504.pdf
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
Arnold, A., Vincent, A., Walukiewicz, I.: Games for synthesis of controlers with partial observation. Theoretical Computer Science 303(1), 7–34 (2003)
Attie, P.C., Arora, A., Emerson, E.A.: Synthesis of fault-tolerant concurrent programs. ACM Transactions on Programming Languages and Systems 26(1), 125–1851 (2004)
Chaum, D.: The dining cryptographers problem: unconditional sender and recipient untraceability. J., Cryptology (1), 65–75 (1988)
Emerson, E.A., Clarke, E.M.: Using branching time logic to synthesize synchronization skeletons. Science of Computer Programming 2, 241–266 (1982)
Engelhardt, K., van der Meyden, R., Su, K.: Modal logics with a hierarchy of local propositional quantifiers. In: Balbiani, P., Suzuki, N., Wolter, F., Zakharyaschev, M. (eds.) Advances in Modal Logic, vol. 4, pp. 9–30. World Scientific, Singapore (2003)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press, Cambridge (1995)
Halpern, J.Y., O’Neill, K.: Anonymity and information hiding in multiagent systems. In: Proceedings of the 16th IEEE Computer Security Foundations Workshop, pp. 75–88 (2003)
Kupferman, O., Vardi, M.Y.: Synthesis with incomplete informatio. In: 2nd International Conference on Temporal Logic, Manchester, pp. 91–106 (July 1997)
Madhusudan, P.: Control and Synthesis of Open Reactive Systems. PhD thesis, University of Madras (November 2001)
Manna, Z., Wolper, P.: Synthesis of communicating processes from temporal logic specifications. ACM Transactions on Programming Languages and Systems 6(1), 68–93 (1984)
Mayr, R.: Undecidable problems in unreliable computations. Theoretical Computer Science 297(1-3), 337–354 (2003)
van der Meyden, R.: Finite state implementations of knowledge-based programs. In: Chandru, V., Vinay, V. (eds.) FSTTCS 1996. LNCS, vol. 1180, pp. 262–273. Springer, Heidelberg (1996)
van der Meyden, R., Su, K.: Symbolic model checking the knowledge of the dining cryptographers. In: Proc. 17th IEEE Computer Security Foundations Workshop, pp. 280–291 (June 2004)
van der Meyden, R., Vardi, M.Y.: Synthesis from knowledge-based specifications. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 34–49. Springer, Heidelberg (1998)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. 16th ACM Symp. on Principles of Programming Languages, Austin (January 1989)
Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol. 372, pp. 652–671. Springer, Heidelberg (1989)
Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: Proc. 31st IEEE Symp. on Foundation of Computer Science, pp. 746–757 (1990)
Vardi, M.Y.: An automata-theoretic approach to fair realizability and synthesis. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 267–292. Springer, Heidelberg (1995)
Walukiewicz, I.: A landscape with games in the background. In: Proc. IEEE Symp. on Logic In computer Science, pp. 356–366 (2004)
Wittbold, J.T., Johnson, D.M.: Information flow in nondeterministic systems. In: Proc. IEEE Symp. on Research in Security and Privacy, pp. 144–161 (1990)
Wong-Toi, H., Dill, D.L.: Synthesizing processes and schedulers from temporal specifications. In: Clarke, E.M., Kurshan, R.P. (eds.) Computer-Aided Verification 1990, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 3, pp. 177–186. AMS (1991)
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
van der Meyden, R., Wilke, T. (2005). Synthesis of Distributed Systems from Knowledge-Based Specifications . In: Abadi, M., de Alfaro, L. (eds) CONCUR 2005 – Concurrency Theory. CONCUR 2005. Lecture Notes in Computer Science, vol 3653. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11539452_42
Download citation
DOI: https://doi.org/10.1007/11539452_42
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28309-6
Online ISBN: 978-3-540-31934-4
eBook Packages: Computer ScienceComputer Science (R0)