Reasoning about group social commitments in multi-agent systems

This paper aims to analayze and reason about group communicating social commitments in Multi-Agent Systems (MASs). In fact, this paper presents Computation Tree Logic Group Commitments (CTLGC), a temporal logic of group commitments for agent communications which extends computation tree logic (CTL) to reason about group social commitments and their fulfillments simultaneously. To do so, we classify groups of communicating agents into divisible and indivisible. After that, we divide group commitments into two categories: one-to-group and group-to-one commitments. Then, we advocate the necessary social accessibility relations that are needed to capture the semantics of each type of group commitments. Thereafter, we use Benthem?s Correspondence Theory for modal logics to prove the soundness and completeness of the proposed CTLGC logic. Particularly, we present a set of reasoning postulates in CTLGC and correspond them to their related classes of frames. We use the NetBill protocol, a concrete example from business domain to illustrate each reasoning postulate. Furthermore, we adopt the interpreted systems as an underlying formalism over which our developed postulates are interpreted. When correspondence exists, this confirms that the CTLGC logic generated by any subset of the proposed postulates is sound and complete with respect to models that are built on the corresponding frames. By so doing, we provide a novel, consistent, formal and computationally grounded semantic to reason about group communicating social commitments and their fulfillments in MASs and prove the soundness and completeness of the proposed logic.