Lewis' theory of counterfactuals is the foundation of many contemporary notions of causality. In this paper, we extend this theory in the temporal direction to enable symbolic counterfactual reasoning on infinite sequences, such as counterexamples found by a model checker and trajectories produced by a reinforcement learning agent. In particular, our extension considers a more relaxed notion of similarity between worlds and proposes two additional counterfactual operators that close a semantic gap between the previous two in this more general setting. Further, we consider versions of counterfactuals that minimize the distance to the witnessing counterfactual worlds, a common requirement in causal analysis. To automate counterfactual reasoning in the temporal domain, we introduce a logic that combines temporal and counterfactual operators, and outline decision procedures for the satisfiability and trace-checking problems of this logic.

翻译：刘易斯的反事实理论是当代许多因果概念的基础。本文在时序方向上扩展了这一理论，以实现对无穷序列（如模型检查器发现的反例和强化学习智能体产生的轨迹）的符号化反事实推理。具体而言，我们的扩展考虑了更宽松的世界相似性概念，并提出了两种额外的反事实算子，以填补此前两种算子在此更一般设定下的语义空缺。此外，我们还研究了使反事实世界与见证反事实世界之间距离最小化的问题版本——这是因果分析中的常见需求。为在时序领域实现反事实推理的自动化，我们引入了一种结合时序与反事实算子的逻辑，并概述了该逻辑的可满足性判定与轨迹验证问题的决策过程。