具有DP的广义可能性模糊时态CTL模型检测

摘要

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