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 and space complexity is . 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.

Key words: model checking, μ-calculus, calculation complexity, NP co-NP problem

摘要： 利用叠代计算μ-演算公式时的单调特性，提出了一个分块计算嵌套μ-演算公式的全局算法，算法时间复杂度为 ，空间复杂度为 。由于算法的空间复杂度低，使得不动点算子嵌套深度很大的μ-演算公式的求解成为可能，这在模型检测方面有着非常重要的意义。

关键词: 模型检测, μ-演算, 计算复杂度, NP co-NP问题

CLC Number: 

• TP311