Enumerating Minimal Unsatisfiable Cores of LTLf formulas
This addresses the need for explainable AI by providing minimal explanations for infeasibility in LTLf formulas, which is incremental as it builds on existing ASP advancements.
The paper tackled the problem of enumerating minimal unsatisfiable cores (MUCs) for LTLf formulas, which is important for explainable AI, by introducing a technique that encodes LTLf into Answer Set Programming (ASP) and leverages ASP solving, achieving good performance on established benchmarks.
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.