Skip to main content
SpringerLink
Log in

Revisiting Satisfiability and Model-Checking for CTLK with Synchrony and Perfect Recall

  • Conference paper
Computational Logic in Multi-Agent Systems (CLIMA 2008)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 5405))

Included in the following conference series:

Abstract

We show that CTL with knowledge modalities but without common knowledge has an undecidable satisfiability problem in the synchronous perfect recall semantics. We also present an adaptation of the classical model-checking algorithm for CTL that handles knowledge operators.

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. Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions of Programming Languages and Systems 8(2), 244–263 (1986)

    Article  MATH  Google Scholar 

  2. Dickhöfer, M., Wilke, T.: Timed alternating tree automata: The automata-theoretic solution to the TCTL model checking problem. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 281–290. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  3. Elgaard, J., Klarlund, N., Møller, A.: Mona 1.x: New techniques for ws1s and ws2s. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 516–520. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  4. Elgot, C.C., Rabin, M.O.: Decidability and undecidability of extensions of second (first) order theory of (generalized) successor. Journal of Symbolic Logic 31(2), 169–181 (1966)

    Article  MATH  Google Scholar 

  5. Fagin, R., Halpern, J., Vardi, M.: Reasoning about knowledge. The MIT Press, Cambridge (2004)

    MATH  Google Scholar 

  6. Halpern, J.Y., Vardi, M.Y.: The complexity of reasoning about knowledge and time: Extended abstract. In: Proceedings of STOC 1986, pp. 304–315 (1986), https://www.cs.rice.edu/~vardi/papers/stoc86r1.pdf.gz

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

    Article  MathSciNet  MATH  Google Scholar 

  8. Kacprzak, M., Lomuscio, A., Niewiadomski, A., Penczek, W., Raimondi, F., Szreter, M.: Comparing BDD and SAT based techniques for model checking Chaum’s Dining Cryptographers Protocol. Fundamenta Informaticae 72(1-3), 215–234 (2006)

    MathSciNet  MATH  Google Scholar 

  9. Lind, D., Marcus, B.: An Introduction to Symbolic Dynamics and Coding. Cambridge University Press, Cambridge (1995)

    Book  MATH  Google Scholar 

  10. Lomuscio, A., Raimondi, F.: The complexity of model checking concurrent programs against CTLK specifications. In: Baldoni, M., Endriss, U. (eds.) DALT 2006. LNCS, vol. 4327, pp. 29–42. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  11. Raimondi, F., Lomuscio, A.: Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams. Journal of Applied Logic 5(2), 235–251 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  12. Shilov, N.V., Garanina, N.O.: Model checking knowledge and fixpoints. In: Proceedings of FICS 2002, Extended version available as Preprint 98, pp. 25–39. Ershov Institute of Informatics, Novosibirsk (2002)

    Google Scholar 

  13. Thomas, W.: Infinite trees and automaton-definable relations over ω-words. Theoretical Computer Science 103(1), 143–159 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  14. van Benthem, J., Pacuit, E.: The tree of knowledge in action: Towards a common perspective. In: Governatori, G., Hodkinson, I.M., Venema, Y. (eds.) Proceedings of AiML 2006, pp. 87–106. College Publications (2006)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  16. 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, pp. 432–445. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LACL, Université Paris Est – Université Paris 12, 61 av. du Général de Gaulle, 94010, Créteil, France

    Cătălin Dima

Authors
  1. Cătălin Dima
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Imperial College London, Ashton Street, L69 3BX, Liverpool, UK

    Michael Fisher

  2. Department of Computing, Imperial College London, 180 Queen’s Gate, SW7 2AZ, London, UK

    Fariba Sadri

  3. Department of Computer Science, Artificial Intelligence Institute, Computational Logic Group, Dresden University of Technology, Nöthnitzer Str. 46, 01187, Dresden, Germany

    Michael Thielscher

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Dima, C. (2009). Revisiting Satisfiability and Model-Checking for CTLK with Synchrony and Perfect Recall. In: Fisher, M., Sadri, F., Thielscher, M. (eds) Computational Logic in Multi-Agent Systems. CLIMA 2008. Lecture Notes in Computer Science(), vol 5405. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02734-5_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-02734-5_8

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-02733-8

  • Online ISBN: 978-3-642-02734-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation