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

作者：江华

来源：计算机学报, 2016, (12): 2547-2561.

• 模型检测
• 移动界程
• μ-演算
• 嵌套谓词等式系 model checking
• mobile ambient
• μ-calculus
• nested predicate equations

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

• 单位
  韶关学院; 闽南师范大学