基于偏序规律的μ-演算一阶谓词界程逻辑模型检测

• 作者: 江华
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 模型检测 移动界程 μ-演算 嵌套谓词等式系
• 年，卷（期）: 2016,（12）
• 所属期刊栏目: 量子计算、计算机理论与算法
• 页码范围: 2547-2561
• 页数: 15页
• 分类号: TP316
• 字数: 9685字
• 语种: 中文
• DOI: 10.11897/SP.J.1016.2016.02547

摘要

基于μ-演算的一阶谓词界程逻辑,用谓词变量构造不动点公式,方便描述闭环系统的性质,公式语义简洁.该逻辑在有限控制移动界程上的模型检测目前性能最好的算法的时间复杂度与公式中不动点算子交错嵌套深度d呈指数关系,空间复杂度与d呈线性关系.文中设计了一个基于μ-演算的一阶谓词界程逻辑在有限控制移动界程上的模型检测高效算法,这也是目前已知的第3个同类算法,算法的时间复杂度与d/2+1呈指数关系,空间复杂度与d呈线性关系.文中所做的工作有:(1)找到了基于μ-演算的一阶谓词界程逻辑模型检测计算过程中的中间结果满足的两组偏序关系;(2)利用找到的偏序关系设计了一个快速模型检测算法;(3)分析了算法的复杂度.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	江华	闽南师范大学粒计算重点实验室	19	55	4.0	6.0