GDT4MAS: an extension of the GDT model to specify and to verify MultiAgent systems

ABSTRACT

The Goal Decomposition Tree model has been introduced in 2005 by Mermet et al. [9] to specify and verify the behaviour of an agent evolving in a dynamic environment. This model presents many interesting characteristics such as its compositional aspect and the definition of proven proof schemas making the proof mechanism reliable. Being interested in specifying and verifying multiagent systems, we have decided to extend the GDT model for specifying Multiagent systems. The object of this article is to present this extension. So, after a brief description of the initial GDT model, we show how we extend it by introducing the specification of the whole MAS. We also introduce the notions of agent type and agent, and we show how external goals allow to specify collaborative agents and to prove the correctness of their collaboration. These notions are illustrated on a toy example of the litterature.

REFERENCES

• 1: N. Alechina, M. Dastani, B. Logan, and J.-J. C. Meyer. A Logic of Agent Programs. In Proceedings of the Twenty-Second AAAI Conference on Artificial Intelligence, pages 795--800. AAAI Press, 2007.
• 2: Rafael H. Bordini , Michael Fisher , Carmen Pardavila , Michael Wooldridge, Model checking agentspeak, Proceedings of the second international joint conference on Autonomous agents and multiagent systems, July 14-18, 2003, Melbourne, Australia [doi>10.1145/860575.860641]
• 3: T. Bosse, C. Jonker, L. van der Meij L., A. Sharpanskykh, and J. Treur. Specification and verification of dynamics in agent models. International Journal of Cooperative Information Systems, to appear.
• 4: Mehdi Dastani, 2APL: a practical agent programming language, Autonomous Agents and Multi-Agent Systems, v.16 n.3, p.214-248, June 2008 [doi>10.1007/s10458-008-9036-y]
• 5: Koen V. Hindriks , Frank S. de Boer , Wiebe van der Hoek , John-Jules Ch. Meyer, Agent Programming with Declarative Goals, Proceedings of the 7th International Workshop on Intelligent Agents VII. Agent Theories Architectures and Languages, p.228-243, July 07-09, 2000
• 6: Michael Fisher, Representing and executing agent-based systems, Proceedings of the workshop on agent theories, architectures, and languages on Intelligent agents, p.307-323, March 1995, Amsterdam, The Netherlands
• 7: M. Fisher. MetateM: the story so far. In Programming Multi-Agent Systems, Third International Workshop, ProMAS 2005, volume 3862 of LNCS, pages 3--22. Springer, 2005.
• 8: B. Mermet, G. Simon, B. Zanuttini, and A. Saval. Specifying and verifying a mas: The robots on mars case study. In M. Dastani, A. El-Fallah, A. Ricci, and M. Winikoff, editors, Programming Multi-Agent Systems, 5th International Workshop, ProMAS 2007, volume 4908 of LNAI, pages 172--189. Springer, 2008.
• 9: G. Simon, B. Mermet, and D. Fournier. Goal Decomposition Tree: An agent model to generate a validated agent behaviour. In M. Baldoni, U. Endriss, A. Omicini, and P. Torroni, editors, Declarative Agent Languages and Technologies III: Third International Workshop, DALT 2005, volume 3904 of LNCS, pages 124--140. Springer Verlag, 2006.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques

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

Keywords:
GDTs, multiagent systems, specification, temporal logic, verification