
Article
LTL satisfiability checking
International Journal on Software Tools for Technology Transfer
(2010)
Abstract
We report here on an experimental investigation of LTL satisfiability checking via a reduction to model checking. By using large LTL formulas, we offer challenging model-checking benchmarks to both explicit and symbolic model checkers. For symbolic model checking, we use CadenceSMV, NuSMV, and SAL-SMC. For explicit model checking, we use SPIN as the search engine, and we test essentially all publicly available LTL translation tools. Our experiments result in two major findings. First, most LTL translation tools are research prototypes and cannot be considered industrial quality tools. Second, when it comes to LTL satisfiability checking, the symbolic approach is clearly superior to the explicit approach.
Keywords
- Linear temporal logic,
- LTL satisfiability,
- Model checking,
- LTL-to-automata,
- LTL translation,
- Sanity check,
- Benchmark
Disciplines
Publication Date
May, 2010
DOI
10.1007/s10009-010-0140-3
Publisher Statement
This article is published as Rozier, Kristin Y., and Moshe Y. Vardi. "LTL satisfiability checking." International Journal on Software Tools for Technology Transfer 12, no. 2 (2010): 123-137. The final publication is available at Springer via https://doi.org/10.1007/s10009-010-0140-3.
Works produced by employees of the U.S. Government as part of their official duties are not copyrighted within the U.S. The content of this document is not copyrighted.
Citation Information
Kristin Yvonne Rozier and Moshe Y. Vardi. "LTL satisfiability checking" International Journal on Software Tools for Technology Transfer Vol. 12 Iss. 2 (2010) p. 123 - 137 Available at: http://works.bepress.com/kristin-yvonne-rozier/4/