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

Model Checking for First-Order Predicate Ambient Logic Based on μ-Calculus with Partial Orders

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

First-order predicate ambient logic based on μ-calculus uses predicate variable to construct fixpoint formula which is convenient to describe the properties of closed-loop system. The formula＇s semantics is brief. For the best model checking algorithm in finite control mobile ambient based on the logic, its time complexity has exponent relation to d and space complexity has linear relation to d, and d is the alternating nesting depth of the formula in fixpoint. This paper comes up with an efficient model checking algorithm for first-order predicate ambient logic in finite control mobile ambient based on μ-calculus, which is the third known kindred algorithm at present, whose time complexity has exponent relation to d/2 ＋ 1, space complexity has linear relation to d. This paper＇s contributions are. （1） getting two groups of partial ordering relation among intermediate results in the process of computing for first-order predicate ambient logic model checking based on μ-calculus; （2） using the partial ordering relation to design a quick algorithm for model checking; （3） analyzing the complexity of this algorithm.