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

Abstract: 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 expressiveness. 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.

Key words: computation tree logic, generalized possibilistic computation tree logic, interval generalized possibilistic computation tree logic, expressiveness