Efficient Discovery of Actual Causality in Stochastic Systems
Arshia Rafieioskouei, Kenneth Rogale, Borzoo Bonakdarpour
TL;DR
The paper tackles the problem of locating actual causes for safety-impairing events in stochastic systems by leveraging probabilistic actual causality (PAC). It introduces an SMT-based approach that encodes the DTMC model, the effect predicate, and a witness cause as an uninterpreted function, and complements it with an abstraction-refinement loop to scale to large models. The methods are validated on three CPS benchmarks—the Mountain Car, Lunar Lander, and an F-16 MPC controller—showing that abstraction-refinement can yield large efficiency gains (up to 95% in some cases) over direct SMT solving, especially for larger DTMCs. The work establishes a principled, scalable pathway for causal discovery in probabilistic settings and lays groundwork for applying PAC in real-world safety analysis of uncertain systems.
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.