Specification and Design of Multi-agent Applications Using Temporal Z

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


This paper proposes a formal approach, based on stepwise refinements, for specifying and designing multi-agent applications. This approach provides a specification language which integrates temporal logic in the Z notation allowing, in this way, to cover static, behavioural, as well as dynamic aspects of multi-agent systems. Moreover, it proposes a methodology giving a set of hints and principles which help and guide the design process. Indeed, this methodology enables the user to develop step by step, in an incremental way, an implementation starting from an abstract requirements (goal) specification. Finally, we illustrate our approach by developing an agent based solution for the pursuit problem.


Temporal Logic Atomic Formula Linear Temporal Logic Active Entity Temporal Formula 
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.
    d’Inverno, M., Kinny, D., Luck, M., Wooldridge, M.: A formal specification of dMARS. In: Intelligent Agents IV: Proceedings of the Fourth International Workshop on Agent Theories, Architectures and Languages (1998)Google Scholar
  2. 2.
    El Fallah, A.: Représentation et manipulation de plans à l’aide des réseaux de Petri. Actes des 2èmes Journées Francophones IAD-SMA (1994)Google Scholar
  3. 3.
    Jmaiel, M., Pepper, P.: Development of communication protocols using algebraic and temporal specifications. Computer Networks Journal 42, 737–764 (2003)zbMATHCrossRefGoogle Scholar
  4. 4.
    Kolyang, R., Santen, T., Wolff, B.: A structure preserving encoding of Z in isabelle-Hol. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 283–298. Springer, Heidelberg (1996)Google Scholar
  5. 5.
    Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, Heidelberg (1992)Google Scholar
  6. 6.
    Meisels, I., Saaltink, M.: The Z/EVES 2.0 reference manual. Technical Report TR-99-5493-03e, ORA Canada, Canada (1999)Google Scholar
  7. 7.
    Spivey, M.: The Z notation, 2nd edn. Prentice Hall International, Englewood Cliffs (1992)Google Scholar
  8. 8.
    Von, V.: An Integration of Z and Timed CSP for specifying Real-Time Embedded Systems. PhD thesis (2002)Google Scholar
  9. 9.
    Woodcock, J., Davies, J.: Using Z: Specification, Refinement and Proof. Prentice Hall, Englewood Cliffs (1996)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  1. 1.Faculté des SciencesÉconomiques et de Gestion de SfaxSfaxTunisia
  2. 2.B.P.W.École Nationale d’Ingénieurs de SfaxSfaxTunisia

Personalised recommendations