# Enumerating Minimal Unsatisfiable Cores of LTLf formulas

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 9 of its 47 references that are in the map.
- First posted on arXiv 14 Sep 2024.

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

- [Explanation in Artificial Intelligence: Insights from the Social Sciences](https://mlsanity.com/paper/1706.07269/) (2017)
- [Multi-shot ASP solving with clingo](https://mlsanity.com/paper/1705.09811/) (2017)
- [ASP-Core-2 Input Language Format](https://mlsanity.com/paper/1911.04326/) (2019)
- [Foundations for Restraining Bolts: Reinforcement Learning with LTLf/LDLf restraining specifications](https://mlsanity.com/paper/1807.06333/) (2018)
- [Axiom Pinpointing](https://mlsanity.com/paper/2003.08298/) (2020)
- [SAT-based Explicit LTLf Satisfiability Checking](https://mlsanity.com/paper/1811.03176/) (2018)
- [A New Rule for LTL Tableaux](https://mlsanity.com/paper/1609.04102/) (2016)
- [Temporal Logics Over Finite Traces with Uncertainty (Technical Report)](https://mlsanity.com/paper/1903.04940/) (2019)
- [Computing unsatisfiable cores for LTLf specifications](https://mlsanity.com/paper/2203.04834/) (2022)

## Abstract (arXiv)

Linear Temporal Logic over finite traces (LTLf) is a widely used formalism with applications in AI, process mining, model checking, and more. The primary reasoning task for LTLf is satisfiability checking; yet, the recent focus on explainable AI has increased interest in analyzing inconsistent formulas, making the enumeration of minimal explanations for infeasibility a relevant task also for LTLf. This paper introduces a novel technique for enumerating minimal unsatisfiable cores (MUCs) of an LTLf specification. The main idea is to encode a LTLf formula into an Answer Set Programming (ASP) specification, such that the minimal unsatisfiable subsets (MUSes) of the ASP program directly correspond to the MUCs of the original LTLf specification. Leveraging recent advancements in ASP solving yields a MUC enumerator achieving good performance in experiments conducted on established benchmarks from the literature.