SMC4AC : A New Symbolic Model Checker for Intelligent Agent Communication

• Autorzy: El Kholy, W. , Bentahar, J. , Qu, H. , El Menshawy, M. , Dssouli, R.
• Języki publikacji: EN

Abstrakty

EN

Social approaches have been put forward to define semantics for intelligent agent communication messages and to tackle the shortcomings of mental approaches. Formal semantics of those social approaches can be model checked as they are focused on public behaviors instead of private mental states. Social conditional commitments are essential concepts in social approaches that can effectively model agent communications. However, conditional commitments exclusively are not able to model agent communication actions, the cornerstone of the fundamental agent communication theory, namely speech act theory. These actions provide mechanisms for dynamic interactions and enable designers to track the evolution of active conditional commitments. From the perspective of model checking, we need to define a formal and computationally grounded semantics for relevant social actions that can directly be applied to active conditional commitments. This manuscript describes a new symbolic model checker, SMC4AC, developed and implemented to automate the verification of interaction among intelligent agents. SMC4AC is the result of developing a new symbolic model checking algorithm devoted to CTLC^α, a combination of CTL and new temporal modalities to represent and reason about conditional commitments and common commitment actions. The core of this paper consists of a new logical language, a detailed description of the symbolic algorithms needed for commitments and their action modalities, complexity analysis, implementation and application. The implementation of our algorithm and its graphical user interface is built on top of the MCMAS symbolic model checker tailored for checking intelligent multi-agent systems. We select business processes and multi-agent interaction protocols as application domains to test and validate the effectiveness and scalability of SMC4AC. We report extensive experimental results, which confirm the theoretical findings and make SMC4AC practical.

Słowa kluczowe

EN

commitment action modalities; conditional commitment; conditional commitment actions; expressiveness; symbolic model checker; verification

• Czasopismo: Fundamenta Informaticae
• Rocznik: 2017
• Tom: Vol. 152, nr 3
• Strony: 223--271
• Opis fizyczny: Bibliogr. 54 poz., tab., wykr.

Twórcy

autor

El Kholy, W.

• Concordia Institute for Information Systems Engineering, Concordia University, Canada,

autor

Bentahar, J.

• Concordia Institute for Information Systems Engineering, Concordia University, Canada,

autor

Qu, H.

• Automatic Control and Systems Engineering, Shefield University, United Kingdom,

autor

El Menshawy, M.

• Faculty of Computers and Information, Menoufia University, Egypt,

autor

Dssouli, R.

• Concordia Institute for Information Systems Engineering, Concordia University, Canada,

Bibliografia

