Modeling and verifying probabilistic Multi-Agent Systems using knowledge and social commitments

• We present an extension of interpreted systems including probabilities and communication channels.
• We introduce a new logic merging probabilities, knowledge, and social commitments.
• We advocate a reduction-based technique to model check the logic and prove its soundness.
• We implement the approach using the PRISM model checker.

Multi-Agent Systems (MASs) have long been modeled through knowledge and social commitments independently. In this paper, we present a new method that merges the two concepts to model and verify MASs in the presence of uncertainty. To express knowledge and social commitments simultaneously in uncertain settings, we define a new multi-modal logic called Probabilistic Computation Tree Logic of Knowledge and Commitments (PCTLkc in short) which combines two existing probabilistic logics namely, probabilistic logic of knowledge PCTLK and probabilistic logic of commitments PCTLC. To model stochastic MASs, we present a new version of interpreted systems that captures the probabilistic behavior and accounts for the communication between interacting components. Then, we introduce a new probabilistic model checking procedure to check the compliance of target systems against some desirable properties written in PCTLkc and report the obtained verification results. Our proposed model checking technique is reduction-based and consists in transforming the problem of model checking PCTLkc into the problem of model checking a well established logic, namely PCTL. So doing provides us with the privilege of re-using the PRISM model checker to implement the proposed model checking approach. Finally, we demonstrate the effectiveness of our approach by presenting a real case study. This framework can be considered as a step forward towards closing the gap of capturing interactions between knowledge and social commitments in stochastic agent-based systems.