Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Computing unsatisfiable cores for LTLf specifications

Marco Roveri, Claudio Di Ciccio, Chiara Di Francescomarino, Chiara Ghidini

TL;DR

This work addresses extracting unsatisfiable cores from LTLf specifications by proposing four UC extraction algorithms that adapt leading LTL/LTLf satisfiability methods. It develops two complementary pathways: LTLet-based reductions (BDDs, SAT, temporal resolution) and native LTLf SAT approaches, augmented with activation variables and past-to-future transformations to handle past operators. The paper introduces preliminary results enabling past-operator handling (via extended $f2l()$ and $P2F$) and activation-variable conditioning, then demonstrates UC extraction through BDD-based, SAT-based, TR-based, and native SAT methods, with an extensive experimental evaluation showing complementary strengths among tools. The findings enable practical debugging of inconsistent LTLf specifications and provide a toolkit of approaches that practitioners can combine to locate causes of unsatisfiability in domains like BPM, planning, and run-time monitoring.

Abstract

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.

Computing unsatisfiable cores for LTLf specifications

TL;DR

This work addresses extracting unsatisfiable cores from LTLf specifications by proposing four UC extraction algorithms that adapt leading LTL/LTLf satisfiability methods. It develops two complementary pathways: LTLet-based reductions (BDDs, SAT, temporal resolution) and native LTLf SAT approaches, augmented with activation variables and past-to-future transformations to handle past operators. The paper introduces preliminary results enabling past-operator handling (via extended and ) and activation-variable conditioning, then demonstrates UC extraction through BDD-based, SAT-based, TR-based, and native SAT methods, with an extensive experimental evaluation showing complementary strengths among tools. The findings enable practical debugging of inconsistent LTLf specifications and provide a toolkit of approaches that practitioners can combine to locate causes of unsatisfiability in domains like BPM, planning, and run-time monitoring.

Abstract

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.
Paper Structure (25 sections, 15 theorems, 9 equations, 7 figures, 2 tables, 4 algorithms)

This paper contains 25 sections, 15 theorems, 9 equations, 7 figures, 2 tables, 4 algorithms.

Table of Contents

  1. Introduction
  2. Background
  3. LTLf Syntax and Semantics
  4. Remark.
  5. Unsatisfiable core
  6. Checking Satisfiability of an LTLf Formula
  7. Symbolic Approaches to Check Language Emptiness for LTL
  8. Temporal Resolution Approaches for LTL Satisfiability
  9. Extracting unsat cores for LTLf
  10. Preliminary results
  11. Extending $\mathsf{f2l}()$ to handle past temporal operators.
  12. Removing past temporal operators.
  13. Activation variables.
  14. LTLf Unsatisfiable Core Extraction via Reduction to LTL
  15. BDD based LTLf Unsatisfiable Core Extraction
  16. ...and 10 more sections

Key Result

Theorem 1

Any LTLf formula without past temporal operators $\varphi$ is satisfiable iff the LTL formula is satisfiable.

Figures (7)

  • Figure 1: Cactus plots for the whole experimental evaluation.
  • Figure 2: Scatter plots comparing search timings for each algorithm pair.
  • Figure 3: Pie chart reporting how the different solvers contributed to the virtual best (a); Contribution of each solver to the virtual best per benchmark family (b), i.e. for each family we report the number of times each algorithm was performing best.
  • Figure 4: Number of conjuncts in $\Gamma$ and respective computation time (in seconds) for each algorithm.
  • Figure 5: Number of conjuncts in $\Gamma$ and respective computation time (in seconds) for each algorithm for three categories: (a) LTLf-specific/benchmarks/LTLFRandomConjunction/V20, (b) LTLf-specific/benchmarks/LTLFRandomConjunction/C100, and (c) LTL-as-LTLf/schuppan/O1Formula.
  • ...and 2 more figures

Theorems & Definitions (28)

  • Definition 1
  • Definition 2
  • Theorem 1: DBLP:conf/aaai/GiacomoMM14
  • Theorem 2: DBLP:journals/ai/LiPZVR20
  • Definition 3: Conflict Sequence DBLP:journals/ai/LiPZVR20
  • Theorem 3: DBLP:journals/ai/LiPZVR20
  • Corollary 1
  • Theorem 4
  • proof
  • Theorem 5
  • ...and 18 more