Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Enumerating Minimal Unsatisfiable Cores of LTLf formulas

Antonio Ielo, Giuseppe Mazzotta, Rafael Peñaloza, Francesco Ricca

TL;DR

A novel technique for enumerating minimal unsatisfiable cores (MUCs) of an LTL specification by encoding a 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.

Abstract

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.

Enumerating Minimal Unsatisfiable Cores of LTLf formulas

TL;DR

A novel technique for enumerating minimal unsatisfiable cores (MUCs) of an LTL specification by encoding a 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 specification.

Abstract

Linear Temporal Logic over finite traces () is a widely used formalism with applications in AI, process mining, model checking, and more. The primary reasoning task for 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 . This paper introduces a novel technique for enumerating minimal unsatisfiable cores (MUCs) of an specification. The main idea is to encode a 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 specification. Leveraging recent advancements in ASP solving yields a MUC enumerator achieving good performance in experiments conducted on established benchmarks from the literature.
Paper Structure (25 sections, 4 theorems, 1 equation, 5 figures, 1 table, 2 algorithms)

This paper contains 25 sections, 4 theorems, 1 equation, 5 figures, 1 table, 2 algorithms.

Table of Contents

  1. Introduction
  2. Related Work
  3. Preliminaries
  4. Answer Set Programming
  5. Syntax and semantics.
  6. MUSes and MSMs
  7. Linear Temporal Logic over Finite Traces
  8. Method
  9. MUS and Probes
  10. MUC enumeration by MUS enumeration
  11. A concrete example of probe
  12. Encoding formulae.
  13. Encoding LTL$_\text{f}$ semantics.
  14. Encoding LTL$_\text{f}$ bounded satisfiabilty.
  15. The probe.
  16. ...and 10 more sections

Key Result

Lemma 3

Let $\rho$ be a probe of depth $k$ for $\varphi$. Let $S$ be a minimal unsatisfiable subset of $\rho(\varphi)$ wrt the objective atoms $\mathcal{O}(\varphi)$. Then $\textsf{Formula}(S)$ is either an MUC of $\varphi$ or it is satisfiable but its shortest satisficing trace has length greater than $k$.

Figures (5)

  • Figure 1: Computation of a single MUC or UC.
  • Figure 2: Percentage of not-fully-enumerated instances (among the formula families RndConj C100, RndConj V20, TRP5y and TRP12y) that are able to enumerate at least a given number of MUCs in a certain amount of time. A cell $(i,j)$ in the heatmap represents the percentage of timed-out instances that are able to enumerate $j$ MUCs in $i$ seconds.
  • Figure 3: Number of not-fully-enumerated instances (among the formula families RndConj C100, RndConj V20, TRP5y and TRP12y) that are able to enumerate the $y$ percent of found MUCs within $x$ seconds of runtime. Thus, a cell $(i,j)$ in the heatmap represents how many instances in the given formula family can enumerate $i$ percent of the found MUCs found in 300s (up to timeout) in $j$ seconds.
  • Figure 4: A point $(x,y)$ in the scatter plot represents that a certain instance has spent $x$ CPU seconds generating $k$-MUCs (e.g., ASP MUS enumeration) and $y$ CPU seconds certifieing $k$-MUCs (e.g., an LTL$_\text{f}$ solver running to prove unsatisfiability). Colors represent the formula family an instance belongs to. For a given point, $x + y$ might not sum up to the 300s timeout, because (i) these modules run concurrently, thus CPU time can exceed 300s; (ii) if the ASP solver or the LTL$_\text{f}$ solver times out before yielding control, no event is recorded.
  • Figure 5: Enumeration of MUCs.

Theorems & Definitions (12)

  • Definition 1: Reification Function
  • Definition 2: $k$-Probe
  • Lemma 3
  • proof
  • Example 4
  • Definition 5: $k$-bound MUC
  • Lemma 6
  • proof
  • Lemma 7
  • Theorem 8
  • ...and 2 more