广义可能性计算树逻辑和计算树逻辑的关系

来源：计算机科学与探索杂志2017年第10期北京时间：

作者：李丹，李永明

单位：陕西师范大学 计算机科学学院，西安 710119

摘要：广义可能性计算树逻辑（generalized possibilistic computation tree logic，GPoCTL）在不确定性模型检测中扮演着非常重要的角色，但其表达能力还尚未研究全面。为此，讨论了GPoCTL与计算树逻辑（computation tree logic，CTL）表达能力之间的关系。首先定义了区间广义可能性计算树逻辑（interval generalized possibilistic computation tree logic，IGPoCTL），并给出了IGPoCTL公式和CTL公式等价的定义。然后证明了CTL是IGPoCTL的一个真子类，因为IGPoCTL是GPoCTL的一种简单分明化形式，则CTL可看作GPoCTL的一个真子类。此外，还给出了IGPoCTL公式和CTL公式[α-]等价的定义，并得出了一些更一般的结果。

关键词：计算树逻辑,广义可能性计算树逻辑,区间广义可能性计算树逻辑,表达能力