Another Look at LTL Model Checking
Abstract
We show how LTL model checking can be reduced to CTL model checking with fairness constraints. Using this reduction, we also describe how to construct a symbolic LTL model checker that appears to be quite efficient in practice. In particular, we show how the SMV model checking system developed by McMillan 16 can be extended to permit LTL specifications. The results that we have obtained are quite surprising. For the examples we considered, the LTL model checker required at most twice as much time and space as the CTL model checker. Although additional examples still need to be tried, it appears that efficient LTL model checking is possible when the specifications are not excessively complicated.
Document Details
- Document Type
- Technical Report
- Publication Date
- Feb 01, 1993
- Accession Number
- ADA277568
Entities
People
- E. Clarke
- K. Hamaguchi
- O. Grumberg
Organizations
- Carnegie Mellon University