Efficient Discovery of Actual Causality in Stochastic Systems

TL;DR

This paper presents a novel method for efficiently identifying actual causes in stochastic systems by formulating the problem as an SMT challenge and employing an abstraction-refinement technique, validated through multiple case studies.

Contribution

It introduces a formal approach to discover probabilistic actual causes in noisy systems using SMT and an abstraction-refinement method for scalability.

Findings

Achieved up to 95% efficiency improvement in cause discovery.

Successfully identified causes of safety violations in three case studies.

Demonstrated effectiveness in complex stochastic system analysis.

Abstract

Identifying the actual cause of events in engineered systems is a fundamental challenge in system analysis. Finding such causes becomes more challenging in the presence of noise and stochastic behavior in real-world systems. In this paper, we adopt the notion of probabilistic actual causality by Fenton-Glynn, which is a probabilistic extension of Halpern and Pearl's actual causality, and propose a novel method to formally reason about causal effect of events in stochastic systems. We (1) formulate the discovery of probabilistic actual causes in computing systems as an SMT problem, and (2) address the scalability challenges by introducing an abstraction-refinement technique that improves efficiency by up to 95%. We demonstrate the effectiveness of our approach through three case studies, identifying probabilistic actual causes of safety violations in (1) the Mountain Car problem, (2) the Lunar Lander benchmark, and (3) MPC controller for an F-16 autopilot simulator.