节点文献
μ-演算嵌套不动点表达式分块计算算法
Blocked Calculation Algorithm with Nesting Fixed-point Expression for μ-calculus
【摘要】 利用叠代计算μ-演算公式时的单调特性,提出了一个分块计算嵌套μ-演算公式的全局算法,算法时间复杂度为O(nd/2),空间复杂度为O(d×n)。由于算法的空间复杂度低,使得不动点算子嵌套深度很大的μ-演算公式的求解成为可能,这在模型检测方面有着非常重要的意义。
【Abstract】 This paper puts forward a blocked calculation algorithm for the nesting μ-calculus formula by using the monotonicity of the iterate calculation of the μ-calculus formula,whose time complexity is O ( n d/2) and space complexity is O ( d×n). For the lower space complexity of the algorithm,it is possible to solve the μ-calculus formula whose fixed-point operator is deep nesting,which is significant in the model checking.
【关键词】 模型检测；
μ-演算；
计算复杂度；
NP∩co-NP问题；
【Key words】 model checking； μ-calculus； calculation complexity； NP ∩ co-NP problem；
【Key words】 model checking； μ-calculus； calculation complexity； NP ∩ co-NP problem；
【基金】 贵州省科学基金资助项目(GGY2004002)
- 【文献出处】 计算机工程 ,Computer Engineering , 编辑部邮箱 ,2008年02期
- 【分类号】TP301.6
- 【被引频次】2
- 【下载频次】101