计算机科学与探索 ›› 2017, Vol. 11 ›› Issue (10): 1681-1688.DOI: 10.3778/j.issn.1673-9418.1607030
李 丹,李永明+
LI Dan, LI Yongming+
摘要: 广义可能性计算树逻辑(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公式[α-]等价的定义,并得出了一些更一般的结果。