面向有限轨迹线性时序逻辑（LTLf）的形式化解释方法
Formal Explanations for Linear Temporal Logic over Finite Traces
AI 导读
一项 arXiv 研究针对有限轨迹上的线性时序逻辑（LTLf）提出溯因解释（AXps）与对比解释（CXps）的轨迹级原生刻画，基于时间索引事件的锁定与解锁，并证明其与基于分类器的表述等价。研究发现 CXps 与一种新提出的 LTLf 时序因果语义一致，并借助 ASP 程序的最小不可满足核与最小修正集枚举实现高效计算，在真实事件日志实验中验证了有效性。
正文 · 原文
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.
| Subjects: | Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI) |
| Cite as: | arXiv:2610.35169 [cs.LO] |
| (or arXiv:2610.35169v1 [cs.LO] for this version) | |
| https://doi.org/10.48550/arXiv.2610.35169 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Antonio Ielo [view email]
[v1]
Mon, 26 Oct 2026 10:33:46 UTC (314 KB)
来源：arXiv cs.AI · arxiv.org