Formal explanations clarify why events satisfy or break temporal rules
Formal Explanations for Linear Temporal Logic over Finite Traces
Logic in Computer ScienceArtificial Intelligence
Summary
When computers check if a sequence of events follows certain time-based rules, it’s important to explain why the rules are met or broken. The authors developed a clear way to provide two types of explanations: what caused the outcome and what changes could reverse it. They proved their approach matches existing methods and created a tool to efficiently find these explanations. Tests on real event data showed their method works well for explaining temporal behaviors.
What this means in practice
- •For ai system developers: Use formal explanations to debug AI systems by pinpointing causes why temporal constraints hold or fail on event sequences.
- •For workflow analysts: Provide understandable feedback on process compliance by explaining which event timings affect adherence to temporal rules in logs.
Authors
Valeria Fionda, Antonio Ielo, Francesco Ricca
Abstract
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.