SAT Meets Tableaux for Linear Temporal Logic Satisfiability

Linear temporal logic ( \(\textsf{LTL}\,\) $\mathsf{LTL}$ ) and its variant interpreted on finite traces ( \(\textsf{LTL}_{\textsf{f}\,}\) ${\mathsf{LTL}}_{\mathsf{f}}$ ) are among the most popular specification languages in the fields of formal verification, artificial intelligence, and others. In this paper, we focus on the satisfiability problem for \(\textsf{LTL}\,\) $\mathsf{LTL}$ and \(\textsf{LTL}_{\textsf{f}\,}\) ${\mathsf{LTL}}_{\mathsf{f}}$ formulas, for which many techniques have been devised during the last decades. Among these are tableau systems, of which the most recent is Reynolds’ tree-shaped tableau. We provide a SAT-based algorithm for \(\textsf{LTL}\,\) $\mathsf{LTL}$ and \(\textsf{LTL}_{\textsf{f}\,}\) ${\mathsf{LTL}}_{\mathsf{f}}$ satisfiability checking based on Reynolds’ tableau, proving its correctness and discussing experimental results obtained through its implementation in the BLACK satisfiability checker.