Quantitative Computation Tree Logic Model Checking Based on Generalized Possibility Measures

We study generalized possibilistic computation tree logic (GPoCTL) model checking in this paper, which is an extension of possibilistic computation logic model checking introduced by Li et al. (2014). The system is modeled by generalized possibilistic Kripke structures, and the verifying property is specified by a GPoCTL formula. Based on generalized possibility measures and generalized necessity measures, the method of GPoCTL model checking is discussed, and the corresponding algorithm and its complexity are shown in detail. Furthermore, the comparison between possibilistic computation tree logic and GPoCTL is given. Finally, a thermostat example is given to illustrate the GPoCTL model-checking method.