Dynamic Model Checking for Multi-agent Systems

  • Nardine Osman
  • David Robertson
  • Christopher Walton
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4327)


This paper is concerned with the problem of obtaining predictable interactions between groups of agents in open environments when individual agents do not expose their bdi logic. The most popular approaches to this in practise have been to model interaction protocols and to model the deontic constraints imposed by individual agents. Both of these approaches are appropriate and necessary but their combination creates the practical problem of ensuring that interaction protocols are meshed with agents that possess compatible deontic constraints. This is essentially an issue of property checking dynamically at run-time. We show how model checking can be applied to this problem.


Model Check Multiagent System Policy Language Travel Agent Interaction Protocol 
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.
    He, H., Haas, H., Orchard, D.: Web services architecture usage scenarios. W3C Working Group Note (2003),
  2. 2.
    Robertson, D.: Multi-agent coordination as distributed logic programming. In: Demoen, B., Lifschitz, V. (eds.) ICLP 2004. LNCS, vol. 3132, pp. 416–430. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  3. 3.
    Robertson, D.: A lightweight coordination calculus for agent social norms. In: Proceedings of Declarative Agent Languages and Technologies workshop at AAMAS, New York, USA (2004)Google Scholar
  4. 4.
    Stirling, C.: Modal and Temporal Properties of Processes. Texts in Computer Science. Springer, Heidelberg (2001)Google Scholar
  5. 5.
    Stirling, C., Walker, D.: Local model checking in the modal mu-calculus. Theoretical Computer Science 89(1), 161–177 (1991)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., Dong, Y., Du, X., Roychoudhury, A., Venkatakrishnan, V.N.: XMC: a logic-programming-based verification toolset. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 576–580. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  7. 7.
    Sagonas, K., Swift, T., Warren, D.S.: XSB as an efficient deductive database engine. In: Proceedings of the 1994 ACM SIGMOD international conference on Management of data (SIGMOD 1994), pp. 442–453. ACM Press, New York (1994)CrossRefGoogle Scholar
  8. 8.
    Wooldridge, M., Fisher, M., Huget, M.P., Parsons, S.: Model checking multi-agent systems with mable. In: Proceedings of the first international joint conference on Autonomous agents and multiagent systems (AAMAS 2002), pp. 952–959. ACM Press, New York (2002)CrossRefGoogle Scholar
  9. 9.
    Benerecetti, M., Giunchiglia, F., Serafini, L.: Model checking multiagent systems. Journal of Logic and Computation 8(3), 401–423 (1998)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Giordano, L., Martelli, A., Schwind, C.: Verifying communicating agents by model checking in a temporal action logic. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS, vol. 3229, pp. 57–69. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  11. 11.
    Walton, C.: Model checking agent dialogues. In: Leite, J., Omicini, A., Torroni, P., Yolum, p. (eds.) DALT 2004. LNCS, vol. 3476, pp. 132–147. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  12. 12.
    Wen, W., Mizoguchi, F.: Analysis and verification of multi-agent interaction protocols. In: Proceedings of the Sixth Asia-Pacific Software Engineering Conference (APSEC 1999), Takamatsu, Japan, pp. 252–259. IEEE Computer Society, Los Alamitos (1999)CrossRefGoogle Scholar
  13. 13.
    Woźna, B., Lomuscio, A., Penczek, W.: Bounded model checking for knowledge and real time. In: Proceedings of the 4th International Joint Conference on Autonomous Agents and Multi-agent systems (AAMAS 2005), pp. 165–172. ACM Press, New York (2005)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Nardine Osman
    • 1
  • David Robertson
    • 1
  • Christopher Walton
    • 1
  1. 1.School of InformaticsThe University of EdinburghEdinburghUK

Personalised recommendations