Skip to main content
SpringerLink
Log in

The Refinement of Multi-Agent Systems

  • Chapter
  • First Online:
Specification and Verification of Multi-agent Systems

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 129.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 169.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Dignum, V.: A model for organizational interaction. Ph.D. thesis, Utrecht University (2003)

    Google Scholar 

  2. 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. 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. 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. 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. 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. Safra, S.: Complexity of automata on infinite objects. Ph.D. thesis, Rehovot, Israel (1989). citeseer.ist.psu.edu/safra89complexity.html

    Google Scholar 

  8. 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. 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. Bratman, M.E.: Intentions, Plans, and Practical Reasoning. Harvard University Press: Cambridge, MA (1987)

    Google Scholar 

  11. 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. 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 11

    Google Scholar 

  13. 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. CEUR-WS.org (2007)

    Google Scholar 

  14. Althoff, C.S., Thomas, W., Wallmeier, N.: Observations on determinization of büchi automata. Theor. Comput. Sci. 363(2), 224–233 (2006). DOI http://dx.doi.org/10.1016/j.tcs.2006.07.026

    Google Scholar 

  15. 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)

    Article  MATH  Google Scholar 

  16. 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)

    Article  Google Scholar 

  17. Misra, J.: A programming model for the orchestration of web services. In: SEFM, pp. 2–11. IEEE Computer Society (2004)

    Google Scholar 

  18. Ö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. 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. 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. 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. 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. 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. 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)

    Article  Google Scholar 

  25. Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison Wesley Publishing Company, Inc., Reading, Massachusetts (1988)

    MATH  Google Scholar 

  26. Brzozowski, J.A.: Derivatives of regular expressions. J. ACM 11(4), 481–494 (1964)

    Article  MATH  MathSciNet  Google Scholar 

  27. 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. 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). http://dx.doi.org/10.1016/0304-3975(94)00214-4

  29. 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)

    Article  MATH  MathSciNet  Google Scholar 

  30. 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)

    Article  MATH  MathSciNet  Google Scholar 

  31. 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 

Download references

Author information

Authors and Affiliations

  1. CWI (Centrum Wiskunde en Informatica), Amsterdam, The Netherlands

    L. Aştefănoaei & F.S. de Boer

Authors
  1. L. Aştefănoaei
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. F.S. de Boer
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to L. Aştefănoaei .

Editor information

Editors and Affiliations

  1. Dept. Information & Computing Sciences, Utrecht University, Padualaan 14, Utrecht, 3584 CH, Netherlands

    Mehdi Dastani

  2. Delft University of Technology, Mekelweg 4, Delft, 2628 CD, Netherlands

    Koen V. Hindriks

  3. Dept. Information & Computer Sciences, Utrecht University, Utrecht, Netherlands

    John-Jules Charles Meyer

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer Science+Business Media, LLC

About this chapter

Cite this chapter

Aştefănoaei, L., de Boer, F. (2010). The Refinement of Multi-Agent Systems. In: Dastani, M., Hindriks, K., Meyer, JJ. (eds) Specification and Verification of Multi-agent Systems. Springer, Boston, MA. https://doi.org/10.1007/978-1-4419-6984-2_2

Download citation

  • DOI: https://doi.org/10.1007/978-1-4419-6984-2_2

  • Published:

  • Publisher Name: Springer, Boston, MA

  • Print ISBN: 978-1-4419-6983-5

  • Online ISBN: 978-1-4419-6984-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation