Abstract
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.
This research has been partially supported by the project PRIN 2003 “Logic-based development and verification of multi-agent systems”, and by the European Commission within the 6th Framework Programme project REWERSE number 506779
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alberti, M., Daolio, D., Torroni, P.: Specification and Verification of Agent Interaction Protocols in a Logic-based System. In: SAC 2004 (March 2004)
Bacchus, F., Kabanza, F.: Planning for temporally extended goals. Annals of Mathematics and AI 22, 5–27 (1998)
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)
Bordini, R., Fisher, M., Pardavila, C., Wooldridge, M.: Model Checking AgentSpeak. In: AAMAS 2003, pp. 409–416 (2003)
Calvanese, D., De Giacomo, G., Vardi, M.Y.: Reasoning about Actions and Planning in LTL Action Theories. In: Proc. KR 2002 (2002)
FIPA Contract Net Interaction Protocol Specification (2002), Available at http://www.fipa.org
Fornara, N., Colombetti, M.: Defining Interaction Protocols using a Commitment-based Agent Communication Language. In: Proc. AAMAS 2003, Melbourne, pp. 520–527 (2003)
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)
Giordano, L., Martelli, A.: On-the-fly Automata Construction for Dynamic Linear Time Temporal Logic. In: TIME 2004 (June 2004)
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)
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)
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)
Guerin, F.: Specifying Agent Communication Languages. PhD Thesis, Imperial College, London (April 2002)
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)
Henriksen, J.G., Thiagarajan, P.S.: Dynamic Linear Time Temporal Logic. Annals of Pure and Applied logic 96(1-3), 187–207 (1999)
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)
Pistore, M., Traverso, P.: Planning as Model Checking for Extended Goals in Non-deterministic Domains. In: Proc. IJCAI 2001, Seattle, pp. 479–484 (2001)
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)
Singh, M.P.: A social semantics for Agent Communication Languages. In: IJCAI 1998 Workshop on Agent Communication Languages, Springer, Berlin (2000)
Wooldridge, M.: Semantic Issues in the Verification of Agent Communication Languages. Autonomous Agents and Multi-Agent Systems 3, 9–31 (2000)
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Giordano, L., Martelli, A., Schwind, C. (2004). Verifying Communicating Agents by Model Checking in a Temporal Action Logic. In: Alferes, J.J., Leite, J. (eds) Logics in Artificial Intelligence. JELIA 2004. Lecture Notes in Computer Science(), vol 3229. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30227-8_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-30227-8_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23242-1
Online ISBN: 978-3-540-30227-8
eBook Packages: Springer Book Archive