×

zbMATH — the first resource for mathematics

Accelerating LTL satisfiability checking by SAT solvers. (English) Zbl 1410.68235
Summary: Satisfiability checking for Linear Temporal Logic (LTL) is a fundamental step in checking for possible errors in LTL assertions. Extant LTL satisfiability checkers use a variety of different search procedures. In this paper, we propose an LTL satisfiability-checking framework that is accelerated by leveraging the state-of-the-art Boolean SAT techniques. Our approach is based on the variant of the obligation-set method, which we proposed in earlier work. We describe here heuristics that allow the use of a Boolean SAT solver to analyse the obligations for a given LTL formula. Moreover, we show the heuristics can be also utilized as the preprocessor for every LTL satisfiability solver. The experimental evaluation indicates that the new approach provides a significant performance improvement compared to its previous version, and becomes competitive with other state-of-the-art solvers.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDF BibTeX XML Cite
Full Text: DOI