Towards Counterfactual Explanation and Assertion Inference for CPS Debugging

TL;DR

DeCaF is a framework that provides counterfactual explanations and assertions for debugging cyber-physical systems by identifying minimal input changes that fix failures and inferring interpretable success conditions.

Contribution

It introduces DeCaF, a novel approach combining counterfactual generation and causal models to improve CPS debugging insights and interpretability.

Findings

DeCaF successfully identifies minimal input changes to fix failures.

Different combinations of counterfactual generators and causal models optimize success rates.

DeCaF infers logical assertions that generalize recovery conditions for CPS.

Abstract

Verification and validation of cyber-physical systems (CPS) via large-scale simulation often surface failures that are hard to interpret, especially when triggered by interactions between continuous and discrete behaviors at specific events or times. Existing debugging techniques can localize anomalies to specific model components, but they provide little insight into the input-signal values and timing conditions that trigger violations, or the minimal, precisely timed changes that could have prevented the failure. In this article, we introduce DeCaF, a counterfactual-guided explanation and assertion-based characterization framework for CPS debugging. Given a failing test input, DeCaF generates counterfactual changes to the input signals that transform the test from failing to passing. These changes are designed to be minimal, necessary, and sufficient to precisely restore correctness. Then, it infers assertions as logical predicates over inputs that generalize recovery conditions in an interpretable form engineers can reason about, without requiring access to internal model details. Our approach combines three counterfactual generators with two causal models, and infers success assertions. Across three CPS case studies, DeCaF achieves its best success rate with KD-Tree Nearest Neighbors combined with M5 model tree, while Genetic Algorithm combined with Random Forest provides the strongest balance between success and causal precision.