An improved algorithm for the evaluation of fixpoint expressions

Many automated finite-state verification procedures can be viewed as fixpoint computations over a finite lattice (typically the powerset of the set of system states). Hence, fixpoint calculi such as the propositional Μ-calculus have proven useful, both as ways to describe verification algorithms and as specification formalisms in their own right. We consider the problem of evaluating expressions in a fixpoint calculus over a given model. A naive algorithm for this task may require time n q , where n is the maximum length of a chain in the lattice and q is the depth of fixpoint nesting. In 1986, Emerson and Lei presented a method requiring about n d steps, where d is the number of alternations between least and greatest fixpoints. More recent algorithms have reduced the exponent by one or two, but the complexity has remained at about nd. In this paper, we present a new algorithm that makes extensive use of monotonicity considerations to solve the problem in about nd/2 steps. Thus, the time required by our method is only about the square root of the time required by the earlier algorithms.