【摘要】 利用叠代计算μ-演算公式时的单调特性,提出了一个分块计算嵌套μ-演算公式的全局算法,算法时间复杂度为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.更多还原