关键词: 广义可能性测度, 计算树逻辑, 范式, 模型检测

Abstract: Normal form of computation tree logic (CTL) plays an important role in model checking. But the normal forms of computation tree logic based on generalized possibilistic measure have not been researched systematically. For improving the generalized possibilistic computation tree logic (GPoCTL) theory, according to existing generalized possibilistic computation tree logic theory and normal forms of classical computation tree logic, this paper defines two normal forms—positive normal form (PNF) and existential normal form (ENF) based on generalized possibilistic computation tree logic, and gives the corresponding language structure and semantic interpretation. Finally, using inductive method, this paper proves that any GPoCTL formula can write into a normal form in PNF or ENF respectively.

Key words: generalized possibility measure, computation tree logic, normal form, model checking