Abstract
In this paper we address the challenges associated with the verification of correctness of communication between agents in Multi-Agent Systems. Our approach applies model-checking techniques to protocols which express interactions between a group of agents in the form of a dialogue. We define a lightweight protocol language which can express a wide range of dialogue types, and we use the SPIN model checker to verify properties of this language. Our early results show this approach has a high success rate in the detection of failures in agent dialogues.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Austin, J.L.: How to Do Things With Words. Oxford University Press, Oxford (1962)
Patil, R., Fikes, R.F., Patel-Schneider, P.F., McKay, D., Finin, T., Gruber, T., Neches, R.: The DARPA Knowledge Sharing Effort: Progress Report. In: Nebel, B., Rich, C., Swartout, W. (eds.) KR 1992. Principles of Knowledge Representation and Reasoning: Proceedings of the Third International Conference, pp. 777–788. Morgan Kaufmann, San Mateo (1992)
Foundation for Intelligent Physical Agents: Fipa specification part 2 - agent communication language (1999), Available at: http://www.fipa.org
Cohen, P.R., Levesque, H.J.: Rational interaction as the basis for communication. Intentions in Communication, 221–256 (1990)
Bratman, M.E.: Intention, Plans, and Practical Reason. Harvard University Press, Cambridge (1987)
Rao, A.S., Georgeff, M.: Decision procedures for BDI logics. Journal of Logic and Computation 8, 293–344 (1998)
Labrou, Y., Finin, T.: Semantics and conversations for an agent communication language. In: Proceedings of the FIfteenth International Joint Conference of Artificial Intelligence (IJCAI 1997), Nagoya, Japan, pp. 584–591 (1997)
Wooldridge, M.: Reasoning about Rational Agents. MIT Press, Cambridge (2000)
Bellifemine, F., Poggi, A., Rimassa, G.: JADE: A FIPA-compliant agent framework. In: Proceedings of the 1999 Conference on Practical Application of Intelligent Agents and Multi-Agent Technology (PAAM 1999), London, UK, pp. 97–108 (1999)
Singh, M.P.: Agent Communication Languages: Rethinking the Principles. IEEE Computer, 40–47 (1998)
Labrou, Y., Finin, T.: Comments on the specification for FIPA 1997 Agent Communication Language (1997), Available at: http://www.cs.umbc.edu/kqml/papers/
Wooldridge, M.: Semantic issues in the verification of agent communication languages. Autonomous Agents and Multi-Agent Systems 3, 9–31 (2000)
Maudet, N., Chaib-draa, B.: Commitment-based and Dialogue-game based Protocols–News Trends in Agent Communication Language. The Knowledge Engineering Review 17, 157–179 (2002)
Flores, R.A., Kremer, R.C.: Bringing Coherence to Agent Conversations. In: Wooldridge, M.J., Weiß, G., Ciancarini, P. (eds.) AOSE 2001. LNCS, vol. 2222, pp. 50–67. Springer, Heidelberg (2002)
Walton, D.N., Krabbe, E.C.W.: Commitment in Dialogue: Basic Concepts of Interpersonal Reasoning. SUNY Press (1995)
McBurney, P., Parsons, S.: Games that agents play: A formal framework for dialogues between autonomous agents. Journal of Logic, Language and Information 11, 315–334 (2002)
Benerecetti, M., Giunchiglia, F., Serafini, L.: Model Checking Multiagent Systems. Journal of Logic and Computation 8, 401–423 (1998)
Wooldridge, M., Fisher, M., Huget, M.P., Parsons, S.: Model Checking Multiagent systems with MABLE. In: Proceedings of the First International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2002), Bologna, Italy (2002)
Bordini, R.H., Fisher, M., Pardavila, C., Wooldridge, M.: Model Checking AgentSpeak. In: Proceedings of the Second International Joint Conference on Autonomous Agents & Multiagent Systems (AAMAS), Melbourne, Australia, pp. 409–416. ACM, New York (2003)
Bordini, R.H., Fisher, M., Visser, W., Wooldridge, M.J.: State-space Reduction Techniques in Agent Verification. In: Proceedings of the Third International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2004), pp. 896–903. ACM Press, New York (2004)
Booth, D., Haas, H., McCabe, F., Newcomer, E., Champion, M., Ferris, C., Orchard, D.: Web Services Architecture. World-Wide-Web Consortium (W3C) (2003), Available at: http://www.w3.org/TR/ws-arch/
Greaves, M., Holmback, H., Bradshaw, J.: What is a Conversation Policy? In: Proceedings of the Workshop on Specifying and Implementing Conversation Policies, Autonomous Agents 1999, Seattle, Washington (1999)
Esteva, M., Rodríguez, J.A., Sierra, C., Garcia, P., Arcos, J.L.: On the Formal Specification of Electronic Institutions. In: Sierra, C., Dignum, F.P.M. (eds.) AgentLink 2000. LNCS (LNAI), vol. 1991, pp. 126–147. Springer, Heidelberg (2001)
Vaconcelos, W.: Norm Verification and Analysis of Electronic Institutions. In: Leite, J., Omicini, A., Torroni, P., Yolum, p. (eds.) DALT 2004. LNCS (LNAI), vol. 3476, pp. 141–155. Springer, Heidelberg (2005)
Harel, D.: Statecharts: A Visual Formalism for Computer System. Science of Computer Programming 8, 231–274 (1987)
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)
Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes (Part 1/2). Information and Computation 100, 1–77 (1992)
Esteva, M., Cruz, D., Sierra, C.: ISLANDER: an electronic institutions editor. In: Proceedings of the First International Joint Conference on Autonomous Agents & Multiagent Systems (AAMAS), Bologna, Italy, pp. 1045–1052. ACM press, New York (2002)
Walton, C.: Multi-Agent Dialogue Protocols. In: Proceedings of the Eighth International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, Florida (2004)
McGinnis, J.P., Robertson, D., Walton, C.: Using Distributed Protocols as an Implementation of Dialogue Games. In: Proceedings of the 1st European Workshop on Multi-Agent Systems (EUMAS 2003), Oxford, UK (2003)
Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM 18, 453–457 (1975)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Walton, C.D. (2005). Model Checking Agent Dialogues. In: Leite, J., Omicini, A., Torroni, P., Yolum, p. (eds) Declarative Agent Languages and Technologies II. DALT 2004. Lecture Notes in Computer Science(), vol 3476. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11493402_8
Download citation
DOI: https://doi.org/10.1007/11493402_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26172-8
Online ISBN: 978-3-540-31927-6
eBook Packages: Computer ScienceComputer Science (R0)