PaperlayerView exact revision on arXiv

Source-linked AI summary

Formal Explanations for Linear Temporal Logic over Finite Traces

Valeria Fionda, Antonio Ielo, Francesco Ricca

arXiv:2610.35169v1cs.LOcs.AI

TL;DR

LTLf explanations matter for understanding why finite traces satisfy or violate specifications, but prior approaches do not connect sufficient reasons with counterfactual causes. This paper defines abductive and contrastive explanations directly over traces using locked and unlocked observations. It proves formal relationships among the explanation notions and reports an effective ASP-based approach on real-world event logs.

  • Problem

    Existing LTLf approaches capture either sufficient reasons or counterfactual causes without connecting the two perspectives.

    Source: Introduction · p. 2

  • Method

    The paper characterizes AXps and CXps on finite traces by locking and unlocking observations, and computes them through ASP programs using minimal unsatisfiable cores and correction sets.

    Source: Introduction · p. 2, AXp and CXp for LTLf · p. 4

  • Results

    The trace-based characterization is equivalent to classifier-based explanations, and CXps coincide with minimal temporal causes; experiments report the approach effective on real-world event logs.

    Source: Relationship with Temporal Causality · p. 6, Conclusion · p. 9

  • Takeaways & Limitations

    The paper provides a direct finite-trace account of abductive and contrastive explanations and demonstrates its application to real-world event logs.

    Source: Conclusion · p. 9

    The formal treatment focuses on violating traces, with the complementary case handled by replacing φ with ¬φ.

    Source: Encoding LTLf Formulas as Binary… · p. 4

Abstract

from arXiv · show

Linear Temporal Logic over Finite Traces (LTLf) is widely used in Artificial Intelligence to specify desired temporal behavior and determine whether finite traces satisfy or violate it. Explaining these outcomes is essential for debugging and trust. However, existing approaches typically capture either sufficient reasons or counterfactual causes, without clarifying their relationship. We introduce a native characterization of abductive (AXps) and contrastive (CXps) explanations directly over finite traces, based on locking and unlocking time-indexed events. We prove its equivalence to the classifier-based formulation, and show that CXps coincide with a recently proposed temporal causality semantics for LTLf. This characterization enables an efficient implementation based on the enumeration of minimal unsatisfiable cores and minimal correction sets of ASP programs. Experiments on real-world event logs demonstrate the effectiveness of the approach.

Introduction

LTLf traces can comply with or violate specifications, and explanations clarify why an outcome holds and what must change to obtain the opposite outcome. The paper defines abductive and contrastive explanations directly over finite traces, addressing the gap between existing approaches that treat these perspectives separately.

Introduction

  • LTLf is a popular AI formalism for temporal reasoning, applied in reinforcement learning, planning, robotics, and business process management.The passage cites examples of applications in each domain.Source: Introduction · p. 1
  • A sufficient reason fixes observations that guarantee the trace’s outcome, while a minimal intervention changes observations to flip that outcome.For the delivery-agent example, the absence of low battery throughout guarantees the charging obligation; adding low battery at an uncharged instant can create a violation.Source: Introduction · p. 1
  • The paper defines AXps and CXps directly over finite traces, filling a gap left by approaches that capture sufficient reasons or counterfactual causes without connecting them.The characterization uses locking and unlocking temporal observations instead of reformulating the trace as a classifier instance.Source: Introduction · p. 1
  • The paper proves equivalence to classifier-based explanations, establishes AXp–CXp hitting-set duality, links CXps to temporal causes, and evaluates an ASP implementation on real-world event logs.The contribution list states these theoretical connections and the event-log evaluation.Source: Introduction · p. 2

Related Work

Prior work studies temporal implicants, temporal causes, and unsatisfiable cores, but does not provide the paper’s combined finite-trace explanation treatment. This work places the explanations in the FXAI framework and implements them using unsatisfiable cores and correction sets.

Formal Explanations

  • The paper specializes the classifier-based FXAI framework to LTLf with an equivalent characterization in terms of formulas and finite traces.Related specializations also address ranking functions and finite-state machines.Source: Related Work · p. 2

Temporal Implicants & Temporal Causality

  • Earlier temporal implicants concern infinite traces and may be computed as a single, non-minimal implicant; this work instead treats finite traces within FXAI.The paper also develops an implementation based on unsatisfiable cores and correction sets.Source: Related Work · p. 2
  • Recent LTLf temporal causality work addresses conjunctive causes but not the dual notion of sufficient reasons; the paper relates that causality notion to CXps.The cited account contrasts conjunctive causes with earlier singleton causes.Source: Related Work · p. 2

Unsatisfiable Cores in Temporal Reasoning

  • The implementation obtains local AXp and CXp explanations as unsatisfiable cores and correction sets of an ASP program, distinguishing them from global explanations of formula unsatisfiability.It uses bounded LTLf satisfiability and a solver based on SAT techniques.Source: Related Work · p. 2

