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

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 (PCTL^kc 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 PCTL^kc and report the obtained verification results. Our proposed model checking technique is reduction-based and consists in transforming the problem of model checking PCTL^kc 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.