Enumerating Minimal Unsatisfiable Cores of LTLf formulas

Antonio Ielo, Giuseppe Mazzotta, Rafael Peñaloza +1

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 f…