On the Interaction between Knowledge and Social Commitments in Multi-Agent Systems

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 F. Al-Saqqar ? J. Bentahar (B) ? K. Sultan ? M. El Menshawy Faculty of Engineering and Computer Science, Concordia University, Montreal, Canada e-mail: bentahar@ciise.concordia.ca F. Al-Saqqar e-mail: f_alsaqq@encs.concordia.ca K. Sultan e-mail: k_sultan@encs.concordia.ca M. El Menshawy e-mail: m_eleme@encs.concordia.ca M. El Menshawy Faculty of Computers and Information, Menofia University, Menofia, Egypt e-mail: moh_marzok75@yahoo.com 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.