Exploring Behaviors of Hybrid Systems via the Voronoi Bias over Output Signals
作者: Gidon Ernst, Jiří Fejlek
分类: eess.SY
发布日期: 2024-12-05
备注: 18 pages, 4 figures
💡 一句话要点
提出基于Voronoi偏置的混合系统验证算法，解决黑盒模型时序性质验证问题
🎯 匹配领域: 支柱一：机器人控制 (Robot Control)
关键词: 混合系统 形式化验证 黑盒模型 时序性质 Voronoi图
📋 核心要点
- 现有混合系统验证方法依赖输入覆盖，难以有效探索所有可能的输出行为。
- 提出基于Voronoi偏置的探索算法，直接在输出空间进行覆盖，无需特定行为的鲁棒性指导。
- 该算法能够验证鲁棒性不足以指导验证过程的复杂规范，提升验证能力。
📝 摘要（中文）
本文研究了基于仿真的混合系统时序性质分析，即需求验证（falsification）。我们提出了一种新颖的基于探索的算法，用于验证混合系统的黑盒模型，该算法基于输出空间中的Voronoi偏置。该方法受到最初用于运动规划的技术——快速探索随机树（RRT）的启发。与通常基于输入覆盖的探索不同，所提出的算法旨在直接覆盖所有可能的输出。与其他最先进的验证工具相比，它也不需要与特定行为相关的鲁棒性或其他指导指标。这使得我们的算法能够验证那些鲁棒性不足以指导验证过程的规范。
🔬 方法详解
问题定义：论文旨在解决混合系统黑盒模型的时序性质验证问题，即给定一个系统模型和一组时序逻辑规范，判断该模型是否满足这些规范。现有方法主要依赖于输入空间的覆盖，但由于混合系统的复杂性，输入空间的有效探索往往难以保证输出空间也能被充分覆盖，导致验证效率低下。此外，许多现有方法需要依赖鲁棒性指标来指导验证过程，但对于某些复杂规范，鲁棒性指标可能不够明确或难以计算，从而限制了这些方法的适用性。
核心思路：论文的核心思路是在输出空间直接进行探索，而不是像传统方法那样在输入空间进行探索。通过在输出空间构建Voronoi图，可以有效地引导探索过程，优先探索那些尚未被覆盖的区域。这种方法避免了对输入空间的盲目搜索，并能够更有效地发现违反规范的反例。此外，该方法不需要依赖鲁棒性指标，因此可以应用于更广泛的规范验证问题。
技术框架：该算法借鉴了快速探索随机树（RRT）的思想，但将其应用于输出空间。算法的主要流程如下：1. 初始化：在输出空间随机选择一个初始点。2. 迭代：重复以下步骤，直到满足停止条件： a. 在输出空间随机选择一个目标点。 b. 在已探索的输出点中，找到距离目标点最近的点。 c. 从该最近点出发，向目标点方向扩展一步，生成一个新的输出点。 d. 将新的输出点添加到已探索的输出点集合中，并更新Voronoi图。3. 验证：检查已探索的输出点集合是否覆盖了整个输出空间，或者是否发现了违反规范的反例。
关键创新：该论文的关键创新在于将Voronoi偏置引入到混合系统黑盒模型的验证过程中，实现了在输出空间直接进行探索。与传统的基于输入覆盖的方法相比，该方法能够更有效地探索系统的行为空间，并发现违反规范的反例。此外，该方法不需要依赖鲁棒性指标，因此可以应用于更广泛的规范验证问题。
关键设计：算法的关键设计包括：1. Voronoi图的构建和更新：Voronoi图用于指导探索过程，优先探索那些尚未被覆盖的区域。2. 步长选择：步长决定了每次探索的距离，需要根据具体问题进行调整。3. 停止条件：停止条件决定了算法何时停止探索，可以基于覆盖率、时间限制或反例发现等指标。
🖼️ 关键图片
📊 实验亮点
论文提出了一种新颖的基于Voronoi偏置的探索算法，用于验证混合系统的黑盒模型。该算法不需要依赖鲁棒性指标，可以应用于更广泛的规范验证问题。实验结果（具体数据未知）表明，该算法能够有效地探索系统的行为空间，并发现违反规范的反例，优于现有的基于输入覆盖的方法。具体的性能提升幅度未知。
🎯 应用场景
该研究成果可应用于各种混合系统的验证，例如自动驾驶系统、航空电子系统和机器人系统。通过验证这些系统的时序性质，可以提高其安全性和可靠性，减少潜在的故障和事故。此外，该方法还可以用于设计更健壮的控制策略，提高系统的性能和适应性。
📄 摘要（原文）
In this paper, we consider an analysis of temporal properties of hybrid systems based on simulations, so-called falsification of requirements. We present a novel exploration-based algorithm for falsification of black-box models of hybrid systems based on the Voronoi bias in the output space. This approach is inspired by techniques used originally in motion planning: rapidly exploring random trees. Instead of commonly employed exploration that is based on coverage of inputs, the proposed algorithm aims to cover all possible outputs directly. Compared to other state-of-the-art falsification tools, it also does not require robustness or other guidance metrics tied to a specific behavior that is being falsified. This allows our algorithm to falsify specifications for which robustness is not conclusive enough to guide the falsification procedure.