%0 Journal Article
%T Fast LTL Satisfiability Checking by SAT Solvers
%A Jianwen Li
%A Geguang Pu
%A Lijun Zhang
%A Moshe Y. Vardi
%A Jifeng He
%J Computer Science
%D 2014
%I arXiv
%X 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. With the sole exception of LTL satisfiability checking based on bounded model checking, which does not provide a complete decision procedure, LTL satisfiability checkers have not taken advantage of the remarkable progress over the past 20 years in Boolean satisfiability solving. In this paper, we propose a new LTL satisfiability-checking framework that is accelerated using a Boolean SAT solver. Our approach is based on the variant of the \emph{obligation-set method}, which we proposed in earlier work. We describe here heuristics that allow the use of a Boolean SAT solver to analyze the obligations for a given LTL formula. The experimental evaluation indicates that the new approach provides a a significant performance advantage.
%U http://arxiv.org/abs/1401.5677v2