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

Model Checking of Generalized Possibilistic Fuzzy-Time CTL with DP

作　　者：魏杰林 袁申 李永明[1] 梁常建[2] WEI Jielin;YUAN Shen;LI Yongming;LIANG Changjian(College of Computer Science,Shaanxi Normal University,Xi’an 710119,China;College of Mathematics and Information Science,Shaanxi Normal University,Xi’an 710119,China)

机构地区：[1]陕西师范大学计算机科学学院,西安710119 [2]陕西师范大学数学与信息科学学院,西安710119

出　　处：《计算机科学与探索》2019年第10期1781-1792,共12页Journal of Frontiers of Computer Science and Technology

基　　金：国家自然科学基金~~

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

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

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]