Temporal Causality in Reactive Systems
Norine Coenen, Bernd Finkbeiner, Hadar Frenkel, Christopher Hahn, Niklas Metzger, and Julian Siber
Counterfactual reasoning is an approach to infer what causes an observed effect by analyzing the hypothetical scenarios where a suspected cause is not present. The seminal works of Halpern and Pearl have provided a workable definition of counterfactual causality for finite settings. In this paper, we propose an approach to check causality that is tailored to reactive systems, i.e., systems that interact with their environment over a possibly infinite duration. We define causes and effects as trace properties which characterize the input and observed output behavior, respectively. We then instantiate our definitions for omega-regular properties and give automata-based constructions for our approach. Checking that an omega-regular property qualifies as a cause can then be encoded as a hyperproperty model-checking problem.
20th International Symposium on Automated Technology for Verification and Analysis (ATVA 2022).