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

摘要

广义可能性计算树逻辑(generalized possibilistic computation tree logic,GPoCTL)在不确定性模型检测中扮演着非常重要的角色,但其表达能力还尚未研究全面.为此,讨论了GPoCTL与计算树逻辑(computa-tion tree logic,CTL)表达能力之间的关系.首先定义了区间广义可能性计算树逻辑(interval generalized pos-sibilistic computation tree logic,IGPoCTL),并给出了IGPoCTL公式和CTL公式等价的定义.然后证明了CTL是IGPoCTL的一个真子类,因为IGPoCTL是GPoCTL的一种简单分明化形式,则CTL可看作GPoCTL的一个真子类.此外,还给出了IGPoCTL公式和CTL公式α-等价的定义,并得出了一些更一般的结果.%Generalized possibilistic computation tree logic (GPoCTL) plays an important role in model checking with uncertainty, there is still further research in its expressiveness. In order to study the expressiveness of GPoCTL, this paper discusses the relationship between GPoCTL and computation tree logic (CTL) with respect to their expres-siveness. Firstly, this paper defines interval generalized possibilistic computation tree logic (IGPoCTL), and gives the definition of the equivalence between IGPoCTL formulae and CTL formulae, and proves that CTL is a proper subclass of IGPoCTL. Because IGPoCTL is obviously a simple crispness of GPoCTL, CTL can be regarded as a proper subclass of GPoCTL. Besides, this paper gives the definition of α-equivalence between IGPoCTL formulae and CTL formulae and gets some more general results.