Towards a Formal Methodology for Designing Multi-agent Applications

  • Amira Regayeg
  • Ahmed Hadj Kacem
  • Mohamed Jmaiel
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3550)


This paper has two purposes. First, it defines a formal language for specifying multi-agent systems. This language is expressive enough to cover individual agent aspects (knowledge, goals, roles, ...) as well as collective aspects of in terms of coordination protocols, organization structure and planning activities. Second, it provides a formal design methodology based on stepwise refinements allowing to develop a design specification starting from an abstract requirements one.


Temporal Logic Linear Temporal Logic Local Goal Active Entity Interaction Protocol 
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.
    Bjorner, D.: New results and trends in formal techniques for the development of software for transportation systems. In: Tarnai, G., Schnieder, E. (eds.) Proceedings of the FORMS2003: Symposium on Formal Methods for Railway Operation and Control Systems, Braunschweig, Germany, pp. 69–76 (1999)Google Scholar
  2. 2.
    Deloach, S., Wood, M.: Analysis and design using mase and agenttool. In: Proceedings of the 12th Midwest Artificial Intelligence and Cognitive Science Conference MAICS 2001. Miami University. Oxford, Ohio (2001)Google Scholar
  3. 3.
    Erasmy, F., Sekerinski, E.: Stepwise refinement of control software-a case study using raise. In: Naftalin, M., Bertrán, M., Denvir, T. (eds.) FME 1994. LNCS, vol. 873, pp. 547–566. Springer, Heidelberg (1994)Google Scholar
  4. 4.
    Fisher, M.: A survey of concurrent MetateM – the language and its applications. In: Gabbay, D.M., Ohlbach, H.J. (eds.) ICTL 1994. LNCS, vol. 827, pp. 480–505. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  5. 5.
    Glaser, N.: The comomas methodology and enironment for multi-agent system development. In: Dickson, L., Zhang, C. (eds.) DAI 1996. LNCS, vol. 1286, pp. 1–16. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  6. 6.
    Hoare, C.A.: Communicating Sequential Processes. Prentice Hall International, Englewood Cliffs (1985)zbMATHGoogle Scholar
  7. 7.
    Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)Google Scholar
  8. 8.
    Jmaiel, M., Pepper, P.: Development of communication protocols using algebraic and temporal specifications. Computer Networks Journal 42, 737–764 (2003)zbMATHCrossRefGoogle Scholar
  9. 9.
    Loulou, M., Hadj-Kacem, A., Jmaiel, M.: Formalization of cooperation in MAS: Towards a generic conceptual model. In: Lemaître, C., Reyes, C.A., González, J.A. (eds.) IBERAMIA 2004. LNCS (LNAI), vol. 3315, pp. 43–52. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  10. 10.
    Luck, M., d’Inverno, M.: A formal framework for agency and autonomy. In: Proceedings of the first international conference on Multi-Agent Systems, pp. 254–260. AAAI Press/MIT Press (1995)Google Scholar
  11. 11.
    Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, Heidelberg (1992)Google Scholar
  12. 12.
    Meisels, I., Saaltink, M.: The Z/EVES 2.0 reference manual. Technical Report TR-99-5493-03e, ORA Canada, Canada (1999)Google Scholar
  13. 13.
    Omicini, A.: Soda: Societies and infrastructures in the analysis and design of agent-based systems. In: Ciancarini, P., Wooldridge, M.J. (eds.) AOSE 2000. LNCS, vol. 1957, pp. 185–193. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  14. 14.
    Padgham, L., Winikoff, M.: Prometheus: A methodology for developing intelligent agents. In: Giunchiglia, F., Odell, J.J., Weiss, G. (eds.) AOSE 2002. LNCS, vol. 2585, pp. 174–185. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  15. 15.
    Regayeg, A., Hadj-Kacem, A., Jmaiel, M.: Specification and Verification of Multi-Agent Applications using Temporal Z. In: Proceedings of IEEE/WIC/ACM International Conference on Intelligent Agent Technology (IAT 2004), Beijing, China, pp. 260–266 (September 2004)Google Scholar
  16. 16.
    Regayeg, A., Hadj-Kacem, A., Jmaiel, M.: Towards a formal methodology for developing multi-agent applications using temporal Z. In: The 3rd ACS/IEEE International Conference on Computer Systems and Applications (AICCSA 2005), Cairo, Egypt (January 2005)Google Scholar
  17. 17.
    Sannella, D.: Algebraic specification and program development by stepwise refinement. In: Bossi, A. (ed.) LOPSTR 1999. LNCS, vol. 1817, pp. 1–9. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  18. 18.
    Spivey, M.: The Z notation, 2nd edn. Prentice Hall International, Englewood Cliffs (1992)Google Scholar
  19. 19.
    Wooldridge, M., Jenning, N., Kinny, D.: The Gaia methodology for agent-oriented analysis and design. Autonomous Agents 3 (2000)Google Scholar
  20. 20.
    Wooldridge, M., Jennings, N.R., Kinny, D.: A methodology for agent-oriented analysis and design. In: Etzioni, O., Müller, J.P., Bradshaw, J.M. (eds.) Proceedings of the Third International Conference on Autonomous Agents (Agents 1999), Seattle, WA, USA, pp. 69–76. ACM Press, New York (1999)CrossRefGoogle Scholar
  21. 21.
    Xu, H., Shatz, S.M.: A framework for model-based design of agent-oriented software. IEEE Transactions on Software Engineering 29(1), 15–30 (2003)CrossRefGoogle Scholar
  22. 22.
    Zambonelli, F., Omicini, A.: Challenges and research directions in agent-oriented software engineering. Autonomous Agents and Multi-Agent Systems 9(3), 253–283 (2004)CrossRefGoogle Scholar
  23. 23.
    Zhu, H.: A formal specification language for agent-oriented software engineering. In: Proceedings of AAMAS 2003, pp. 1174–1175, Melbourne, Australia (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Amira Regayeg
    • 1
  • Ahmed Hadj Kacem
    • 1
  • Mohamed Jmaiel
    • 2
  1. 1.Faculté des Sciences Économiques et de Gestion de SfaxSfaxTunisia
  2. 2.École Nationale d’Ingénieurs de Sfax, B.P.W.SfaxTunisia

Personalised recommendations