Verifying Communicating Agents by Model Checking in a Temporal Action Logic

  • Laura Giordano
  • Alberto Martelli
  • Camilla Schwind
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3229)


In this paper we address the problem of specifying and verifying systems of communicating agents in a Dynamic Linear Time Temporal Logic (DLTL). This logic provides a simple formalization of the communicative actions in terms of their effects and preconditions. Furthermore it allows to specify interaction protocols by means of temporal constraints representing permissions and commitments. Agent programs, when known, can be formulated in DLTL as complex actions (regular programs). The paper addresses several kinds of verification problems including the problem of compliance of agents to the protocol, and describes how they can be solved by model checking in DLTL using automata.


Model Check Multiagent System Social Approach Interaction Protocol Domain Description 
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.
    Alberti, M., Daolio, D., Torroni, P.: Specification and Verification of Agent Interaction Protocols in a Logic-based System. In: SAC 2004 (March 2004)Google Scholar
  2. 2.
    Bacchus, F., Kabanza, F.: Planning for temporally extended goals. Annals of Mathematics and AI 22, 5–27 (1998)zbMATHMathSciNetGoogle Scholar
  3. 3.
    Benerecetti, M., Giunchiglia, F., Serafini, L.: Model Checking Multiagent Systems. Journal of Logic and Computation. Special Issue on Computational Aspects of Multi-Agent Systems 8(3), 401–423 (1998)zbMATHMathSciNetGoogle Scholar
  4. 4.
    Bordini, R., Fisher, M., Pardavila, C., Wooldridge, M.: Model Checking AgentSpeak. In: AAMAS 2003, pp. 409–416 (2003)Google Scholar
  5. 5.
    Calvanese, D., De Giacomo, G., Vardi, M.Y.: Reasoning about Actions and Planning in LTL Action Theories. In: Proc. KR 2002 (2002)Google Scholar
  6. 6.
    FIPA Contract Net Interaction Protocol Specification (2002), Available at
  7. 7.
    Fornara, N., Colombetti, M.: Defining Interaction Protocols using a Commitment-based Agent Communication Language. In: Proc. AAMAS 2003, Melbourne, pp. 520–527 (2003)Google Scholar
  8. 8.
    Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple On-the-fly Automatic verification of Linear Temporal Logic. In: Proc. 15th Work. Protocol Specification, Testing and Verification, Warsaw, June 1995, North Holland, Amsterdam (1995)Google Scholar
  9. 9.
    Giordano, L., Martelli, A.: On-the-fly Automata Construction for Dynamic Linear Time Temporal Logic. In: TIME 2004 (June 2004)Google Scholar
  10. 10.
    Giordano, L., Martelli, A., Schwind, C.: Reasoning About Actions in Dynamic Linear Time Temporal Logic. In: FAPR 2000 - Int. Conf. on Pure and Applied Practical Reasoning, London (September 2000); Also in The Logic Journal of the IGPL 9(2), 289-303 (March 2001)Google Scholar
  11. 11.
    Giordano, L., Martelli, A., Schwind, C.: Specifying and Verifying Systems of Communicating Agents in a Temporal Action Logic. In: Cappelli, A., Turini, F. (eds.) AI*IA 2003. LNCS (LNAI), vol. 2829, pp. 262–274. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  12. 12.
    Giunchiglia, F., Traverso, P.: Planning as Model Checking. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS, vol. 1809, pp. 1–20. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  13. 13.
    Guerin, F.: Specifying Agent Communication Languages. PhD Thesis, Imperial College, London (April 2002)Google Scholar
  14. 14.
    Guerin, F., Pitt, J.: Verification and Compliance Testing. In: Huget, M.-P. (ed.) Communication in Multiagent Systems. LNCS (LNAI), vol. 2650, pp. 98–112. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  15. 15.
    Henriksen, J.G., Thiagarajan, P.S.: Dynamic Linear Time Temporal Logic. Annals of Pure and Applied logic 96(1-3), 187–207 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    Huget, M.P., Wooldridge, M.: Model Checking for ACL Compliance Verification. In: Dignum, F.P.M. (ed.) ACL 2003. LNCS (LNAI), vol. 2922, pp. 75–90. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  17. 17.
    Pistore, M., Traverso, P.: Planning as Model Checking for Extended Goals in Non-deterministic Domains. In: Proc. IJCAI 2001, Seattle, pp. 479–484 (2001)Google Scholar
  18. 18.
    Reiter, R.: The frame problem in the situation calculus: a simple solution (sometimes) and a completeness result for goal regression. In: Lifschitz, V. (ed.) Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pp. 359–380. Academic Press, London (1991)Google Scholar
  19. 19.
    Singh, M.P.: A social semantics for Agent Communication Languages. In: IJCAI 1998 Workshop on Agent Communication Languages, Springer, Berlin (2000)Google Scholar
  20. 20.
    Wooldridge, M.: Semantic Issues in the Verification of Agent Communication Languages. Autonomous Agents and Multi-Agent Systems 3, 9–31 (2000)CrossRefGoogle Scholar
  21. 21.
    Wooldridge, M., Fisher, M., Huget, M.P., Parsons, S.: Model Checking Multi- Agent Systems with MABLE. In: AAMAS 2002, Bologna, Italy, pp. 952–959 (2002)Google Scholar
  22. 22.
    Yolum, P., Singh, M.P.: Flexible Protocol Specification and Execution: Applying Event Calculus Planning using Commitments. In: AAMAS 2002, Bologna, Italy, pp. 527–534 (2002)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Laura Giordano
    • 1
  • Alberto Martelli
    • 2
  • Camilla Schwind
    • 3
  1. 1.Dipartimento di InformaticaUniversità del Piemonte OrientaleAlessandria
  2. 2.Dipartimento di InformaticaUniversità di TorinoTorino
  3. 3.MAP, CNRSMarseilleFrance

Personalised recommendations