Enumerating Minimal Unsatisfiable Cores of LTLf formulas
<|reference_start|>Enumerating Minimal Unsatisfiable Cores of LTLf formulas: 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.<|reference_end|>
@article{ielo2024enumerating,
    title={Enumerating Minimal Unsatisfiable Cores of LTLf formulas},
    author={Antonio Ielo, Giuseppe Mazzotta, Rafael Pe~naloza, Francesco Ricca},
    journal={arXiv preprint arXiv:2409.09485},
    year={2024},
    archivePrefix={arXiv},
    eprint={2409.09485},
    primaryClass={cs.AI cs.LO}
}