Search
  • All Journals
Advanced Search
Search articles by Title, Author, Keywords, DOI
7.7CiteScore
2.0Impact Factor
Advanced Search
MAP  >  The Knowledge Engineering Review
2015 Volume 30
Article Contents
Next Previous
RESEARCH ARTICLE   Open Access    

Computational logics and verification techniques of multi-agent commitments: survey

  • 1.

    Montreal

  • 2.

    Shebin El Kom

  • 3.

    Department of Computer Engineering

More Information
  • Abstract: Agent communication languages (ACLs) are fundamental mechanisms that enable agents in multi-agent systems to talk, communicate with each other in order to satisfy their individual and social goals in a cooperative and competitive manner. Social approaches are advocated to overcome the shortcomings of ACL semantics delineated by using mental approaches in the figure of agents’ mental notions. Over the last two decades, social commitments have been the subject of considerable research in some of those social approaches as they provide a powerful representation for modeling and reasoning upon multi-agent interactions in the form of mutual contractual obligations. They particularly provide a declarative, flexible, verifiable, and social semantics for ACL messages while respecting agents’ autonomy, heterogeneity, and openness.In this manuscript, we go through prominent and predominate proposals in the literature to explore the state of the art on how temporal logics can be devoted to define a formal semantics for ACL messages in terms of social commitments and associated actions. We explain each proposal and point out if and how it meets seven crucial criteria, four of them introduced by Munindar P. Singh to have a well-defined semantics for ACL messages. Far from deciding the best proposal, our aim is to present the advantages (strengths) and limitations of those proposals to designers and developers using a concrete running example and to compare between them, so that they can make the best choice with regard to their needs. We explore and evaluate current specification languages and different verification techniques that have been discussed within those proposals to, respectively, specify and verify commitment-based protocols. We also investigate logical languages of actions advocated to specify, model, and execute commitment-based protocols in other contributed proposals. Finally, we suggest some solutions that can contribute to address the identified limitations.
  • 加载中
  • Alberti M., Chesani F., Gavanelli M., Lamma E., Mello P. & Torroni P.2008. Verifiable agent interaction in abductive logic programming: the SCIFF framework. ACM Transactions on Computational Logic9(4), 1–43.

    Google Scholar

    Al-Saqqar F., Bentahar J., Sultan K. & El-Menshawy M.2014. On the interaction between knowledge and social commitments in multi-agent systems. Applied Intelligence41(1), 235–259.

    Google Scholar

    Al-Saqqar F., Bentahar J., Sultan K., Wan W. & Khosrowshahi Asl E.2015. Model checking temporal knowledge and commitments in multi-agent systems using reduction. Simulation Modelling Practice and Theory51, 45–68.

    Google Scholar

    Alur R., Henzinger T.A. & Kupferman O.2002. Alternating-time temporal logic. Journal of ACM49(5), 672–713.

    Google Scholar

    Artikis A. & Pitt J.V.2009. Specifying open agent systems: a survey. In ESAW, Artikis, A., Picard, G. & Vercouter, L. (eds), Lecture Notes in Computer Science 5485, 29–45. Springer.

    Google Scholar

    Artikis A., Sergot M. & Pitt J.2009. Specifying norm-governed computational societies. ACM Transactions on Computational Logic10(1), 1–42.

    Google Scholar

    Baldoni M., Baroglio C. & Marengo E.2010. Behavior oriented commitment-based protocols. In ECAI, Coelho, H., Studer, R. & Wooldridge, M. (eds), 215. IOS Press, 137–142.

    Google Scholar

    Baldoni M., Baroglio C. & Marengo E.2011. Commitment-based protocols with behavioral rules and correctness properties of MAS. In DALT, Omicini, A., Sardiña, S. & Vasconcelos, W. (eds), LNCS 6619. 60–77. Springer.

    Google Scholar

    Baldoni M., Baroglio C., Marengo E. & Patti V.2013. Constitutive and regulative specifications of commitment protocols: a decoupled approach. ACM Transactions on Intelligent Systems and Technology4(2), 22.

    Google Scholar

    Bentahar J., El-Menshawy M., Qu H. & Dssoulia R.2012. Communicative commitments: model checking and complexity analysis. Knowledge-Based Systems35, 21–34. Elsevier.

    Google Scholar

    Bentahar J., Maamar Z., Wan W., Benslimane D., Thiran P. & Subramanian S.2008. Agent-based communities of web services: an argumentation-driven approach. Service Oriented Computing and Applications2(4), 219–238.

    Google Scholar

    Bentahar J., Meyer J.-J.Ch. & Wan W.2010. Model checking agent communication. In Specification and Verification of Multi-Agent Systems, chapter 3, 1st edition, Dastani, M., Hindriks, K. & Meyer, J.-J.Ch. (eds). Springer, pp. 67–102.

    Google Scholar

    Bentahar J., Meyer J.-J.Ch. & Wan W.2009. Model checking communicative agent-based systems. Knowledge-Based Systems22, 142–159.

    Google Scholar

    Bentahar J., Moulin B. & Chaib-draa B.2003. Towards a formal framework for conversational agents, In Proceedings of the International Workshop onACLCP.

    Google Scholar

    Bentahar J., Moulin B. & Chaib-draa B.2004a. Commitment and argument network: a new formalism for agent communication. In ACL, Dignum, F. (ed.), LNCS 2922. 146–165. Springer.

    Google Scholar

    Bentahar J., Moulin B., Meyer J.-J.Ch. & Chaib-draa B.2004b. A logical model for commitment and argument network for agent communication. In Proceedings of the 3rd International Conference on AAMAS, 792–799. IEEE Computer Society.

    Google Scholar

    Bentahar J., Moulin B., Meyer J.-J.Ch. & Lespérance Y.2007. A new logical semantics for agent communication. In CLIMA, Inoue, K., Satoh, K. & Toni, F. (eds), LNCS 4371. 151–170. Springer.

    Google Scholar

    Bhat G., Cleaveland R. & Groce A.2001. Efficient model checking via Büchi tableau automata. In CAV, Berry, G., Comon, H. & Finkel, A. (eds), LNCS 2102. 38–52. Springer.

    Google Scholar

    Bresciani P., Perini A., Giorgini P., Giunchiglia F. & Mylopoulos J.2004. Tropos: an agent-oriented software development methodology. Autonomous Agents and Multi-Agent Systems8(3), 203–236.

    Google Scholar

    Cabri G., Leonardi L., Ferrari L. & Zambonelli F.2010. Role-based software agent interaction models: a survey. Knowledge Engineering Review25(4), 397–419.

    Google Scholar

    Castelfranchi C.1995. Commitments: from individual intentions to groups and organizations. In ICMAS, Lesser, V. & Gasser, L. (eds). The MIT Press, 41–48.

    Google Scholar

    Chesani F., Mello P., Montali M. & Torroni P.2013. Representing and monitoring social commitments using the e.Autonomous Agents and Multi-Agent Systems27(1), 85–130.

    Google Scholar

    Chesani F., Mello P., Montali M. & Torroni P.2009. Commitment tracking via the reactive event calculus. In IJCAI, Boutilier, C. (ed.). AAAI Press, 91–96.

    Google Scholar

    Chopra A. & Singh M.2004. Nonmonotonic commitment machines. In ACL, Dignum, F. (ed.), LNCS 2922. 183–200. Springer.

    Google Scholar

    Chopra A. & Singh M.2006. Contextualizing commitment protocols. In AAMAS, Nakashima H., Wellman M., Weiss, G. & Stone, P. (eds). ACM, 1345–1352.

    Google Scholar

    Chopra A. & Singh M.2008. Constitutive interoperability. In AAMAS, Padgham, L., Parkes, D., Müller, J. & Parsons, S. (eds), 2. IFAAMAS, 797–804.

    Google Scholar

    Chopra A. & Singh M.2009. Multiagent commitment alignment. In Proceedings of the 8th International Joint Conference on AAMAS, 937–944. ACM Press.

    Google Scholar

    Chopra A.K., Artikis A., Bentahar J., Colombetti M., Dignum F., Fornara N., Jones A.J.I., Singh M.P. & Yolum P.2013. Research directions in agent communication. ACM Transactions on Intelligent Systems and Technology4(2), 20. ACM.

    Google Scholar

    Cimatti A., Clarke E., Giunchiglia E., Giunchiglia F., Pistore M., Roveri M., Sebastiani R. & Tacchella A.2002. NuSMV: an open source tool for symbolic model checking. In CAV, Brinksma, E. & Larsen, K.G. (eds), LNCS 2404. 359–364. Springer.

    Google Scholar

    Clarke E. & Emerson E.1982. Design and synthesis of synchronization skeletons using branching time temporal logic. In Logics of Programs, Kozen, D. (ed.), LNCS 131. 52–71.

    Google Scholar

    Clarke E., Emerson E. & Sistla A.1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. In Proceedings of the 10th ACM SIGACT-SIGPLAN Symposium on PPL, POPL’83, 117–126. ACM.

    Google Scholar

    Clarke E., Grumberg O. & Peled D.1999. Model Checking. The MIT Press, Cambridge, USA.

    Google Scholar

    Cohen P. & Levesque H.1990. Intention is choice with commitment. Artificial Intelligence42(2–3), 213–261.

    Google Scholar

    Colombetti M.2000. A commitment-based approach to agent speech acts and conversations. In Proceedings of International Workshop on ALCP, 4th International Conference on Autonomous Agents (Agents 2000), 21–29.

    Google Scholar

    Colombetti M., Fornara N. & Verdicchio M.2004. A social approach to communication in multiagent systems. In DALT, Leite, J.A., Omicini, A., Sterling, L. & Torroni, P. (eds), LNCS 2990. 191–220. Springer.

    Google Scholar

    Desai N., Cheng Z., Chopra A. & Singh M.2007. Toward verification of commitment protocols and their compositions. In AAMAS, Durfee, E.H., Yokoo, M., Huhns, M.N. & Shehory, O. (eds). IFAAMAS, 144–146.

    Google Scholar

    Desai N., Mallya A., Chopra A. & Singh M.2005. Interaction protocols as design abstractions for business processes. IEEE Transactions on Software Engineering31(12), 1015–1027.

    Google Scholar

    Desai N. & Singh M.2007. A modular action description language for protocol composition. In Proceedings of the 22nd AAAI Conference on Artificial Intelligence, 962–967.

    Google Scholar

    Dignum F. & Greaves M. (eds) 2000. Issues in Agent Communication, LNCS 1916. Springer.

    Google Scholar

    El-Kholy W., Bentahar J., El-Menshawy M., Qu H. & Dssouli R.2014a. Conditional commitments: reasoning and model checking. ACM Transaction on Software Engineering and Methodology24(2), 9:1–9:49. ACM.

    Google Scholar

    El-Kholy W., Bentahar J., El-Menshawy M., Qu H. & Dssouli R.2014b. Modeling and verifying choreographed multi-agent-based web service compositions regulated by commitment protocols. Expert Systems with Applications41, 7478–7494. Elsevier.

    Google Scholar

    El-Kholy W., El-Menshawy M., Bentahar J., Qu H. & Dssouli R.2014c. Verifying multiagent-based web service compositions regulated by commitment protocols. In Proceedings of 21th IEEE International Conference on Web Services (ICWS), 49–56. IEEE.

    Google Scholar

    El-Kholy W., El-Menshawy M., Bentahar J., Qu H. & Dssouli R.2015. Formal specification and automatic verification of conditional commitments. IEEE Intelligent Systems30(2), 36–44. IEEE.

    Google Scholar

    El-Menshawy M., Bentahar J. & Dssouli R.2009a. Enhancing engineering methodology for communities of web services. In MALLOW, Baldoni, M. et al. (eds), 494. CEUR-WS.org. pp. 33–42.

    Google Scholar

    El-Menshawy M., Bentahar J. & Dssouli R.2009b. An integrated semantics of social commitments and associated operations. In MALLOW, Baldoni, M. et al. (eds), 494. CEUR-WS.org. pp. 222–230.

    Google Scholar

    El-Menshawy M., Bentahar J. & Dssouli R.2010a. Modeling and verifying business interactions via commitments and dialogue actions. In KES-AMSTA, Jedrzejowicz, P., Nguyen, N.T., Howlett, R.J. & Jain, L.C. (eds), LNCS 6071. 11–21. Springer.

    Google Scholar

    El-Menshawy M., Bentahar J. & Dssouli R.2010b. Verifiable semantic model for agent interactions using social commitments. In LADS, Dastani, M., Fallah-Seghrouchni, A.E., Leite, J. & Torroni, P. (eds), LNCS 6039. 128–152. Springer.

    Google Scholar

    El-Menshawy M., Bentahar J. & Dssouli R.2011a. Model checking commitment protocols. In IEA–AIE, Mehrotra, K.G. et al. (eds), LNCS 6704. 37–47. Springer.

    Google Scholar

    El-Menshawy M., Bentahar J. & Dssouli R.2011b. Symbolic model checking commitment protocols using reduction. In DALT, Omicini, A., Sardina, S. & Vasconcelos, W. (eds), LNAI 6619. 185–203. Springer.

    Google Scholar

    El-Menshawy M., Bentahar J., El-Kholy W. & Dssouli R.2013a. Verifying conformance of multi-agent commitment-based protocols. Expert Systems with Applications40(1), 122–138. Elsevier.

    Google Scholar

    El-Menshawy M., Bentahar J., El-Kholy W. & Dssouli R.2013b. Reducing model checking commitments for agent communication to model checking ARCTL and GCTL*. Autonomous Agent Multi-Agent Systems27(3), 375–418. Springer.

    Google Scholar

    El-Menshawy M., Bentahar J., Qu H. & Dssouli R.2011c. On the verification of social commitments and time. In AAMAS, Sonenberg, L., Stone, P., Tumer, K. & Yolum, P. (eds). IFAAMAS, 483–490.

    Google Scholar

    Emerson E.1990. Temporal and modal logic. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics (B), chapter 16, van Leeuwen, J. (ed.). Elsevier, 995–1072.

    Google Scholar

    Emerson E. & Halpern J.1986. Sometimes and not never, revisited: on branching versus linear time temporal logic. Journal of ACM33(1), 151–178.

    Google Scholar

    Fagin R., Halpern J., Moses Y. & Vardi M.1995. Reasoning About Knowledge. The MIT Press.

    Google Scholar

    Fornara N. & Colombetti M.2002. Operational specification of a commitment-based agent communication language. In Proceedings of the 1st International Joint Conference on AAMS, 535–542. ACM.

    Google Scholar

    Fornara N. & Colombetti M.2003. Defining interaction protocols using a commitment-based agent communication language. In Proceedings of the 2nd International Joint Conference on AAMAS, 520–527. ACM.

    Google Scholar

    Fornara N., Viganò F., Verdicchio M. & Colombetti M.2008. Artificial institutions: a model of institutional reality for open multi-agent systems. AI and Law16(1), 89–105.

    Google Scholar

    Gascueña J. & Fernández-Caballero A.2011. On the use of agent technology in intelligent, multisensory and distributed surveillance. Knowledge Engineering Review26(2), 191–208.

    Google Scholar

    Gerard S. & Singh M.2013. Formalizing and verifying protocol refinements. ACM Transactions on Intelligent Systems and Technology4(2), 21.

    Google Scholar

    Giordano L., Martelli A. & Schwind C.2003. Specifying and verifying systems of communicating agents in a temporal action logic. In AI*IA, Cappelli, A. & Turini, F. (eds), LNCS 2829. 262–274. Springer.

    Google Scholar

    Giordano L., Martelli A. & Schwind C.2007. Specifying and verifying interaction protocols in a temporal action logic. Journal of Applied Logic5(2), 214–234.

    Google Scholar

    Giunchiglia E., Lee J., Lifschitz V., McCain N. & Turner H.2004. Nonmonotonic causal theories. Artificial Intelligence153(1–2), 49–104.

    Google Scholar

    Gray J.1978. Notes on database operating systems. In Advanced Course: Operating Systems, Flynn, M.J., Gray, J., Jones, A.K., Lagally, K., Opderbeck, H., Popek, G.J., Randell, B., Saltzer, J.H. & Wiehle, H. (eds), LNCS 60. 393–481.

    Google Scholar

    Günay A. & Yolum P.2013. Constraint satisfaction as a tool for modeling and checking feasibility of multiagent commitments. Applied Intelligence39(3), 489–509.

    Google Scholar

    Habermas J.1984. The Theory of Communicative Action. The Polity Press.

    Google Scholar

    Hamblin C.1970. Fallacies. Methuen.

    Google Scholar

    Holzmann G.1997. The model checker SPIN. Software Engineering23(5), 279–295.

    Google Scholar

    Huth M. & Ryan M.2004. Logic in Computer Science: Modelling and Reasoning About System, 2nd edition. Cambridge University Press.

    Google Scholar

    Jennings N.1993. Commitments and conventions: the foundation of coordination in multi-agent systems. Knowledge Engineering Review8(3), 223–250.

    Google Scholar

    Kafali Ö., Günay A. & Yolum P.2014. Detecting and predicting privacy violations in online social networks. Distributed and Parallel Databases32, 161–190.

    Google Scholar

    Kafali Ö. & Torroni P.2011. Social commitment delegation and monitoring. In CLIMA XII, Leite, J., Torroni, P., Ågotnes, T., Boella, G. & van der Torre, L. (eds), Lecture Notes in Computer Science 6814. 171–189. Springer.

    Google Scholar

    Kafali Ö. & Torroni P.2012. Exception diagnosis in multiagent contract executions. Annals of Mathematics and Artificial Intelligence64(1), 73–107.

    Google Scholar

    Labrou Y. & Finin T.1998. Semantics and conversations for an agent communication language. In ATAL, Singh, M.P., Rao, A.S. & Wooldridge, M. (eds), LNCS 1365. 209–214. Springer.

    Google Scholar

    Lim M. & Zhang Z.2012. A multi-agent system using iterative bidding mechanism to enhance manufacturing agility. Expert Systems with Applications39, 8259–8273.

    Google Scholar

    Lomuscio A., Pecheur C. & Raimondi F.2007. Automatic verification of knowledge and time with NuSMV. In Proceedings of the 20th International Joint Conference on AI, 1384–1389.

    Google Scholar

    Lomuscio A., Qu H. & Raimondi F.2009. MCMAS: a model checker for the verification of multi-agent systems. In CAV, Bouajjani, A. & Maler, O. (eds), LNCS 5643. 682–688. Springer.

    Google Scholar

    Lomuscio A., Qu H. & Solanki M.2012. Towards verifying contract regulated service composition. Autonomous Agents and Multi-Agent Systems24(3), 345–373.

    Google Scholar

    Mallya A. & Huhns M.2003. Commitments among agents. IEEE Internet Computing7(4), 90–93.

    Google Scholar

    Mallya A. & Singh M.2007. An algebra for commitment protocols. Autonomous Agents and Multi-Agent Systems14(2), 143–163.

    Google Scholar

    Mallya A., Yolum P. & Singh M.2004. Resolving commitments among autonomous agents. In ACL, Dignum, F. (ed.), LNCS 2922. 166–182. Springer.

    Google Scholar

    Marengo E., Baldoni M., Baroglio C., Chopra A., Patti V. & Singh M.2011. Commitments with regulations: reasoning about safety and control in REGULA. In AAMAS, Tumer, K., Yolum, P., Sonenberg, L. & Stone, P. (eds). IFAAMAS, 467–474.

    Google Scholar

    Maudet N. & Chaib-Draa B.2002. Commitment-based and dialogue-game based protocols: new trends in agent communication languages. Knowledge Engineering Review17(2), 157–179.

    Google Scholar

    Nakano M., Hasegawa Y., Funakoshi K., Takeuchi J., Torii T., Nakadai K., Kanda N., Komatani K., Okuno H. & Tsujino H.2011. A multi-expert model for dialogue and behavior control of conversational robots and agents. Knowledge-Based Systems24(2), 248–256.

    Google Scholar

    Pecheur C. & Raimondi F.2007. Symbolic model checking of logics with actions. In Model Checking and Artificial Intelligence, Edelkamp, S. & Lomuscio, A. (eds), LNCS 4428. 113–128. Springer.

    Google Scholar

    Penczek W. & Lomuscio A.2003. Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae55(2), 167–185.

    Google Scholar

    Pham D. & Harland J.2007. Temporal linear logics as a basis for flexible agent interactions. In AAMAS, Durfee, E., Yokoo, M., Huhns, M. & Shehory, O. (eds). 124–131.

    Google Scholar

    Pnueli A.1977. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on FOCS, 46–57. IEEE Computer Society Press.

    Google Scholar

    Reichenbach H.1947. Elements of Symbolic Logic. Macmillan.

    Google Scholar

    Richiardia M.2012. Agent-based computational economics: a short introduction. Knowledge Engineering Review27(2), 137–149.

    Google Scholar

    Sacerdoti E.1977. The Structure of Plans and Behavior. Elsevier.

    Google Scholar

    Schnoebelen P.2003. The complexity of temporal logic model checking. In Advances in Modal Logic, Philippe Balbiani, Nobu-Yuki Suzuki, Frank Wolter & Michael Zakharyaschev (eds), Advances in Modal Logic 4. 1–44. King’s College Publications.

    Google Scholar

    Searle J.1969. Speech Acts: An Essay in the Philosophy of Language. Cambridge University Press.

    Google Scholar

    Shanahan M.1997. Solving the Frame Problem: A Mathematical Investigation of the Common Sense Law of Inertia. The MIT Press.

    Google Scholar

    Shanahan M.2000. An abductive event calculus planner. Logic Programming44, 207–239.

    Google Scholar

    Singh M.1991. Social and psychological commitments in multiagent systems. In AAAI Fall Symposium on KA at SOL, 104–106.

    Google Scholar

    Singh M.1996. A Conceptual Analysis of Commitments in Multiagent Systems. Technical report, North Carolina State University.

    Google Scholar

    Singh M.1997. Commitments among autonomous agents in information-rich Environments. In MAAMAW, Boman, M. & van de Velde, W. (eds), LNCS 1237. 141–155. Springer.

    Google Scholar

    Singh M.1998. Agent communication languages: rethinking the principles. IEEE Computer Society31(12), 40–47.

    Google Scholar

    Singh M.1999. An ontology for commitments in multiagent systems: toward a unification of normative concepts. AI and Law7(1), 97–113.

    Google Scholar

    Singh M.2000. A social semantics for agent communication languages. In Issues in Agent Communication, Dignum, F. & Greaves, M. (eds), LNCS 1916. 31–45. Springer.

    Google Scholar

    Singh M.2007. Formalizing communication protocols for multiagent systems. In IJCAI, Veloso, M.M. (ed.). Morgan Kaufmann Publishers Inc., 1519–1524.

    Google Scholar

    Singh M.2008. Semantical considerations on dialectical and practical commitments. In AAAI, Fox, D. & Gomes, C.P. (eds). AAAI Press, 176–181.

    Google Scholar

    Singh M. & Chopra A.2010. Programming multiagent systems without programming agents. In ProMAS, Braubach, L., Briot, J.-P. & Thangarajah, J. (eds), LNCS 5919. 1–14. Springer.

    Google Scholar

    Singh M., Chopra A. & Desai N.2009. Commitment-based service-oriented architecture. IEEE Computer42(11), 72–79.

    Google Scholar

    Sirbu M.1997. Credits and debits on the internet. IEEE Spectrum34(2), 23–29.

    Google Scholar

    Sklar E. & Richards D.2010. Agent-based systems for human learners. Knowledge Engineering Review25(2), 111–135.

    Google Scholar

    Spoletini P.2005. Verification of Temporal Logic Specification via Model Checking. PhD thesis, Politecnico di Milano.

    Google Scholar

    Spoletini P. & Verdicchio M.2007. Commitment monitoring in a multi-agent system. In CEEMAS, Burkhard, H.-D., Lindemann, G., Verbrugge, R. & Varga, L.Z. (eds), LNCS 4696. 83–92. Springer.

    Google Scholar

    Spoletini P. & Verdicchio M.2009. An automata-based monitoring technique for commitment-based multiagent systems. In COIN, Hübner, J.F., Matson, E.T., Boissier, O. & Dignum, V. (eds), LNCS 5428. 172–187. Springer.

    Google Scholar

    Sultan K., Bentahar J. & El-Menshawy M.2014. Model checking probabilistic social commitments for intelligent agent communication. Applied Soft Computing22, 397–409.

    Google Scholar

    Sultan K., El-Menshawy M. & Bentahar J.2013. Reasoning about social commitments in the presence of uncertainty. In IEEE 12th International Conference on Intelligent Software Methodologies, Tools and Techniques, 29–35.

    Google Scholar

    Telang P. & Singh M.2009a. Business modeling via commitments. In SOCASE, Kowalczyk, R., Vo, Q., Maamar, Z. & Huhns, M. (eds), LNCS 5907. 111–125. Springer.

    Google Scholar

    Telang P. & Singh M.2009b. Enhancing Tropos with commitments. In Conceptual Modeling: Foundations and Applications, Borgida, A., Chaudhri, V.K., Giorgini, P. & Yu, E.S.K. (eds), LNCS 5600. 417–435. Springer.

    Google Scholar

    Telang P. & Singh M.2012. Specifying and verifying cross-organizational business models: an agent-oriented approach. IEEE Transactions on Services Computing5(3), 305–318. IEEE.

    Google Scholar

    Torroni P., Chesani F., Mello P. & Montali M.2010. Social commitments in time: satisfied or compensated. In DALT, Baldoni, M., Bentahar, J., van Riemsdijk, M.B. & Lloyd, J. (eds), LNCS 5948. 228–243. Springer.

    Google Scholar

    Venkatraman M. & Singh M.1999. Verifying compliance with commitment protocols: enabling open web-based multiagent systems. Autonomous Agents and Multi-Agent Systems2(3), 217–236.

    Google Scholar

    Verdicchio M. & Colombetti M.2003. A logical model of social commitment for agent communication. In Proceedings of the 2nd International Joint Conference on AAMAS, 528–535.

    Google Scholar

    Verdicchio M. & Colombetti M.2004. A logical model of social commitment for agent communication. In ACL, Dignum, F. (ed.), LNCS 2922. 128–145. Springer.

    Google Scholar

    Verdicchio M. & Colombetti M.2005. Dealing with time in content language expressions. In AC, van Eijk, R., Huget, M. & Dignum, F. (eds), LNCS 3396. 91–105. Springer.

    Google Scholar

    Verdicchio M. & Colombetti M.2006. From message exchanges to communicative acts to commitments. Electronic Notes in Theoretical Computer Science157, 75–94.

    Google Scholar

    Vidoni R., Garca-Sánchez F., Gasparetto A. & Martnez-Béjar R.2011. An intelligent framework to manage robotic autonomous agents. Expert Systems with Applications38, 7430–7439.

    Google Scholar

    Walton D. & Krabbe E.1995. Commitment in Dialogue: Basic Concepts of Interpersonal Reasoning. State University of New York Press.

    Google Scholar

    Weiss G.1999. Multiagent Systems: A Modern Approach to Distributed Artificial Intelligence. The MIT Press.

    Google Scholar

    Winikoff M.2007. Implementing commitment-based interactions. In AAMAS, Durfee, E., Yokoo, M., Huhns, M. & Shehory, O. (eds). ACM, 873–880.

    Google Scholar

    Winikoff M., Liu W. & Harland J.2005. Enhancing commitment machines. In DALT, Leite, J.A., Omicini, A., Torroni, P. & Yolum, P. (eds), LNCS 3476. 198–220. Springer.

    Google Scholar

    Wooldridge M.2000. Semantic issues in the verification of agent communication languages. Autonomous Agents and Multi-Agent Systems3(1), 9–31.

    Google Scholar

    Wooldridge M.2009. An Introduction to Multi-Agent Systems. John Wiley and Sons.

    Google Scholar

    Xing J. & Singh M.2001. Formalization of commitment-based agent interaction. In SAC, 115–120. ACM.

    Google Scholar

    Xing J. & Singh M.2003. Engineering commitment-based multiagent systems: a temporal logic approach. In Proceedings of the 2nd International Joint Conference on AAMAS, 891–898.

    Google Scholar

    Yolum P.2007. Design time analysis of multiagent protocols. Data and Knowledge Engineering63(1), 137–154.

    Google Scholar

    Yolum P. & Singh M.2002a. Commitment machines. In ATAL, Meyer, J.-J.Ch. & Tambe, M. (eds), LNCS 2333. 235–247. Springer.

    Google Scholar

    Yolum P. & Singh M.2002b. Flexible protocol specification and execution: applying event calculus planning using commitments. In Proceedings of the International Joint Conference on AAMAS, 527–534. ACM.

    Google Scholar

    Yolum P. & Singh M.2004. Reasoning about commitments in the event calculus: an approach for specifying and executing protocols. Annals of Mathematics and Artificial Intelligence42(1–3), 227–253.

    Google Scholar

  • Cite this article

    Mohamed El Menshawy, Jamal Bentahar, Warda El Kholy, Pinar Yolum, Rachida Dssouli. 2015. Computational logics and verification techniques of multi-agent commitments: survey. The Knowledge Engineering Review 30(5)564−606, doi: 10.1017/S0269888915000065
    Mohamed El Menshawy, Jamal Bentahar, Warda El Kholy, Pinar Yolum, Rachida Dssouli. 2015. Computational logics and verification techniques of multi-agent commitments: survey. The Knowledge Engineering Review 30(5)564−606, doi: 10.1017/S0269888915000065
    shu
