@conference {12799,
	title = {Efficient model checking via the equational μ-calculus},
	booktitle = {, Eleventh Annual IEEE Symposium on Logic in Computer Science, 1996. LICS {\textquoteright}96. Proceedings},
	year = {1996},
	month = {1996/07/27/30},
	pages = {304 - 312},
	publisher = {IEEE},
	organization = {IEEE},
	abstract = {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*},
	keywords = {Automata, BDD-based algorithms, Boolean functions, Calculus, compositional model-checking approaches, computational complexity, Computer science, CTL*, Data structures, Encoding, equational variant, equational μ-calculus, Equations, expressive temporal logic, Logic, Maintenance, modal μ-calculus, Model checking, on-the-fly procedures, Surges, temporal logic, temporal logic model checking, unified framework},
	isbn = {0-8186-7463-6},
	doi = {10.1109/LICS.1996.561358},
	author = {Bhat,G. and Cleaveland, Rance}
}
