Skip to main content
SpringerLink
Log in
Book cover

Pacific Rim International Workshop on Multi-Agents

PRIMA 2006: Agent Computing and Multi-Agent Systems pp 46–58Cite as

Model Checking for Epistemic and Temporal Properties of Uncertain Agents

  • Conference paper

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

Abstract

In this paper, we introduce a probabilistic epistemic temporal logic, called PETL, which is a combination of temporal logic and probabilistic knowledge logic. The model checking algorithm is given. Furthermore, we present a probabilistic epistemic temporal logic, called μPETL, which generalizes μ-calculus by adding probabilistic knowledge modality. Similar to μ-calculus, μPETL is a succinct and expressive language. It is showed that temporal modalities such as “always”, “sometime” and “until”, and probabilistic knowledge modalities such as “probabilistic knowledge” and “probabilistic common knowledge” can be expressed in such a logic. PETL is proven to be a sublogic of μPETL. The model checking technique for μPETL is also studied.

This work was supported by the National Science Foundation of China under Grant 60473036.

This is a preview of subscription content, 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   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bacchus, F.: Representing and reasoning with probabilistic knowledge: a logical approach to probabilities. MIT Press, Cambridge, Mass (1990)

    Google Scholar 

  2. Bourahla, M., Benmohamed, M.: Model Checking Multi-Agent Systems. Informatica 29, 189–197 (2005)

    MATH  Google Scholar 

  3. Bradfield, J., Stirling, C.: Modal Logics and mu-Calculi: An Introduction. In: Handbook of Process Algebra, Ch. 4, Elsevier, Amsterdam (2001)

    Google Scholar 

  4. Clarke, E.M., Grumberg, J.O., Peled, D.A.: Model checking. MIT Press, Cambridge (1999)

    Google Scholar 

  5. Cao, Z., Shi, C.: Probabilistic Belief Logic and Its Probabilistic Aumann Semantics. J. Comput. Sci. Technol. 18(5), 571–579 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  6. van Ditmarsch, H., van der Hoek, W., Kooi, B.P.: Dynamic Epistemic Logic with Assignment. In: AAMAS-2005, pp. 141–148 (2005)

    Google Scholar 

  7. de, N., Ferreira, C., Fisher, M., van der Hoek, W.: Practical Reasoning for Uncertain Agents. In: Alferes, J.J., Leite, J.A. (eds.) JELIA 2004. LNCS (LNAI), vol. 3229, pp. 82–94. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  8. de, N., Ferreira, C., Fisher, M., van der Hoek, W.: Logical Implementation of Uncertain Agents. In: Bento, C., Cardoso, A., Dias, G. (eds.) EPIA 2005. LNCS (LNAI), vol. 3808, pp. 536–547. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  9. Fagin, R., Halpern, J.Y.: Reasoning about knowledge and probability. J. ACM 41(2), 340–367 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  10. Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about knowledge. The MIT Press, Cambridge (1995)

    MATH  Google Scholar 

  11. Halpern, J.Y., Moses, Y.: Knowledge and common knowledge in a distributed environment. J. ACM 37(3), 549–587 (1990)

    Article  MATH  MathSciNet  Google Scholar 

  12. van der Hoek, W.: Some considerations on the logic PFD: A logic combining modality and probability. J. Applied Non-Classical Logics 7(3), 287–307 (1997)

    Google Scholar 

  13. van der Hoek, W., Wooldridge, M.: Model Checking Knowledge, and Time. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 95–111. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  14. van der Hoek, W., Wooldridge, M.: Cooperation, Knowledge, and Time: Alternating-time Temporal Epistemic Logic and its Applications. Studia Logica 75, 125–157 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  15. Jurdzinski, M.: Deciding the winner in parity games is in UP∩co-UP. Information Processing Letters 68, 119–134 (1998)

    Article  MathSciNet  Google Scholar 

  16. Jurdzinski, M., Paterson, M., Zwick, U.: A Deterministic Subexponential Algorithm for Solving Parity Games. In: Proceedings of ACM-SIAM Symposium on Discrete Algorithms, SODA 2006, pp. 117–123 (2006)

    Google Scholar 

  17. Kacprzak, M., Lomuscio, A., Penczek, W.: Verification of multiagent systems via unbounded model checking. In: AAMAS 2004, pp. 638–645 (2004)

    Google Scholar 

  18. Kooi, B.P.: Probabilistic Dynamic Epistemic Logic. Journal of Logic, Language and Information 12, 381–408 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  19. McMillan, K.L.: Symbolic model checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, Dordrecht (1993)

    Google Scholar 

  20. Milch, B., Koller, D.: Probabilistic Models for Agent’s Beliefs and Decisions. In: Proc. 16th Conference on Uncertainty in Artificial Intelligence, pp. 389–396 (2000)

    Google Scholar 

  21. Walukiewicz, I.: Completeness of Kozen’s axiomatisation of the propositional μ-calculus. Information and Computation 157, 142–182 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  22. Wooldridge, M., Fisher, M., Huget, M., Parsons, S.: Model checking multiagent systems with mable. In: AAMAS 2002, pp. 952–959 (2002)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science and Engineering, Nanjing University of Aero. & Astro., Nanjing, 210016, China

    Zining Cao

Authors
  1. Zining Cao
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Key Laboratory of Intelligent Information Processing, Institute of Computing Technology, Chinese Academy of Sciences, 100080, Beijing

    Zhong-Zhi Shi

  2. Asian Institute of Technology, P.O. Box 4, 12120, Klong Luang, Pathumthani, Thailand

    Ramakoti Sadananda

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cao, Z. (2006). Model Checking for Epistemic and Temporal Properties of Uncertain Agents. In: Shi, ZZ., Sadananda, R. (eds) Agent Computing and Multi-Agent Systems. PRIMA 2006. Lecture Notes in Computer Science(), vol 4088. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11802372_8

Download citation

  • DOI: https://doi.org/10.1007/11802372_8

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-36707-9

  • Online ISBN: 978-3-540-36860-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation