Partial-order Algorithm of Model Checking in μ-Predicate Ambient Logic

Hua Jiang ； Rong-De Lin ； Fu-Min Zou ； Ling-Xiang Li

《電腦學刊》 29卷5期 (2018/10) Pp. 142-159

https://doi.org/10.3966/199115992018102905012

摘要

This paper introduces a kind of partial-order algorithm of model-checking in finitecontrol mobile ambients against μ-predicate ambient logic (Ambient logic based on first-order μ- calculus). Based on Tarski's fixpoint theorem, nested predicate equations and Block Dependency Graph, a group of partial ordering relation between inter-mediate results in the process of model checking is given, and thus a kind of local model-checking algorithm is proposed. To our knowledge, this is the first algorithm which exponent of time complexity is d/2+2, the exponent of space complexity is d/2 (d is the alternate nesting depth of fixpoint operator in the formula) and this is the third model-checking algorithm for predicate ambient logic with recursion. This paper's contributions are: (1) getting a group of partial ordering relation between intermediate results in the computing process of model checking for μ- calculus first-order predicate ambient logic based on Tarski's fixpoint theorem; (2) using the partial ordering relation to design an algorithm for model checking in mobile ambients; (3) analyzing the complexity of the algorithm.

關鍵字

algorithms and complexity ； mobile ambient ； model checking ； predicate ambient logic