El Menshawy, Mohamed, Bentahar, Jamal, El Kholy, Warda and Dssouli, Rachida (2013) Reducing model checking commitments for agent communication to model checking ARCTL and GCTL*. Autonomous Agents and Multi-Agent Systems, 27 (3). pp. 375-418. ISSN 1387-2532
Preview |
Text (application/pdf)
873kBdssouli.pdf - Accepted Version |
Official URL: http://dx.doi.org/10.1007/s10458-012-9208-7
Abstract
Social commitments have been extensively and effectively used to represent and model business contracts among autonomous agents having competing objectives in a variety of areas (e.g., modeling business processes and commitment-based protocols). However, the formal verification of social commitments and their fulfillment is still an active research topic. This paper presents CTLC+ that modifies CTLC, a temporal logic of commitments for agent communication that extends computation tree logic (CTL) logic to allow reasoning about communicating commitments and their fulfillment. The verification technique is based on reducing the problem of model checking CTLC+ into the problem of model checking ARCTL (the combination of CTL with action formulae) and the problem of model checking GCTL* (a generalized version of CTL* with action formulae) in order to respectively use the extended NuSMV symbolic model checker and the CWB-NC automata-based model checker as a benchmark. We also prove that the reduction techniques are sound and the complexity of model checking CTLC+ for concurrent programs with respect to the size of the components of these programs and the length of the formula is PSPACE-complete. This matches the complexity of model checking CTL for concurrent programs as shown by Kupferman et al. We finally provide two case studies taken from business domain along with their respective implementations and experimental results to illustrate the effectiveness and efficiency of the proposed technique. The first one is about the NetBill protocol and the second one considers the Contract Net protocol.
| Divisions: | Concordia University > Gina Cody School of Engineering and Computer Science > Concordia Institute for Information Systems Engineering |
|---|---|
| Item Type: | Article |
| Refereed: | Yes |
| Authors: | El Menshawy, Mohamed and Bentahar, Jamal and El Kholy, Warda and Dssouli, Rachida |
| Journal or Publication: | Autonomous Agents and Multi-Agent Systems |
| Date: | 2013 |
| Digital Object Identifier (DOI): | 10.1007/s10458-012-9208-7 |
| Keywords: | Social commitments Agent communication Verification Reduction |
| ID Code: | 977850 |
| Deposited By: | Danielle Dennie |
| Deposited On: | 26 Sep 2013 19:18 |
| Last Modified: | 18 Jan 2018 17:45 |
References:
1.Ågotnes, T., Goranko, V., & Jamroga, W. (2008). Strategic commitment and release in logics for multi-agent systems (Extended abstract). Technical Report IfI-08-01, Clausthal University of Technology, Clausthal-Zellerfeld.2.Artikis A., Pitt J. V. (2009) Specifying open agent systems: A survey. In: Artikis A., Picard G., Vercouter L. (Eds.) ESAW, LNCS. Springer, Heidelberg, pp 29–45
3.Baldoni M., Baroglio C., Marengo E. (2010) Behavior oriented commitment-based protocols. In: Coelho H., Studer R., Wooldridge M. (Eds.) ECAI. IOS Press, Amsterdam, pp 137–142
4.Bentahar J., Meyer J.-J. Ch., Wan W. (2009) Model checking communicative agent-based systems. Knowledge-Based Systems 22(3): 142–159
5.Bentahar, J., Meyer, J.-J. Ch., & Wan, W. (2010). Model checking agent communication. In M. Dastani, K. V. Hindriks, & J.-J. Ch. Meyer (Eds.), Specification and verification of multi-agent systems (1st edn., Chap. 3, pp. 67–102). Heidelberg: Springer.
6.Bentahar J., Moulin B., Chaib-draa B. (2004) Commitment and argument network: A new formalism for agent communication. In: Dignum F. (Ed.) ACL 2003, LNCS. Springer, Heidelberg, pp 146–165
7.Bentahar, J., Moulin, B., Meyer, J.-J. Ch., & Chaib-draa, B. (2004). A logical model for commitment and argument network for agent communication. In Proceedings of the 3rd International Joint Conference on AAMAS (pp. 792–799). Washington, DC: IEEE Computer Society.
8.Bentahar J., Moulin B., Meyer J.-J. Ch., Lespérance Y. (2007) A new logical semantics for agent communication. In: Inoue K., Satoh K., Toni F. (Eds.) CLIMA VII, LNCS. Springer, Heidelberg, pp 151–170
9.Bhat, G. (1998). Tableau-based approaches to model-checking. Ph.D. thesis, Department of Computer Science, North Carolina State University, Raleigh, NC.
10.Bhat G., Cleavel R., Groce A. (2001) Efficient model checking via Büchi tableau automata. In: Berry G., Comon H., Finkel A. (Eds.) CAV, LNCS. Springer, Heidelberg, pp 38–52
11.Castelfranchi C. (1995) Commitments: From individual intentions to groups and organizations. In: Lesser V. R., Gasser L. (Eds.) ICMAS. MIT Press, Cambridge, MA, pp 41–48
12.Cheng, Z. (2006). Verifying commitment-based business protocols and their compositions: Model checking using promela and spin. Ph.D. thesis, North Carolina State University, Raleigh, NC.
13.Chesani, F., Mello, P., Montali, M., & Torroni, P. (2009). Commitment tracking via the reactive event calculus. In C. Boutilier (Ed.), IJCAI, Pasadena, CA, pp. 91–96.
14.Chopra, A. K., & Singh, M. P. (2009). Multiagent commitment alignment. In C. Sierra, C. Castelfranchi, K. S. Decker, & J. S. Sichman (Eds.), International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2009), Budapest, pp. 937–944.
15.Clarke E. M., Grumberg O., Peled D. A. (1999) Model checking. MIT Press, Cambridge, MA
16.Colombetti, M. (2000). A commitment-based approach to agent speech acts and conversations. In Proceedings of the Fourth International Conference on Autonomous Agents, Workshop on Agent Languages and Conversation Policies, Barcelona, pp. 21–29.
17.Desai, N., Cheng, Z., Chopra, A. K., & Singh, M. (2007). Toward verification of commitment protocols and their compositions. In E. H. Durfee, M. Yokoo, M. N. Huhns, & O. Shehory (Eds.), AAMAS (pp. 144–146). Richland, SC: IFAAMAS.
18.Desai N., Chopra A. K., Singh M. P. (2009) Amoeba: A methodology for modeling and evolution of cross-organizational business processes. ACM Transaction on Software Engineering and Methodology 19(2): 1–40
19.Dong J., Peng T., Zhao Y. (2010) Automated verification of security pattern compositions. Information & Software Technology 52(3): 274–295
20.El-Menshawy M., Bentahar J., Dssouli R. (2010) Modeling and verifying business interactions via commitments and dialogue actions. In: Jedrzejowicz P., Nguyen N. T., Howlett R. J., Jain L. C. (Eds.) KES-AMSTA (2), LNCS. Springer, Heidelberg, pp 11–21
21.El-Menshawy, M., Bentahar, J., & Dssouli, R. (2010). Verifiable semantic model for agent interactions using social commitments. In M. Dastani, A. E. Fallah-Seghrouchni, J. Leite, & P. Torroni (Eds.), LADS, LNCS (Vol. 6039, pp. 128–152). Heidelberg: Springer.
22.El-Menshawy M., Bentahar J., Dssouli R. (2011) Symbolic model checking commitment protocols using reduction. In: Omicini A., Sardina S., Vasconcelos W. (Eds.) DALT, LNAI. Springer, Heidelberg, pp 185–203
23.El-Menshawy, M., Benthar, J., Qu, H., & Dssouli, R. (2011). On the verification of social commitments and time. In Proceedings of the 10th International Conference on AAMAS, Taipei, pp. 483–890.
24.Emerson E. A., Mok A. K., Sistla A. P., Srinivasan J. (1992) Quantitative temporal reasoning. Journal of Real-Time Systems 4(4): 331–352
25.Fagin R., Halpern J. Y., Moses Y., Vardi M. Y. (1995) Reasoning about knowledge. MIT Press, Cambridge, MA
26.Fornara, N., & Colombetti, M. (2002). Operational specification of a commitment-based agent communication language. In Proceedings of the 1st International Conference on AAMAS (pp. 535–542). New York: ACM.
27.Fornara N., Viganò F., Verdicchio M., Colombetti M. (2008) Artificial institutions: A model of institutional reality for open multi-agent systems. Artificial intelligence and Law 16(1): 89–105
28.Gerard, S. N., & Singh, M. P. (2011). Formalizing and verifying protocol refinements. ACM Transactions on Intelligent Systems and Technology, 2(3) (in press).
29.Jamroga, W., & Ågotnes, T. (2007). Modular interpreted systems. In Proceedings of the 6th International Conference on AAMAS (pp. 131:1–131:8). New York: ACM.
30.Jones A. J. I., Parent X. (2007) A convention-based approach to agent communication languages. Group Decision and Negotiation 16(2): 101–141
31.Jones N. D. (1975) Space-bounded reducibility among combinatorial problems. Computer and System Sciences 11(1): 68–85
32.Kova M., Bentahar J., Maamar Z., Yahyaoui H. (2009) A formal verification approach of conversations in composite web services using NuSMV. In: Fujita H., Marík V. (Eds.) SoMeT. IOS Press, Amsterdam, pp 245–261
33.Kozen, D. (1977). Lower bounds for natural proof systems. In Proceedings of the 18th IEEE Symposium on Foundation of Computer Science, Providence, RI, pp. 254–266.
34.Kupferman O., Vardi M., Wolper P. (2000) An automata-theoretic approach to branching-time model checking. Journal of the ACM 47(2): 312–360
35.Lomuscio, A., Pecheur, C., & Raimondi, F. (2007) Automatic verification of knowledge and time with NuSMV. In Proceedings of the 20th International Joint Conference on Artificial Intelligence (pp. 1384–1389). San Francisco: Morgan Kaufmann.
36.Lomuscio A., Penczek W., Qu H. (2010) Partial order reductions for model checking temporal-epistemic logics over interleaved multi-agent systems. Fundamenta Informaticae 101(1–2): 71–90
37.Lomuscio A., Qu H., Raimondi F. (2009) MCMAS: A model checker for the verification of multi-agent systems. In: Bouajjani A., Maler O. (eds) CAV, LNCS. Springer, pp 682–688
38.Lynch N. (1977) Log space recognition and translation of parenthesis languages. Journal of ACM 24(4): 583–590
39.Mallya A. U., Huhns M. N. (2003) Commitments among agents. IEEE Internet Computing 7(4): 90–93
40.Mallya A. U., Singh M. P. (2007) An algebra for commitment protocols. Autonomous Agents and Multi-Agent Systems 14(2): 143–163
41.Mallya, A. U., Yolum, P., & Singh, M. P. (2004). Resolving commitments among autonomous agents. In Dignum F. (Ed.), ACL 2003, LNCS (Vol. 2922, 166–182). Heidelberg: Springer.
42.Pecheur, C., & Raimondi, F. (2007). Symbolic model checking of logics with actions. In S. Edelkamp, & A. Lomuscio (Eds.), Model checking and artificial intelligence (MoChArt 2006), LNCS (Vol. 4428, pp. 113–128). Heidelberg: Springer.
43.Penczek W., Lomuscio A. (2003) Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae 55(2): 167–185
44.Savitch W. J. (1970) Relationships between nondeterministic and deterministic tape complexities. Computer and System Sciences 4(2): 177–192
45.Searle J. R. (1969) Speech acts: An essay in the philosophy of language. Cambridge University Press, Cambridge
46.Singh, M. P. (1996). A conceptual analysis of commitments in multi-agent systems. Technical Report, North Carolina State University, Raleigh, NC.
47.Singh M. P. (1998) Agent communication languages: Rethinking the principles. IEEE Computer 31(12): 40–47
48.Singh M. P. (1999) An ontology for commitments in multiagent systems: Toward a unification of normative concepts. Artificial intelligence and Law 7(1): 97–113
49.Singh M. P. (2000) A social semantics for agent communication languages. In: Dignum F., Greaves M. (Eds.) Issues in agent communication, LNCS. Springer, Heidelberg, pp 31–45
50.Singh M. P. (2008) Semantical considerations on dialectical and practical commitments. In: Fox D., Gomes C. P. (Eds.) AAAI. AAAI Press, Menlo Park, CA, pp 176–181
51.Singh M. P., Chopra A. K., Desai N. (2009) Commitment-based service-oriented architecture. IEEE Computer 42(11): 72–79
52.Sirbu M. A. (1997) Credits and debits on the Internet. IEEE Spectrum 34(2): 23–29
53.Telang P., Singh M. (2009) Enhancing tropos with commitments: A business meta-model and methodology. In: Borgida A., Chaudhri V. K., Giorgini P., Yu E. S. K. (Eds.) Conceptual modeling: Foundations and applications, LNCS. Springer, Heidelberg, pp 417–435
54.Telang, P. R., & Singh, M. P. (2011). Specifying and verifying cross-organizational business models: An agent-oriented approach. IEEE Transactions on Services Computing, 4 (in press).
55.Torroni P., Chesani F., Mello P., Montali M. (2010) Social commitments in time: Satisfied or compensated. In: Baldoni M., Bentahar J., Riemsdijk M. B., Lloyd J. (Eds.) DALT, LNCS. Springer, Heidelberg, pp 228–243
56.Vardi M. Y., Wolper P. (1994) Reasoning about infinite computations. Information and Computation 115(1): 1–37
57.Venkatraman M., Singh M. P. (1999) Verifying compliance with commitment protocols: Enabling open web-based multiagent systems. Autonomous Agents and Multi-Agent Systems 2(3): 217–236
58.Verdicchio, M., & Colombetti, M. (2003). A logical model of social commitment for agent communication. In Proceedings of the 2nd International Conference on AAMAS (pp. 528–535). New York: ACM.
59.Winikoff, M. (2007). Implementing commitment-based interactions. In E. Durfee, M. Yokoo, M. Huhns, & O. Shehory (Eds.), AAMAS, Honolulu, HI, pp. 873–880.
60.Wooldridge M. (2002) An introduction to multi-agent system. Wiley, New York
61.Wooldridge M. (2009) An introduction to multiagent systems. Wileys, New York
62.Xing, J., & Singh, M. P. (2003). Engineering commitment-based multi-agent systems: A temporal logic approach. In Proceedings of the 2nd International Conference on AAMAS (pp. 891–898). New York: ACM.
63.Yolum P. (2007) Design time analysis of multi-agent protocols. Data and Knowledge Engineering 63: 137–154
64.Yolum P., Singh M. P. (2002) Commitment machines. In: Meyer J.-J. Ch., Tambe M. (Eds.) ATAL, LNCS. Springer, Heidelberg, pp 235–247
65.Yolum, P., & Singh, M. P. (2002). Flexible protocol specification and execution: Applying event calculus planning using commitment. In Proceedings of the 1st International Conference on AAMAS (pp. 527–534). New York: ACM.
66.Yolum P., Singh M. P. (2004) Reasoning about commitments in the event calculus: An approach for specifying and executing protocols. Annals of Mathematics and Artificial Intelligence 42(1–3): 227–253
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.
Repository Staff Only: item control page
Download Statistics
Download Statistics