Model checking agent-based communities against uncertain group commitments and knowledge

摘要

In recent years, the use of Multi-Agent Systems (MASs) to solve complex problems has grown rapidly. Social communicative commitments have been widely employed in such systems as a means of communication allowing heterogeneous agents to cooperate. However, to prevent undesirable outcomes, communicative commitments and their interactions with agents' knowledge need to be verified. This paper aims at verifying MASs where agents have knowledge and communicate through manipulating uncertain social commitments, especially when the scope of commitments moves beyond the common agent-to-agent scheme. We introduce a model checking method for verifying those systems and capitalize on the interaction between not only individual but also group communicative commitments and knowledge in the presence of uncertainty. System's properties are expressed using the Probabilistic Computation Tree Logic of Knowledge and Commitment (PCTLkc+). In the proposed approach, model checking PCTLkc+ is reduced to model checking the probabilistic branching-time logic PCTL. This is achieved by transforming PCTLkc+ model to a Markov Decision Process (MDP), and reducing PCTLkc+ formulae into PCTL formulae compatible with PRISM, a reference model checking tool for probabilistic temporal systems. Thereafter, we provide the soundness and completeness proofs of the reduction technique, and compute its time complexity. The effectiveness of the proposed approach is evaluated by implementing it on top of PRISM using two concrete applications, namely Online Shopping System from the business domain, and Insurance Claim Processing from the industrial domain. The obtained results of the two case studies underscore the scientific value of our proposed framework and confirm that verifying commitment-based probabilistic epistemic MASs has become attainable by utilizing this approach. The presented work outperforms existing proposals because it considers the problem of modeling and verifying MASs where group social commitments are interacting with participating agents' knowledge in the presence of uncertainty, which has not been addressed yet in the literature.