Zhanyou Ma

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.

Model checking is an automated formal verification method to verify whether epistemic multi-agent systems adhere to property specifications. Although there is an extensive literature on qualitative properties such as safety and liveness, there is still a lack of quantitative and uncertain property verifications for these systems. In uncertain environments, agents must make judicious decisions based on subjective epistemic. To verify epistemic and measurable properties in multi-agent systems, this paper extends fuzzy computation tree logic by introducing epistemic modalities and proposing a new Fuzzy Computation Tree Logic of Knowledge (FCTLK). We represent fuzzy multi-agent systems as distributed knowledge bases with fuzzy epistemic interpreted systems. In addition, we provide a transformation algorithm from fuzzy epistemic interpreted systems to fuzzy Kripke structures, as well as transformation rules from FCTLK formulas to Fuzzy Computation Tree Logic (FCTL) formulas. Accordingly, we transform the FCTLK model checking problem into the FCTL model checking. This enables the verification of FCTLK formulas by using the fuzzy model checking algorithm of FCTL without additional computational overheads. Finally, we present correctness proofs and complexity analyses of the proposed algorithms. Additionally, we further illustrate the practical application of our approach through an example of a train control system.

The verification of reachability properties of fuzzy systems is usually based on the fuzzy Kripke structure or possibilistic Kripke structure. However, fuzzy Kripke structure or possibilistic Kripke structure is not enough to describe nondeterministic and concurrent fuzzy systems in real life. In this paper, firstly, we propose the generalized possibilistic decision process as the model of nondeterministic and concurrent fuzzy systems, and deduce the possibilities of sets of paths of the generalized possibilistic decision process relying on defining of schedulers. Then, we give fuzzy matrices calculation methods of the maximal possibilities and the minimal possibilities of eventual reachability, always reachability, constrained reachability, repeated reachability and persistent reachability. Finally, we propose a model checking approach to convert the verification of safety property into the analysis of reachabilities.

In this paper, we focus on the symmetrical relationship between multi-properties objective reachability problems and multi-objective sets reachability problems over FKS based on Zadeh logic. First, we give the formal definitions of those two problems. Then, we study their relationships and find that a multi-properties objective reachability problem and a special case of multi-objective sets reachability problems have symmetry. Finally, we give a polynomial time algorithm based on this symmetry to convert a multi-properties objective reachability problem to a multi-objective sets reachability problem. In addition, an illustrative example is listed to express some possible application methods based on our work.

In order to solve the problems in fuzzy computation tree logic model checking with cost operator, we propose a fuzzy decision process computation tree logic model checking method with cost. Firstly, we introduce a fuzzy decision process model with cost, which can not only describe the uncertain choice and transition possibility of systems, but also quantitatively describe the cost of the systems. Secondly, under the model of the fuzzy decision process with cost, we give the syntax and semantics of the fuzzy computation tree logic with cost operators. Thirdly, we study the problem of computation tree logic model checking for fuzzy decision process with cost, and give its matrix calculation method and algorithm. We use the example of medical expert systems to illustrate the method and model checking algorithm.

Model checking is a formal automatic verification technology for complex concurrent systems. It is used widely in the verification and analysis of computer software and hardware systems, communication protocols, security protocols, etc. The generalized possibilistic μ-calculus model-checking algorithm for decision processes is studied to solve the formal verification problem of concurrent systems with nondeterministic information and incomplete information on the basis of possibility theory. Firstly, the generalized possibilistic decision process is introduced as the system model. Then, the classical proposition μ-calculus is improved and extended, and the concept of generalized possibilistic μ-calculus (GPo_μ) is given to describe the attribute characteristics of nondeterministic systems. Then, the GPo_μ model-checking algorithm is proposed, and the model-checking problem is simplified to fuzzy matrix operations. Finally, a specific example and a case study are analyzed and verified. Compared with the classical μ-calculus, the generalized possibilistic μ-calculus has a stronger expressive power and can better characterize the attributes of nondeterministic systems. The model-checking algorithm can give the possibility that the system satisfies the attributes. The research work provides a new idea and method for model checking nondeterministic systems.