%0 Conference Paper %B , Eleventh Annual IEEE Symposium on Logic in Computer Science, 1996. LICS '96. Proceedings %D 1996 %T Efficient model checking via the equational μ-calculus %A Bhat,G. %A Cleaveland, Rance %K Automata %K BDD-based algorithms %K Boolean functions %K Calculus %K compositional model-checking approaches %K computational complexity %K Computer science %K CTL* %K Data structures %K Encoding %K equational variant %K equational μ-calculus %K Equations %K expressive temporal logic %K Logic %K Maintenance %K modal μ-calculus %K Model checking %K on-the-fly procedures %K Surges %K temporal logic %K temporal logic model checking %K unified framework %X 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* %B , Eleventh Annual IEEE Symposium on Logic in Computer Science, 1996. LICS '96. Proceedings %I IEEE %P 304 - 312 %8 1996/07/27/30 %@ 0-8186-7463-6 %G eng %R 10.1109/LICS.1996.561358