| 模糊交互时态逻辑的模型检测 |
| |
| 引用本文： | 袁红娟,马艳芳,潘海玉.模糊交互时态逻辑的模型检测[J].计算机工程与科学,2017,39(12):2290-2296. |
| |
| 作者姓名： | 袁红娟 马艳芳 潘海玉 |
| |
| 作者单位： | （1.泰州学院计算机科学与技术学院，江苏 泰州 225300;2.桂林电子科技大学广西可信软件重点实验室，广西 桂林 541004;
3.淮北师范大学计算机科学与技术学院，安徽 淮北 235000） |
| |
| 基金项目： | 国家自然科学基金(61672023，61673352)；安徽省自然科学基金(1708085MF159)；江苏高校“青蓝工程”；广西可信软件重点实验室研究课题(kx201609)；泰州市科技支撑社会发展计划(TS2015040) |
| |
| 摘 要： | 交互时态逻辑已被广泛应用于开放系统的规范描述,交互时态逻辑的模型检测技术是一个比较重要的验证方法。为了形式化描述和验证具有模糊不确定性信息的开放系统的性质,提出了一种模糊交互时态逻辑,并讨论了它的模型检测问题。首先,引入了模糊交互时态逻辑的基于路径和基于不动点的两种语义,证明了其等价性。然后,基于其等价性,给出了模糊交互时态逻辑的模型检测算法和复杂性分析。
|
| 关 键 词： | 交互时态逻辑 计算树逻辑 并发博弈结构 模型检测 模糊逻辑 |
| 收稿时间： | 2017-07-01 |
| 修稿时间： | 2017-12-25 |
Model checking for fuzzy alternating-time temporal logic |
| |
| YUAN Hong-juan,MA Yan-fang,PAN Hai-yu.Model checking for fuzzy alternating-time temporal logic[J].Computer Engineering & Science,2017,39(12):2290-2296. |
| |
| Authors: | YUAN Hong-juan MA Yan-fang PAN Hai-yu |
| |
| Affiliation: | （1.College of Computer Science and Technology,Taizhou University,Taizhou 225300；
2.Guangxi Key Laboratory of Trusted Software,Guilin University of Electronic Technology,Guilin 541004；
3.College of Computer Science and Technology,Huaibei Normal University,Huaibei 235000,China） |
| |
| 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. |
| |
| Keywords: | alternating-time temporal logic computation tree logic concurrent game structure model checking fuzzy logic |
|
| 点击此处可从《计算机工程与科学》浏览原始摘要信息 |
|
点击此处可从《计算机工程与科学》下载全文 |
|
