CISPA
Browse

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.

History

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

2022-07-05

Open Access Type

  • Unknown

BibTeX

@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

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC