计算机工程与应用 ›› 2017, Vol. 53 ›› Issue (9): 51-56.DOI: 10.3778/j.issn.1002-8331.1511-0249

• 理论与研发 • 上一篇    下一篇

命题μ-演算局部模型检测高效算法设计

李前利,江  华   

  1. 闽南师范大学 粒计算重点实验室,福建 漳州 363000
  • 出版日期:2017-05-01 发布日期:2017-05-15

Local model checking algorithm for evaluation of propositional μ-calculus

LI Qianli, JIANG Hua   

  1. Key Lab of Granular Computing, Minnan Normal University, Zhangzhou, Fujian 363000, China
  • Online:2017-05-01 Published:2017-05-15

摘要: 命题μ-演算局部模型检测算法中,目前最好的算法的时间复杂度与不动点算子交替嵌套深度[d]呈指数关系。针对命题μ-演算局部模型检测算法的计算过程进行分析,得到迭代计算的中间迭代值间满足的一组偏序关系,然后利用该偏序关系设计了一个局部模型检测算法,算法时间复杂度的指数部分为[d2],大大提高了算法的计算效率。

关键词: &mu, -演算, 局部模型检测, 不动点, 偏序关系

Abstract: In this paper, the computing process of fixpoint alternant iteration of local model checking for propositional [μ]-calculus is analyzed and a set of partial order relation about intermediate values of iterative calculation is proven. Then a local model checking algorithm is designed by the partial order relation. At present, the index of time complexity of existing local model checking algorithm is [d]([d] is the alternation depth of the formula). The index of time complexity is reduced from [d] to [d2]. The computational efficiency of the algorithm is improved greatly.