• [1] Clarke E, Grumberg O, Peled D. Model Checking. MIT Press, Cambridge, 1999.
• [2] Clarke EM, Emerson EA, Sifakis J. Model checking: Algorithmic verification and debugging. Communications of the ACM, 2009;52(11):74–84. doi:10.1145/1592761.1592781.
• [3] Fagin R, Halpern J, Moses Y, Vardi M. Reasoning about Knowledge. MIT Press, 1995. ISBN-13:978-0262562003, 10:0262562006.
• [4] Gammie P, van der Meyden R. MCK: Model Checking the Logic of Knowledge. In: Proceedings of 16th International Conference on Computer Aided Verification (CAV’04), volume 3114 of LNCS. Springer, 2004 pp. 479–483.
• [5] Bentahar J, El-Menshawy M, Qu H, Dssoulia R. Communicative Commitments: Model Checking and Complexity Analysis. Knowledge-Based Systems, 2012;35:21–34. URL http://dx.doi.org/10.1016/j.knosys.2012.04.010.
• [6] El-Kholy W, Bentahar J, El-Menshawy M, Qu H, Dssouli R. Conditional Commitments: Reasoning and Model Checking. ACM Transaction on Software Engineering and Methodology, 2014;24(2):9:1–9–49. doi:10.1145/2685613.
• [7] El-Menshawy M, Benthar J, Qu H, Dssouli R. On the Verification of Social Commitments and Time. In: Sonenberg L, Stone P, Tumer K, Yolum P (eds.), AAMAS. IFAAMAS, 2011 pp. 483–490. URL http://dl.acm.org/citation.cfm?id=2031678.2031686.
• [8] Cimatti A, Clarke EM, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A. NuSMV 2: An Open Source Tool for Symbolic Model Checking. In: Brinksma E, Larsen KG (eds.), Proceedings of the 14th International Conference on Computer Aided Verification (CAV’02),, volume 2404 of LNCS. Springer, 2002 pp. 359–364. ISBN: 3-540-43997-8.
• [9] Lomuscio A, Qu H, Raimondi F. MCMAS: A Model Checker for the Verification of Multi-Agent Systems. In: Bouajjani A, Maler O (eds.), CAV, volume 5643 of LNCS. 2009 pp. 682–688. doi:10.1007/978-3-642-02658-4 55.
• [10] Austin JL. How to Do Things with Words. Oxford University Press: Oxford, England, 1962.
• [11] Baldoni M, Baroglio C, Capuzzimati F, Marengo E, Patti V. A Generalized Commitment Machine for 2CL Protocols and its Prolog Implementation. In: Lisi FA (ed.), CILC, volume 857. CEUR-WS.org, 2012 pp.2–16.
• [12] Bentahar J, Moulin B, Meyer JJC, Lespérance Y. A New Logical Semantics for Agent Communication. In: Inoue K, Satoh K, Toni F (eds.), CLIMA VII, volume 4371 of LNCS. Springer, 2007 pp. 151–170.
• [13] Singh M. Semantical Considerations on Dialectical and Practical Commitments. In: Proc. of AAAI. 2008 pp. 176–181. ISBN: 978-1-57735-368-3.
• [14] El-Kholy W, El-Menshawy M, Bentahar J, Qu H, Dssouli R. Formal Specification and Automatic Verification of Conditional Commitments. IEEE Intelligent Systems, 2015;30(2):36–44. doi:10.1109/MIS.2015.6.
• [15] Yolum P, Singh MP. Reasoning about Commitments in the Event Calculus: An Approach for Sepcifying and Executing Protocols. Annals of Mathematics and Artificial Intelligence, 2004;42(1–3):227–253. 10.1023/B:AMAI.0000034528.55456.d9.
• [16] Chesani F, Mello P, Montali M, Torroni P. Representing and monitoring social commitments using the event calculus. Autonomous Agents and Multi-Agent Systems, 2013;27(1):85–130. doi:10.1007/s10458-012-9202-0.
• [17] Montali M, Calvanese D, De Giacomo G. Verification of data-aware commitment-based multiagent system. In: Bazzan ALC, Huhns MN, Lomuscio A, Scerri P (eds.), Proceedings of the international conference on Autonomous Agents and Multi-Agent Systems. IFAAMAS/ACM, 2014 pp. 157–164. ISBN: 978-1-4503-2738-1.
• [18] Son TC, Pontelli E, Sakama C. Formalizing Commitments Using Action Languages. In: Sakama C, Sardiña S, Vasconcelos WW, Winikoff M (eds.), Declarative Agent Languages and Technologies IX - 9th International Workshop DALT, volume 7169 of LNCS. Springer, 2012 pp. 67–83. doi:10.1007/978-3-642-29113-5 6.
• [19] Son TC, Pontelli E, Sakama C. An Experiment in Formalizing Commitments Using Action Languages. In: Proceedings of Logical Formalizations of Commonsense Reasoning, AAAI Spring Symposium. AAAI, 2011 pp. 168–171. doi:10.1007/978-3-642-29113-5_6.
• [20] El-Menshawy M, Bentahar J, Dssouli R. Verifiable Semantic Model for Agent Interactions using Social Commitments. In: Dastani M, Fallah-Seghrouchni AE, Leite J, Torroni P (eds.), LADS, volume 6039 of LNCS. 2010 pp. 128–152. doi:10.1007/978-3-642-13338-1_8.
• [21] Singh M, Chopra A, Desai N. Commitment based Service-Oriented Architecture. IEEE Computer, 2009;42(11):72–79. ISSN: 0018-9162.
• [22] Ferrario R, Guarino N. Commitment-Based Modeling of Service Systems. In: Snene M (ed.), Proceedings of the third International Conference on Exploring Services Science, volume 103 of LNBIP. Springer, 2012 pp. 170–185. doi:10.1007/978-3-642-28227-0_13.
• [23] Nardi JC, de Almeida Falbo R, Almeida JPA, Guizzardi G, Pires LF, van Sinderen M, Guarino N, Fonseca CM. A commitment-based reference ontology for services. Information Systems, 2015;54:263–288. doi:10.1016/j.is.2015.01.012.
• [24] Baldoni M, Baroglio C, Marengo E, Patti V, Capuzzimati F. Engineering commitment-based business protocols with the 2CL methodology. Autonomous Agents and Multi-Agent Systems, 2014;28(4):519–557. doi:10.1007/s10458-013-9233-1.
• [25] Baldoni M, Baroglio C, Capuzzimati F. Programming JADE and Jason Agents Based on Social Relationships Using a Uniform Approach. In: Koch F, Guttmann C, Busquets D (eds.), Advances in Social Computing and Multiagent Systems - 6th International Workshop on Collaborative Agents Research and Development, CARE 2015 and Second International Workshop on Multiagent Foundations of Social Computing, MFSC, volume 541. Springer, 2015 pp. 167–184. doi:10.1007/978-3-319-24804-2_11.
• [26] Baldoni M, Baroglio C, Capuzzimati F, Micalizio R. Programming with Commitments and Goals in JaCaMo+. In: Weiss G, Yolum P, Bordini RH, Elkind E (eds.), Proceedings of the International Conference on Autonomous Agents and Multiagent Systems, AAMAS. ACM, 2015 pp. 1705–1706. URL http://dl.acm.org/citation.cfm?id=2772879.2773395.
• [27] Singh M. A Social Semantics for Agent Communication Languages. In: Dignum F, Greaves M (eds.), Issues in Agent Communication, volume 1916 of LNCS. 2000 pp. 31–45. doi:10.1007/10722777_3.
• [28] Spoletini P, Verdicchio M. Commitment Monitoring in a Multi-Agent System. In: Burkhard HD, Lindemann G, Verbrugge R, Varga LZ (eds.), CEEMAS, volume 4696 of LNCS. Springer, 2007 pp. 83–92.
• [29] Spoletini P, Verdicchio M. An Automata-Based Monitoring Technique for Commitment-Based Multiagent Systems. In: Hübner JF, Matson ET, Boissier O, Dignum V (eds.), COIN, volume 5428 of LNCS. Springer, 2009 pp. 172–187.
• [30] El-Menshawy M, Bentahar J, El-Kholy W, Dssouli R. Computational Logics and Verification Techniques of Multi-Agent Commitments: Survey. Cambridge University Press. The Knowledge Engineering Review, 2015;30(5):564–606. URL https://doi.org/10.1017/S0269888915000065.
• [31] Baldoni M, Baroglio C, Marengo E. Behavior Oriented Commitment-based Protocols. In: Coelho H, Studer R, Wooldridge M (eds.), ECAI, volume 215. IOS Press, 2010 pp. 137–142.
• [32] Schnoebelen P. The Complexity of Temporal Logic Model Checking. In: Advances in Modal Logic, volume 4. 2002 pp. 1–44.
• [33] El-Menshawy M, Bentahar J, El-Kholy W, Dssouli R. Reducing Model Checking Commitments for Agent Communication to Model Checking ARCTL and GCTL*. Autonomous Agent Multi-Agent Systems, 2013;27(3):375–418. doi:10.1007/s10458-012-9208-7.
• [34] El-Menshawy M, Bentahar J, El-Kholy W, Dssouli R. Verifying Conformance of Multi-Agent Commitment-based Protocols. Expert Systems with Applications, 2013;40(1):122–138. doi:10.1016/j.eswa.2012.07.030.
• [35] El-Kholy W, Bentahar J, El-Menshawy M, Qu H, Dssouli R. Modeling and verifying choreographed multiagent-based web service compositions regulated by commitment protocols. Expert Systems with Applications, 2014;41:7478–7494. URL http://dx.doi.org/10.1016/j.eswa.2014.05.046.
• [36] El-Kholy W, El-Menshawy M, Bentahar J, Qu H, Dssouli R. Verifying Multiagent-based Web Service Compositions Regulated by Commitment Protocols. In: Proceedings of 21th IEEE International Conference on Web Services (ICWS). IEEE, 2014 pp. 49–56. doi:10.1109/ICWS.2014.20.
• [37] Kupferman O, Vardi MY, Wolper P. An Automata-Theoretic Approach to Branching-Time Model Checking. ACM, 2000;47(2):312–360. doi:10.1145/333979.333987.
• [38] Singh M, Huhns M. Service-Oriented Computing: semantics, processes, agents. JohnWiley & Sons, 2005. ISBN: 978-0-470-09148-7.
• [39] Desai N, Chopra AK, Singh MP. Amoeba: A Methodology for Modeling and Evolution of Cross-Organizational Business Processes. ACM Transaction on Software Engineering and Methodology, 2009;19(2):1–40. URL http://dx.doi.org/10.1145/1571629.1571632.
• [40] Desai N, Narendra N, Singh M. Checking correctness of business contracts via commitments. In: Padgham L, Parkes DC, Müller JP, Parsons S (eds.), AAMAS. IFAAMAS, 2008 pp. 787–794. ISBN: 978-0-9817381-1-6.
• [41] Baldoni M, Baroglio C, Marengo E, Patti V. Constitutive and regulative specifications of commitment protocols: A decoupled approach. Trans. on Int. Syst. and Tech., 2013;4(2):22. doi:10.1145/2438653.2438657.
• [42] El-Menshawy M, Bentahar J, Dssouli R. Verifiable Semantic Model for Agent Interactions using Social Commitments. In: Dastani M, Fallah-Seghrouchni AE, Leite J, Torroni P (eds.), LADS, volume 6039 of LNCS. 2010 pp. 128–152. doi:10.1007/978-3-642-13338-1_8.
• [43] Xing J, Singh M. Engineering Commitment-Based Multiagent Systems: A Temporal Logic Approach. In: Proc. of the 2nd Int. Joint Conf. on AAMAS. 2003 pp. 891–898. doi:10.1145/860575.860719.
• [44] Desai N, Mallya A, Chopra A, Singh M. Interaction Protocols as Design Abstractions for Business Processes. IEEE Trans. on Software Engineering, 2005;31(12):1015–1027. doi:10.1109/TSE.2005.140.
• [45] Chesani F, Mello P, Montali M, Torroni P. Representing and monitoring social commitments using the event calculus. Autonomous Agents and Multi-Agent Systems, 2013;27(1):85–130. doi:10.1007/s10458-012-9202-0.
• [46] Searle J. The construction of social reality. Free Press, New York, 1995. ISBN: 0029280451, 9780029280454.
• [47] Chopra AK, Singh MP. Multiagent Commitment Alignment. In: Sierra C, Castelfranchi C, Decker KS, Sichman JS (eds.), AAMAS. 2009 pp. 937–944. ISBN:978-0-9817381-7-8.
• [48] Pecheur C, Raimondi F. Symbolic Model Checking of Logics with Actions. In: Edelkamp S, Lomuscio A (eds.), Model Checking and Artificial Intelligence (MoChArt 2006), volume 4428 of LNCS. Springer, 2007 pp. 113–128. doi:10.1007/978-3-540-74128-2_8.
• [49] Lomuscio A, Qu H, Solanki M. Towards Verifying Contract Regulated Service Composition. Autonomous Agents and Multi-Agent Systems, 2012;24(3):345–373. doi:10.1007/s10458-010-9152-3.
• [50] Bentahar J, Meyer JJC, Wan W. Model Checking Agent Communication. In: Dastani M, Hindriks KV, Meyer JJC (eds.), Specification and Verification of Multi-Agent Systems, chapter 3, pp. 67–102. Springer, first edition, 2010. doi:10.1007/978-1-4419-6984-2_3.
• [51] Torroni P, Chesani F, Yolum P, Gavanelli M, Singh MP, Lamma E, Alberti M, Mello P. Modelling Interactions via Commitments and Expectations. In: Dignum V (ed.), Handbook of Research on Multi-Agent Systems: Semantics and Dynamics of Organizational Models, chapter 11, pp. 263–284. IGI Global, Hershey, Pennsylvania, 2009.
• [52] Telang P, Singh M. Specifying and Verifying Cross-Organizational Business Models: An Agent Oriented Approach. IEEE Trans. on Serv. Comp., 2012;5(3):305–318. doi:10.1109/TSC.2011.4.
• [53] Yolum P, Singh MP. Commitment Machines. In: Meyer JJC, Tambe M (eds.), ATAL, volume 2333 of LNCS. Springer, 2002 pp. 235–247. doi:10.1007/3-540-45448-9_17.
• [54] Singh MP. Formalizing Communication Protocols for Multi-agent Systems. In: Veloso MM (ed.), IJCAI. 2007 pp. 1519–1524. URL http://dl.acm.org/citation.cfm?id=1625275.1625521.

Identyfikatory

DOI

10.3233/FI-2017-1519