Skip to main content
SpringerLink
Log in

Model Checking Knowledge and Time

  • Conference paper
  • First Online:
Model Checking Software (SPIN 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2318))

Included in the following conference series:

Abstract

Model checking as an approach to the automatic verification of finite state systems has focussed predominantly on system specifications expressed in temporal logic. In the distributed systems community, logics of knowledge (epistemic logics) have been advocated for expressing desirable properties of protocols and systems. A range of logics combining temporal and epistemic components have been developed for this purpose. However, the model checking problem for temporal logics of knowledge has received (comparatively) little attention. In this paper, we address ourselves to this problem. Following a brief survey of the relevant issues and literature, we introduce a temporal logic of knowledge (Halpern and Vardi’s logic CKL n). We then develop an approach to CKL n model checking that combines ideas from the interpreted systems semantics for knowledge with the logic of local propositions developed by Engelhardt et al. With our approach, local propositions provide a means to reduce CKL n model checking to linear temporal logic model checking. After introducing and exploring the ideas underpinning our approach, we present a case study (the bit transmission problem) in which spin was used to establish temporal epistemic properties of a system implemented in PROMELA.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. M. Benerecetti, F. Giunchiglia, and L. Serafini. A model checking algorithm for multiagent systems. In J. P. Müller, M. P. Singh, and A. S. Rao, editors, Intelligent Agents V (LNAI Volume 1555). Springer-Verlag: Berlin, Germany, 1999.

    Google Scholar 

  2. E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press: Cambridge, MA, 2000.

    Google Scholar 

  3. C. Dixon, M. Fisher, and M. Wooldridge. Resolution for temporal logics of knowledge. Journal of Logic and Computation, 8(3):345–372, 1998.

    Article  MATH  MathSciNet  Google Scholar 

  4. E. A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science Volume B: Formal Models and Semantics, pages 996–1072. Elsevier Science Publishers B.V.: Amsterdam, The Netherlands, 1990.

    Google Scholar 

  5. K. Engelhardt, R. van der Meyden, and Y. Moses. Knowledge and the logic of local propositions. In Proceedings of the 1998 Conference on Theoretical Aspects of Reasoning about Knowledge (TARK98), pages 29–41, Evanston, IL, July 1998.

    Google Scholar 

  6. R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning About Knowledge. The MIT Press: Cambridge, MA, 1995.

    MATH  Google Scholar 

  7. R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Knowledge-based programs. Distributed Computing, 10(4):199–225, 1997.

    Article  Google Scholar 

  8. R. Goldblatt. Logics of Time and Computation (CSLI Lecture Notes Number 7). Center for the Study of Language and Information, Ventura Hall, Stanford, CA 94305, 1987. (Distributed by Chicago University Press).

    Google Scholar 

  9. J. Y. Halpern and M. Y. Vardi. The complexity of reasoning about knowledge and time. I. Lower bounds. Journal of Computer and System Sciences, 38:195–237, 1989.

    Article  MATH  MathSciNet  Google Scholar 

  10. J. Y. Halpern and M. Y. Vardi. Model checking versus theorem proving: A manifesto. In V. Lifschitz, editor, AI and Mathematical Theory of Computation-Papers in Honor of John McCarthy, pages 151–176. The Academic Press: London, England, 1991.

    Google Scholar 

  11. J. Y. Halpern and L. D. Zuck. 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.

    Article  MATH  MathSciNet  Google Scholar 

  12. J. Hintikka. Knowledge and Belief. Cornell University Press: Ithaca, NY, 1962.

    Google Scholar 

  13. G. Holzmann. Design and Validation of Computer Protocols. Prentice Hall International: Hemel Hempstead, England, 1991.

    Google Scholar 

  14. G. Holzmann. The Spin model checker. IEEE Transaction on Software Engineering, 23(5):279–295, May 1997.

    Article  MathSciNet  Google Scholar 

  15. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag: Berlin, Germany, 1992.

    Google Scholar 

  16. Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems-Safety. Springer-Verlag: Berlin, Germany, 1995.

    Google Scholar 

  17. K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers: Boston, MA, 1993.

    MATH  Google Scholar 

  18. J.-J. Ch. Meyer and W. van der Hoek. Epistemic Logic for AI and Computer Science. Cambridge University Press: Cambridge, England, 1995.

    MATH  Google Scholar 

  19. A. S. Rao and M. P. Georgeff. A model-theoretic approach to the verification of situated reasoning systems. In Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence (IJCAI-93), pages 318–324, Chambéry, France, 1993.

    Google Scholar 

  20. R. van der Meyden. Finite state implementations of knowledge-based programs. In Proceedings of the Conference on Foundations of Software Technology and Theoretical Computer Science (LNCS Volume 1180), pages 262–273, 1996.

    Google Scholar 

  21. R. van der Meyden. Knowledge based programs: On the complexity of perfect recall in finite environments. In Y. Shoham, editor, Proceedings of the Sixth Conference on Theoretical Aspects of Rationality and Knowledge, pages 31–50, De Zeeuwse Stromen, Renesse, Holland, March 1996.

    Google Scholar 

  22. R. van der Meyden and N. Shilov. Model checking knowledge and time in systems with perfect recall. In Proceedings of the Conference on Foundations of Software Technology and Theoretical Computer Science (LNCS Volume 1738), pages 432–445. Springer-Verlag: Berlin, Germany, 1999.

    Google Scholar 

  23. M. Y. Vardi. Implementing knowledge-based programs. In Proceedings of the Sixth Conference on Theoretical Aspects of Rationality and Knowledge (TARK 1996), pages 15–30, De Zeeuwse Stromen, Renesse, The Netherlands, March 1996.

    Google Scholar 

  24. M. Y. Vardi. Branching vs. linear time: Final showdown. In T. Margaria and W. Yi, editors, Proceedings of the 2001 Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2001 (LNCS Volume 2031), pages 1–22. Springer-Verlag: Berlin, Germany, April 2001.

    Google Scholar 

  25. M. Wooldridge, C. Dixon, and M. Fisher. A tableau-based proof method for temporal logics of knowledge and belief. Journal of Applied Non-Classical Logics, 8(3):225–258, 1998.

    MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Information and Computing Sciences, Universiteit Utrecht, 3584, Utrecht, CH, The Netherlands

    Wiebe van der Hoek

  2. Department of Computer Science, University of Liverpool, L69 7ZF, Liverpool, UK

    Wiebe van der Hoek & Michael Wooldridge

Authors
  1. Wiebe van der Hoek
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michael Wooldridge
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Mathematics and Computer Science, Eindhoven University of Technology, P.O. Box 513, 5600, MB Eindhoven, The Netherlands

    Dragan Bošnački

  2. Institute for Computer Science, Albert-Ludwigs-University Freiburg, Georges-Koehler-Allee Geb. 051, 79199, Freiburg, Germany

    Stefan Leue

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

van der Hoek, W., Wooldridge, M. (2002). Model Checking Knowledge and Time. In: Bošnački, D., Leue, S. (eds) Model Checking Software. SPIN 2002. Lecture Notes in Computer Science, vol 2318. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46017-9_9

Download citation

  • DOI: https://doi.org/10.1007/3-540-46017-9_9

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43477-1

  • Online ISBN: 978-3-540-46017-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation