TY - CONF
T1 - Efficient model checking via the equational μ-calculus
T2 - , Eleventh Annual IEEE Symposium on Logic in Computer Science, 1996. LICS '96. Proceedings
Y1 - 1996
A1 - Bhat,G.
A1 - Cleaveland, Rance
KW - Automata
KW - BDD-based algorithms
KW - Boolean functions
KW - Calculus
KW - compositional model-checking approaches
KW - computational complexity
KW - Computer science
KW - CTL*
KW - Data structures
KW - Encoding
KW - equational variant
KW - equational μ-calculus
KW - Equations
KW - expressive temporal logic
KW - Logic
KW - Maintenance
KW - modal μ-calculus
KW - Model checking
KW - on-the-fly procedures
KW - Surges
KW - temporal logic
KW - temporal logic model checking
KW - unified framework
AB - 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*
JA - , Eleventh Annual IEEE Symposium on Logic in Computer Science, 1996. LICS '96. Proceedings
PB - IEEE
SN - 0-8186-7463-6
M3 - 10.1109/LICS.1996.561358
ER -