模糊交互时态逻辑的模型检测

摘要：

交互时态逻辑已被广泛应用于开放系统的规范描述,交互时态逻辑的模型检测技术是一个比较重要的验证方法.为了形式化描述和验证具有模糊不确定性信息的开放系统的性质,提出了一种模糊交互时态逻辑,并讨论了它的模型检测问题.首先,引入了模糊交互时态逻辑的基于路径和基于不动点的两种语义,证明了其等价性.然后,基于其等价性,给出了模糊交互时态逻辑的模型检测算法和复杂性分析.

关键词：交互时态逻辑、计算树逻辑、并发博弈结构、模型检测、模糊逻辑

所属期刊栏目：39

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

资助基金：国家自然科学基金61672023,61673352;安徽省自然科学基金1708085MF159;江苏高校“青蓝工程”;广西可信软件重点实验室研究课题kx201609;泰州市科技支撑社会发展计划TS2015040

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

页数：共7页

页码：2290-2296