SAT Meets Tableaux for Linear Temporal Logic Satisfiability

Linear temporal logic ( ) and its variant interpreted on finite traces ( _ ) 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 and _ 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 and _ satisfiability checking based on Reynolds’ tableau, proving its correctness and discussing experimental results obtained through its implementation in the BLACK satisfiability checker.