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

被引：0
作者：
Jiang H. [1 ,2 ]
机构：
[1] Key Laboratory of Granular Computing, Minnan Normal University, Zhangzhou, 363000, Fujian
[2] School of Information Science and Engineering, Shaoguan University, Shaoguan, 512005, Guangdong
来源：
Jisuanji Xuebao/Chinese Journal of Computers | 2016年 / 39卷 / 12期
基金：
中国国家自然科学基金;
关键词：
Mobile ambient; Model checking; Nested predicate equations; μ-calculus;
D O I：
10.11897/SP.J.1016.2016.02547
中图分类号：
学科分类号：
摘要：
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.
引用
收藏
页码：2547 / 2561
页数：14
相关论文
共 31 条
  • [1] Cardelli L., Gordon A.D., Mobile ambients, Theoretical Computer Science, 240, 1, pp. 177-213, (2000)
  • [2] Cardelli L., Gordon A.D., Anytime, anywhere: Modal logics for mobile ambients, Proceedings of the POPL'2000, pp. 365-377, (2000)
  • [3] Cardelli L., Gordon A.D., Logical properties of name restriction, Proceedings of the 5th International Conference on Typed Lambda, Calculi and Applications, pp. 46-60, (2001)
  • [4] Cardelli L., Ghelli G., A query language based on the ambient logic, Proceedings of the 2001 European Symposium on Programming, pp. 1-22, (2001)
  • [5] Lin H.-M., Space logic of mobile ambients, Science in China Series E: Technological Sciences, 34, 2, pp. 139-150, (2004)
  • [6] Lin H.M., A predicate mu-calculus for mobile ambients, Journal of Computer Science and Technology, 20, 1, pp. 95-104, (2005)
  • [7] Charatonik W., Talbot J.M., The decidability of model checking mobile ambients, Proceedings of the 15th Annual Conference of European Association for Computer Science Logic, pp. 339-354, (2001)
  • [8] Charatonik W., Dal Zilio S., Gordon A.D., Et al., The complexity of model checking mobile ambients, Proceedings of the 4th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2001), pp. 152-167, (2001)
  • [9] Charatonik W., Gordon A., Talbot J.M., Finite-control mobile ambients, Proceedings of the ESOP 2002: the 11th European Symposium on Programming, pp. 295-313, (2002)
  • [10] Jiang H., Li X., Model checking for mobile ambients, Journal of Computer Research and Development, 46, 10, pp. 1750-1757, (2009)
1234