Specification and verification of agent interaction protocols in a logic-based system

ABSTRACT

In multiagent systems, agent interaction is ruled by means of interaction protocols. Compliance to protocols can be hardwired in agent programs; however, this requires that only "certified" agents interact. In open societies, composed of autonomous and heterogeneous agents whose internal structure is, in general, not accessible, interaction protocols should be specified in terms of the agent observable behaviour, and compliance should be verified by an external entity.In this paper, we propose a Java-Prolog-CHR system for verification of compliance of agents' behaviour to protocols specified in a logic-based formalism (Social Integrity Constraints). We also present the application of the formalism and the system to the specification and verification of the FIPA Contract-Net protocol.

REFERENCES

• 1: FIPA Contract Net Interaction Protocol. Technical report, Foundation for Intelligent Physical Agents, 2002. Available at http://www.fipa.org.
• 2: SICStus Prolog 3.9.0 Manual. February 2002.
• 3: M. Alberti, A. Ciampolini, M. Gavanelli, E. Lamma, P. Mello, and P. Torroni. A social acl semantics by deontic constraints. In V. Marik, J. Muller, and M. Pechoucek, editors, Proceedings of the 3rd International/Central and Eastern European Conference on Multi-Agent Systems, number 2691 in Lecture Notes in Artificial Intelligence, pages 204--213, Prague, Czech Republic, June 2003. Springer Verlag.
• 4: M. Alberti, M. Gavanelli, E. Lamma, P. Mello, and P. Torroni. Specification and verification of agent interactions using social integrity constraints. In W. van der Hoek, A. Lomuscio, E. de Vink, and M. Wooldridge, editors, Proceedings of the Workshop on Logic and Communication in Multi-Agent Systems (LCMAS), Eindhoven, the Netherlands, June 29 2003.
• 5: Alexander Artikis , Jeremy Pitt , Marek Sergot, Animated specifications of computational societies, Proceedings of the first international joint conference on Autonomous agents and multiagent systems: part 3, July 15-19, 2002, Bologna, Italy [doi>10.1145/545056.545070]
• 6: U. Endriss, N. Maudet, F. Sadri, and F. Toni. Protocol conformance for logic-based agents. In G. Gottlob and T. Walsh, editors, Proceedings of the 18th International Joint Conference on Artificial Intelligence (IJCAI-2003), pages 679--684. Morgan Kaufmann Publishers, August 2003.
• 7: FIPA Communicative Act Library Specification. Experimental specification XC00037H, Foundation for Intelligent Physical Agents, Aug. 2001. Published on August 10th, 2001, available for download from the FIPA website: http://www.fipa.org.
• 8: Nicoletta Fornara , Marco Colombetti, Operational specification of a commitment-based agent communication language, Proceedings of the first international joint conference on Autonomous agents and multiagent systems: part 2, July 15-19, 2002, Bologna, Italy [doi>10.1145/544862.544868]
• 9: T. Frühwirth. Theory and practice of constraint handling rules. Journal of Logic Programming, 37(1--3):95--138, Oct. 1998.
• 10: J. Jaffar and M. Maher. Constraint logic programming: a survey. Journal of Logic Programming, 19--20:503--582, 1994.
• 11: R Kowalski , M Sergot, A logic-based calculus of events, New Generation Computing, v.4 n.1, p.67-95, 1986 [doi>10.1007/BF03037383]
• 12: J. W. Lloyd, Foundations of logic programming; (2nd extended ed.), Springer-Verlag New York, Inc., New York, NY, 1987
• 13: J. Muller and J. Odell. Agent UML: A formalism for specifying multiagent interaction. Agent-Oriented Software Engineering, pages 91--103, 2001.
• 14: Pinar Yolum , Munindar P. Singh, Flexible protocol specification and execution: applying event calculus planning using commitments, Proceedings of the first international joint conference on Autonomous agents and multiagent systems: part 2, July 15-19, 2002, Bologna, Italy [doi>10.1145/544862.544867]

INDEX TERMS

Keywords:
agents, computational logic, verification