LTLf satisfiability checking

TL;DR

This paper introduces a novel direct method for checking the satisfiability of LTLf formulas over finite traces, leveraging semantics differences from LTL and SAT solving to improve efficiency.

Contribution

The paper presents a new direct approach to LTLf satisfiability checking that outperforms existing reduction-based methods by exploiting semantics and SAT solving techniques.

Findings

The new approach outperforms existing methods in experiments.

Specialized heuristics improve satisfiability checking efficiency.

Implementation demonstrates practical effectiveness.

Abstract

We consider here Linear Temporal Logic (LTL) formulas interpreted over \emph{finite} traces. We denote this logic by LTLf. The existing approach for LTLf satisfiability checking is based on a reduction to standard LTL satisfiability checking. We describe here a novel direct approach to LTLf satisfiability checking, where we take advantage of the difference in the semantics between LTL and LTLf. While LTL satisfiability checking requires finding a \emph{fair cycle} in an appropriate transition system, here we need to search only for a finite trace. This enables us to introduce specialized heuristics, where we also exploit recent progress in Boolean SAT solving. We have implemented our approach in a prototype tool and experiments show that our approach outperforms existing approaches.