Efficient Discovery of Actual Causality in Stochastic Systems
作者: Arshia Rafieioskouei, Kenneth Rogale, Borzoo Bonakdarpour
分类: eess.SY
发布日期: 2025-07-11 (更新: 2025-11-19)
💡 一句话要点
提出一种基于SMT和抽象精化的方法，高效发现随机系统中事件的概率性实际原因。
🎯 匹配领域: 支柱一：机器人控制 (Robot Control)
关键词: 概率性因果推理 SMT求解 抽象精化 随机系统 系统分析
📋 核心要点
- 现实系统中噪声和随机性使得确定事件的实际原因变得困难，现有方法难以有效处理。
- 将概率性实际因果关系发现形式化为SMT问题，并采用抽象-精化技术提高效率。
- 在Mountain Car、Lunar Lander和F-16自动驾驶仪等案例中验证了方法的有效性，效率提升高达95%。
📝 摘要（中文）
在工程系统中，识别事件的实际原因是系统分析中的一项基本挑战。在现实世界的系统中，由于噪声和随机行为的存在，寻找这些原因变得更具挑战性。本文采用了Fenton-Glynn提出的概率性实际因果关系的概念，它是Halpern和Pearl的实际因果关系的概率性扩展，并提出了一种新的方法来正式推理随机系统中事件的因果效应。我们（1）将计算系统中概率性实际原因的发现形式化为一个SMT问题，并且（2）通过引入一种抽象-精化技术来解决可扩展性挑战，该技术将效率提高了高达95%。我们通过三个案例研究证明了我们方法的有效性，识别了（1）Mountain Car问题，（2）Lunar Lander基准，以及（3）F-16自动驾驶仪模拟器的MPC控制器中安全违规的概率性实际原因。
🔬 方法详解
问题定义：论文旨在解决在随机系统中，如何高效准确地识别事件的概率性实际原因的问题。现有方法在处理具有噪声和随机行为的复杂系统时，面临着可扩展性和计算效率的挑战，难以在合理的时间内找到实际原因。
核心思路：论文的核心思路是将概率性实际因果关系的发现问题转化为一个可使用SMT求解器解决的形式化问题。通过将系统行为建模为逻辑公式，并利用SMT求解器进行推理，可以自动地找到导致特定事件发生的概率性实际原因。为了提高效率，引入了抽象-精化技术，通过简化模型来加速求解过程。
技术框架：该方法包含以下主要步骤：1. 系统建模：将随机系统建模为状态转移系统，并用逻辑公式表示系统行为。2. 因果关系形式化：使用Fenton-Glynn的概率性实际因果关系定义，将因果关系形式化为逻辑约束。3. SMT编码：将因果关系发现问题编码为SMT问题。4. 抽象-精化：使用抽象模型进行初步求解，如果抽象模型无法找到解，则逐步精化模型，直到找到解或达到最大精化次数。5. 求解：使用SMT求解器求解SMT问题，得到概率性实际原因。
关键创新：该论文的关键创新在于将概率性实际因果关系发现问题形式化为SMT问题，并引入了抽象-精化技术来提高求解效率。与传统的因果推理方法相比，该方法能够处理随机系统中的不确定性，并能够自动地找到实际原因。抽象-精化技术显著减少了SMT求解器的搜索空间，提高了求解效率。
关键设计：抽象-精化技术的关键在于如何选择合适的抽象级别和精化策略。论文中采用了一种基于状态空间划分的抽象方法，将状态空间划分为若干个抽象状态，并使用抽象状态之间的转移关系来近似原始系统的行为。精化策略则根据SMT求解器的反馈信息，逐步细化抽象状态的划分，直到找到解或达到最大精化次数。具体的参数设置和损失函数（如果存在）在论文中未明确说明，可能需要参考相关文献或实验结果进行调整。
📊 实验亮点
实验结果表明，该方法在Mountain Car、Lunar Lander和F-16自动驾驶仪等案例中能够有效地识别安全违规的概率性实际原因。与没有使用抽象-精化技术的基线方法相比，该方法的效率提高了高达95%，证明了抽象-精化技术在提高求解效率方面的显著优势。具体的性能数据和对比基线在论文中给出了详细的定量分析。
🎯 应用场景
该研究成果可应用于各种工程系统，例如自动驾驶、机器人、航空航天等领域，用于诊断系统故障、识别安全隐患、优化系统设计。通过自动发现事件的概率性实际原因，可以帮助工程师更好地理解系统行为，提高系统的可靠性和安全性，并降低维护成本。
📄 摘要（原文）
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.