Model checking generalized possibilistic computation tree logic based on decision processes
Zhanyou Ma, Yongming Li · Scientia Sinica Informationis · 2016
We study model-checking generalized possibilistic computation tree logic (GPoCTL) and its application in system verification, in particular, nondeterministic systems. Firstly, we introduce generalized possibilistic decision-making processes (GPDP) as system models and GPoCTL formulae under GPDP to describe the properties of the system. Then, we provide a model-checking algorithm for GPoCTL. The main advantage of the algorithm is that it can use scheduling in the decision making processes to convert the model-checking problem into operations of the fuzzy matrix or fixed point of fuzzy matrix functions, which need polynomial time. Finally, an example is given to illustrate the application of the model-checking generalized possibilistic computation tree logic in verification of a nondeterministic system.