AN IMPROVED ALGORITHM FOR THE EVALUATION OF FIXPOINT EXPRESSIONS

Many automated finite-state verification procedures can be viewed as f ixpoint computations over a finite lattice (typically the powerset of the set of system states). For this reason, fixpoint calculi such as t hose proposed by Kozen and Park have proved useful, both as ways to de scribe verification algorithms and as specification formalisms in thei r own right. We consider the problem of evaluating expressions in thes e calculi over a given model. A naive algorithm for this task may requ ire 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 pres ented a method requiring about n(d) steps, where d is the number of al ternations between least and greatest fixpoints. More recent algorithm s have succeeded in reducing the exponent by one or two, but the compl exity has remained at about n(d). In this paper, we present a new algo rithm that makes extensive use of monotonicity considerations to solve the problem in about n(d/2) steps.