Model checking is particularly well-suited for the automated verification of finite-state systems, both for software and for hardware. It was first put forward by Clark, Emerson, Quielle and Sifakis in 1981. Verify the desired properties with the method of exhaustive search of the state space, which is model checking’s basic idea. The general steps of model checking is:(1) to give a abstract model of the current system; (2) to introduce the according logic to describe the system’s properties; (3) to validate the properties by the means of model checking algorithms. If the model behaves as it was designed to behave, then return true, else return false and provide us with a counterexample at the same time.The basic model of model checking is transition system in classical circum-stance. As computer softwares and hardwares become more and more complicated, there usually exists much uncertain information between transition states. Many quantitative extensions of the transition system have been proposed for this purpose, such as models that embed state changes into time, models that assign probabil-ities, possibilities, truth-value or statistical values. Zadeh proposed the theory of fuzzy sets in 1965, which pay attention to the non-additive case. Possibility mea-sure is a common kind of non-additive measure. Professor Li proposed extended model checking theory based on possibilistic theorey, which combined possibili-ty measures with model checking. Although possibilistic computation tree logic is more expressive than computation tree logic, it is restrictive. Some uncertain-ties, which can be described through possibility theory, still could not be handled directly using possibilistic computation tree logic model checking. To deal with uncertainties in possibility theory, more powerful quantitative model checking is needed. Hence, Professor Li introduced the extended model——generalized pos-sibilistic Kripke structure and established the theory of model checking based on generalized possibility measures.The main contributation of this paper is:1. Firstly, we give the syntaxes and semantics of generalized possibilistic com-putation tree logic’s expansion(GPoCTL*), generalized possibilistic computation tree logic’s reduction (GPoCTL-) and generalized possibilistic reward computa-tion tree logic (GPoRCTL) in terms of the generalized possibility measures. Based on the classical bisimulation and generalized possibility measures. We define the possibilistic bisimulation and discuss some relative properties.2. The equivalence relations among GPoCTL, GPoCTL*, GPoCTL- and bisi-miliar states are proved. That is to say, the logical characterizations of possibilistic bisimulation based on generalized possibility measures is presented.3. Quantative computation tree logic model checking based on generalized pos-sibility measures has been studied, fixed-point semantics of generalized possibilistic computation tree logic is presented in this paper to refine model checking algo-rithms, which is different from the fixed point semantics of calssical computation tree logic. |