Answer Set Programming

The section introduces ASP rule and program concepts, then defines minimal unsatisfiable subsets relative to objective atoms. These definitions support the paper’s ASP-based explanation computation.

Answer Set Programming

  • An ASP atom is a predicate applied to terms, and a literal is either an atom or its negation as failure.Rules have a head and a conjunction of body literals; a missing head denotes a constraint, and an empty body denotes a fact.Source: Answer Set Programming · pp. 2–3
  • An ASP program is a finite set of safe rules, where each variable appears in a positive body literal.The passage also defines grounding, the Herbrand base, interpretations, and answer sets.Source: Answer Set Programming · p. 3
  • A MUS relative to objective atoms is an inclusion-minimal set whose enforced truth makes the augmented program incoherent.The definition tests minimality by requiring every proper subset not to be an unsatisfiable subset.Source: Answer Set Programming · p. 3

Linear Temporal Logic on Finite Traces

LTLf interprets temporal formulas over finite traces, with states represented as sets of propositions. Its semantics define how formulas hold at positions and across the trace.

Linear Temporal Logic on Finite Traces

Formal Explanations

The paper characterizes abductive and contrastive explanations for finite traces by locking or unlocking time-indexed observations. Minimal explanations capture, respectively, observations that force violation and observations whose change can permit satisfaction.

Formal Explanations

  • A trace compatible with locked literals preserves their truth values while leaving all other propositions and time instants unconstrained.The compatible traces have the same length as the original trace.Source: AXp and CXp for LTLf · p. 4
  • An abductive explanation locks enough trace observations to make violation unavoidable, while a contrastive explanation unlocks enough observations to make satisfaction possible.Observations are time-indexed temporal literals, including events and non-events.Source: AXp and CXp for LTLf · p. 4
  • Thus, AXp and CXp are subset-minimal members of corresponding weak explanation classes: an AXp has no proper subset that is a WAXp, and a CXp none that is a WCXp.Source: AXp and CXp for LTLf · p. 4
  • For the violating delivery trace, locking low at the final instant is an AXp, while unlocking ¬deliver at time 0, req at time 1, and low at time 1 is a CXp.The CXp permits a satisfying trace by adding deliver at time 0 and removing req and low at time 1.Source: AXp and CXp for LTLf · p. 4

Equivalence to Classifier Explanations

The paper encodes LTLf satisfaction as a binary classifier over time-indexed Boolean features and maps between feature sets and trace literals. It proves that classifier-based and trace-based explanations correspond, and that trace-based AXps and CXps satisfy hitting-set duality.

Encoding LTLf Formulas as Binary Classifiers

  • Each time-indexed atom becomes a Boolean feature, and each assignment represents a trace that the LTLf classifier labels by satisfaction.The classifier outputs 1 when the represented trace satisfies the formula and 0 otherwise.Source: Encoding LTLf Formulas as Binary… · p. 4

Equivalence to Classifier Explanations

  • The mapping litπ(S) selects the literals of trace π over features in S, while feat(E) maps trace literals back to their features.These mappings preserve the relevant feature–literal correspondence.Source: Encoding LTLf Formulas as Binary… · pp. 4–5
  • Classifier-based weak abductive and contrastive explanations correspond to trace-based explanations through the feature-to-literal mapping.The paper establishes the correspondence separately for WAXps and WCXps.Source: Encoding LTLf Formulas as Binary… · p. 5
  • The correspondence also holds for minimal AXps and CXps, which are related by hitting-set duality in the trace-based formulation.Every AXp is a minimal hitting set of all CXps, and vice versa.Source: Encoding LTLf Formulas as Binary… · p. 5

Relationship with Temporal Causality

The paper relates temporal causality for counterexample traces to contrastive explanations. It proves that a minimal set of literal interventions restoring satisfaction is exactly a CXp.

Relationship with Temporal Causality

  • A minimal cause for violation flips a set of literals in a counterexample trace to produce a satisfying trace, with no proper subset of flips doing so.The altered trace replaces each selected literal with its opposite.Source: Relationship with Temporal Causality · p. 5
  • The traces obtainable by intervening on literals outside E are exactly those compatible with the literals locked in E.This equates the alteration-trace and compatible-trace views used in the relationship proof.Source: Relationship with Temporal Causality · p. 5
  • A set of literals is a minimal cause for violation if and only if it is a CXp for the counterexample trace.The paper also notes that its explicit AXp/CXp duality enables efficient cause computation.Source: Relationship with Temporal Causality · p. 6

Complexity

The paper analyzes the complexity of checking temporal explanations at fixed trace length and connects AXps to minimal unsatisfiable sets. Weak explanation checking is NP-complete for WCXps and coNP-complete for WAXps; checking minimal AXps and CXps is DP-complete and coNP-complete, respectively.

