Enumerating Minimal Unsatisfiable Cores of LTLf formulas

TL;DR

This paper presents a new method for efficiently enumerating minimal unsatisfiable cores of LTLf formulas by encoding them into ASP, aiding explainability in AI and formal verification.

Contribution

It introduces a novel ASP-based encoding technique that directly maps minimal unsatisfiable cores of LTLf formulas to ASP minimal unsatisfiable subsets, enabling effective enumeration.

Findings

The ASP encoding effectively finds MUCs in LTLf formulas.

Experimental results show good performance on benchmark problems.

The method enhances explainability in AI and formal verification tasks.

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.