Fast LTL Satisfiability Checking by SAT Solvers

TL;DR

This paper introduces a new framework for LTL satisfiability checking that leverages modern SAT solvers, significantly improving performance over previous methods by applying heuristics to analyze obligations.

Contribution

It presents a novel LTL satisfiability checking approach using SAT solvers and heuristics based on the obligation-set method, enhancing efficiency.

Findings

Significant performance improvements over existing LTL satisfiability checkers.

Effective heuristics enable SAT solvers to analyze obligations efficiently.

Experimental results demonstrate the approach's practical advantages.

Abstract

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.