  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.
