File(s) not publicly available

Temporal Causality in Reactive Systems

Version 2 2023-12-11, 20:15
Version 1 2023-11-29, 18:21
conference contribution
posted on 2023-12-11, 20:15 authored by Norine CoenenNorine Coenen, Bernd FinkbeinerBernd Finkbeiner, Hadar FrenkelHadar Frenkel, Christopher Hahn, Niklas MetzgerNiklas Metzger, Julian SiberJulian 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 ω-regular properties and give automata-based constructions for our approach. Checking that an ω-regular property qualifies as a cause can then be encoded as a hyperproperty model checking problem.


Preferred Citation

Norine Coenen, Bernd Finkbeiner, Hadar Frenkel, Christopher Hahn, Niklas Metzger and Julian Siber. Temporal Causality in Reactive Systems. In: International Symposium on Automated Technology for Verification and Analysis (ATVA). 2022.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

International Symposium on Automated Technology for Verification and Analysis (ATVA)

Legacy Posted Date


Open Access Type

  • Unknown


@inproceedings{cispa_all_3722, title = "Temporal Causality in Reactive Systems", author = "Coenen, Norine and Finkbeiner, Bernd and Frenkel, Hadar and Hahn, Christopher and Metzger, Niklas and Siber, Julian", booktitle="{International Symposium on Automated Technology for Verification and Analysis (ATVA)}", year="2022", }

Usage metrics


    No categories selected


    Ref. manager