Papers for

workflow analysts

Papers whose findings have a practical use for this group, as judged from the abstract. Open a paper to read what it means in practice.

Formal explanations clarify why events satisfy or break temporal rules

Formal Explanations for Linear Temporal Logic over Finite Traces

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.

Mon 26 OctLogic in Computer ScienceArtificial Intelligence
The gist
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.
Open → 2610.35169v1