Efficient Discovery of Actual Causality using Abstraction-Refinement

📄 arXiv: 2407.16629v3 📥 PDF

作者: Arshia Rafieioskouei, Borzoo Bonakdarpour

分类: cs.LO, eess.SY

发布日期: 2024-07-23 (更新: 2024-08-30)

💡 一句话要点

提出基于抽象-精化的因果发现方法，用于定位嵌入式和CPS系统中的安全违规根因。

🎯 匹配领域: 支柱一：机器人控制 (Robot Control) 支柱二：RL算法与架构 (RL & Architecture)

关键词: 实际因果关系 抽象-精化 形式化方法 SMT求解 嵌入式系统

📋 核心要点

  1. 现有方法难以在大规模系统中高效地发现实际因果关系，尤其是在嵌入式和信息物理系统中定位安全违规的根本原因。
  2. 该方法通过抽象-精化策略，在较小的抽象模型中寻找潜在原因，然后逐步细化抽象，从而降低了计算复杂度。
  3. 实验表明，该方法在多个案例研究中显著提高了效率，包括神经网络控制器、强化学习控制器和MPC控制器。

📝 摘要（中文）

本文提出了一种新颖有效的方法，用于正式推理工程系统中事件的因果效应，并应用于查找嵌入式和信息物理系统中的安全违规的根本原因。我们的动机来自于Halpern和Pearl提出的实际因果关系的概念，该概念侧重于特定事件的因果效应，而不是试图对科学和自然现象进行一般性陈述的类型级因果关系。我们的第一个贡献是将计算系统中实际因果关系的发现建模为SMT求解问题，计算系统由转换系统建模。由于因果关系分析的数据集往往很大，为了解决自动形式推理的可扩展性问题，我们的第二个贡献是一种基于抽象-精化的新技术，该技术允许在较小的抽象因果模型中识别实际原因。我们通过三个案例研究证明了我们方法的有效性（提高了几个数量级），这些案例研究用于查找（1）Mountain Car的神经网络控制器，（2）通过强化学习获得的Lunar Lander的控制器，以及（3）F-16自动驾驶仪模拟器的MPC控制器中安全违规的实际原因。

🔬 方法详解

问题定义：论文旨在解决在复杂的计算系统中，如何高效地发现导致特定安全违规的实际因果关系。现有方法，特别是基于形式化方法的因果推理，在处理大规模系统时面临可扩展性问题，计算成本高昂。传统的类型级因果关系分析无法精确地定位特定事件的根本原因。

核心思路：论文的核心思路是利用抽象-精化技术来降低因果推理的计算复杂度。通过首先在抽象的模型上进行因果分析，快速排除大量不相关的事件，然后逐步细化抽象模型，聚焦于潜在的实际原因，最终确定导致安全违规的根本原因。这种方法避免了直接在大规模原始模型上进行推理，从而提高了效率。

技术框架：该方法包含以下主要阶段：1) 系统建模：将计算系统建模为转换系统。2) 抽象：构建原始模型的抽象模型，降低模型的复杂性。3) 因果分析：在抽象模型上进行因果分析，识别潜在的实际原因。4) 精化：如果抽象模型上的因果分析结果不够精确，则逐步细化抽象模型，增加模型的细节。5) 验证：在原始模型上验证最终确定的实际原因。整个流程迭代进行，直到找到满足要求的实际原因。

关键创新：该方法最重要的技术创新点在于将抽象-精化技术应用于实际因果关系的发现。与直接在原始模型上进行推理的方法相比，抽象-精化技术能够显著降低计算复杂度，提高效率。此外，将实际因果关系发现建模为SMT求解问题，为自动化因果分析提供了基础。

关键设计：论文中关于抽象和精化的具体策略（例如，如何选择抽象级别、如何细化抽象模型）以及SMT求解器的具体配置等技术细节未知。论文中使用的抽象方法和精化策略的选择会直接影响方法的效率和精度，这部分是实现该方法需要考虑的关键设计。

📊 实验亮点

实验结果表明，该方法在三个案例研究中显著提高了效率。具体来说，在Mountain Car的神经网络控制器、Lunar Lander的强化学习控制器和F-16自动驾驶仪模拟器的MPC控制器中，该方法能够有效地找到安全违规的实际原因，并且效率比传统方法提高了几个数量级。具体的性能数据和对比基线未知。

🎯 应用场景

该研究成果可应用于各种工程系统，特别是嵌入式系统、信息物理系统和控制系统等，用于诊断系统故障、定位安全漏洞、优化系统设计和提高系统可靠性。通过自动发现实际因果关系，可以帮助工程师快速定位问题的根本原因，并采取相应的措施进行修复和改进，从而降低维护成本和提高系统安全性。

📄 摘要（原文）

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.