Li, Jianwen; Pu, Geguang; Zhang, Lijun; Vardi, Moshe Y.; He, Jifeng Accelerating LTL satisfiability checking by SAT solvers. (English) Zbl 1410.68235 J. Log. Comput. 28, No. 6, 1011-1030 (2018). 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. Cited in 1 Document 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.) Keywords:linear temporal logic; LTL satisfiability checking; SAT-based LTL satisfiability checking; obligation formula; satisfiability checking PDFBibTeX XMLCite \textit{J. Li} et al., J. Log. Comput. 28, No. 6, 1011--1030 (2018; Zbl 1410.68235) Full Text: DOI