Advertisement

Model Checking for PRS-Like Agents

  • Wayne Wobcke
  • Marc Chee
  • Krystian Ji
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3809)

Abstract

The key problem in applying verification techniques such as model checking to agent architectures is to show how to map systematically from an agent program to a model structure that not only includes the possible behaviours of the agent in its environment, but which also captures appropriate mental notions, such as belief, desire and intention, that may be used by the designer to reason about the agent. In this paper, we present an algorithm providing a mapping from agent programs under a simplified PRS-type agent architecture to a reachability graph structure extended to include representations of beliefs, goals and intentions, and illustrate the translation with a simple “waypoint following” agent. We conclude with a brief discussion of the differences between the internal (operational) notion of intention used in the architecture and the formal (external) notion of intention used in the modelling.

Keywords

Model Check Multiagent System Agent Program Execution Path Execution State 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Bordini, R.H., Fisher, M., Pardavila, C., Wooldridge, M.: Model Checking AgentSpeak. In: Proceedings of the Second International Joint Conference on Autonomous Agents and Multiagent Systems, pp. 409–416 (2003)Google Scholar
  2. 2.
    Bratman, M.E.: Intention, Plans, and Practical Reason. Harvard University Press, Cambridge (1987)Google Scholar
  3. 3.
    Cohen, P.R., Levesque, H.J.: Intention is Choice with Commitment. Artificial Intelligence 42, 213–261 (1990)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)zbMATHGoogle Scholar
  5. 5.
    Georgeff, M.P., Lansky, A.L.: Reactive Reasoning and Planning. In: Proceedings of the Sixth National Conference on Artificial Intelligence (AAAI-1987), pp. 677–682 (1987)Google Scholar
  6. 6.
    Harel, D.: First-Order Dynamic Logic. Springer, Berlin (1979)zbMATHGoogle Scholar
  7. 7.
    Holzmann, G.J.: The Model Checker SPIN. IEEE Transactions on Software Engineering 23(5), 279–295 (1997)CrossRefMathSciNetGoogle Scholar
  8. 8.
    Penczek, W., Lomuscio, A.: Verifying Epistemic Properties of Multi-agent Systems via Bounded Model Checking. In: Proceedings of the Second International Joint Conference on Autonomous Agents and Multiagent Systems, pp. 209–216 (2003)Google Scholar
  9. 9.
    Raimondi, F., Lomuscio, A.: Verification of Multiagent Systems via Ordered Binary Decision Diagrams: An Algorithm and Its Implementation. In: Proceedings of the Third International Joint Conference on Autonomous Agents and Multiagent Systems, pp. 630–637 (2004)Google Scholar
  10. 10.
    Rao, A.S.: AgentSpeak(L): BDI Agents Speak Out in a Logical Computable Language. In: Van de Velde, W., Perram, J.W. (eds.) Agents Breaking Away. Springer, Berlin (1996)Google Scholar
  11. 11.
    Rao, A.S., Georgeff, M.P.: Modeling Rational Agents within a BDI-Architecture. In: Proceedings of the Second International Conference on Principles of Knowledge Representation and Reasoning (KR 1991), pp. 473–484 (1991)Google Scholar
  12. 12.
    Rao, A.S., Georgeff, M.P.: An Abstract Architecture for Rational Agents. In: Proceedings of the Third International Conference on Principles of Knowledge Representation and Reasoning (KR 1992), pp. 439–449 (1992)Google Scholar
  13. 13.
    Rao, A.S., Georgeff, M.P.: A Model-Theoretic Approach to the Verification of Situated Reasoning Systems. In: Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence, pp. 318–324 (1993)Google Scholar
  14. 14.
    Rao, A.S., Georgeff, M.P.: Decision Procedures for BDI Logics. Journal of Logic and Computation 8, 293–343 (1998)zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    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.) Foundations of Software Technology and Theoretical Computer Science: 19th Conference. Springer, Berlin (1999)Google Scholar
  16. 16.
    Wobcke, W.R.: An Operational Semantics for a PRS-like Agent Architecture. In: Stumptner, M., Corbett, D., Brooks, M. (eds.) AI 2001: Advances in Artificial Intelligence. Springer, Berlin (2001)Google Scholar
  17. 17.
    Wobcke, W.R.: Modelling PRS-like Agents’ Mental States. In: Ishizuka, M., Sattar, A. (eds.) PRICAI 2002: Trends in Artificial Intelligence. Springer, Berlin (2002)Google Scholar
  18. 18.
    Wobcke, W.R.: Model Theory for PRS-Like Agents: Modelling Belief Update and Action Attempts. In: Zhang, C., Guesgen, H.W., Yeap, W.K. (eds.) PRICAI 2004: Trends in Artificial Intelligence. Springer, Berlin (2004)Google Scholar
  19. 19.
    Wooldridge, M.J.: Reasoning About Rational Agents. MIT Press, Cambridge (2000)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Wayne Wobcke
    • 1
  • Marc Chee
    • 1
  • Krystian Ji
    • 1
    • 2
  1. 1.School of Computer Science and EngineeringUniversity of New South WalesSydneyAustralia
  2. 2.National ICT AustraliaUniversity of New South WalesSydneyAustralia

Personalised recommendations