Specifying and verifying interaction protocols in a temporal action logic. (English) Zbl 1122.68122
Summary: In this paper we develop a logical framework for specifying and verifying systems of communicating agents and interaction protocols. The framework is based on Dynamic Linear Time Temporal Logic (DLTL), which extends LTL by strengthening the until operator by indexing it with the regular programs of dynamic logic. The framework provides a simple formalization of the communicative actions in terms of their effects and preconditions and the specification of an interaction protocol by means of temporal constraints. We adopt a social approach to agent communication, where communication can be described in terms of changes in the social relations between participants, and protocols in terms of creation, manipulation and satisfaction of commitments among agents. The description of the interaction protocol and of communicative actions is given in a temporal action theory, and agent programs, when known, can be specified as complex actions (regular programs in DLTL). The paper addresses several kinds of verification problems (including the problem of verifying compliance of agents with the protocol), which can be formalized either as validity or as satisfiability problems in the temporal logic and can be solved by model checking techniques. In particular, we show that the verification of the compliance of an agent with the protocol requires to move to the logic DLTL\(^{\otimes}\), the product version of DLTL.
MSC:
| 68T27 | Logic in artificial intelligence |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
Software:
SPINReferences:
| [1] | M. Alberti, D. Daolio, P. Torroni, M. Gavanelli, E. Lamma, P. Mello, Specification and verification of agent interaction protocols in a logic-based system, in: SAC’04, 2004, pp. 72-78; M. Alberti, D. Daolio, P. Torroni, M. Gavanelli, E. Lamma, P. Mello, Specification and verification of agent interaction protocols in a logic-based system, in: SAC’04, 2004, pp. 72-78 · Zbl 1270.68160 |
| [2] | Bacchus, F.; Kabanza, F., Planning for temporally extended goals, Ann. Math. AI, 22, 5-27 (1998) · Zbl 1034.68549 |
| [3] | Benerecetti, M.; Giunchiglia, F.; Serafini, L., Model checking multiagent systems, J. Logic Comput., 8, 3, 401-423 (1998), (special issue on Computational Aspects of Multi-Agent Systems) · Zbl 0904.68159 |
| [4] | R. Bordini, M. Fisher, C. Pardavila, M. Wooldridge, Model checking AgentSpeak, in: AAMAS 2003, 2003, pp. 409-416; R. Bordini, M. Fisher, C. Pardavila, M. Wooldridge, Model checking AgentSpeak, in: AAMAS 2003, 2003, pp. 409-416 |
| [5] | R. Bordini, M. Fisher, W. Visser, M. Wooldridge, State-space reduction techniques in agent verification, in: AAMAS 2004, 2004, pp. 894-901; R. Bordini, M. Fisher, W. Visser, M. Wooldridge, State-space reduction techniques in agent verification, in: AAMAS 2004, 2004, pp. 894-901 |
| [6] | D. Calvanese, G. De Giacomo, M.Y. Vardi, Reasoning about actions and planning in LTL action theories, in: Proc. KR’02, 2002, pp. 593-602; D. Calvanese, G. De Giacomo, M.Y. Vardi, Reasoning about actions and planning in LTL action theories, in: Proc. KR’02, 2002, pp. 593-602 |
| [7] | FIPA contract net interaction protocol specification, 2002, available at |
| [8] | N. Fornara, M. Colombetti, Defining interaction protocols using a commitment-based agent communication language, in: Proc. AAMAS’03, Melbourne, 2003, pp. 520-527; N. Fornara, M. Colombetti, Defining interaction protocols using a commitment-based agent communication language, in: Proc. AAMAS’03, Melbourne, 2003, pp. 520-527 |
| [9] | Gerth, R.; Peled, D.; Vardi, M. Y.; Wolper, P., Simple on-the-fly automatic verification of linear temporal logic, (Proc. 15th Work. Protocol Specification, Testing and Verification. Proc. 15th Work. Protocol Specification, Testing and Verification, Warsaw (1995), North-Holland: North-Holland Amsterdam) |
| [10] | L. Giordano, A. Martelli, On-the-fly automata construction for dynamic linear time temporal logic, in: Proc. TIME 04, 2004, pp. 133-139; L. Giordano, A. Martelli, On-the-fly automata construction for dynamic linear time temporal logic, in: Proc. TIME 04, 2004, pp. 133-139 |
| [11] | Giordano, L.; Martelli, A.; Schwind, C., Ramification and causality in a modal action logic, J. Logic Comput., 10, 5, 625-662 (2000) · Zbl 0966.68196 |
| [12] | Giordano, L.; Martelli, A.; Schwind, C., Reasoning about actions in dynamic linear time temporal logic, FAPR’00—Int. Conf. on Pure and Applied Practical Reasoning, London, September 2000. FAPR’00—Int. Conf. on Pure and Applied Practical Reasoning, London, September 2000, Logic J. IGPL, 9, 2, 289-303 (2001) |
| [13] | Giordano, L.; Martelli, A.; Schwind, C., Specifying and verifying systems of communicating agents in a temporal action logic, (Proc. AI*IA’03. Proc. AI*IA’03, Pisa. Proc. AI*IA’03. Proc. AI*IA’03, Pisa, Lecture Notes in Artificial Intelligence, vol. 2829 (2003), Springer: Springer Berlin), 262-274 · Zbl 1274.68580 |
| [14] | Giordano, L.; Martelli, A.; Schwind, C., Verifying communicating agents by model checking in a temporal action logic, (Proc. Logics in Artificial Intelligence, 9th European Conference, JELIA 2004. Proc. Logics in Artificial Intelligence, 9th European Conference, JELIA 2004, Lisbon, Portugal. Proc. Logics in Artificial Intelligence, 9th European Conference, JELIA 2004. Proc. Logics in Artificial Intelligence, 9th European Conference, JELIA 2004, Lisbon, Portugal, Lecture Notes in Artificial Intelligence, vol. 3229 (2004), Springer: Springer Berlin), 57-69 · Zbl 1111.68677 |
| [15] | L. Giordano, A. Martelli, C. Schwind, Specialization of interaction protocols in a temporal action logic, in: LCMAS05, 3rd Int. Workshop on Logic and Communication in Multi-Agent Systems, Edinburgh, 2005; L. Giordano, A. Martelli, C. Schwind, Specialization of interaction protocols in a temporal action logic, in: LCMAS05, 3rd Int. Workshop on Logic and Communication in Multi-Agent Systems, Edinburgh, 2005 · Zbl 1273.68374 |
| [16] | F. Giunchiglia, P. Traverso, Planning as model checking, in: Proc. the 5th European Conf. on Planning (ECP’99), Durham, UK, 1999, pp. 1-20; F. Giunchiglia, P. Traverso, Planning as model checking, in: Proc. the 5th European Conf. on Planning (ECP’99), Durham, UK, 1999, pp. 1-20 |
| [17] | Greaves, M.; Holmback, H.; Bradshaw, J., What is a conversation policy?, (Issues in Agent Communication. Issues in Agent Communication, Lecture Notes in Computer Science, vol. 1916 (2000), Springer: Springer Berlin), 118-131 |
| [18] | F. Guerin, Specifying agent communication languages, PhD thesis, Imperial College, London, April 2002; F. Guerin, Specifying agent communication languages, PhD thesis, Imperial College, London, April 2002 |
| [19] | Guerin, F.; Pitt, J., Verification and compliance testing, (Communications in Multiagent Systems. Communications in Multiagent Systems, Lecture Notes in Artificial Intelligence, vol. 2650 (2003), Springer: Springer Berlin), 98-112 · Zbl 1020.68678 |
| [20] | Henriksen, J. G.; Thiagarajan, P. S., A product version of dynamic linear time temporal logic, (Proc. CONCUR’97. Proc. CONCUR’97, Lecture Notes in Computer Science, vol. 1243 (1997), Springer: Springer Berlin), 45-58 · Zbl 1512.68156 |
| [21] | Henriksen, J. G.; Thiagarajan, P. S., Dynamic linear time temporal logic, Ann. Pure Appl. Logic, 96, 1-3, 187-207 (1999) · Zbl 0931.03033 |
| [22] | Holzmann, G. J., The SPIN Model Checker. Primer and Reference Manual (2003), Addison-Wesley: Addison-Wesley Reading, MA |
| [23] | Huget, M. P.; Wooldridge, M., Model checking for ACL compliance verification, (Proc. ACL 2003. Proc. ACL 2003, Lecture Notes in Computer Science, vol. 2922 (2003), Springer: Springer Berlin), 75-90 |
| [24] | G.N. Kartha, V. Lifschitz, Actions with indirect effects (preliminary report), in: Proc. KR’94, 1994, pp. 341-350; G.N. Kartha, V. Lifschitz, Actions with indirect effects (preliminary report), in: Proc. KR’94, 1994, pp. 341-350 |
| [25] | Jennings, N. R., Commitments and conventions: the foundation of coordination in multi-agent systems, Knowledge Engrg. Rev., 8, 3, 233-250 (1993) |
| [26] | Lifschitz, V., Frames in the space of situations, Artificial Intelligence, 46, 365-376 (1990) · Zbl 0743.68122 |
| [27] | Maudet, N.; Chaib-draa, B., Commitment-based and dialogue-game based protocols: new trends in agent communication languages, Knowledge Engrg. Rev., 17, 2, 157-179 (2002) |
| [28] | S. Narayanan, S. McIlraith, Simulation, verification and automated composition of web services, in: Proceedings of the Eleventh International World Wide Web Conference (WWW-11), 2002, pp. 77-88; S. Narayanan, S. McIlraith, Simulation, verification and automated composition of web services, in: Proceedings of the Eleventh International World Wide Web Conference (WWW-11), 2002, pp. 77-88 |
| [29] | Penczek, W.; Lomuscio, A., Verifying epistemic properties of multi-agent systems via bounded model checking, Fundamenta Informaticae, 55, 2, 167-185 (2003) · Zbl 1111.68512 |
| [30] | M. Pistore, P. Traverso, Planning as model checking for extended goals in non-deterministic domains, in: Proc. IJCAI’01, Seattle, 2001, pp. 479-484; M. Pistore, P. Traverso, Planning as model checking for extended goals in non-deterministic domains, in: Proc. IJCAI’01, Seattle, 2001, pp. 479-484 |
| [31] | Reiter, R., The frame problem in the situation calculus: a simple solution (sometimes) and a completeness result for goal regression, (Lifschitz, V., Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy (1991), Academic Press: Academic Press New York), 359-380 · Zbl 0755.68124 |
| [32] | Singh, M. P., Agent communication languages: rethinking the principles, IEEE Computer, 31, 12, 40-47 (1998) |
| [33] | Singh, M. P., A social semantics for agent communication languages, (Issues in Agent Communication 2000. Issues in Agent Communication 2000, Lecture Notes in Computer Science, vol. 1916 (2000), Springer: Springer Berlin), 31-45 |
| [34] | P. Traverso, M. Pistore, Automated composition of semantic web services into executable processes, in: Proc. Third International Semantic Web Conference (ISWC2004), 2004, pp. 380-394; P. Traverso, M. Pistore, Automated composition of semantic web services into executable processes, in: Proc. Third International Semantic Web Conference (ISWC2004), 2004, pp. 380-394 |
| [35] | Venkatraman, M.; Singh, M. P., Verifying compliance with commitment protocols, Autonomous Agents and Multi-Agent Systems, 2, 3, 217-236 (1999) |
| [36] | Wooldridge, M., Semantic issues in the verification of agent communication languages, Autonomous Agents and Multi-Agent Systems, 3, 9-31 (2000) |
| [37] | M. Wooldridge, M. Fisher, M.P. Huget, S. Parsons, Model checking multi-agent systems with MABLE, in: Proc. AAMAS’02, Bologna, Italy, 2002, pp. 952-959; M. Wooldridge, M. Fisher, M.P. Huget, S. Parsons, Model checking multi-agent systems with MABLE, in: Proc. AAMAS’02, Bologna, Italy, 2002, pp. 952-959 |
| [38] | P. Yolum, M.P. Singh, Flexible protocol specification and execution: applying event calculus planning using commitments, in: Proc. AAMAS’02, Bologna, Italy, 2002, pp. 527-534; P. Yolum, M.P. Singh, Flexible protocol specification and execution: applying event calculus planning using commitments, in: Proc. AAMAS’02, Bologna, Italy, 2002, pp. 527-534 |
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.
