L. Tan, O. Sokolsky, and I. Lee. Department of Computer and Information Science, University of Pennsylvania.

Technical report MS-CIS-03-02

This paper presents a faster on-the-fly algorithm for full mu-calculus. The algorithm evaluates the fixpoints for a revised version of hierachical equation system. The procedure to evaluate components of equation systems are derived from LAFP while avoids the construction of dependence set. Our main result, SLP, shows in practice how ``counter'' and ``reverse list'' may be used to eliminate the extra cost in implementation. SLP is a linear-space algorithm and matches the best global linear-space algorithms. In practice, it shows the superior performance comparable to the on-the-fly algorithm designed for a special fragment of mu-calculus.