[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

Reducing model checking commitments for agent communication to model checking ARCTL and GCTL*

  • Published:
Autonomous Agents and Multi-Agent Systems Aims and scope Submit manuscript

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

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

    Google Scholar 

  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

    Google Scholar 

  4. Bentahar J., Meyer J.-J. Ch., Wan W. (2009) Model checking communicative agent-based systems. Knowledge-Based Systems 22(3): 142–159

    Article  Google Scholar 

  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

    Google Scholar 

  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

    Google Scholar 

  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

    Google Scholar 

  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

    Google Scholar 

  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

    Google Scholar 

  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

    Article  Google Scholar 

  19. Dong J., Peng T., Zhao Y. (2010) Automated verification of security pattern compositions. Information & Software Technology 52(3): 274–295

    Article  Google Scholar 

  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

    Google Scholar 

  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

    Google Scholar 

  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

    Article  Google Scholar 

  25. Fagin R., Halpern J. Y., Moses Y., Vardi M. Y. (1995) Reasoning about knowledge. MIT Press, Cambridge, MA

    MATH  Google Scholar 

  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

    Article  Google Scholar 

  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

    Article  Google Scholar 

  31. Jones N. D. (1975) Space-bounded reducibility among combinatorial problems. Computer and System Sciences 11(1): 68–85

    Article  MathSciNet  MATH  Google Scholar 

  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

    Google Scholar 

  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

    Article  MathSciNet  MATH  Google Scholar 

  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

    MathSciNet  MATH  Google Scholar 

  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

    Article  MathSciNet  MATH  Google Scholar 

  39. Mallya A. U., Huhns M. N. (2003) Commitments among agents. IEEE Internet Computing 7(4): 90–93

    Article  Google Scholar 

  40. Mallya A. U., Singh M. P. (2007) An algebra for commitment protocols. Autonomous Agents and Multi-Agent Systems 14(2): 143–163

    Article  Google Scholar 

  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

    MathSciNet  MATH  Google Scholar 

  44. Savitch W. J. (1970) Relationships between nondeterministic and deterministic tape complexities. Computer and System Sciences 4(2): 177–192

    Article  MathSciNet  MATH  Google Scholar 

  45. Searle J. R. (1969) Speech acts: An essay in the philosophy of language. Cambridge University Press, Cambridge

    Book  Google Scholar 

  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

    Article  Google Scholar 

  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

    Article  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Google Scholar 

  51. Singh M. P., Chopra A. K., Desai N. (2009) Commitment-based service-oriented architecture. IEEE Computer 42(11): 72–79

    Article  Google Scholar 

  52. Sirbu M. A. (1997) Credits and debits on the Internet. IEEE Spectrum 34(2): 23–29

    Article  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Google Scholar 

  56. Vardi M. Y., Wolper P. (1994) Reasoning about infinite computations. Information and Computation 115(1): 1–37

    Article  MathSciNet  MATH  Google Scholar 

  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

    Article  Google Scholar 

  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

    Google Scholar 

  61. Wooldridge M. (2009) An introduction to multiagent systems. Wileys, New York

    Google Scholar 

  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

    Article  Google Scholar 

  64. Yolum P., Singh M. P. (2002) Commitment machines. In: Meyer J.-J. Ch., Tambe M. (Eds.) ATAL, LNCS. Springer, Heidelberg, pp 235–247

    Google Scholar 

  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

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Faculty of Engineering and Computer Science, Concordia University, Montreal, QC, Canada

    Mohamed El Menshawy, Jamal Bentahar, Warda El Kholy & Rachida Dssouli

Authors
  1. Mohamed El Menshawy
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jamal Bentahar
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Warda El Kholy
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Rachida Dssouli
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Mohamed El Menshawy.

Rights and permissions

Reprints and permissions

About this article

Cite this article

El Menshawy, M., Bentahar, J., El Kholy, W. et al. Reducing model checking commitments for agent communication to model checking ARCTL and GCTL* . Auton Agent Multi-Agent Syst 27, 375–418 (2013). https://doi.org/10.1007/s10458-012-9208-7

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10458-012-9208-7

Keywords

Search

Navigation