## 1 Introduction  
The continuous enhancement of computer functions makes systems increasingly complex; for the purpose of the correctness of the systems, it usually spends more time on verification than on construction [1]. Formal methods are important methods to ensure the correctness and security of computer systems. They can integrate verification early in the design process and ensure the credibility of the system through strict logical reasoning and mathematical calculations. Model checking is a formal automatic verification technology that can provide a complete formal verification framework of system attributes [2]. The classical model-checking technology is mainly used for qualitative research on the system--that is, to verify if the system satisfies the system attributes described by temporal logic formulas, such as Computation Tree Logic (CTL), Linear Temporal Logic (LTL), and \(\upmu\)-calculus [3, 4]. If it is satisfied, the model checker returns \"True\"; otherwise, it returns \"False\" with specific counterexamples. However, in the design of actual systems, nondeterministic systems containing uncertain or inconsistent information are often encountered, so the qualitative research on the systems cannot meet the actual needs. In recent years, some scholarshave proposed quantitative extensions to classical model checking, such as models that embed features into probability [5; 6], possibility [7; 8; 9], and multi-valued [10; 11; 12], etc. Different model-checking approaches are applicable to different model types. [PERSON] et al. [13] proposed a model-checking algorithm based on the probabilistic labeled transition systems and \(\upmu\)-calculus to check whether the states in the finite probabilistic labeled transition systems satisfiy the logical formulas; [PERSON] et al. [14] extended the classical CTL and Kripke structure and proposed a multi-valued model checking algorithm. [PERSON] et al. [15] studied the multi-valued \(\upmu\)-calculus model checking problem based on multi-valued Kripke structures and reduced it into several classical model-checking problems. The advantage of the reduction method is that the verification can be done automatically using existing model-checking tools. [PERSON] et al. [16] defined a multi-valued \(\upmu\)-calculus and proposed a new model-checking logic framework to verify arbitrary properties of multi-valued \(\upmu\)-calculus, which is more widely used. Recently, [PERSON] et al. [17] combined fuzzy logic with CTL, proposed Fuzzy Computation Tree Logic (FCTL), which is a fuzzy extension of classical CTL, and discussed model-checking problems. [PERSON] et al. [18; 19; 20; 21] extended the classical LTL and CTL model-checking technology; they defined a quantitative model-checking verification method on the basis of possibility measures. Compared to probabilistic model checking, the possibilistic model checking does not need to satisfy countable additivity, and it is mainly used for the model checking of non-additive systems. Probabilistic model checking already has mature model-checking tools, such as PRISM PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour. It has been used to analyse systems from many different application domains, including communication and multimedia protocols, randomised distributed algorithms, security protocols, biological systems and many others [22], etc., while possibilistic model checking is still in the theoretical research. Possibilistic model checking uses the theory of possibility measure as the theoretical basis for system modeling, which is suitable for systems with uncertain information in possibility theory [7]. There is some research on quantitative model-checking verification methods on the basis of possibility measures. [PERSON] et al. proposed Generalized Possibilistic LTL (GPoLTL), which is an extension of LTL, and gave quantitative model checking methods of linear-time properties based on generalized possibility measures in [18].