An Improved Algorithm for 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). For this reason, fixpoint calculi such as those proposed by Kozen and Park have proved useful, both as ways to describe verification algorithms and as specification formalisms in their own right. We consider the problem of evaluating expressions in these calculi over a given model. A naive algorithm for this task may require time nq, 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 nd steps, where d is the number of alternations between least and greatest fixpoints. More recent algorithms have succeeded in reducing 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.