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

计算机工程与科学

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

袁红娟1,2,马艳芳3,潘海玉1,2

（1.泰州学院计算机科学与技术学院，江苏泰州 225300;2.桂林电子科技大学广西可信软件重点实验室，广西桂林 541004;

3.淮北师范大学计算机科学与技术学院，安徽淮北 235000）

收稿日期:2017-07-01 修回日期:2017-09-05 出版日期:2017-12-25 发布日期:2017-12-25
基金资助:
国家自然科学基金(61672023，61673352)；安徽省自然科学基金(1708085MF159)；江苏高校“青蓝工程”；广西可信软件重点实验室研究课题(kx201609)；泰州市科技支撑社会发展计划(TS2015040)

Model checking for fuzzy alternating-time temporal logic

YUAN Hong-juan1,2 ,MA Yan-fang3,PAN Hai-yu1,2

（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）

Received:2017-07-01 Revised:2017-09-05 Online:2017-12-25 Published:2017-12-25

摘要/Abstract

摘要：

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

关键词:

交互时态逻辑, 计算树逻辑, 并发博弈结构, 模型检测, 模糊逻辑

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

袁红娟1,2,马艳芳3,潘海玉1,2. 模糊交互时态逻辑的模型检测[J]. 计算机工程与科学.

YUAN Hong-juan1,2,MA Yan-fang3,PAN Hai-yu1,2. Model checking for fuzzy alternating-time temporal logic[J]. Computer Engineering & Science.

[1]	余昊昊, 唐滨. 基于FastCAE的Geant4集成关键技术研究[J]. 计算机工程与科学, 2025, 47(02): 210-218.
[2]	雷志超, 蒋嘉俊, 马驰卓, 周文静, 王楚正. 基于邻域关系感知图神经网络的DDI预测[J]. 计算机工程与科学, 2024, 46(05): 907-915.
[3]	刘子源, 马占有, 李霞, 高滢囡, 何娜娜, 黄瑞祺. 基于模糊测度的模糊分支时态逻辑模型检测[J]. 计算机工程与科学, 2024, 46(04): 676-683.
[4]	范韫. 基于EMD距离的稀疏自编码器[J]. 计算机工程与科学, 2022, 44(05): 894-900.
[5]	张志远, 陈海进. 基于动态矩阵的未知环境地图构建与路径规划[J]. 计算机工程与科学, 2022, 44(03): 563-570.
[6]	李召恺, 马占有, 李健祥, 郭昊. 基于模糊决策过程的模糊计算树逻辑模型检测[J]. 计算机工程与科学, 2022, 44(02): 266-275.
[7]	冯琪堯, 张惊雷, . 基于混合注意力机制的目标跟踪算法[J]. 计算机工程与科学, 2022, 44(02): 276-282.
[8]	张鑫, 冯秀芳. WiFi环境下基于CGRU-ELM混合模型的手势识别[J]. 计算机工程与科学, 2022, 44(02): 298-305.
[9]	万本庭, 方地长. 区间值广义正交模糊Frank算子及群决策方法[J]. 计算机工程与科学, 2022, 44(02): 345-354.
[10]	耿召里, 李目, 曹淑睿, 刘昶忻. 基于混合反向学习策略的鲸鱼优化算法[J]. 计算机工程与科学, 2022, 44(02): 355-363.
[11]	沈郭鑫, 蒋中云. 基于密度和中心指标的Canopy二分K-均值算法优化[J]. 计算机工程与科学, 2022, 44(02): 372-380.
[12]	崔振礼, 罗宇. 一种嵌入式双操作系统架构中外设资源动态迁移的研究与实现[J]. 计算机工程与科学, 2022, 44(01): 9-15.
[13]	侯兴旺, 赵若宇, 张玉书. 一种精确缩略图保持的图像加密方案[J]. 计算机工程与科学, 2022, 44(01): 60-67.
[14]	张晶, 李煜, . 改进的无约束优化3D-DV-Hop定位算法[J]. 计算机工程与科学, 2022, 44(01): 75-83.
[15]	火元莲, 徐晓鹏, 郑海亮. 基于无线能量采集的多跳网络安全传输中的路径选择[J]. 计算机工程与科学, 2021, 43(12): 2150-2156.