ExplainabilityTransparencyAccountabilitycs.AI
Enumerating Minimal Unsatisfiable Cores of LTLf formulas
Antonio Ielo, Giuseppe Mazzotta, Rafael Peñaloza, Francesco Ricca
September 14, 2024
arXiv.org
Key Takeaways
-
Explainability is becoming central to AI systems: The paper highlights that as AI moves toward responsible and trustworthy systems, understanding why specifications fail—not just whether they work—has become increasingly important across applications like process mining and model checking.
-
Minimal explanations help identify root causes: By enumerating minimal unsatisfiable cores (MUCs), the technique helps practitioners pinpoint the smallest sets of conflicting requirements in a specification, making it easier to diagnose and fix problems rather than seeing only that "something is wrong."
-
Technical translation enables practical solutions: The researchers converted a complex logical problem (LTLf formulas) into a different computational framework (Answer Set Programming) where existing tools could efficiently find minimal explanations, demonstrating how responsible AI often requires creative technical bridges rather than building everything from scratch.
-
Performance matters for real-world adoption: The paper emphasizes that good experimental performance on established benchmarks is necessary for these explainability techniques to be practically useful in actual AI systems, not just theoretically sound.
Abstract
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.