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

摘要：

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

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

所属期刊栏目：13

分类号：TP301.2(计算技术、计算机技术)

资助基金：The National Natural Science Foundation of China under Grant No.11671244

在线出版日期：2019-11-05（万方平台首次上网日期，不代表论文的发表时间）

页数：共12页

页码：1781-1792