Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Efficient Discovery of Actual Causality using Abstraction-Refinement

Arshia Rafieioskouei, Borzoo Bonakdarpour

TL;DR

This article proposes a novel and effective method to formally reason about the causal effect of events in engineered systems, with application for finding the root-cause of safety violations in embedded and cyber-physical systems.

Abstract

Causality is the relationship where one event contributes to the production of another, with the cause being partly responsible for the effect and the effect partly dependent on the cause. In this paper, we propose a novel and effective method to formally reason about the causal effect of events in engineered systems, with application for finding the root-cause of safety violations in embedded and cyber-physical systems. We are motivated by the notion of actual causality by Halpern and Pearl, which focuses on the causal effect of particular events rather than type-level causality, which attempts to make general statements about scientific and natural phenomena. Our first contribution is formulating discovery of actual causality in computing systems modeled by transition systems as an SMT solving problem. Since datasets for causality analysis tend to be large, in order to tackle the scalability problem of automated formal reasoning, our second contribution is a novel technique based on abstraction-refinement that allows identifying for actual causes within smaller abstract causal models. We demonstrate the effectiveness of our approach (by several orders of magnitude) using three case studies to find the actual cause of violations of safety in (1) a neural network controller for a Mountain Car, (2) a controller for a Lunar Lander obtained by reinforcement learning, and (3) an MPC controller for an F-16 autopilot simulator.

Efficient Discovery of Actual Causality using Abstraction-Refinement

TL;DR

This article proposes a novel and effective method to formally reason about the causal effect of events in engineered systems, with application for finding the root-cause of safety violations in embedded and cyber-physical systems.

Abstract

Causality is the relationship where one event contributes to the production of another, with the cause being partly responsible for the effect and the effect partly dependent on the cause. In this paper, we propose a novel and effective method to formally reason about the causal effect of events in engineered systems, with application for finding the root-cause of safety violations in embedded and cyber-physical systems. We are motivated by the notion of actual causality by Halpern and Pearl, which focuses on the causal effect of particular events rather than type-level causality, which attempts to make general statements about scientific and natural phenomena. Our first contribution is formulating discovery of actual causality in computing systems modeled by transition systems as an SMT solving problem. Since datasets for causality analysis tend to be large, in order to tackle the scalability problem of automated formal reasoning, our second contribution is a novel technique based on abstraction-refinement that allows identifying for actual causes within smaller abstract causal models. We demonstrate the effectiveness of our approach (by several orders of magnitude) using three case studies to find the actual cause of violations of safety in (1) a neural network controller for a Mountain Car, (2) a controller for a Lunar Lander obtained by reinforcement learning, and (3) an MPC controller for an F-16 autopilot simulator.
Paper Structure (28 sections, 1 theorem, 11 equations, 9 figures, 1 table, 1 algorithm)

This paper contains 28 sections, 1 theorem, 11 equations, 9 figures, 1 table, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries -- Actual Causality
  3. Causal Models
  4. Causal Formulas
  5. Actual Causality
  6. SMT-based Discovery of Actual Causality
  7. Transition Systems
  8. SMT-based Formulation of Actual Causality
  9. Abstraction-Refinement for Causal Models
  10. Overall Idea
  11. Approximating Causal Transition Systems
  12. Detailed Description of the Algorithm
  13. Correctness
  14. Experimental Evaluation
  15. Implementation
  16. ...and 13 more sections

Key Result

Theorem 1

Let $\mathcal{T}$ be a concrete causal transition system and $\varphi_c$ and $\varphi_e$ be two causal formulas. If $\varphi_c$ is an actual cause of $\varphi_e$ identified by Algorithm alg:absref (for $\hat{\mathcal{T}}$ and $\check{\mathsf{Tr}}$), then $\varphi_c$ is an actual cause of $\varphi_e$

Figures (9)

  • Figure 1: Over/under-approximations of the concrete model and their relation to HP conditions of the form $\exists\exists\forall$.
  • Figure 2: Overall idea of our algorithm -- Steps of abstraction-refinement approach.
  • Figure 3: (a) Schematic of the mountain car example. (b) Graph illustrating the causal model and relationships between the variables at a snapshot in time $t$.
  • Figure 4: Three traces for the mountain car example.
  • Figure 5: HP conditions adapted for causal transition systems.
  • ...and 4 more figures

Theorems & Definitions (12)

  • Definition 1
  • Definition 2
  • Definition 3
  • Example 1
  • Example 2
  • Definition 4
  • Definition 5
  • Definition 6
  • Example 3
  • Example 4
  • ...and 2 more