The μ-Calculus Model-Checking Algorithm for Generalized Possibilistic Decision Process

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 mu-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 mu-calculus is improved and extended, and the concept of generalized possibilistic mu-calculus (GPo(mu)) is given to describe the attribute characteristics of nondeterministic systems. Then, the GPo(mu) 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 mu-calculus, the generalized possibilistic mu-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.