LTL satisfiability checking |
| |
Authors: | Kristin Y Rozier Moshe Y Vardi |
| |
Affiliation: | 1. NASA Ames Research Center, Moffett Field, CA, 94035, USA 2. Rice University, Houston, TX, 77005, USA
|
| |
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: | |
本文献已被 SpringerLink 等数据库收录! |
|