Abstract
The specification formalism employed in model checking is usually some flavour of temporal or process algebraic language that expresses properties of the behavioural aspects of a system. Knowledge [5] is a modality that is orthogonal to the behavioural dimension, capturing properties of information flow. Logics of knowledge have been shown to be a useful framework for the analysis of distributed algorithms and security protocols, and model checking of these logics was first mooted by Halpern and Vardi [6]. Since that time theoretical aspects of model checking the logic of knowledge and its combinations with temporal logic have been studied [8–10]. The system MCK introduced in this paper implements parts of this theory.
Work of the first author conducted while employed at UNSW. Work funded by an Australian Research Council Discovery grant. National ICT Australia is funded through the Australian Government’s Backing Australia’s Ability initiative, in part through the Australian Research Council.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Benerecetti, M., Giunchiglia, F., Serafini, L.: Multiagent model checking. Journal of Logic and Computation 8(3), 401–423 (1997)
Bertoli, P., Cimatti, A., Pistore, M., Taverso, P.: Plan validation for extended goals under partial observability (preliminary report). In: AIPS 2002 Workshop on Planning via Model Checking, Toulouse, France (April 2002)
Engelhardt, K., van der Meyden, R., Moses, Y.: Knowledge and the logic of local propositions. In: Gilboa, I. (ed.) Theoretical Aspects of Rationality and Knowledge, July 1998, pp. 29–41. Morgan Kaufmann, San Francisco (1998)
Bordini, R.H., Fisher, M., Pardavila, C., Visser, W., Wooldridge, M.: Model checking multi-agent programs with CASP. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 110–113. Springer, Heidelberg (2003)
Halpern, J., Moses, Y.: Knowledge and common knowledge in a distributed environment. Journal of the ACM 37(3), 549–587 (1990)
Halpern, J., Vardi, M.Y.: Model checking vs. theorem proving: A manifesto. Technical Report RJ 7963, IBM Almaden Research Center (1991)
van der Hoek, W., Wooldridge, M.: Model checking knowledge and time. In: 9th Workshop on SPIN (Model Checking Software), Grenoble (April 2002)
van der Meyden, R.: Common knowledge and update in finite environments. Information and Computation 140(2) (1998)
van der Meyden, R., Shilov, N.S.: Model checking knowledge and time in systems with perfect recall. In: Pandu Rangan, C., Raman, V., Sarukkai, S. (eds.) FST TCS 1999. LNCS, vol. 1738, pp. 262–273. Springer, Heidelberg (1999)
van der Meyden, R., Su, K.: Symbolic model checking the knowledge of the dining cryptographers. In: IEEE Computer Security Foundations Workshop (2004)
Shilov, N.Y., Garanina, N.O.: Model checking knowledge and fixpoints. In: FLOC workshop on Fixed Points in Computer Science (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gammie, P., van der Meyden, R. (2004). MCK: Model Checking the Logic of Knowledge. In: Alur, R., Peled, D.A. (eds) Computer Aided Verification. CAV 2004. Lecture Notes in Computer Science, vol 3114. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27813-9_41
Download citation
DOI: https://doi.org/10.1007/978-3-540-27813-9_41
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22342-9
Online ISBN: 978-3-540-27813-9
eBook Packages: Springer Book Archive