,
Clemens Dubslaff
,
Florian Funke
,
Simon Jantsch
,
Rupak Majumdar
,
Jakob Piribauer
,
Robin Ziemek
Creative Commons Attribution 4.0 International license
In view of the growing complexity of modern software architectures, formal models are increasingly used to understand why a system works the way it does, opposed to simply verifying that it behaves as intended. This paper surveys approaches to formally explicate the observable behavior of reactive systems. We describe how Halpern and Pearl’s notion of actual causation inspired verification-oriented studies of cause-effect relationships in the evolution of a system. A second focus lies on applications of the Shapley value to responsibility ascriptions, aimed to measure the influence of an event on an observable effect. Finally, formal approaches to probabilistic causation are collected and connected, and their relevance to the understanding of probabilistic systems is discussed.
@InProceedings{baier_et_al:LIPIcs.ICALP.2021.1,
author = {Baier, Christel and Dubslaff, Clemens and Funke, Florian and Jantsch, Simon and Majumdar, Rupak and Piribauer, Jakob and Ziemek, Robin},
title = {{From Verification to Causality-Based Explications}},
booktitle = {48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
pages = {1:1--1:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-195-5},
ISSN = {1868-8969},
year = {2021},
volume = {198},
editor = {Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.1},
URN = {urn:nbn:de:0030-drops-140709},
doi = {10.4230/LIPIcs.ICALP.2021.1},
annote = {Keywords: Model Checking, Causality, Responsibility, Counterfactuals, Shapley value}
}