Complexity

  • Bounded-length LTLf satisfiability is NP-complete, and checking whether a set is a weak contrastive explanation (WCXp) is NP-complete.The fixed trace length makes the decision problems searches for models over bounded-length traces.Source: Complexity · p. 6
  • Checking whether a set is a weak abductive explanation (WAXp) is coNP-complete.Source: Complexity · p. 6
  • A deletion-based procedure computes an AXp or CXp with a polynomial or linear number of oracle calls, respectively.These call counts follow from coNP- and NP-complete weak-explanation checking.Source: Complexity · p. 6
  • A clause set S is an MUS exactly when its mapped temporal literals λ(S) form an AXp.The reduction identifies clauses with literals ¬ri in a length-one trace; MUS means unsatisfiable with every proper subset satisfiable.Source: Complexity · p. 6
  • Checking whether a set is a minimal AXp is DP-complete, while checking whether a set is a minimal CXp is coNP-complete.Source: Complexity · p. 6

Computing AXps and CXps in ASP

The ASP implementation encodes finite-trace satisfaction and uses constraints to lock selected time-indexed events to their values in the input trace. MUS/MCS enumeration over these constraints yields AXps/CXps.

Encoding LTLf satisfaction

  • The ASP satisfaction encoding evaluates a formula over a trace, with a unique answer set containing sat exactly when the trace satisfies φ.The encoding reifies formulas and traces, then evaluates temporal operators over time points.Source: Computing AXps and CXps in ASP · pp. 7–8

Searching for models

  • A guess program generates candidate traces, while a constraint discards traces that are not models of φ.The search bounds determine trace length, and projected answer sets yield satisfying traces.Source: Computing AXps and CXps in ASP · p. 8

Encoding explanations

  • For explanations, the guess program generates interventions on the input trace, and constraints lock selected temporal literals to their original values.Models with those constraints correspond one-to-one with traces compatible with the locked literals.Source: Computing AXps and CXps in ASP · p. 8
  • When the input trace violates φ, the constrained program is incoherent and therefore admits unsatisfiable cores and correction sets over the locking constraints.Source: Computing AXps and CXps in ASP · p. 8

Enumerating explanations

  • Selectors choose which locking constraints are active, so minimal unsatisfiable subsets and minimal correction sets correspond to AXps and CXps through MUS/MCS and AXp/CXp hitting-set dualities.Source: Computing AXps and CXps in ASP · p. 8

Experiments

The experiments evaluate ASP-based MUS/MCS enumeration on real-world Declare event logs and compare CXp enumeration with caupybara on a synthetic family. The approach completes about 30% of real-log instances within the timeout and scales farther than caupybara on the synthetic benchmark.

Experimental setup

  • The benchmark used six real-world Declare event logs and generated one explanation problem per unique trace, pairing it with φ if it violated φ and ¬φ otherwise; 3,467 problems yielded 3,422 instances after 45 incoherent cases were discarded.Source: Experiments · pp. 8–9

Real-world event logs

  • About 30% of the 3,422 real-log instances were completed within the timeout; incomplete instances still yielded several AXps and CXps in most cases.The 3,422 explanation problems came from six real-world event logs; 155 incomplete instances produced zero CXps, attributed to joint enumeration when many AXps were present.Source: Experiments · pp. 8–9
  • The mean time to the first AXp was 0.091 ± 0.032s (median 0.09s), and the mean time to the first CXp was 1.05 ± 1.58s (median 0.41s).Source: Experiments · p. 9

Comparison with caupybara

  • On P(N), caupybara exceeded the 10-second budget beyond N=4 even for one CXp, while the full approach enumerated all CXps through N=12.The comparison used caupybara with bound=N; Figure 2 plots time to the first and all CXps for caupybara, the full approach, and a CXp-only variant.Source: Experiments · p. 9, Figure 2 · p. 9
  • The CXp-only variant found a first CXp in under 0.1s but completed enumeration only through N=10 and slowed overall as CXp enumeration continued.Source: Experiments · p. 9

Conclusion

The conclusion specializes abductive and contrastive explanations to finite-trace temporal logic with an idiomatic definition equivalent to the classifier-based formulation. It connects CXps to temporal causality and reports an ASP implementation with effective real-event-log experiments.

Conclusion

  • The paper gives an idiomatic LTLf definition of abductive and contrastive explanations and proves it equivalent to the classifier-based formulation.Source: Conclusion · p. 9
  • The paper proves that CXps coincide with a recently proposed notion of temporal causality.Source: Conclusion · p. 9
  • The characterization supports efficient explanation enumeration using MUS/MCS duality instantiated in ASP, and experiments demonstrate effectiveness on real-world event logs.Source: Conclusion · p. 9
Loading 2610.35169v1…