Abstract
Using model checking to verify that interaction protocols have given properties is widely recognized as an important issue in multi-agent systems where autonomous and heterogeneous agents need to successfully regulate and coordinate their interactions. In this paper, we investigate the use of symbolic model checkers to verify the compliance of a special kind of interaction protocols called commitment protocols with some properties such as liveness and safety. These properties are expressed as formulae in a new temporal logic, called CTLC, which extends the temporal logic CTL with modality for social commitments. Our approach shows that the problem of model checking CTLC can be reduced to the problem of model checking either CTLK or ARCTL, which are extensions of CTL. We finally present an implementation and report on the experimental results of verifying the Contract Net Protocol modeled in terms of commitments and associated actions using the symbolic model checkers MCMAS and extended NuSMV.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bentahar, J., Meyer, J.J.C., Wan, W.: Model Checking Agent Communication. In: Dastani, M., Hindriks, K.V., Meyer, J.J.C. (eds.) Specification and Verification of Multi-Agent Systems, 1st edn., pp. 67–102. Springer, Heidelberg (2010)
Bentahar, J., Moulin, B., Chaib-draa, B.: Specifying and Implementing a Persuasion Dialogue Game using Commitment and Argument Network. In: Rahwan, I., Moraïtis, P., Reed, C. (eds.) ArgMAS 2004. LNCS (LNAI), vol. 3366, pp. 130–148. Springer, Heidelberg (2005)
Bhat, G., Cleaveland, R., Groce, A.: Efficient Model Checking via Büchi Tableau Automata. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 38–52. Springer, Heidelberg (2001)
Bordini, R.H., Fisher, M., Pardavila, C., Wooldridge, M.: Model Checking Agentspeak. In: Proceedings of the 2nd International Joint Conference on Autonomous Agents and Multiagent Systems, pp. 409–416. ACM, Melbourne (2003)
Cheng, Z.: Verifying Commitment based Business Protocols and their Compositions: Model Checking using Promela and Spin. Ph.D. thesis, North Carolina State University (2006)
Chopra, A.K., Singh, M.P.: Nonmonotonic Commitment Machines. In: Dignum, F. (ed.) ACL 2003. LNCS (LNAI), vol. 2922, pp. 183–200. Springer, Heidelberg (2004)
Chopra, A.K., Singh, M.P.: Producing Compliant Interactions: Conformance, Coverage and Interoperability. In: Baldoni, M., Endriss, U. (eds.) DALT IV 2006. LNCS (LNAI), vol. 4327, pp. 1–15. Springer, Heidelberg (2006)
Cimatti, A., Clarke, E., 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, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
Desai, N., Cheng, Z., Chopra, A.K., Singh, M.P.: Toward Verification of Commitment Protocols and their Compositions. In: Proceedings of the 6th International Joint Conference on Autonomous Agents and Multiagent Systems, pp. 144–146. ACM, Honolulu (2007)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. The MIT Press, Cambridge (1995)
Fornara, N., Colombetti, M.: Operational Specification of a Commitment-based Agent Communication Language. In: Proceedings of the 1st International Joint Conference on Autonomous Agents and Multiagent Systems, pp. 535–542. ACM, Bologna (2002)
Gerard, S.N., Singh, M.P.: Protocol Refinement: Formalization and Verification. In: Artikis, A., Bentahar, J., Chopra, A.K., Dignum, F. (eds.) AAMAS Workshop on Agent Communication (AC), Toronto, Canada, pp. 19–36 (2010)
Guerin, F., Pitt, J.: Guaranteeing Properties for E-Commerce Systems. In: Padget, J.A., Shehory, O., Parkes, D.C., Sadeh, N.M., Walsh, W.E. (eds.) AMEC IV 2002. LNCS (LNAI), vol. 2531, pp. 253–272. Springer, Heidelberg (2002)
Lamport, L.: Proving the Correctness of Multiprocess Programs. IEEE Transactions on Software Engineering 3(2), 125–143 (1977)
Lomuscio, A., Pecheur, C., Raimondi, F.: Automatic Verification of Knowledge and Time with Nusmv. In: Proceedings of the 20th International Joint Conference on Artificial Intelligence, pp. 1384–1389. Morgan Kaufmann Publishers Inc., Hyderabad (2007)
Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: A Model Checker for the Verification of Multi-Agent Systems. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 682–688. Springer, Heidelberg (2009)
Manna, Z., Pnueli, A.: The Temporal Logic of Rreactive and Concurrent Systems: Specification, 1st edn. Springer, Inc., New York (1991)
Medellin, R., Atkinson, K., McBurney, P.: Model Checking Command Dialogues. In: Proceedings of 2009 AAAI Fall Symposium on The Uses of Computational Argumentation, pp. 58–63. AAAI Press, Arlington (2009)
Pecheur, C., Raimondi, F.: Symbolic model checking of logics with actions. In: Edelkamp, S., Lomuscio, A. (eds.) MoChArt IV. LNCS (LNAI), vol. 4428, pp. 113–128. Springer, Heidelberg (2007)
Penczek, W., Lomuscio, A.: Verifying Epistemic Properties of Multi-Agent Systems via Bounded Model Checking. Fundamenta Informaticae 55(2), 167–185 (2003)
Raimondi, F.: Model Checking Multi-Agent Systems. Ph.D. thesis, University College London (2006)
Singh, M.P.: An Ontology for Commitments in Multiagent Systems: Toward a Unification of Normative Concepts. Artificial Intelligent and Law 7(1), 97–113 (1999)
Singh, M.P.: Formalizing Communication Protocols for Multiagent Systems. In: Proceedings of the 20th International Joint Conference on Artificial Intelligence, pp. 1519–1524. Morgan Kaufmann Publishers, Inc., Hyderabad (2007)
Venkatraman, M., Singh, M.P.: Verifying Compliance with Commitment Protocols: Enabling Open Web-based Multiagent Systems. Autonomous Agents and Multi-Agent Systems 2(3), 217–236 (1999)
Viganò, F., Colombetti, M.: Symbolic Model Checking of Institutions. In: Proceedings of the 9th International Conference on Electronic Commerce, pp. 35–44. ACM Press, Minneapolis (2007)
Yolum, P.: Design Time Analysis of Multi-Agent Protocols. Data and Knowladge Engineering 63(1), 137–1154 (2007)
Yolum, P., Singh, M.P.: Commitment machines. In: Meyer, J.J.C., Tambe, M. (eds.) ATAL 2001. LNCS (LNAI), vol. 2333, pp. 235–247. Springer, Heidelberg (2002)
Yolum, P., Singh, M.P.: Reasoning about Commitments in the Event Calculus: An Approach for Sepcifying and Executing Protocols. Annals of Mathematics and Artificial Intelligence 42(1-3), 227–253 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
El-Menshawy, M., Bentahar, J., Dssouli, R. (2011). Symbolic Model Checking Commitment Protocols Using Reduction. In: Omicini, A., Sardina, S., Vasconcelos, W. (eds) Declarative Agent Languages and Technologies VIII. DALT 2010. Lecture Notes in Computer Science(), vol 6619. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20715-0_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-20715-0_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-20714-3
Online ISBN: 978-3-642-20715-0
eBook Packages: Computer ScienceComputer Science (R0)