Verifying agents’ conformance with multiparty protocols. (English) Zbl 1250.68267
Fisher, Michael (ed.) et al., Computational logic in multi-agent systems. 9th international workshop, CLIMA IX, Dresden, Germany, September 29–30, 2008. Revised selected and invited papers. Berlin: Springer (ISBN 978-3-642-02733-8/pbk). Lecture Notes in Computer Science 5405. Lecture Notes in Artificial Intelligence, 17-36 (2009).
Summary: 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.
For the entire collection see [Zbl 1169.68002].
For the entire collection see [Zbl 1169.68002].
MSC:
| 68T42 | Agent technology and artificial intelligence |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
References:
| [1] | 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) · Zbl 1185.68419 |
| [2] | 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) · Zbl 1236.68245 · doi:10.1007/11750734_15 |
| [3] | 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) · Zbl 1236.68245 · doi:10.1007/11948148_28 |
| [4] | Bordeaux, L., Salaün, G., Berardi, D., Mecella, M.: When are two web-agents compatible, VLDB-TES (2004) |
| [5] | 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) · doi:10.1007/11961536_1 |
| [6] | 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) |
| [7] | Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000) |
| [8] | 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) · Zbl 1071.68002 · doi:10.1016/j.tcs.2004.07.004 |
| [9] | 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) · Zbl 1111.68677 · doi:10.1007/978-3-540-30227-8_8 |
| [10] | 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) · Zbl 1112.03014 · doi:10.1007/s10472-006-9020-7 |
| [11] | 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) · doi:10.1007/978-3-540-74782-6_14 |
| [12] | 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) |
| [13] | 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) · Zbl 1122.68122 |
| [14] | 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) · doi:10.1007/3-540-63141-0_4 |
| [15] | Henriksen, J.G., Thiagarajan, P.S.: Dynamic Linear Time Temporal Logic. Annals of Pure and Applied logic 96(1-3), 187–207 (1999) · Zbl 0931.03033 · doi:10.1016/S0168-0072(98)00039-6 |
| [16] | Lomuscio, A., Qu, H., Solanki, M.: Towards verifying compliance in agent-based web service compositions. In: AAMAS 2008, pp. 265–272 (2008) |
| [17] | 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) · Zbl 1010.68502 · doi:10.1007/3-540-45657-0_13 |
| [18] | Reiter, R.: Knowledge in Action. MIT Press, Cambridge (2001) · Zbl 1018.03022 |
| [19] | 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) · Zbl 0755.68124 · doi:10.1016/B978-0-12-450010-5.50026-8 |
| [20] | 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) · doi:10.1007/10722777_3 |
| [21] | 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) · doi:10.1007/11841197_1 |
| [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) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
