Abstract: In order to enhance the expression ability of computation tree logic in time series, this paper studies model checking of generalized possibilistic fuzzy-time computation tree logic with decision process based on generalized possibilistic measures, decision process and computation tree logic. First, generalized possibilistic decision process is introduced as the system model; the fuzzy-time temporal operator is used to construct fuzzy-time computing tree logic and its semantics under generalized possibilistic measure are given. Then the new generalized possibilistic fuzzy-time computation tree logic is presented for describing system properties. Finally, in generalized possibilistic scheduling, the calculation methods of fuzzy-time temporal operators such as “soon, within, last, nearly” are discussed through fuzzy matrix operation, and the corresponding model checking algorithm is presented. It is proven that generalized possibilistic fuzzy-time computation tree logic is an extension of generalized possibilistic computation tree logic in fuzzy-time series and has stronger expression ability.

Key words: fuzzy-time temporal, decision process, generalized possibilistic measures, computation tree logic, model checking

摘要： 为了增强计算树逻辑在时序上的表达能力，以广义可能性测度、决策过程和计算树逻辑为基础，研究了具有决策过程的广义可能性模糊时态计算树逻辑的模型检测。首先采用广义可能性决策过程作为系统模型；然后引入模糊时态算子，构造了模糊时态计算树逻辑并给出其在广义可能性测度下的语义，得到新的广义可能性模糊时态计算树逻辑用来描述系统属性；最后在广义可能性调度下通过模糊矩阵运算讨论了“soon、within、last、nearly”等几类模糊时态连接词的具体计算方法，给出相应的模型检测算法。经验证明，广义可能性模糊时态计算树逻辑是广义可能性计算树逻辑在模糊时序上的扩充，具有更强的表达能力。

关键词: 模糊时态, 决策过程, 广义可能性测度, 计算树逻辑, 模型检测