计算机工程与科学2017，Vol.39Issue(12)：2290-2296,7.DOI:10.3969/j.issn.1007-130X.2017.12.018
模糊交互时态逻辑的模型检测
Model checking for fuzzy alternating-time temporal logic
摘要
Abstract
Alternating-time temporal logic has been widely used as the specification language of open systems,and its model checking is one of the most important verification methods for open systems.To describe and check the properties of the open systems with fuzzy uncertainty information,we propose fuzzy alternating-time temporal logic and discuss its model-checking problem.Firstly,we present two semantics,the path semantics and the fixed point semantics,which are equal in value.Based on the result,the model-checking algorithm is given and its time complexity is discussed.关键词
交互时态逻辑/计算树逻辑/并发博弈结构/模型检测/模糊逻辑Key words
alternating-time temporal logic/computation tree logic/concurrent game structure/model checking/fuzzy logic分类
信息技术与安全科学引用本文复制引用
袁红娟,马艳芳,潘海玉..模糊交互时态逻辑的模型检测[J].计算机工程与科学,2017,39(12):2290-2296,7.基金项目
国家自然科学基金(61672023,61673352) （61672023,61673352）
安徽省自然科学基金(1708085MF159) （1708085MF159）
江苏高校“青蓝工程” （）
广西可信软件重点实验室研究课题(kx201609) （kx201609）
泰州市科技支撑社会发展计划(TS2015040) （TS2015040）
