μ-演算嵌套不动点表达式分块计算算法  

Blocked Calculation Algorithm with Nesting Fixed-point Expression for μ-calculus

作　　者：江华[1] 谭新星[2] 李祥[1] 

机构地区：[1]贵州大学计算机理论与软件研究所,贵阳550025 [2]广东韶关学院计算机系,韶关512005

出　　处：《计算机工程》2008年第2期4-7,共4页Computer Engineering

基　　金：贵州省科学基金资助项目(GGY2004002)

摘　　要：利用叠代计算μ-演算公式时的单调特性,提出了一个分块计算嵌套μ-演算公式的全局算法,算法时间复杂度为O(nd/2),空间复杂度为O(d×n)。由于算法的空间复杂度低,使得不动点算子嵌套深度很大的μ-演算公式的求解成为可能,这在模型检测方面有着非常重要的意义。This paper puts forward a blocked calculation algorithm for the nesting μ-calculus formula by using the monotonicity of the iterate calculation of the p-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问题 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]