LTL satisfiability checking

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-S...

Full description

Saved in:
Bibliographic Details
Published in:International journal on software tools for technology transfer 2010-05, Vol.12 (2), p.123-137
Main Authors: Rozier, Kristin Y., Vardi, Moshe Y.
Format: Article
Language:English
Subjects:
Applied sciences
Computer Science
Computer science
control theory
systems
Exact sciences and technology
Information systems. Data bases
Memory organisation. Data processing
Software
Software Engineering
Software Engineering/Programming and Operating Systems
Spin 07
Technology transfer
Theory of Computation
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1433-2779
1433-2787
DOI:10.1007/s10009-010-0140-3