Model checking agentspeak

ABSTRACT

This paper introduces ASF, a variation of the BDI logic programming language ASL intended to permit the model-theoretic verification of multi-agent systems. After briefly introducing ASF and discussing its relationship to ASL, we show how ASF programs can be transformed into Prm, the model specification language for the Spin model-checking system. We also describe how specifications written in a simplified form of BDI logic can be transformed into Spin-format linear temporal logic formulae. With our approach, it is thus possible to automatically verify whether or not multi-agent systems implemented in ASF satisfy specifications expressed as BDI logic formulæ. We illustrate our approach with a short case study, in which we show how BDI properties of a simulated auction system implemented in ASF were verified.

REFERENCES

• 1: Massimo Benerecetti , Fausto Giunchiglia, Model Checking-Based Analysis of Multiagent Systems, Proceedings of the First International Workshop on Formal Approaches to Agent-Based Systems-Revised Papers, p.1-15, April 05-07, 2000
• 2: Rafael H. Bordini , Ana L. C. Bazzan , Rafael de O. Jannone , Daniel M. Basso , Rosa M. Vicari , Victor R. Lesser, AgentSpeak(XL): efficient intention selection in BDI agents via decision-theoretic task scheduling, Proceedings of the first international joint conference on Autonomous agents and multiagent systems: part 3, July 15-19, 2002, Bologna, Italy [doi>10.1145/545056.545122]
• 3: R. H. Bordini and Á. F. Moreira. Proving the asymmetry thesis principles for a BDI agent-oriented programming language. Electronic Notes in Theoretical Computer Science, 70(5), 2002.
• 4: E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press: Cambridge, MA, 2000.
• 5: M. d'Inverno and M. Luck. Engineering AgentSpeak(L): A formal computational model. J. Logic and Computation, 8(3):1--27, 1998.
• 6: M. Fisher and W. Visser. Verification of autonomous spacecraft control --- a logical vision of the future. In Proc. Workshop on AI Planning and Scheduling For Autonomy in Space Applications, Manchester, UK, 2002.
• 7: Klaus Havelund , Mike Lowry , John Penix, Formal Analysis of a Space-Craft Controller Using SPIN, IEEE Transactions on Software Engineering, v.27 n.8, p.749-765, August 2001 [doi>10.1109/32.940728]
• 8: Wiebe van der Hoek , Michael Wooldridge, Model Checking Knowledge and Time, Proceedings of the 9th International SPIN Workshop on Model Checking of Software, p.95-111, April 11-13, 2002
• 9: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 10: Rodrigo Machado , Rafael H. Bordini, Running AgentSpeak(L) Agents on SIM_AGENT, Revised Papers from the 8th International Workshop on Intelligent Agents VIII, p.158-174, August 01-03, 2001
• 11: Á. F. Moreira and R. H. Bordini. An operational semantics for a BDI agent-oriented programming language. In Proc. Workshop on Logics for Agent-Based Systems (LABS-02), held in conjunction with the Eighth International Conf. on Principles of Knowledge Representation and Reasoning (KR-2002), Toulouse, France, pages 45--59, 2002.
• 12: Nicola Muscettola , P. Pandurang Nayak , Barney Pell , Brian C. Williams, Remote Agent: to boldly go where no AI system has gone before, Artificial Intelligence, v.103 n.1-2, p.5-47, Aug. 1998 [doi>10.1016/S0004-3702(98)00068-X]
• 13: Anand S. Rao, AgentSpeak(L): BDI agents speak out in a logical computable language, Proceedings of the 7th European workshop on Modelling autonomous agents in a multi-agent world : agents breaking away: agents breaking away, p.42-55, February 1996, Einhoven, The Netherlands
• 14: A. S. Rao and M. P. Georgeff. A model-theoretic approach to the verification of situated reasoning systems. In Proc. Thirteenth International Joint Conf. on Artificial Intelligence (IJCAI-93), pages 318--324, Chambéry, France, 1993.
• 15: A. S. Rao and M. P. Georgeff. Decision procedures for BDI logics. J. Logic and Computation, 8(3):293--343, 1998.
• 16: Willem Visser , Klaus Havelund , Guillaume Brat , SeungJoon Park, Model Checking Programs, Proceedings of the 15th IEEE international conference on Automated software engineering, p.3, September 11-15, 2000
• 17: M. Wooldridge. Reasoning about Rational Agents. The MIT Press, Cambridge, MA, 2000.
• 18: Michael Wooldridge , Michael Fisher , Marc-Philippe Huget , Simon Parsons, Model checking multi-agent systems with MABLE, Proceedings of the first international joint conference on Autonomous agents and multiagent systems: part 2, July 15-19, 2002, Bologna, Italy [doi>10.1145/544862.544965]

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
        I.2.11 Distributed Artificial Intelligence
            Subjects: Languages and structures

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
        I.2.11 Distributed Artificial Intelligence
            Subjects: Multiagent systems

General Terms:
Languages, Verification

Keywords:
AgentSpeak, BDI logic programming, model checking, spin