Based on the function monotonicity in the μ-calculus formula, this paper presents a global model-checking algorithm for calculating the alternating nesting μ-calculus formula, whose time complexity is O((2n+1){sup}([(d+3)/4]+[(d+2)/4]) and space complexity is O(dn). It is the first known algorithm whose space complexity is O(dn) and the exponent part of time complexity is d/2 for a global model-checking algorithm in the full μ-calculus formula at present.
展开▼
