Closure and Complexity of Temporal Causality

TL;DR

This work investigates temporal causality for infinite computations, focusing on which temporal property classes remain closed under causal inference and how complex it is to synthesize causes from effects. It introduces a universal preimage framework with a topological backbone (Cantor distance, Hausdorff metric, and the Borel hierarchy) to prove closure results: safety, reachability, and recurrence are closed under causality, while persistence and obligation are not. The paper provides both lower and upper bounds on the size of cause representations, revealing doubly exponential lower bounds in the effect size for several classes and near-matching exponential or doubly-exponential upper bounds in system size and effect size. These results refine the understanding of explainable verification and model-checking explanations, and connect temporal-causality reasoning to broader themes in hyperproperties and incomplete-information synthesis.

Abstract

Temporal causality defines what property causes some observed temporal behavior (the effect) in a given computation, based on a counterfactual analysis of similar computations. In this paper, we study its closure properties and the complexity of computing causes. For the former, we establish that safety, reachability, and recurrence properties are all closed under causal inference: If the effect is from one of these property classes, then the cause for this effect is from the same class. We also show that persistence and obligation properties are not closed in this way. These results rest on a topological characterization of causes which makes them applicable to a wide range of similarity relations between computations. Finally, our complexity analysis establishes improved upper bounds for computing causes for safety, reachability, and recurrence properties. We also present the first lower bounds for all of the classes.

Figures (2)

• Figure 1: Results on closure under causality of property classes in Manna and Pneuli's hierarchy of temporal properties MannaP89. Classes colored green are closed under causal inference, while classes colored in red are not. Note that $\varphi$ and $\psi$ are formulas containing no future operators.
• Figure 2: Figure \ref{['fig:example']} illustrated the reactive system with the input $i$ and output $o$ that is used to outline temporal causality in Example \ref{['ex:intro']}. The system sets the output $o$ continuously whenever the input $i$ is enabled less than three time units apart. Figure \ref{['fig:closure']} pictures a chain in $(\mathit{traces}(\mathcal{T}),\leq_{\pi_a})$ to illustrate that the cause $C$ (enclosed by the blue frame) on $\pi_a$ is the largest downward closed set of traces satisfying the effect $E$ (shaded yellow), which is the complement of the upward closure of $\overline{E}$.

Theorems & Definitions (51)

• Definition 1: Manna and Pneuli MannaP89
• Definition 2: Temporal Cause FinkbeinerFMS24
• Example 1
• Lemma 1: Finkbeiner et al. FinkbeinerFMS24
• Definition 3
• Definition 4
• Definition 5
• Definition 6
• Remark 1
• Theorem 1: Universal Closure