Computing unsatisfiable cores for LTLf specifications
This work addresses the need for debugging unsatisfiable specifications in LTLf, which is incremental as it adapts known methods to a specific problem.
The paper tackled the problem of extracting unsatisfiable cores from LTLf specifications, which are used in domains like planning and monitoring, by developing four algorithms based on existing satisfiability methods and showing their feasibility and effectiveness through experimental evaluation on benchmarks.
Linear-time temporal logic on finite traces (LTLf) is rapidly becoming a de-facto standard to produce specifications in many application domains (e.g., planning, business process management, run-time monitoring, reactive synthesis). Several studies approached the respective satisfiability problem. In this paper, we investigate the problem of extracting the unsatisfiable core in LTLf specifications. We provide four algorithms for extracting an unsatisfiable core leveraging the adaptation of state-of-the-art approaches to LTLf satisfiability checking. We implement the different approaches within the respective tools and carry out an experimental evaluation on a set of reference benchmarks, restricting to the unsatisfiable ones. The results show the feasibility, effectiveness, and complementarities of the different algorithms and tools.