Linear temporal logic ( LTL\, LTL ) and its variant interpreted on finite traces ( LTLf\, LTLf ) 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 LTL\, LTL and LTLf\, LTLf 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 LTL\, LTL and LTLf\, LTLf satisfiability checking based on Reynolds’ tableau, proving its correctness and discussing experimental results obtained through its implementation in the BLACK satisfiability checker.
No takes yet. Share an insight, caveat, or question.
Geatti et al. (2024) studied this question.
Synapse has enriched 5 closely related papers on similar clinical questions. Consider them for comparative context: