# LTLf satisfiability checking

arXiv: https://arxiv.org/abs/1403.1666 · HTML: https://mlsanity.com/paper/1403.1666/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 7 Mar 2014.

## Built on by (most cited first, 3 of 3)

- [Computing unsatisfiable cores for LTLf specifications](https://mlsanity.com/paper/2203.04834/) (2022)
- [Stakeholder utility measures for declarative processes and their use in process comparisons](https://mlsanity.com/paper/2202.03520/) (2022)
- [Measuring Rule-based LTLf Process Specifications: A Probabilistic Data-driven Approach](https://mlsanity.com/paper/2305.05418/) (2023)

## Abstract (arXiv)

We consider here Linear Temporal Logic (LTL) formulas interpreted over 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 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.