Skip to main content
SpringerLink
Log in

Directions for Agent Model Checking*

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

Abstract

In this chapter we provide a perspective on current and future work in the area of agent model-checking. In particular, we describe our approach, which was the first to provide comprehensive verification of practical agent programming languages. It provides a library of general agent concepts that has been formally defined and implemented in Java, upon which interpreters for various agent programming languages can be succinctly programmed. The Java library has been prepared so that it can be efficiently used with an existing Java model checker, thus facilitating the verification of (heterogeneous) multi-agent programs. Besides giving an overview of our approach, in this chapter we identify its current shortfalls and discuss where we aim to target future development.

* This work was partially supported by EPSRC, through projects EP/D054788 and EP/D052548.

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.

  1. Rao, A.S., Georgeff, M.: BDI Agents: From Theory to Practice. In: Proceedings of the First International Conference on Multi-Agent Systems (ICMAS), pp. 312–319. San Francisco, CA (1995)

    Google Scholar 

  2. Cohen, P.R., Levesque, H.J.: Intention is choice with commitment. Artificial Intelligence 42(2-3), 213–261 (1990)

    Article  MATH  MathSciNet  Google Scholar 

  3. Fisher, M.: MetateM: The Story so Far. In: Proc. 3rd International Workshop on Programming Multiagent Systems (ProMAS), LNAI, vol. 3862, pp. 3–22. Springer Verlag (2006)

    Google Scholar 

  4. Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley (2003)

    Google Scholar 

  5. Fisher, M., Kakoudakis, T.: Flexible Agent Grouping in Executable Temporal Logic. In: Gergatsoulis, Rondogiannis (eds.) Intensional Programming II. World Scientific Publishing Co. (2000)

    Google Scholar 

  6. Bordini, R.H., Dastani, M., Dix, J., El Fallah Seghrouchni, A. (eds.): Multi-Agent Programming: Languages, Platforms and Applications. Springer-Verlag (2005)

    Google Scholar 

  7. Pokahr, A., Braubach, L., Lamersdorf, W.: Jadex: A BDI reasoning engine. chap. 6, pp. 149–174

    Google Scholar 

  8. Fisher, M., Ghidini, C., Hirsch, B.: Programming Groups of Rational Agents. In: Computational Logic in Multi-Agent Systems (CLIMA-IV), Lecture Notes in Computer Science, vol. 3259, pp. 849–856. Springer-Verlag (2004)

    Google Scholar 

  9. Ricci, A., Viroli, M., Cimadamore, M.: Prototyping Concurrent Systems with Agents and Artifacts: Framework and Core Calculus. Electronic Notes in Theoretical Computer Science 194(4), 111–132 (2008)

    Article  Google Scholar 

  10. Ferber, J., Gutknecht, O.: A Meta-model for the Analysis and Design of Organizations in Multi-agent Systems. In: Proc. Third International Conference on Multi-Agent Systems (ICMAS), pp. 128–135 (1998)

    Google Scholar 

  11. Sierhuis, M.: Multiagent Modeling and Simulation in Human-Robot Mission Operations (2006). (http://ic.arc.nasa.gov/ic/publications)

  12. Bordini, R.H., Fisher, M., Visser, W., Wooldridge, M.: State-Space Reduction Techniques in Agent Verification. In: Proceedings of the 3rd International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS), pp. 896–903. IEEE Computer Society (2004)

    Google Scholar 

  13. Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model Checking Programs. Automated Software Engineering 10(2), 203–232 (2003)

    Article  Google Scholar 

  14. Visser, W., Pasareanu, C.S., Khurshid, S.: Test Input Generation with Java PathFinder. In: Proc. ACM/SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), pp. 97–107 (2004)

    Google Scholar 

  15. Rao, A.S., Georgeff, M.P.: An Abstract Architecture for Rational Agents. In: Proc. International Conference on Knowledge Representation and Reasoning (KR&R), pp. 439–449 (1992)

    Google Scholar 

  16. Dastani, M., Tinnemeier, N.A.M., Meyer, J.-J. Ch.: A programming language for normative multi-agent systems. In: V. Dignum (ed.) Multi-Agent Systems: Semantics and Dynamics of Organizational Models, chap. 16. IGI Global (2008)

    Google Scholar 

  17. Walton, C.D.: Verifiable Agent Dialogues. Journal of Applied Logic 5(2), 197–213 (2007)

    Article  MATH  MathSciNet  Google Scholar 

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

  19. Hepple, A., Dennis, L.A., Fisher, M.: A Common Basis for Agent Organisations in BDI Languages. In: Proc. International Workshop on LAnguages, methodologies and Development tools for multi-agent systemS (LADS), Lecture Notes in Artificial Intelligence, vol. 5118, pp. 171–88. Springer-Verlag (2008)

    Google Scholar 

  20. Gardelli, L., Viroli, M., Omicini, A.: Design Patterns for Self-Organizing Multiagent Systems. In: Proc. 2nd International Workshop on Engineering Emergence in Decentralised Autonomic Systems (EEDAS), pp. 61–70. CMS Press, London, UK (2007)

    Google Scholar 

  21. Rao, A.S., Georgeff, M.P.: Decision Procedures for BDI Logics. Journal of Logic and Computation 8(3), 293–342 (1998)

    Article  MATH  MathSciNet  Google Scholar 

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

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

  24. Fox, M.S.: An Organizational View of Distributed Systems. In: Distributed Artificial Intelligence, pp. 140–150. Morgan Kaufmann Publishers Inc., San Francisco, USA (1988)

    Google Scholar 

  25. Xu, B., Qian, J., Zhang, X., Wu, Z., Chen, L.: A Brief Survey of Program Slicing. SIGSOFT Software Engineering Notes 30(2), 1–36 (2005)

    Article  Google Scholar 

  26. Cohen, P.R., Levesque, H.J.: Teamwork. Tech. Rep. 504, SRI International, Menlo Park, CA (1991)

    Google Scholar 

  27. Dennis, L.A., Farwer, B.: Gwendolen: A BDI Language for Verifiable Agents. In: B. Löwe (ed.) Logic and the Simulation of Interaction and Reasoning. AISB, Aberdeen (2008)

    Google Scholar 

  28. Kumar, S., Cohen, P.R.: STAPLE: An Agent Programming Language Based on the Joint Intention Theory. In: Proc. 3rd International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS), pp. 1390–1391. IEEE Computer Society (2004)

    Google Scholar 

  29. Smith, R.G., Davis, R.: Frameworks for Cooperation in Distributed Problem Solving. IEEE Transactions on Systems, Man, and Cybernetics 11(1) (1980)

    Google Scholar 

  30. Wooldridge, M.: Reasoning about Rational Agents. MIT Press (2000)

    Google Scholar 

  31. Paulson, L.C.: A Generic Theorem Prover, Lecture Notes in Computer Science, vol. 828. Springer-Verlag (1994)

    Google Scholar 

  32. Dennis, L.A., Hepple, A., Fisher, M.: Language Constructs for Multi-Agent Programming. In: Proc. 8th International Workshop on Computational Logic in Multi-Agent Systems (CLIMA), Lecture Notes in Artificial Intelligence, vol. 5056, pp. 137–156. Springer (2008)

    Google Scholar 

  33. Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press (2004). (2nd Edition)

    Google Scholar 

  34. Dennis, L.A., Farwer, B., Bordini, R.H., Fisher, M., Wooldridge, M.: A Common Semantic Basis for BDI Languages. In: Proc. 7th International Workshop on Programming Multiagent Systems (ProMAS), Lecture Notes in Artificial Intelligence, vol. 4908, pp. 124–139. Springer Verlag (2008)

    Google Scholar 

  35. Dennis, L.A., Tinnemeier, N.A.M., Meyer, J.-J. Ch.: Model checking normative agent organisations. In: Computational Logic in Multi-Agent Systems (CLIMA-X) (2009). To Appear

    Google Scholar 

  36. Fisher, M., Ghidini, C., Kakoudakis, T.: Dynamic Team Formation in Executable Agent-Based Systems. In: Rouff et al. [374]

    Google Scholar 

  37. Bordini, R.H., Hübner, J.F., Wooldridge, M.: Programming Multi-Agent Systems in AgentSpeak Using Jason. Wiley Series in Agent Technology. John Wiley & Sons (2007)

    Google Scholar 

  38. Zambonelli, F., Jennings, N.R., Wooldridge, M.: Organisational Rules as an Abstraction for the Analysis and Design of Multi-Agent Systems. International Journal of Software Engineering and Knowledge Engineering 11(3), 303–328 (2001)

    Article  Google Scholar 

  39. Hübner, J.F., Sichman, J.S., Boissier, O.: A Model for the Structural, Functional, and Deontic Specification of Organizations in Multiagent Systems. In: Proc. 16th Brazilian Symposium on Artificial Intelligence (SBIA), pp. 118–128. Springer-Verlag, London, UK (2002)

    Google Scholar 

  40. Vázquez-Salceda, J., Dignum, V., Dignum, F.: Organizing Multiagent Systems. Journal of Autonomous Agents and Multi-Agent Systems 11(3), 307–360 (2005)

    Article  Google Scholar 

  41. Pynadath, D.V., Tambe, M., Chauvat, N., Cavedon, L.: Towards Team-Oriented Programming. In: Intelligent Agents VI — Proc. 6th International Workshop on Agent Theories, Architectures, and Languages (ATAL), Lecture Notes in Artificial Intelligence, vol. 1757, pp. 233–247. Springer-Verlag (1999)

    Google Scholar 

  42. Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems 8(2), 244–263 (1986)

    Article  MATH  Google Scholar 

  43. Berezin, S., Clarke, E.M., Biere, A., Zhu, Y.: Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function. Formal Methods in System Design 20(2), 159–186 (2002)

    Article  MATH  Google Scholar 

  44. Floyd, R.W.: Assigning Meaning to Programs. In: J.T. Schwartz (ed.) Mathematical Aspects of Computer Science: Proc. American Mathematics Soc. symposia, vol. 19, pp. 19–31. American Mathematical Society, Providence RI (1967)

    Google Scholar 

  45. Bratman, M.E.: Intentions, Plans, and Practical Reasoning. Harvard University Press: Cambridge, MA (1987)

    Google Scholar 

  46. Pynadath, D.V., Tambe, M.: The Communicative Multiagent Team Decision Problem: Analyzing Teamwork Theories and Models. Journal of Artificial Intelligence Research 16, 389–423 (2002)

    MATH  MathSciNet  Google Scholar 

  47. Tip, F.: A Survey of Program Slicing Techniques. Journal of Programming Languages 3(3), 121–189 (1995)

    Google Scholar 

  48. Meyer, J.-J Ch., van der Hoek, W., van Linder, B.: A Logical Approach to the Dynamics of Commitments. Artificial Intelligence 113(1-2), 1–40 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  49. Bordini, R.H., Dastani, M., Dix, J., El Fallah Seghrouchni, A. (eds.): Multi-Agent Programming: Languages, Tools and Applications. Springer-Verlag (2009)

    Google Scholar 

  50. Lewis, D., Dobson, S.: Autonomic, Pervasive and Context-Aware Systems. Jouranl of Network System Management 15(1), 1–3 (2007)

    Article  Google Scholar 

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

  52. Ferber, J., Gutknecht, O., Michel, F.: From Agents to Organizations: An Organizational View of Multi-agent Systems, vol. 2935, pp. 214–230. Springer (2004)

    Google Scholar 

  53. Georgeff, M.P., Lansky, A.L.: Reactive Reasoning and Planning. In: Proc. American National Conference on Artificial Intelligence (AAAI), pp. 677–682 (1987)

    Google Scholar 

  54. Fisher, M., Bordini, R.H., Sierhuis, M.: Analysing Human-Agent Teamwork. In: Proc. 10th ESA Workshop on Advanced Space Technologies for Robotics and Automation (ASTRA). Katwijk, Netherlands. (2008)

    Google Scholar 

  55. Levesque, H.J., Cohen, P.R., Nunes, J.H.T.: On Acting Together. In: Proc. 8th American National Conference on Artificial Intelligence (AAAI), pp. 94–99 (1990)

    Google Scholar 

  56. Cohen, P.R., Levesque, H.J.: Confirmations and Joint Action. In: Proc. International Joint Conference on Artificial Intelligence (IJCAI), pp. 951–959 (1991)

    Google Scholar 

  57. Rao, A.S.: AgentSpeak(L): BDI agents speak out in a logical computable language. In: W.V. de Velde, J. Perrame (eds.) Agents Breaking Away: Proceedings of the Seventh European Workshop on Modelling Autonomous Agents in a Multi-Agent World (MAAMAW’96), pp. 42–55. Springer Verlag, LNAI 1038 (1996)

    Google Scholar 

  58. Fisher, M., Bordini, R., Hirsch, B., Torroni, P.: Computational Logics and Agents: A Roadmap of Current Technologies and Future Trends. Computational Intelligence 23(1), 61–91 (2007)

    Article  MathSciNet  Google Scholar 

  59. Bordini, R.H., Fisher, M., Wooldridge, M., Visser, W.: Property-Based Slicing for Agent Verification. Journal of Logic and Computation to appear (2009)

    Google Scholar 

  60. Bordini, R.H., Fisher, M., Visser, W., Wooldridge, M.: Model Checking Rational Agents. IEEE Intelligent Systems 19(5), 46–52 (2004)

    Google Scholar 

  61. Cimatti, A., Clarke, E., Giunchuglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Proc. 14th International Conference on Computer Aided Verification (CAV), LNCS, vol. 2404, pp. 359–364. Springer-Verlag (2002)

    Google Scholar 

  62. Ball, T., Rajamani, S.K.: The SLAM Toolkit. In: Proc. 13th International Conference on Computer Aided Verification (CAV), Lecture Notes in Computer Science, vol. 2102, pp. 260–264. Springer (2001)

    Google Scholar 

  63. Tidhar, G.: Team-Oriented Programming: Preliminary Report. Tech. Rep. 1993-41, Australian Artificial Intelligence Institute (1993)

    Google Scholar 

  64. Tambe, M.: Teamwork in Real-world Dynamic Environments. In: Proc. 1st International Conference on Multi–Agent Systems (ICMAS). MIT Press (1995)

    Google Scholar 

  65. Kinny, D., Ljungberg, M., Rao, A.S., Sonenberg, E., Tidhar, G., Werner, E.: Planned Team Activity. In: Artificial Social Systems — Selected Papers from the Fourth European Workshop on Modelling Autonomous Agents and Multi-Agent Worlds (MAAMAW), Lecture Notes in Artificial Intelligence, vol. 830, pp. 226–256. Springer-Verlag (1992)

    Google Scholar 

  66. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)

    Google Scholar 

  67. Bordini, R.H., Fisher, M., Sierhuis, M.: Formal Verification of Human-robot Teamwork. In: Proceedings of the 4th ACM/IEEE International Conference on Human Robot Interaction (HRI), pp. 267–268. ACM (2009)

    Google Scholar 

  68. Hirsch, B.: Programming Rational Agents. Ph.D. thesis, Department of Computer Science, University of Liverpool (2005)

    Google Scholar 

  69. Bordini, R.H., Dennis, L.A., Farwer, B., Fisher, M.: Automated Verification of Multi-Agent Programs. In: Proc. 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 69–78 (2008)

    Google Scholar 

  70. Dennis, L.A., Fisher, M.: Programming Verifiable Heterogeneous Agent Systems. In: Proc. 6th International Workshop on Programming in Multi-Agent Systems (ProMAS), Lecture Notes in Computer Science, vol. 5442, pp. 40–55. Springer Verlag (2008)

    Google Scholar 

  71. Sierhuis, M.: Modeling and Simulating Work Practice. BRAHMS: a multiagent modeling and simulation language for work system analysis and design. Ph.D. thesis, Social Science and Informatics (SWI), University of Amsterdam, SIKS Dissertation Series No. 2001-10, Amsterdam, The Netherlands (2001)

    Google Scholar 

  72. Dastani, M., van Riemsdijk, M.B., Meyer, J.-J. Ch.: Programming Multi-Agent Systems in 3APL. chap. 2, pp. 39–67

    Google Scholar 

  73. Rao, A.S., Georgeff, M.P.: Modeling Agents within a BDI-Architecture. In: Proc. International Conference on Principles of Knowledge Representation and Reasoning (KR&R). Morgan Kaufmann, Cambridge, Massachusetts (1991)

    Google Scholar 

  74. Winikoff, M.: Implementing Commitment-Based Interactions. In: Proc. 6th International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS), pp. 1–8. ACM, New York, NY, USA (2007)

    Google Scholar 

  75. Maruichi, T., Ichikawa, M., Tokoro, M.: Modelling Autonomous Agents and their Groups. In: Y. Demazeau, J.P. Müller (eds.) Decentralized AI 2 — Proc. 2nd European Workshop on Modelling Autonomous Agents and Multi-Agent Worlds (MAAMAW). Elsevier/North Holland (1991)

    Google Scholar 

  76. Webster, M.P., Dennis, L.A., Fisher, M.: Model-Checking Auctions, Coalitions and Trust. Tech. Rep. ULCS-09-004, University of Liverpool, Department of Computer Science (2009). http://www.csc.liv.ac.uk/research/

Download references

Author information

Authors and Affiliations

  1. Institute of Informatics, Federal University of Rio Grande do Sul, Porto Alegre, RS, Brazil

    R.H. Bordini

  2. Department of Computer Science, University of Liverpool, Liverpool, UK

    L.A. Dennis & M. Fisher

  3. School of Engineering and Computing Sciences, Durham University, Durham, UK

    B. Farwer

Authors
  1. R.H. Bordini
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. L.A. Dennis
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. B. Farwer
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. M. Fisher
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to R.H. Bordini .

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

Bordini, R., Dennis, L., Farwer, B., Fisher, M. (2010). Directions for Agent Model Checking*. 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_4

Download citation

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

  • 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