发表机构
Bar-Ilan University（巴伊兰大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文为反应式系统提出时间充分理由与对比性解释的统一形式化定义，提升至符号化表示，并分析其验证与查找复杂度，用原型实现验证方法有效性。
AI 中文摘要
我们针对反应式系统的时间因果性与可解释性问题展开研究，并在此背景下探讨充分理由与对比性解释。这两种概念在神经网络语境中是广为人知的可解释性度量。在本工作中，我们将这些概念统一应用于反应式系统及以时序逻辑给出的形式化规范，为充分理由和对比性解释提供专门的定义。随后，我们将这些定义提升至时间充分理由与时间对比性解释，从而提供更通用且符号化的可解释性表示。我们分析了不同类型解释的验证与查找的复杂度，并通过原型实现演示了我们的方法。
英文摘要
We address the problem of temporal causality and explainability for reactive systems, and, in this setting, study sufficient reasons and contrastive explanations. These two notions are well-known explainability measures in the context of neural networks. In this work, we unify these notions for reactive systems and formal specifications given in temporal logic, providing dedicated definitions for sufficient reasons and contrastive explanations. We then lift these definitions to \emph{temporal} sufficient reasons and contrastive explanations, providing more general and symbolic representations of explainability. We analyze the complexity of both verifying and finding explanations of the different types, and we demonstrate our approach using a prototype implementation.
