Computing Unsatisfiable Cores for LTL_f Specifications

Linear-time temporal logic on finite traces (LTL_f) is rapidly becoming a de-facto standard to produce specifications in many application domains (including planning, business process management, run-time monitoring, and reactive synthesis). Several studies have challenged the satisfiability problem thus far. In this paper, we focus instead on unsatisfiable LTL_f specifications, with the objective of extracting the subset of formulae that cause inconsistencies within them, i.e., the unsatisfiable cores. We provide four algorithms to this end, which leverage the adaptation of a range of state-of-the-art algorithms to LTL_f satisfiability checking. We implement those algorithms extending the respective implementations and carry out an experimental evaluation on a set of reference benchmarks, restricting to the unsatisfiable specifications. The results put in evidence that the different algorithms and tools exhibit complementary features determining their efficiency and efficacy. Indeed, our findings suggest exploring different strategies and algorithmic solutions for the extraction of unsatisfiable cores from LTL_f specifications, thus confirming the challenging and multi-faceted nature of this problem.