Towards ASP-based Minimal Unsatisfiable Cores Enumeration for LTLf

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