Model Checking for Epistemic and Temporal Properties of Uncertain Agents

Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4088)


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.


Model Check Temporal Logic Multiagent System Epistemic Logic Kripke Structure 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bacchus, F.: Representing and reasoning with probabilistic knowledge: a logical approach to probabilities. MIT Press, Cambridge, Mass (1990)Google Scholar
  2. 2.
    Bourahla, M., Benmohamed, M.: Model Checking Multi-Agent Systems. Informatica 29, 189–197 (2005)zbMATHGoogle Scholar
  3. 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. 4.
    Clarke, E.M., Grumberg, J.O., Peled, D.A.: Model checking. MIT Press, Cambridge (1999)Google Scholar
  5. 5.
    Cao, Z., Shi, C.: Probabilistic Belief Logic and Its Probabilistic Aumann Semantics. J. Comput. Sci. Technol. 18(5), 571–579 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 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. 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)CrossRefGoogle Scholar
  8. 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)CrossRefGoogle Scholar
  9. 9.
    Fagin, R., Halpern, J.Y.: Reasoning about knowledge and probability. J. ACM 41(2), 340–367 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about knowledge. The MIT Press, Cambridge (1995)zbMATHGoogle Scholar
  11. 11.
    Halpern, J.Y., Moses, Y.: Knowledge and common knowledge in a distributed environment. J. ACM 37(3), 549–587 (1990)zbMATHCrossRefMathSciNetGoogle Scholar
  12. 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. 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)CrossRefGoogle Scholar
  14. 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)zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    Jurdzinski, M.: Deciding the winner in parity games is in UP∩co-UP. Information Processing Letters 68, 119–134 (1998)CrossRefMathSciNetGoogle Scholar
  16. 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. 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. 18.
    Kooi, B.P.: Probabilistic Dynamic Epistemic Logic. Journal of Logic, Language and Information 12, 381–408 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    McMillan, K.L.: Symbolic model checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, Dordrecht (1993)Google Scholar
  20. 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. 21.
    Walukiewicz, I.: Completeness of Kozen’s axiomatisation of the propositional μ-calculus. Information and Computation 157, 142–182 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  22. 22.
    Wooldridge, M., Fisher, M., Huget, M., Parsons, S.: Model checking multiagent systems with mable. In: AAMAS 2002, pp. 952–959 (2002)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  1. 1.Department of Computer Science and EngineeringNanjing University of Aero. & Astro.NanjingChina

Personalised recommendations