Abstract
The paper deals with the problem of agents conformance with multiparty protocols. We introduce a notion of conformance of a set of k agents with a multiparty protocol with k roles, which requires the agents to be interoperable and to produce correct executions of the protocol. We introduce conditions that enable each agent to be independently verified with respect to the protocol. We assume that protocols are specified in a temporal action theory and we show that the problem of verifying the conformance of an agent with a protocol can be solved by making use of automata based techniques. Protocols with nonterminating computations, modeling reactive agents, can also be captured in this framework.
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., Chesani, F., Gavanelli, M., Lamma, E., Mello, P., Montali, M.: An abductive framework for a-priori verification of web agents. In: Principles and Practice of Declarative Programming (PPDP 2006). ACM Press, New York (2006)
Baldoni, M., Baroglio, C., Martelli, A., Patti, V.: Verification of protocol conformance and agent interoperability. In: Toni, F., Torroni, P. (eds.) CLIMA 2005. LNCS, vol. 3900, pp. 265–283. Springer, Heidelberg (2006)
Baldoni, M., Baroglio, C., Martelli, A., Patti, V.: A Priori Conformance Verification for Guaranteeing Interoperability in Open Environments. In: Dan, A., Lamersdorf, W. (eds.) ICSOC 2006. LNCS, vol. 4294, pp. 339–351. Springer, Heidelberg (2006)
Bordeaux, L., Salaün, G., Berardi, D., Mecella, M.: When are two web-agents compatible, VLDB-TES (2004)
Chopra, A.K., Singh, M.P.: Producing Compliant Interactions: Conformance, Coverage, and Interoperability. In: Baldoni, M., Endriss, U. (eds.) DALT 2006. LNCS, vol. 4327, pp. 1–15. Springer, Heidelberg (2006)
Chopra, A.K., Singh, M.P.: Constitutive Interoperability. In: Proc. of the 7th Conf. on Autonomous Agents and Multiagent Systems (AAMAS 2008), pp. 797–804 (2008)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)
Fu, X., Bultan, T., Su, J.: Conversation protocols: a formalism for specification and verification of reactive electronic services. Theor. Comput. Sci. 328(1-2), 19–37 (2004)
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 (LNAI), vol. 3229, pp. 57–69. Springer, Heidelberg (2004)
Giordano, L., Martelli, A.: Tableau-based Automata Construction for Dynamic Linear Time Temporal Logic. Annals of Mathematics and Artificial Intelligence 46(3), 289–315 (2006)
Giordano, L., Martelli, A.: Verifying Agent Conformance with Protocols Specified in a Temporal Action Logic. In: Basili, R., Pazienza, M.T. (eds.) AI*IA 2007. LNCS (LNAI), vol. 4733, pp. 145–156. Springer, Heidelberg (2007)
Giordano, L., Martelli, A.: Web Service Composition in a Temporal Action Logic. In: 4th Int. Workshop on AI for Service Composition, AICS 2006, Riva del Garda, August 28 (2006)
Giordano, L., Martelli, A., Schwind, C.: Specifying and Verifying Interaction Protocols in a Temporal Action Logic. Journal of Applied Logic (Special issue on Logic Based Agent Verification) 5(2007), 214–234 (2007)
Henriksen, J.G., Thiagarajan, P.S.: A product Version of Dynamic Linear Time Temporal Logic. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 45–58. Springer, Heidelberg (1997)
Henriksen, J.G., Thiagarajan, P.S.: Dynamic Linear Time Temporal Logic. Annals of Pure and Applied logic 96(1-3), 187–207 (1999)
Lomuscio, A., Qu, H., Solanki, M.: Towards verifying compliance in agent-based web service compositions. In: AAMAS 2008, pp. 265–272 (2008)
Rajamani, S.K., Rehof, J.: Conformance checking for models of asynchronous message passing software. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 166–179. Springer, Heidelberg (2002)
Reiter, R.: Knowledge in Action. MIT Press, Cambridge (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: Dignum, F.P.M., Greaves, M. (eds.) Issues in Agent Communication. LNCS, vol. 1916, pp. 31–45. Springer, Heidelberg (2000)
van der Aalst, W.M.P., Pesic, M.: DecSerFlow: Towards a Truly Declarative Service Flow Language. In: Bravetti, M., Núñez, M., Zavattaro, G. (eds.) WS-FM 2006. LNCS, vol. 4184, pp. 1–23. Springer, Heidelberg (2006)
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
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Giordano, L., Martelli, A. (2009). Verifying Agents’ Conformance with Multiparty Protocols. In: Fisher, M., Sadri, F., Thielscher, M. (eds) Computational Logic in Multi-Agent Systems. CLIMA 2008. Lecture Notes in Computer Science(), vol 5405. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02734-5_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-02734-5_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02733-8
Online ISBN: 978-3-642-02734-5
eBook Packages: Computer ScienceComputer Science (R0)