# Computing unsatisfiable cores for LTLf specifications

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 7 of its 70 references that are in the map.
- First posted on arXiv 9 Mar 2022.

## Builds on (most cited first, 7 of 7)

- [Monitoring Constraints and Metaconstraints with Temporal Logics on Finite Traces](https://mlsanity.com/paper/2004.01859/) (2020)
- [SAT-based Explicit LTLf Satisfiability Checking](https://mlsanity.com/paper/1811.03176/) (2018)
- [One-Pass and Tree-Shaped Tableau Systems for TPTL and TPTLb+Past](https://mlsanity.com/paper/1809.03101/) (2018)
- [LTLf satisfiability checking](https://mlsanity.com/paper/1403.1666/) (2014)
- [SAT-based Explicit LTL Reasoning](https://mlsanity.com/paper/1507.02519/) (2015)
- [Computing Minimal Sets on Propositional Formulae I: Problems & Reductions](https://mlsanity.com/paper/1402.3011/) (2014)
- [Consistency of Property Specification Patterns with Boolean and Constrained Numerical Signals](https://mlsanity.com/paper/1712.04162/) (2017)

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

- [Measuring Inconsistency in Declarative Process Specifications](https://mlsanity.com/paper/2206.07080/) (2022)
- [Enumerating Minimal Unsatisfiable Cores of LTLf formulas](https://mlsanity.com/paper/2409.09485/) (2024)
- [Symbolic Temporal Supervision of LLM Agents Using Contracts](https://mlsanity.com/paper/2609.18128/) (2026)

## Abstract (arXiv)

Linear-time temporal logic on finite traces (LTLf) is rapidly becoming a de-facto standard to produce specifications in many application domains (e.g., planning, business process management, run-time monitoring, reactive synthesis). Several studies approached the respective satisfiability problem. In this paper, we investigate the problem of extracting the unsatisfiable core in LTLf specifications. We provide four algorithms for extracting an unsatisfiable core leveraging the adaptation of state-of-the-art approaches to LTLf satisfiability checking. We implement the different approaches within the respective tools and carry out an experimental evaluation on a set of reference benchmarks, restricting to the unsatisfiable ones. The results show the feasibility, effectiveness, and complementarities of the different algorithms and tools.