2026-07-21T12:58:02Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:14070 2024-03-06T10:53:23Z ddc:004 open_access

From Verification to Causality-Based Explications (Invited Talk) Baier, Christel Dubslaff, Clemens Funke, Florian Jantsch, Simon Majumdar, Rupak Piribauer, Jakob Ziemek, Robin Model Checking Causality Responsibility Counterfactuals Shapley value 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Christel Baier and Clemens Dubslaff and Florian Funke and Simon Jantsch and Rupak Majumdar and Jakob Piribauer and Robin Ziemek 2021 Is Part Of LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2021.1 urn:nbn:de:0030-drops-140709 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.1 eng https://creativecommons.org/licenses/by/4.0/legalcode