Skip to main content
SpringerLink
Log in

Model Checking Knowledge and Linear Time: PSPACE Cases

  • Conference paper
Book cover Logical Foundations of Computer Science (LFCS 2007)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4514))

Included in the following conference series:

Abstract

We present a general algorithm scheme for model checking logics of knowledge, common knowledge and linear time, based on bisimulations to a class of structures that capture the way that agents update their knowledge. We show that the scheme leads to PSPACE implementations of model checking the logic of knowledge and linear time in several special cases: perfect recall systems with a single agent or in which all communication is by synchronous broadcast, and systems in which knowledge is interpreted using either the agents’ current observation only or its current observation and clock value. In all these results, common knowledge operators may be included in the language. Matching lower bounds are provided, and it is shown that although the complexity bound matches the PSPACE complexity of the linear time temporal logic LTL, as a function of the model size the problems considered have a higher complexity than LTL.

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

Access this chapter

Log in via an institution
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.

References

  1. Baltag, A., Moss, L.S., Solecki, S.: The logic of public announcements, common knowledge, and private suspicions. In: TARK ’98: Proc. 7th Conf. Theoretical Aspects of Rationality and Knowledge, pp. 43–56 (1998)

    Google Scholar 

  2. Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. J. ACM 28(1), 114–133 (1981)

    MATH  MathSciNet  Google Scholar 

  3. Cimatti, A., Pecheur, C., Cavada, R.: Formal verification of diagnosability via symbolic model checking. In: IJCAI, pp. 363–369 (2003)

    Google Scholar 

  4. Cimatti, A., Pecheur, C., Lomuscio, A.: Applications of model checking for multi-agent systems: Verification of diagnosability and recoverability. In: CS&P ’05: Proc. Int. Work. Concurrency, Specification, and Programming (2005)

    Google Scholar 

  5. Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)

    MATH  Google Scholar 

  6. Fisler, K., Vardi, M.Y.: Bisimulation and model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 338–342. Springer, Heidelberg (1999)

    Google Scholar 

  7. Gammie, P., van der Meyden, R.: MCK: Model checking the logic of knowledge. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 479–483. Springer, Heidelberg (2004)

    Google Scholar 

  8. Shilov, N.V., Garanina, N.O.: Well-structured model checking of multiagent systems. In: Virbitskaite, I., Voronkov, A. (eds.) PSI 2006. LNCS, vol. 4378, pp. 363–376. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  9. Halpern, J.Y., Moses, Y.: Knowledge and Common Knowledge in a Distributed Environment. J. ACM 37(3) (1990)

    Google Scholar 

  10. Halpern, J.Y., O’Neill, K.R.: Anonymity and information hiding in multiagent systems. In: CSFW, pp. 75–88. IEEE Computer Society Press, Los Alamitos (2003)

    Google Scholar 

  11. Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: POPL ’85: Proc. 12th ACM SIGACT-SIGPLAN Symp. Principles of Programming Languages, pp. 97–107. ACM Press, New York (1985)

    Chapter  Google Scholar 

  12. Lomuscio, A., Raimondi, F.: The complexity of model checking concurrent programs against CTLK specifications. In: Nakashima, H., Wellman, M.P., Weiss, G., Stone, P. (eds.) AAMAS, pp. 548–550. ACM Press, New York (2006)

    Chapter  Google Scholar 

  13. Lomuscio, A., Raimondi, F.: MCMAS: A model checker for multi-agent systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, pp. 450–454. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  14. Park, D.M.R.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981)

    Chapter  Google Scholar 

  15. Savitch, W.J.: Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci. 4(2), 177–192 (1970)

    MATH  MathSciNet  Google Scholar 

  16. Shilov, N.V., Garanina, N.O.: Model checking knowledge and fixpoints. In: Ésik, Z., Ingólfsdóttir, A. (eds.) FICS, volume NS-02-2 of BRICS Notes Series, pp. 25–39. University of Aarhus (2002)

    Google Scholar 

  17. Shilov, N.V., Garanina, N.O., Choe, K.-M.: Update and abstraction in model checking of knowledge and branching time. Fundamenta Informaticae 72(1–3), 347–361 (2006)

    MATH  MathSciNet  Google Scholar 

  18. Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733–749 (1985)

    MATH  MathSciNet  Google Scholar 

  19. Sweazey, P., Smith, A.J.: A class of compatible cache consistency protocols and their support by the IEEE futurebus. In: ISCA ’86: Proc. 13th Int. Symp. Computer Architecture, pp. 414–423. IEEE Computer Society Press, Los Alamitos (1986)

    Google Scholar 

  20. Syverson, P.F.: Knowledge, belief, and semantics in the analysis of cryptographic protocols. J. Computer Security 1(3–4), 317–334 (1992)

    Google Scholar 

  21. 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)

    Google Scholar 

  22. van der Meyden, R.: Common knowledge and update in finite environments. Information and Computation 140(2), 115–157 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  23. van der Meyden, R., Shilov, N.V.: Model checking knowledge and time in systems with perfect recall (extended abstract). In: Pandu Rangan, C., Raman, V., Ramanujam, R. (eds.) FST TCS 1999. LNCS, vol. 1738, p. 432. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  24. van der Meyden, R., Su, K.: Symbolic model checking the knowledge of the dining cryptographers. In: CFSW 2004: Proc. 17th IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, Los Alamitos (2004)

    Google Scholar 

  25. van der Meyden, R., Wilke, T.: Synthesis of distributed systems from knowledge-based specifications. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 562–576. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  26. van der Meyden, R., Zhang, C.: Algorithmic verification of noninterference properties. In: Proceedings Workshop on Views on Designing Complex Systems, Bertinoro, Italy, Sep. 2006. ENTCS, to appear (2006)

    Google Scholar 

  27. van Eijck, J., Orzan, S.: Modelling the epistemics of communication with functional programming. In: van Eekelen, M. (ed.) TFP ’05: 6th Symp. Trends in Functional Programming, pp. 44–59 (2005)

    Google Scholar 

  28. Vardi, M.Y.: Implementing knowledge-based programs. In: Shoham, Y. (ed.) TARK ’96: Proc. 6th Conf. Theoretical Aspects of Rationality and Knowledge, pp. 15–30. Morgan Kaufmann, San Francisco (1996)

    Google Scholar 

  29. Vardi, M.Y., Wolper, P.: Automata theoretic techniques for modal logics of programs (extended abstract). In: STOC, pp. 446–456. ACM Press, New York (1984)

    Google Scholar 

  30. Wozna, B., Lomuscio, A., Penczek, W.: Bounded model checking for knowledge and real time. In: AAMAS ’05: 4th Int. J. Conf. Autonomous Agents and Multiagent Systems, Utrecht, 25–29 July 2005, pp. 165–172. ACM Press, New York (2005)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science and Engineering, The University of New South Wales, and National ICT Australia , Sydney, NSW 2052, Australia

    Kai Engelhardt, Peter Gammie & Ron van der Meyden

Authors
  1. Kai Engelhardt
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Peter Gammie
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ron van der Meyden
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Sergei N. Artemov Anil Nerode

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer Berlin Heidelberg

About this paper

Cite this paper

Engelhardt, K., Gammie, P., van der Meyden, R. (2007). Model Checking Knowledge and Linear Time: PSPACE Cases. In: Artemov, S.N., Nerode, A. (eds) Logical Foundations of Computer Science. LFCS 2007. Lecture Notes in Computer Science, vol 4514. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72734-7_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-72734-7_14

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-72732-3

  • Online ISBN: 978-3-540-72734-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation