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

摘要： 计算树逻辑（computation tree logic，CTL）的范式在模型检测方法中具有重要意义，但基于广义可能性测度的计算树逻辑的范式尚未有系统研究。为了进一步完善广义可能性计算树（generalized possibilistic computation tree logic，GPoCTL）理论，在现有的广义可能性计算树逻辑理论的基础上，参考经典计算树逻辑的范式，给出了广义可能性计算树逻辑的两种不同的范式——正态范式（positive normal form，PNF）和存在范式（existential normal form，ENF），及其对应的语构和语义解释。最后利用归纳假设法证明了任意的广义可能性计算树逻辑公式都有与之等价的PNF公式和ENF公式。

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