[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

Verifying Multi-agent Programs by Model Checking

  • Published:
Autonomous Agents and Multi-Agent Systems Aims and scope Submit manuscript

    We’re sorry, something doesn't seem to be working properly.

    Please try refreshing the page. If that doesn't work, please contact support so we can address the problem.

Abstract

This paper gives an overview of our recent work on an approach to verifying multi-agent programs. We automatically translate multi-agent systems programmed in the logic-based agent-oriented programming language AgentSpeak into either Promela or Java, and then use the associated Spin and JPF model checkers to verify the resulting systems. We also describe the simplified BDI logical language that is used to write the properties we want the systems to satisfy. The approach is illustrated by means of a simple case study.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

  1. E. Allen Emerson (1990) Temporal and modal logic J. Leeuwen Particlevan (Eds) Handbook of theoretical computer science Elsevier Science Amsterdam 997–1072

    Google Scholar 

  2. Benerecetti, M., & Cimatti, A. Symbolic model checking for multi-agent systems. In Proceedings of the model checking and artificial intelligence workshop (MoChArt-2002), held with 15th ECAI, 21–26 July, Lyon, France, (pp. 1–8).

  3. Biesiadecki, J., Maimone, M. W., & Morrison, J. (2001). The Athena SDM rover: A testbed for marsrover mobility. In Sixth international symposium on AI, robotics and automation in space (ISAIRAS-01), June, Montreal, Canada.

  4. Bordini, R. H., Fisher, M., Pardavila, C., & Wooldridge, M. (2003). Model checking AgentSpeak. In J. S. Rosenschein, T. Sandholm, M. Wooldridge, & M. Yokoo (Eds.), Proceedings of the second international joint conference on autonomous agents and multi-agent systems (AAMAS-2003), Melbourne, Australia, 14–18 July, (pp. 409–416) New York, NY, ACM Press.

  5. R. H. Bordini M. Fisher W. Visser M. Wooldridge (2004a) ArticleTitleModel checking rational agents IEEE Intelligent Systems 19 IssueID5 46–52 Occurrence Handle10.1109/MIS.2004.47

    Article  Google Scholar 

  6. Bordini, R. H., Fisher, M., Visser, W., & Wooldridge, M. (2004b) State-space reduction techniques in agent verification. In N. R. Jennings, C. Sierra, L. Sonenberg & M. Tambe (Eds.). Proceedings of the third international joint conference on autonomous agents and multi-agent systems (AAMAS-2004), New York, NY, 19–23 July (pp. 896–903) New York, NY, ACM Press.

  7. Bordini, R. H., Fisher, M., Visser W., & Wooldridge, M (2004c) Verifiable multi-agent programs. In M. Dastani, J. Dix, & A. El Fallah-Seghrouchni, (Eds.)Programming multi-agent systems, proceedings of the first international workshop (ProMAS-03), held with AAMAS-03, 15 July, 2003, Melbourne, Australia (Selected Revised and Invited Papers), number 3067 in Lecture notes in artificial intelligence, (pp. 72–89) Berlin, Springer-Verlag.

  8. Bordini, R. H., Hübner, J. F., et al. (2005) Jason. http://jason.sourceforge.net/.

  9. Bordini, R. H., Hübner, J. F., & Vieira, R. (2005). Jason and the golden fleece of agent-oriented programming. In R. H. Bordini, M. Dastani, J. Dix, & A. El Fallah Seghrouchni, (Eds.) Multi-agent programming: Languages, Platforms and applications, chap. 1 Springer-Verlag.

  10. Bordini, R. H., & Moreira, Á. F. (2004 September). Proving BDI properties of agent-oriented programming languages: The asymmetry thesis principles in AgentSpeak(L). Annals of Mathematics and Artificial Intelligence, 42 (1–3), 197–226. Special issue on computational logic in multi-agent systems.

  11. Bordini R. H., Visser W., Fisher, M., Pardavila, C., & Wooldridge, M. (2003). Model checking multi-agent programs with CASP. In W.A. Hunt Jr. & F. Somenzi, (Eds.) Proceedgins of the fifteenth conference on computer-aided verification (CAV-2003), Boulder, CO, 8–12 July, number 2725 in Lecture Notes in Computer Science, (pp. 110–113) Berlin: Springer-Verlag. Tool description.

  12. E. M. Clarke O. Grumberg D. A. Peled (2000) Model checking The MIT Press Cambridge, MA

    Google Scholar 

  13. P. R. Cohen H. J. Levesque (1990) ArticleTitleIntention is choice with commitment Artificial Intelligence 42 IssueID3 213–261 Occurrence Handle10.1016/0004-3702(90)90055-5 Occurrence Handle91d:68114

    Article  MathSciNet  Google Scholar 

  14. Corbett, J., Dwyer, M., Hatcliff, J., Pasareanu, C., Robby, S. L., & Zheng, H. (2000, June) Bandera : Extracting finite-state models from java source code. In Proceedings of the 22nd international conference on software engineering, Limeric, Ireland: ACM Press.

  15. d’Inverno, M., Kinny, D., Luck, M., & Wooldridge, M. (1998). A formal specification of dMARS. In M. P. Singh, A. S. Rao, & M. Wooldridge, (Eds.), Intelligent agents IV—proceedings of the fourth international workshop on agent theories, architectures, and languages (ATAL-97), providence, RI, 24–26 July, 1997, number 1365 in Lecture notes in artificial intelligence, (pp. 155–176). Berlin: Springer-Verlag.

  16. M. d’Inverno M. Luck (1998) ArticleTitleEngineering AgentSpeak(L): A formal computational model Journal of Logic and Computation 8 IssueID3 1–27

    Google Scholar 

  17. Fisher, M. (2005, January) Temporal development methods for agent-Based systems. Journal of Autonomous Agents and Multi-Agent Systems, 10(1), 41–66.

    Google Scholar 

  18. Fisher, M., & Visser, W. (2002). Verification of autonomous spacecraft control—a logical vision of the future. In Proceedings of the workshop on AI planning and scheduling for autonomy in space applications, co-located with TIME-2002, 7–9 July, Manchester, UK.

  19. D. Harel D. Kozen J. Tiuryn (2000) Dynamic logic The MIT Press Cambridge, MA

    Google Scholar 

  20. Havelund, K., Lowry, M., & Penix, J. (2001, August). Formal analysis of a space craft controller using SPIN. IEEE Transactions on Software Engineering, 27(8).

  21. W. Hoek Particlevan der M. Wooldridge (2002) Model checking knowledge and time D. Bošnački S. Leue (Eds) Model checking software, proceedings of SPIN 2002 (LNCS Volume 2318) Springer-Verlag Berlin, Germany 95–111

    Google Scholar 

  22. Holzmann, G. (1997, May). The Spin model checker. IEEE Transaction on Software Engineering, 23(5), 279–295

    Google Scholar 

  23. Holzmann, G. J. (1991). Design and validation of computer protocols. Prentice Hall.

  24. Java PathFinder. http://javapathfinder.sourceforge.net.

  25. D. Kinny (1993) The distributed multi-agent reasoning system architecture and language specification Australian Artificial Intelligence Institute Melbourne, Australia

    Google Scholar 

  26. Labrou, Y., & Finin, T. (1994, November). A semantics approach for KQML—a general purpose communication language for software agents. In Proceedings of the third international conference on information and knowledge management (CIKM’94). ACM Press.

  27. N. Muscettola P. P. Nayak B. Pell B. C. Williams (1998) ArticleTitleRemote agents: To boldly go where no AI system has gone before Artificial Intelligence 103 5–47 Occurrence Handle10.1016/S0004-3702(98)00068-X

    Article  Google Scholar 

  28. Muscettola, N., Nayak, P. P., Pell, B., & Williams, B. C. (1998b, August) Remote agent: To boldly go where no AI system has gone before. Artificial Intelligence, 103(1–2), 5–47.

  29. G. D. Plotkin (1981) A structural approach to operational semantics Computer Science Department, Aarhus University Aarhus

    Google Scholar 

  30. Rao, A. S. (1996). AgentSpeak(L): BDI agents speak out in a logical computable language. In W. Van de Velde & J. Perram, (Eds.) Proceedings of the seventh workshop on modelling autonomous agents in a multi-agent world (MAAMAW’96) 22–25 January, Eindhoven, The Netherlands, number 1038 in Lecture notes in artificial intelligence (pp. 42–55) London. Springer-Verlag.

  31. Rao, A. S., & Georgeff, M. P. (1993) A model-theoretic approach to the verification of situated reasoning systems. In Proceedings of the thirteenth international joint conference on artificial intelligence (IJCAI-93) (pp. 318–324) Chambéry, France.

  32. A. S. Rao M. P. Georgeff (1998) ArticleTitleDecision procedures for BDI logics Journal of Logic and Computation 8 IssueID3 293–343 Occurrence Handle10.1093/logcom/8.3.293 Occurrence Handle99h:03007

    Article  MathSciNet  Google Scholar 

  33. Robby, M. Dwyer, B., & Hatcliff, J. (2003, March). Bogor: An extensible and highly-modular model checking framework. In In the proceedings of the fourth joint meeting of the european software engineering conference and ACM SIGSOFT symposium on the foundations of software engineering (ESEC/FSE).

  34. Shoham, Y. (1990). Agent-oriented programming. Technical report STAN–CS–1335–90, computer science department, Stanford University, Stanford, CA 94305.

  35. M. P. Singh A. S. Rao M. P. Georgeff (1999) Formal methods in DAI: Logic-based representation and reasoning G. Weiß (Eds) Multiagent systems—a modern approach to distributed artificial intelligence MIT Press Cambridge, MA 331–376

    Google Scholar 

  36. Visser, W., Havelund, K., Brat, G., & Park, S. (2000). Model checking programs. In Proceedings of the fifteenth international conference on automated software engineering (ASE’00), 11–15 September, Grenoble, France (pp. 3–12) IEEE Computer Society.

  37. Washington, R., Golden, K., Bresina, J., Smith, D. E., Anderson, C., & Smith, T. (1999). Autonomous rovers for mars exploration. In Aerospace conference, 6–13 March, Aspen, CO, Vol. 1 (pp. 237–251) IEEE.

  38. M. Wooldridge (2000) Reasoning about rational agents The MIT Press Cambridge, MA

    Google Scholar 

  39. M. Wooldridge M. Fisher M.-P. Huget S. Parsons (2002) Model checking multiagent systems with MABLE C. Castelfranchi W. L. Johnson (Eds) Proceedings of the first international joint conference on autonomous agents and multi-agent systems (AAMAS-2002), 15–19 July, Bologna, Italy ACM Press New York, NY 952–959

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Durham, U.K

    Rafael H. Bordini

  2. University of Liverpool, U.K

    Michael Fisher & Michael Wooldridge

  3. RIACS/NASA Ames Research Center, U.S.A

    Willem Visser

Authors
  1. Rafael H. Bordini
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michael Fisher
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Willem Visser
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Michael Wooldridge
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Rafael H. Bordini.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Bordini, R.H., Fisher, M., Visser, W. et al. Verifying Multi-agent Programs by Model Checking. Auton Agent Multi-Agent Syst 12, 239–256 (2006). https://doi.org/10.1007/s10458-006-5955-7

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10458-006-5955-7

Keywords