Formalizing Properties of Mobile Agent Systems

  • Lorenzo Bettini
  • Rocco De Nicola
  • Michele Loreti
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2315)


The wide-spreading of Internet has stimulated the introduction of new programming paradigms and languages that model interactions among hosts by means of mobile agents, and that are centered around the notions of location awareness. In this paper we show how to use formal tools, specifically a modal logic, for formalizing properties for mobile agent systems. We concentrate on one of these new languages, Klaim, and we use it to specify a system that permits maintaining the software installed on several heterogeneous computers distributed over a network by taking advantage of the mobile agent paradigm.


Modal Logic Mobile Agent Private Locality Abstract Action Formal Tool 
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.
    L. Bettini, R. De Nicola, G. Ferrari, and R. Pugliese. Interactive Mobile Agents in X-Klaim. In P. Ciancarini and R. Tolksdorf, editors, Proc. of the 7th Int. IEEE Workshops on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE), pages 110–115. IEEE Computer Society Press, 1998.Google Scholar
  2. 2.
    L. Bettini, R. De Nicola, and M. Loreti. Software Update via Mobile Agent Based Programming. In Proc. of ACM SAC 2002, Special Track on Agents, Interactions, Mobility, and Systems. ACM Press, 2002. To appear.Google Scholar
  3. 3.
    L. Caires and L. Cardelli. A Spatial Logic for Concurrency (Part I). In proceeding of TACS2001, 2001. to appear.Google Scholar
  4. 4.
    L. Cardelli and A. D. Gordon. Mobile Ambients. In M. Nivat, editor, Foundations of Software Science and Computation Structures (FoSSaCS’98), volume 1378 of LNCS, pages 140–155. Springer, 1998.CrossRefGoogle Scholar
  5. 5.
    L. Cardelli and A. D. Gordon. Anytime, Anywhere: Modal Logics for Mobile Ambients. In 27th Annual Symposium on Principles of Programming Languages (POPL) (Boston, MA). ACM, 2000.Google Scholar
  6. 6.
    L. Cardelli and A. D. Gordon. Logical Properties of Name Restriction. In proceeding of TLCA’01, volume 2044 of Lecure Note in Computer Science. Springer, 2001.Google Scholar
  7. 7.
    N. Carriero and D. Gelernter. Linda in Context. Comm. of the ACM, 32(4):444–458, 1989.CrossRefGoogle Scholar
  8. 8.
    A. Carzaniga, G. Picco, and G. Vigna. Designing Distributed Applications with Mobile Code Paradigms. In R. Taylor, editor, Proc. of the 19th Int. Conf. on Software Engineering (ICSE’ 97), pages 22–33. ACM Press, 1997.Google Scholar
  9. 9.
    R. De Nicola, G. Ferrari, and R. Pugliese. Klaim: a Kernel Language for Agents Interaction and Mobility. IEEE Transactions on Software Engineering, 24(5):315–330, 1998.CrossRefGoogle Scholar
  10. 10.
    R. De Nicola and M. Loreti. A Modal Logic for Klaim. In T. Rus, editor, Proc of Algebraic Methodology and Software Technology, 8th Int. Conf. AMAST 2000, number 1816 in LNCS, pages 339–354. Springer, 2000.CrossRefGoogle Scholar
  11. 11.
    R. De Nicola and M. Loreti. A Modal Logic for Mobile Agents. Technical report, Dipartimento di Sistemi ed Informatica, Universitá degli Studi di Firenze, 2001. available at
  12. 12.
    D. Gelernter. Generative Communication in Linda. ACM Transactions on Programming Languages and Systems, 7(1):80–112, 1985.zbMATHCrossRefGoogle Scholar
  13. 13.
    C. Harrison, D. Chess, and A. Kershenbaum. Mobile agents: Are they a good idea? Research Report 19887, IBM Research Division, 1994.Google Scholar
  14. 14.
    M. Hennessy and R. Milner. Algebraic Laws for Nondeterminism and Concurrency. Journal of the ACM, 32(1):137–161, Jan. 1985.zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    F. Knabe. An overview of mobile agent programming. In Proceedings of the Fifth LOMAPS workshop on Analysis and Veri.cation of Multiple—Agent Languages, number 1192 in LNCS. Springer-Verlag, 1996.Google Scholar
  16. 16.
    D. Lange and M. Oshima. Seven good reasons for mobile agents. Communications of the ACM, 42(3):88–89, March 1999.CrossRefGoogle Scholar
  17. 17.
    X. Leroy, D. Rémy, J. Vouillon, and D. Doligez. The Objective Caml system, documentation and user’s guide., 1999.
  18. 18.
    M. Loreti. Languages and Logics for Network Aware Programming. PhD thesis, Università di Siena, 2002. Available at
  19. 19.
    R. Milner. Communication and Concurrency. Prentice Hall, 1989.Google Scholar
  20. 20.
    R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, Part I. LFCS Report Series ECS-LFCS-89-85, University of Edinburgh, June 1989.Google Scholar
  21. 21.
    R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, Part II. LFCS Report Series ECS-LFCS-89-86, University of Edinburgh, June 1989.Google Scholar
  22. 22.
    R. Milner, J. Parrow, and D. Walker. Modal logics for mobile processes. Theoretical Computer Science, 114:149–171, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  23. 23.
    A. Park and P. Reichl. Personal Disconnected Operations with Mobile Agents. In Proc. of 3rd Workshop on Personal Wireless Communications, PWC’98, 1998.Google Scholar
  24. 24.
    T. Thorn. Programming Languages for Mobile Code. ACM Computing Surveys, 29(3):213–239, 1997. Also Technical Report 1083, University of Rennes IRISA.CrossRefGoogle Scholar
  25. 25.
    J. E. White. Telescript Technology: The Foundation for the Electronic Marketplace. White paper, General Magic, Inc., Mountain View, CA, 1994.Google Scholar
  26. 26.
    J. E. White. Mobile Agents. In J. Bradshaw, editor, Software Agents. AAAI Press and MIT Press, 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Lorenzo Bettini
    • 1
  • Rocco De Nicola
    • 1
  • Michele Loreti
    • 1
  1. 1.Dipartimento di Sistemi e InformaticaUniversitá di FirenzeItaly

Personalised recommendations