Formal Verification of Trust in Multi-Agent Systems Under Generalized Possibility Theory

In multi-agent systems, the interactions between autonomous agents within dynamic and uncertain environments are crucial for achieving their objectives. Current research leverages model checking techniques to verify these interactions, with social accessibility relations commonly used to formalize agent interactions. In multi-agent systems that incorporate generalized possibility measures, the quantification, computation, and model checking of trust properties present significant challenges. This paper introduces an indirect model checking algorithm designed to transform social trust under uncertainty into quantifiable properties for verification. A Generalized Possibilistic Trust Interpreted System (GPTIS) is proposed to model and characterize multi-agent systems with trust-related uncertainties. Subsequently, the trust operators are extended based on Generalized Possibilistic Computation Tree Logic (GPoCTL) to develop the Generalized Possibilistic Trust Computation Tree Logic (GPTCTL), which is employed to express the trust properties of the system. Then, a model checking algorithm that maps trust accessibility relations to trust actions is introduced, thereby transforming the model checking of GPTCTL on GPTIS into model checking of GPoCTL on Generalized Possibility Kripke Structures (GPKSs). The proposed algorithm is provided with a correctness proof and complexity analysis, followed by an example demonstrating its practical feasibility.