Linear Temporal Logic over finite traces ($\text{LTL}_f$) is a widely used formalism with applications in AI, process mining, model checking, and more. The primary reasoning task for $\text{LTL}_f$ 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 $\text{LTL}_f$. This paper introduces a novel technique for enumerating minimal unsatisfiable cores (MUCs) of an $\text{LTL}_f$ specification. The main idea is to encode a $\text{LTL}_f$ 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 $\text{LTL}_f$ specification. Leveraging recent advancements in ASP solving yields a MUC enumerator achieving good performance in experiments conducted on established benchmarks from the literature.

翻译：有限迹线性时序逻辑（$\text{LTL}_f$）是一种广泛使用的形式化方法，在人工智能、过程挖掘、模型检测等领域具有重要应用。$\text{LTL}_f$的主要推理任务是可满足性检验；然而，近期对可解释人工智能的关注增强了对分析不一致公式的兴趣，使得枚举不可行性的最小解释也成为$\text{LTL}_f$的相关任务。本文提出了一种枚举$\text{LTL}_f$规范的最小不可满足核（MUC）的新技术。其核心思想是将$\text{LTL}_f$公式编码为答案集编程（ASP）规范，使得ASP程序的最小不可满足子集（MUS）直接对应于原始$\text{LTL}_f$规范的MUC。利用ASP求解技术的最新进展，我们实现了一个MUC枚举器，在文献中已有基准测试上进行的实验表明其具有良好的性能。