Efficient model checking via the equational μ-calculus

This paper studies the use of an equational variant of the modal μ-calculus as a unified framework for efficient temporal logic model checking. In particular we show how an expressive temporal logic, CTL*, may be efficiently translated into the μ-calculus. Using this translation, one may then employ μ-calculus model-checking techniques, including on-the-fly procedures, BDD-based algorithms and compositional model-checking approaches, to determine if systems satisfy formulas in CTL*