Paper: Efficient model checking via the equational /spl mu/-calculus (at LICS 1996)
Authors: Girish Bhat Rance CleavelandAbstract
This paper studies the use of an equational variant of the modal /spl mu/-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 /spl mu/-calculus. Using this translation, one may then employ /spl mu/-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*.
BibTeX
@InProceedings{BhatCleaveland-Efficientmodelcheck, author = {Girish Bhat and Rance Cleaveland}, title = {Efficient model checking via the equational /spl mu/-calculus}, booktitle = {Proceedings of the Eleventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1996}, year = 1996, editor = {Edmund M. Clarke}, month = {July}, pages = {304-312}, location = {New Brunswick, NJ, USA}, publisher = {IEEE Computer Society Press} }