An Improved Algorithm for the Evaluation of Alternating Fixpoint Expressions in the mu-Calculus

Based on the function monotonicity in the mu- calculus formula, this paper presents a global model-checking algorithm for calculating the alternating nesting mu - calculus formula, whose time complexity is 0((2n +1 )^{lfloor(d+3)I4rfloor +lfloor(d+2)/4rfloor}) 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 mu- calculus formula at present.