Abstract
Both knowledge and social commitments have received considerable attention in Multi-Agent Systems (MASs), specially for multi-agent communication. Plenty of work has been carried out to define their semantics. However, the relationship between social commitments and knowledge has not been investigated yet. In this paper, we aim to explore such a relationship from the semantics and model checking perspectives with respect to CTLK logic (an extension of CTL logic with modality for reasoning about knowledge) and CTLC logic (an extension of CTL with modalities for reasoning about commitments and their fulfillments). To analyze this logical relationship, we simply combine the two logics in one new logic named CTLKC. The purpose of such a combination is not to advocate a new logic, but only to express and figure out some reasoning postulates merging both knowledge and commitments as they are currently defined in the literature. By so doing, we identify some paradoxes in the new logic showing that simply combining current versions of commitment and knowledge logics results in a logical language that violates some fundamental intuitions. Consequently, we propose CTLKC+, a new logic that fixes the identified paradoxes and allows us to reason about social commitments and knowledge simultaneously in a consistent manner. Furthermore, we address the problem of model checking CTLKC+ by reducing it to the problem of model checking GCTL∗, a generalized version of CTL∗ with action formulae. By doing so, we directly benefit from CWB-NC, the model checker of GCTL∗. Using this reduction, we also prove that the computational complexity of model checking CTLKC+ is still PSPACE-complete for concurrent programs as the complexity of model checking CTLK and CTLC separately.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Alberti M, Gavanelli M, Lamma E, Mello P, Torroni P (2004) Specification and verification of agent interaction using social integrity constraints. Electron Notes Theor Comput Sci 85(2):94–116
Aldewereld H (2007) Autonomy vs conformity: an institutional perspective on norms and protocols. PhD thesis, Universiteit Utrecht, Utrecht, The Netherlands
Aldewereld H, Álvarez Napagao S, Dignum F, Vázquez-Salceda J (2009) Engineering social reality with inheritance relations. In: Aldewereld H, Dignum V, Picard G (eds) ESAW. Lecture notes in computer science, vol 5881. Springer, Berlin, pp 116–131
Aldewereld H, Álvarez Napagao S, Dignum F, Vázquez-Salceda J (2010) Making norms concrete. In: van der Hoek W, Kaminka GA, Lespérance Y, Luck M, Sen S (eds) 9th international conference on autonomous agents and multiagent systems (AAMAS 2010), Toronto, Canada, 10–14 May 2010, vols 1–3, pp 807–814. IFAAMAS
Anger FD, Clarke EM (1993) New and used temporal models: an issue of time. Appl Intell 3(1):5–15
Baier C, Katoen J-P (2008) Principles of model checking. Representation and mind series. MIT Press, Cambridge
Baldoni M, Baroglio C, Marengo E (2010) Behavior-oriented commitment-based protocols. In: ECAI, pp 137–142
Bennett B, Cohn AG, Wolter F, Zakharyaschev M (2002) Multi-dimensional modal logic as a framework for spatio-temporal reasoning. Appl Intell 17(3):239–251
Bentahar J, El-Menshawy M, Qu H, Dssouli R (2012) Communicative commitments: model checking and complexity analysis. Knowl-Based Syst 35:21–34
Bentahar J, Meyer J-J, Wan W (2010) Model checking agent communication. In: Specification and verification of multi-agent systems. Springer, Berlin, pp 67–102
Bhat G, Cleaveland R, Groce A (2001) Efficient model checking via Büchi tableau automata. In: Berry G, Comon H, Finkel A (eds) CAV 2001. Lecture notes in computer science. Springer, Berlin, pp 38–52
Blackburn P, de Rijke M, Venema Y (2001) Modal logic. Cambridge University Press, New York
Both F, Hoogendoorn M, van der Mee A, Treur J, de Vos M (2012) An intelligent agent model with awareness of workflow progress. Appl Intell 36(2):498–510
Clarke E, Grumberg O, Peled D (1999) Model checking. MIT Press, Cambridge
Cox B, Tygar JD, Sirbu M (1995) Netbill security and transaction protocol. In: First USENIX workshop on electronic commerce, pp 77–88
Desai N, Cheng Z, Chopra AK, Singh MP (2007) Toward verification of commitment protocols and their compositions. In: AAMAS, pp 144–146
Desai N, Chopra AK, Singh MP (2009) Amoeba: a methodology for modeling and evolving cross-organizational business processes. ACM Trans Softw Eng Methodol 19(2):6
Dignum F, Greaves M (eds) (2000) Issues in agent communication. Lecture notes in computer science, vol 1916. Springer, Berlin
Dignum F, Meyer J-JC, Wieringa R, Kuiper R (1996) A modal approach to intentions, commitments and obligations: intention plus commitment yields obligation. In: DEON, pp 80–97
Dourlens S, Ramdane-Cherif A, Monacelli E (2013) Multi levels semantic architecture for multimodal interaction. Appl Intell 38(4):586–599
El-Menshawy M (2012) Model checking logics of social commitments for agent communication. PhD thesis, Concordia University, Montreal, Canada
El-Menshawy M, Bentahar J, Dssouli R (2010) Verifiable semantic model for agent interactions using social commitments. In: LADS, pp 128–152
El-Menshawy M, Bentahar J, El-Kholy W, Dssouli R (2013) Reducing model checking commitments for agent communication to model checking arctl and gctl*. Auton Agents Multi-Agent Syst 27(3):375–418
El-Menshawy M, Bentahar J, El-Kholy W, Dssouli R (2013) Verifying conformance of multi-agent commitment-based protocol. Expert Syst Appl 40(1):122–138
El-Menshawy M, Bentahar J, Qu H, Dssouli R (2011) On the verification of social commitments and time. In: AAMAS, pp 483–490
Fagin R, Halpern JY, Moses Y, Vardi MY (1995) Reasoning about knowledge. MIT Press, Cambridge
Fornara N, Colombetti M (2004) A commitment-based approach to agent communication. Appl Artif Intell 18(9–10):853–866
Fornara N, Viganò F, Verdicchio M, Colombetti M (2008) Artificial institutions: a model of institutional reality for open multiagent systems. Artif Intell Law 16(1):89–105
Gabbay DM (2003) Many-dimensional modal logics: theory and applications. Studies in logic and the foundations of mathematics series. Elsevier/North-Holland, Amsterdam
Grossi D, Aldewereld H, Vázquez-Salceda J, Dignum F (2006) Ontological aspects of the implementation of norms in agent-based electronic institutions. Comput Math Organ Theory 12(2–3):251–275
Günay A, Yolum P (2013) Constraint satisfaction as a tool for modeling and checking feasibility of multiagent commitments. Appl Intell 39(3):489–509
Halpern JY (1995) Reasoning about knowledge: a survey. Technical report, IBM Almaden Research Center
Halpern JY, Moses Y (1990) Knowledge and common knowledge in a distributed environment. J ACM 37(3):549–587
Halpern JY, Rêgo LC (2013) Reasoning about knowledge of unawareness revisited. Math Soc Sci 65(2):73–84
Halpern JY, Shore RA (2004) Reasoning about common knowledge with infinitely many agents. Inf Comput 191(1):1–40
Hintikka J (1962) Knowledge and belief: an introduction to the logic of the two notions. Cornell University Press, Ithaca
Kupferman O, Vardi M, Wolper P (2000) An automata-theoretic approach to branching-time model checking. J ACM 47(2):312–360
Lenzen W (1978) Recent work in epistemic logic. Acta philosophica fennica, vol 30. North-Holland, Amsterdam
Lomuscio A, Penczek W (2012) Symbolic model checking for temporal-epistemic logic. In: Logic programs, norms and action, pp 172–195
Lomuscio A, Raimondi F (2006) The complexity of model checking concurrent programs against ctlk specifications. In: Declarative agent languages and technologies IV. Lecture notes in computer science, vol 4327. Springer, Berlin, pp 29–42
Mallya AU, Singh MP (2007) An algebra for commitment protocols. Auton Agents Multi-Agent Syst 14(2):143–163
Mousavi A, Nordin MJ, Othman ZA (2012) Ontology-driven coordination model for multiagent-based mobile workforce brokering systems. Appl Intell 36(4):768–787
Obeid N (2005) A formalism for representing and reasoning with temporal information, event and change. Appl Intell 23(2):109–119
Parikh R, Ramanujam R (1985) Distributed processes and the logic of knowledge. In: Logic of programs, pp 256–268
Penczek W, Lomuscio A (2003) Verifying epistemic properties of multi-agent systems via bounded model checking. In: AAMAS, pp 209–216
Raimondi F (2006) Model checking multi-agent systems. PhD thesis, University College, London, London
Rosenschein SJ (1985) Formal theories of knowledge in AI and robotics. New Gener Comput 3(4):345–357
Searle JR (1969) Speech acts: an essay in the philosophy of language. Cambridge University Press, Cambridge
Serrano E, Such JM, Botía J, García-Fornes A (2013) Strategies for avoiding preference profiling in agent-based e-commerce environments. Appl Intell. doi:10.1007/s10489-013-0448-2
Singh MP (1998) Agent communication languages: rethinking the principles. Computer 31(12):40–47
Singh MP (1999) An ontology for commitments in multiagent systems. Artif Intell Law 7(1):97–113
Singh MP (2000) A social semantics for agent communication languages. In: Issues in agent communication, pp 31–45
Sirbu MA (1997) Credits and debits on the Internet. IEEE Spectr 34(2):23–29
Su C, Li H (2012) An affective learning agent with petri-net-based implementation. Appl Intell 37(4):569–585
van der Meyden R, shu Wong K (2003) Complete axiomatizations for reasoning about knowledge and branching time. Stud Log 75(1):93–123
Venkatraman M, Singh MP (1999) Verifying compliance with commitment protocols. Auton Agents Multi-Agent Syst 2(3):217–236
Wan W, Bentahar J, Hamza AB (2012) Quantitative model checking of knowledge. In: SoMeT, pp 91–107
Winikoff M (2007) Implementing commitment-based interactions. In: AAMAS, pp 873–880
Wooldridge M (2000) Computationally grounded theories of agency. In: ICMAS, pp 13–22
Wooldridge M (2002) Introduction to multiagent systems. Wiley, New York
Wooldridge M, Lomuscio A (2000) Multi-agent VSK logic. In: JELIA, pp 300–312
Yolum P, Singh MP (2004) Reasoning about commitments in the event calculus: an approach for specifying and executing protocols. Ann Math Artif Intell 42(1–3):227–253
Acknowledgements
We would like to thank the anonymous reviewers for their valuable technical comments and suggestions. The first, second, third, and fourth authors would like to thank, respectively, Al al-Bayt University (Jordan), the Natural Sciences and Engineering Research Council of Canada (NSERC), the Ministry of Higher Education (Libya), and Menofia University (Egypt) for their financial supports.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Al-Saqqar, F., Bentahar, J., Sultan, K. et al. On the interaction between knowledge and social commitments in multi-agent systems. Appl Intell 41, 235–259 (2014). https://doi.org/10.1007/s10489-013-0513-x
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10489-013-0513-x