Abstract
In open multi-agent systems agent interaction is usually ruled by public protocols defining the rules the agents should respect in message exchanging. The respect of such rules guarantees interoperability. Given two agents that agree on using a certain protocol for their interaction, a crucial issue (known as “a priori conformance test”) is verifying if their interaction policies, i.e. the programs that encode their communicative behavior, will actually produce interactions which are conformant to the agreed protocol. An issue that is not always made clear in the existing proposals for conformance tests is whether the test preserves agents’ capability of interacting, besides certifying the legality of their possible conversations. This work proposes an approach to the verification of a priori conformance, of an agent’s conversation policy to a protocol, which is based on the theory of formal languages. The conformance test is based on the acceptance of both the policy and the protocol by a special finite state automaton and it guarantees the interoperability of agents that are individually proved conformant. Many protocols used in multi-agent systems can be expressed as finite state automata, so this approach can be applied to a wide variety of cases with the proviso that both the protocol specification and the protocol implementation can be translated into finite state automata. In this sense the approach is general. Easy applicability to the case when a logic-based language is used to implement the policies is shown by means of a concrete example, in which the language DyLOG, based on computational logic, is used.
This research has partially been funded by the European Commission and by the Swiss Federal Office for Education and Science within the 6th Framework Programme project REWERSE number 506779 (cf. http://rewerse.net), and it has also been supported by MIUR PRIN 2005 “Specification and verification of agent interaction protocols” national project.
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., Gavanelli, M., Lamma, E., Mello, P.: Specification and verification of agent interaction protocols in a logic-based system. In: ACM SAC 2004, pp. 72–78. ACM, New York (2004)
Alonso, G., Casati, F., Kuno, H., Machiraju, V.: Web Services. Springer, Heidelberg (2004)
Baldoni, M., Baroglio, C., Martelli, A., Patti, V.: Reasoning about self and others: Communicating agents in a modal action logic. In: Blundo, C., Laneve, C. (eds.) ICTCS 2003. LNCS, vol. 2841, pp. 228–241. Springer, Heidelberg (2003)
Baldoni, M., Baroglio, C., Martelli, A., Patti, V.: Reasoning about interaction protocols for customizing web service selection and composition. In: Journal of Logic and Algebraic Programming, Special issue on Web Services and Formal Methods (2006) (to appear)
Baldoni, M., Baroglio, C., Martelli, A., Patti, V., Schifanella, C.: Verifying protocol conformance for logic-based communicating agents. In: Leite, J., Torroni, P. (eds.) CLIMA 2004. LNCS, vol. 3487, pp. 192–212. Springer, Heidelberg (2005)
Baldoni, M., Baroglio, C., Martelli, A., Patti, V., Schifanella, C.: Verifying the conformance of web services to global interaction protocols: a first step. In: Bravetti, M., Kloul, L., Zavattaro, G. (eds.) EPEW/WS-EM 2005. LNCS, vol. 3670, pp. 257–271. Springer, Heidelberg (2005)
Baldoni, M., Giordano, L., Martelli, A., Patti, V.: Programming Rational Agents in a Modal Action Logic. Annals of Mathematics and Artificial Intelligence, Special issue on Logic-Based Agent Implementation 41(2-4), 207–257 (2004)
Barbuceanu, M., Fox, M.: Cool: A language for describing coordination in multiagent systems. In: Proceedings International Conference on Multi Agent Systems (ICMAS 1995), pp. 17–24. MIT Press, Massachusetts (1995)
Bentahar, J., Moulin, B., Meyer, J.J., Chaib-Draa, B.: A computational model for conversation policies for agent communication. In: Leite, J., Torroni, P. (eds.) CLIMA 2004. LNCS, vol. 3487, pp. 178–195. Springer, Heidelberg (2005)
Bordini, R., Fisher, M., Pardavila, C., Wooldridge, M.: Model Checking AgentSpeak. In: Proc. of 2nd International Joint Conference on Autonomous Agents and Multi-Agent Systems, AAMAS 2003 (2003)
Bravetti, M., Kloul, L., Zavattaro, G. (eds.): EPEW/WS-EM 2005. LNCS, vol. 3670. Springer, Heidelberg (2005)
Busi, N., Gorrieri, R., Guidi, C., Lucchi, R., Zavattaro, G.: Choreography and Orchestration: a synergic approach for system design. In: Proc. the 3rd Int. Conf. on Service Oriented Computing (2005)
Cabac, L., Moldt, D.: Formal semantics for AUML agent interaction protocol diagrams. In: Odell, J.J., Giorgini, P., Müller, J.P. (eds.) AOSE 2004. LNCS, vol. 3382, pp. 47–61. Springer, Heidelberg (2005)
Endriss, U., Maudet, N., Sadri, F., Toni, F.: Protocol conformance for logic-based agents. In: Gottlob, G., Walsh, T. (eds.) Proc. of IJCAI 2003, pp. 679–684. Morgan Kaufmann, San Francisco (August 2003)
Endriss, U., Maudet, N., Sadri, F., Toni, F.: Logic-based agent communication protocols. In: Dignum, F.P.M. (ed.) ACL 2003. LNCS (LNAI), vol. 2922, pp. 91–107. Springer, Heidelberg (2004)
Eshuis, R., Wieringa, R.: Tool support for verifying UML activity diagrams. IEEE Trans. on Software Eng. 7(30) (2004)
FIPA. Fipa 97, specification part 2: Agent communication language. Technical report, FIPA (Foundation for Intelligent Physical Agents) (November 1997)
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) (accepted for publication)
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)
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)
Hopcroft, J.E., Ullman, J.D.: Introduction to automata theory, languages, and computation. Addison-Wesley Publishing Company, Reading (1979)
Huget, M.P., Koning, J.L.: Interaction Protocol Engineering. In: Huget, M.-P. (ed.) Communication in Multiagent Systems. LNCS (LNAI), vol. 2650, pp. 179–193. Springer, Heidelberg (2003)
Mamdani, A., Pitt, J.: Communication protocols in multi-agent systems: A development method and reference architecture. In: Dignum, F.P.M., Greaves, M. (eds.) Issues in Agent Communication. LNCS, vol. 1916, pp. 160–177. Springer, Heidelberg (2000)
Maudet, N., Chaib-draa, B.: Commitment-based and dialogue-based protocols: new trends in agent communication languages. Knowledge engineering review 17(2) (2002)
Odell, J., Parunak, H.V.D., Bauer, B.: Extending UML for agents. In: Proc. of the Agent-Oriented Information System Workshop at AAAI 2000 (2000)
Pitt, J., Guerin, F., Stergiou, C.: Protocols and intentional specifications of multi-party agent conversations for brokerage and auctions. In: Autonomous Agents 2000, Barcelona, pp. 269–276. ACM Press, New York (2000)
Singh, M.P.: A social semantics for agent communication languages. In: Proc. of IJCAI 1998 Workshop on Agent Communication Languages. Springer, Berlin (2000)
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)
WS-CDL (2004), http://www.w3.org/tr/2004/wd-ws-cdl-10-20041217/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baldoni, M., Baroglio, C., Martelli, A., Patti, V. (2006). Verification of Protocol Conformance and Agent Interoperability. In: Toni, F., Torroni, P. (eds) Computational Logic in Multi-Agent Systems. CLIMA 2005. Lecture Notes in Computer Science(), vol 3900. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11750734_15
Download citation
DOI: https://doi.org/10.1007/11750734_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33996-0
Online ISBN: 978-3-540-33997-7
eBook Packages: Computer ScienceComputer Science (R0)