Abstract
We define an epistemic logic for labelled transition systems by introducing equivalence relations for the agents on the states of the labelled transition system. The idea is that agents observe the dynamics of the system modulo their ability to distinguish states and in the process learn about the current state and past history of the execution. This is in the spirit of dynamic epistemic logic but is a direct combination of Hennessy-Milner logic and epistemic logic. We give an axiomatization for the logic and prove a completeness theorem with respect to the class of models obtained by unfolding labelled transition systems.
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
Kozen, D., Parikh, R.: An elementary proof of the completeness of PDL. Theoretical Computer Science 14, 113–118 (1981)
Halpern, J.Y., Moses, Y.: Knowledge and common knowledge in a distributed environment. In: Proceedings of the Third ACM Symposium on Principles of Distributed Computing, pp. 50–61 (1984); A revised version appears as IBM Research Report RJ 4421 (August 1987)
Chadha, R., Delaune, S., Kremer, S.: Epistemic Logic for the Applied Pi Calculus. In: Lee, D., Lopes, A., Poetzsch-Heffter, A. (eds.) FMOODS/FORTE 2009. LNCS, vol. 5522, pp. 182–197. Springer, Heidelberg (2009)
van Ditmarsch, H., van der Hoek, W., Kooi, B.: Dynamic Epistemic Logic. Synthese Library, vol. 337. Springer, Heidelberg (2008)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press (1995)
Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge Tracts in Theoretical Computer Science, vol. 53. Cambridge University Press (2001)
Milner, R.: Communication and Concurrency. Prentice-Hall (1989)
Milner, R.: Operational and Algebraic Semantics of Concurrent Processes. In: Handbook of Theoretical Computer Science, vol. B, pp. 1201–1242. MIT Press (1990)
Popkorn, S.: First Steps in Modal Logic. Cambridge University Press (1994)
Kripke, S.: Semantical analysis of modal logic. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 9, 67–96 (1963)
Hintikka, J.: Knowledge and Belief. Cornell University Press (1962)
Halpern, J., Moses, Y.: Knowledge and common knowledge in a distributed environment. JACM 37, 549–587 (1990)
Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. Journal of the ACM 32, 137–162 (1985)
Fischer, M., Ladner, R.: Propositional dynamic logic of regular programs. Journal of Computer and System Sciences (1979)
Panangaden, P., Taylor, K.E.: Concurrent common knowledge. In: Proceedings of the Seventh Annual ACM Symposium on Principles of Distributed Computing, pp. 197–209 (1988)
Panangaden, P., Taylor, K.E.: Concurrent common knowledge. Distributed Computing 6, 73–93 (1992)
Saraswat, V.A., Rinard, M., Panangaden, P.: Semantic foundations of concurrent constraint programming. In: Proceedings of the Eighteenth Annual ACM Symposium on Principles of Programming Languages (1991)
Neiger, G., Toueg, S.: Substituting for real time and common knowledge in asynchronous distributed systems. In: Proceedings of the Sixth ACM Symposium on Principles of Distributed Computing, pp. 281–293 (1987)
Neiger, G., Tuttle, M.R.: Common Knowledge and Consistent Simultaneous Coordination. In: van Leeuwen, J., Santoro, N. (eds.) WDAG 1990. LNCS, vol. 486, pp. 334–352. Springer, Heidelberg (1991)
Halpern, J.Y., Tuttle, M.R.: Knowledge, probability and adversaries. In: Proceedings of the Eighth Annual ACM Symposium on Principles of Distributed Computing, pp. 103–118. ACM (1989)
Halpern, J.Y., Moses, Y., Tuttle, M.R.: A knowledge-based analysis of zero knowledge. In: Proceedings of the 20th ACM Symposium on Theory of Computing, pp. 132–147 (1988)
Dechesne, F., Mousavi, M.R., Orzan, S.: Operational and Epistemic Approaches to Protocol Analysis: Bridging the Gap. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 226–241. Springer, Heidelberg (2007)
Mardare, R., Priami, C.: A decidable extension of Hennessy-Milner logic with spatial operators. Technical Report DIT-06-009, Ingegneria e Scienza dell’Informazione, University of Trento (2006)
Mardare, R., Priami, C.: Decidable Extensions of Hennessy-Milner Logic. In: Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 196–211. Springer, Heidelberg (2006)
Chatzikokolakis, K., Knight, S., Panangaden, P., Palamidessi, C.: Epistemic strategies and games on concurrent processes. ACM Transactions on Computational Logic (in press, 2012)
Pacuit, E., Simon, S.: Reasoning with protocols under imperfect information. The Review of Symbolic Logic 4, 412–444 (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Knight, S., Mardare, R., Panangaden, P. (2012). Combining Epistemic Logic and Hennessy-Milner Logic. In: Constable, R.L., Silva, A. (eds) Logic and Program Semantics. Lecture Notes in Computer Science, vol 7230. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-29485-3_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-29485-3_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-29484-6
Online ISBN: 978-3-642-29485-3
eBook Packages: Computer ScienceComputer Science (R0)