Model checking for first-order predicate ambient logic based on μ-calculus with partial orders

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. © 2016, Science Press. All right reserved.