Item

Abstract

Causality has been the issue of philosophic debate since Hippocrates. It is
used in formal verification and testing, e.g., to explain counterexamples or
construct fault trees. Recent work defines actual causation in terms of Pearl's
causality framework, but most definitions brought forward so far struggle with
examples where one event preempts another one. A key point to capturing such
examples in the context of programs or distributed systems is a sound treatment
of control flow. We discuss how causal models should incorporate control flow
and discover that much of what Pearl/Halpern's notion of contingencies tries to
capture is captured better by an explicit modelling of the control flow in
terms of structural equations and an arguably simpler definition. Inspired by
causality notions in the security domain, we bring forward a definition of
causality that takes these control-variables into account. This definition
provides a clear picture of the interaction between control flow and causality
and captures these notoriously difficult preemption examples without secondary
concepts. We give convincing results on a benchmark of 34 examples from the
literature.