Quantitative µ-Calculus Model Checking Algorithm Based on Generalized Possibility Measures
Panqing Zhang, Jiulei Jiang, Zhanyou Ma, Heng Zhu · 2019
Model checking is an effective technique for automatically verifying the correctness of software and hardware systems. In order to formalize verification of nondeterministic systems, based on the possibility measure theory, lattice theory and fuzzy logic, we first introduce the generalized possibilistic Kripke structure as a system model, then we give the concept of generalized possibilistic μ-calculus language to describe the properties of the system, and then we propose the generalized possibilistic μ-calculus model checking algorithm. Finally, we give the concrete example to verify the correctness and feasibility of the model checking algorithm. The research results expand the application range of the generalized possibility measures in the model checking.