Model checking agent-based communities against uncertain group commitments and knowledge. (1st September 2021)

• Record Type: Journal Article
• Authors: Sultan, Khalid; Bentahar, Jamal; Yahyaoui, Hamdi; Mizouni, Rabeb
• Is Part Of: Expert systems with applications. Volume 177(2021)
• Publication Date: 2021-09-01
• Subjects: Multi-agent systems -- Probabilistic model checking -- Verification -- Social commitments -- Knowledge; Expert systems (Computer science) -- Periodicals; Systèmes experts (Informatique) -- Périodiques; Electronic journals; 006.33
• DOI: 10.1016/j.eswa.2021.114792
• Languages: English
• ISSNs: 0957-4174

Abstract

Highlights: We propose a new probabilistic verification approach for agent-based systems. We consider the interaction between group commitments and knowledge. We transform model checking our extended commitment logic to model checking PCTL. We prove the soundness and completeness of the approach and analyze its complexity. We use PRISM to implement and evaluate our technique on two concrete case studies. Abstract: 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 ( PCTL kc + ). In the proposed approach, model checking PCTL kc + is reduced to model checking the probabilistic branching-time logic PCTL. This is achieved by transforming PCTL kc + model to a Markov Decision Process (MDP), and reducing PCTL kc + 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.