Download PDF

Article Metrics

Article views(23) PDF downloads(153)

Other Articles By Authors

RESEARCH ARTICLE   Open Access    

Computational logics and verification techniques of multi-agent commitments: survey

  • 1.

    Montreal

  • 2.

    Shebin El Kom

  • 3.

    Department of Computer Engineering

  • Published online: 06 August 2015
The Knowledge Engineering Review  30,  2015, 30(5): 564−606  |  Cite this article

Abstract: Abstract: Agent communication languages (ACLs) are fundamental mechanisms that enable agents in multi-agent systems to talk, communicate with each other in order to satisfy their individual and social goals in a cooperative and competitive manner. Social approaches are advocated to overcome the shortcomings of ACL semantics delineated by using mental approaches in the figure of agents’ mental notions. Over the last two decades, social commitments have been the subject of considerable research in some of those social approaches as they provide a powerful representation for modeling and reasoning upon multi-agent interactions in the form of mutual contractual obligations. They particularly provide a declarative, flexible, verifiable, and social semantics for ACL messages while respecting agents’ autonomy, heterogeneity, and openness.In this manuscript, we go through prominent and predominate proposals in the literature to explore the state of the art on how temporal logics can be devoted to define a formal semantics for ACL messages in terms of social commitments and associated actions. We explain each proposal and point out if and how it meets seven crucial criteria, four of them introduced by Munindar P. Singh to have a well-defined semantics for ACL messages. Far from deciding the best proposal, our aim is to present the advantages (strengths) and limitations of those proposals to designers and developers using a concrete running example and to compare between them, so that they can make the best choice with regard to their needs. We explore and evaluate current specification languages and different verification techniques that have been discussed within those proposals to, respectively, specify and verify commitment-based protocols. We also investigate logical languages of actions advocated to specify, model, and execute commitment-based protocols in other contributed proposals. Finally, we suggest some solutions that can contribute to address the identified limitations.

    HTML

    Acknowledgments

    • The authors would like to thank the anonymous reviewers for their valuable comments and suggestions of changes and improvements. The authors also would like to thank NSERC (Canada) and Menofia University (Egypt) for their financial support.

    • FIPA-ACL message structure specification, http://www.fipa.org/specs/fipa00061/

    • FIPA-SL content language specification, http://www.fipa.org/specs/fipa00008/index.html

    • See FIPA-ACL interaction protocols (2001, 2002), http://www.fipa.org/repository/ips.php3

    • Temporal logic, a special case of modal logic, consents to reason about temporal relations and qualitative aspects of time in an abstract sense.

    • A computation path is an infinite sequence of system’s states.

    • The state explosion problem means that the number of global states in a model grows exponentially with the number of variables, or concurrent components, constituting the modeled system.

    • http://www.cs.sunysb.edu/cwb/

    Rights and permissions
    • © Cambridge University Press, 2015 2015Cambridge University Press
References (134)
  • About this article
    Cite this article
    Mohamed El Menshawy, Jamal Bentahar, Warda El Kholy, Pinar Yolum, Rachida Dssouli. 2015. Computational logics and verification techniques of multi-agent commitments: survey. The Knowledge Engineering Review 30(5)564−606, doi: 10.1017/S0269888915000065
    Mohamed El Menshawy, Jamal Bentahar, Warda El Kholy, Pinar Yolum, Rachida Dssouli. 2015. Computational logics and verification techniques of multi-agent commitments: survey. The Knowledge Engineering Review 30(5)564−606, doi: 10.1017/S0269888915000065
    shu

    • Catalog

      /

      DownLoad:  Full-Size Img  PowerPoint
      Return
      Return