The Refinement of Multi-Agent Systems



This chapter introduces an encompassing theory of refinement which supports a top-down methodology for designing multi-agent systems. We present a general modelling framework where we identify different abstraction levels of BDI agents. On the one hand, at a higher level of abstraction we introduce the language BUnity as a way to specify “what” an agent can do. On the other hand, at a more concrete layer we introduce the language BUpL as implementing not only what an agent can do but also “when” the agent can do. At this stage of individual agent design, refinement is understood as trace inclusion. Having the traces of an implementation included in the traces of a given specification means that the implementation is correct with respect to the specification.

We generalise the theory of agent refinement to multi-agent systems in the presence of new coordination mechanisms extended with real time. The generalisation is such that refinement is compositional. This means that refinement at the individual level implies refinement at the multi-agent system level. Compositionality is an important property since it reduces heavily the verification process. Thus having a theory of refinement is a crucial step towards the verification of multi-agent systems’ correctness.


Transition Rule Linear Temporal Logic Belief Base Label Transition System Conditional Action 
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. 145.
    Dignum, V.: A model for organizational interaction. Ph.D. thesis, Utrecht University (2003)Google Scholar
  2. 368.
    Ricci, A., Viroli, M., Omicini, A.: Give agents their artifacts: the A&A approach for engineering working environments in mas. In: E.H. Durfee, M. Yokoo, M.N. Huhns, O. Shehory (eds.) AAMAS, p. 150. IFAAMAS (2007)Google Scholar
  3. 31.
    Behrmann, G., David, A., Larsen, K.G., Håkansson, J., Pettersson, P., Yi, W., Hendriks, M.: UPPAAL 4.0. In: QEST, pp. 125–126. IEEE Computer Society (2006)Google Scholar
  4. 311.
    Meng, S., Arbab, F.: Web services choreography and orchestration in Reo and constraint automata. In: Y. Cho, R.L. Wainwright, H. Haddad, S.Y. Shin, Y.W. Koo (eds.) SAC, pp. 346–353. ACM (2007)Google Scholar
  5. 49.
    Boella, G., Broersen, J., van der Torre, L.: Reasoning about constitutive norms, counts-as conditionals, institutions, deadlines and violations. In: PRIMA, pp. 86–97 (2008)Google Scholar
  6. 239.
    Hopcroft, J.E., Motwani, R., Rotwani, Ullman, J.D.: Introduction to Automata Theory, Languages and Computability. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA (2000)Google Scholar
  7. 382.
    Safra, S.: Complexity of automata on infinite objects. Ph.D. thesis, Rehovot, Israel (1989). Scholar
  8. 82.
    Bosse, T., Jonker, C.M., van der Meij, L., Sharpanskykh, A., Treur, J.: Specification and verification of dynamics in cognitive agent models. In: IAT, pp. 247–254 (2006)Google Scholar
  9. 196.
    van Glabbeek, R.J.: The linear time-branching time spectrum (extended abstract). In: J.C.M. Baeten, J.W. Klop (eds.) CONCUR, Lecture Notes in Computer Science, vol. 458, pp. 278–297. Springer (1990)Google Scholar
  10. 86.
    Bratman, M.E.: Intentions, Plans, and Practical Reasoning. Harvard University Press: Cambridge, MA (1987)Google Scholar
  11. 214.
    Hessel, A., Larsen, K.G., Mikucionis, M., Nielsen, B., Pettersson, P., Skou, A.: Testing real-time systems using UPPAAL. In: R.M. Hierons, J.P. Bowen, M. Harman (eds.) Formal Methods and Testing, Lecture Notes in Computer Science, vol. 4949, pp. 77–117. Springer (2008)Google Scholar
  12. 421.
    van Riemsdijk, M.B., Astefanoaei, L., de Boer, F.S.: Using the Maude term rewriting language for agent development with formal foundations. In: this volume, Chapter 11Google Scholar
  13. 25.
    Baldoni, M., Baroglio, C., Martelli, A., Patti, V., Schifanella, C.: ervice selection by choreography-driven matching. In: C. Pautasso, T. Gschwind (eds.) WEWST, CEUR Workshop Proceedings, vol. 313. (2007)Google Scholar
  14. 9.
    Althoff, C.S., Thomas, W., Wallmeier, N.: Observations on determinization of büchi automata. Theor. Comput. Sci. 363(2), 224–233 (2006). DOI Google Scholar
  15. 85.
    Bouyer, P., Brinksma, E., Larsen, K.G.: Optimal infinite scheduling for multi-priced timed automata. Formal Methods in System Design 32(1), 3–23 (2008)MATHCrossRefGoogle Scholar
  16. 222.
    Hindriks, K.V., de Boer, F.S., van der Hoek, W., Meyer, J.-J. Ch.: Agent programming in 3APL. Autonomous Agents and Multi-Agent Systems 2(4), 357–401 (1999)CrossRefGoogle Scholar
  17. 317.
    Misra, J.: A programming model for the orchestration of web services. In: SEFM, pp. 2–11. IEEE Computer Society (2004)Google Scholar
  18. 326.
    Ölveczky, P.C., Meseguer, J.: The Real-Time Maude tool. In: C.R. Ramakrishnan, J. Rehof (eds.) TACAS, Lecture Notes in Computer Science, vol. 4963, pp. 332–336. Springer (2008)Google Scholar
  19. 124.
    Dastani, M., Grossi, D., Meyer, J.-J. Ch., Tinnemeier, N.: Normative multi-agent programs and their logics. In: KRAMAS’08: Proceedings of the Workshop on Knowledge Representation for Agents and Multi-Agent Systems (2008)Google Scholar
  20. 10.
    Alur, R.: Timed automata. In: N. Halbwachs, D. Peled (eds.) CAV, Lecture Notes in Computer Science, vol. 1633, pp. 8–22. Springer (1999)Google Scholar
  21. 18.
    Arbab, F., Astefanoaei, L., de Boer, F.S., Dastani, M., Meyer, J.-J. Ch., Tinnemeier, N.: Reo connectors as coordination artifacts in 2APL systems. In: PRIMA, pp. 42–53 (2008)Google Scholar
  22. 105.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.L. (eds.): All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, Lecture Notes in Computer Science, vol. 4350. Springer (2007)Google Scholar
  23. 296.
    Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems. Springer-Verlag New York, Inc., New York, NY, USA (1992)Google Scholar
  24. 73.
    Bordini, R.H., Fisher, M., Visser, W., Wooldridge, M.: Verifying Multi-Agent Programs by Model Checking. Journal of Autonomous Agents and Multi-Agent Systems 12(2), 239–256 (2006)CrossRefGoogle Scholar
  25. 94.
    Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison Wesley Publishing Company, Inc., Reading, Massachusetts (1988)MATHGoogle Scholar
  26. 90.
    Brzozowski, J.A.: Derivatives of regular expressions. J. ACM 11(4), 481–494 (1964)MATHCrossRefMathSciNetGoogle Scholar
  27. 415.
    Tinnemeier, N., Dastani, M., Meyer, J.-J. Ch.: Orwell’s nightmare for agents? programming multi-agent organisations. In: Proc. of ProMAS’08 (2008)Google Scholar
  28. 319.
    Muller, D.E., Schupp, P.E.: Simulating alternating tree automata by nondeterministic automata: new results and new proofs of the theorems of rabin, mcnaughton and safra. Theor. Comput. Sci. 141(1-2), 69–107 (1995).
  29. 60.
    de Boer, F.S., Hindriks, K.V., van der Hoek, W., Meyer, J.-J. Ch.: A Verification Framework for Agent Programming with Declarative Goals. Journal of Applied Logic 5(2), 277–302 (2007)MATHCrossRefMathSciNetGoogle Scholar
  30. 355.
    Raimondi, F., Lomuscio, A.: Automatic Verification of Multi-agent Systems by Model Checking via Ordered Binary Decision Diagrams. Journal of Applied Logic 5(2), 235–251 (2007)MATHCrossRefMathSciNetGoogle Scholar
  31. 190.
    Gelernter, D., Zuck, L.D.: On what linda is: Formal description of linda as a reactive system. In: D. Garlan, D.L. Métayer (eds.) COORDINATION, Lecture Notes in Computer Science, vol. 1282, pp. 187–204. Springer (1997)Google Scholar

Copyright information

© Springer Science+Business Media, LLC 2010

Authors and Affiliations

  1. 1.CWI (Centrum Wiskunde en Informatica)AmsterdamThe Netherlands

Personalised recommendations