Safety Verification and Navigation for Autonomous Vehicles based on Signal Temporal Logic Constraints

📄 arXiv: 2409.10689v1 📥 PDF

作者: Aditya Parameshwaran, Yue Wang

分类: eess.SY, cs.RO

发布日期: 2024-09-16

备注: 6 pages, 3 figures, SAE WCX 2023 Conference

💡 一句话要点

提出基于信号时序逻辑约束的MPC控制器，用于自动驾驶车辆的安全验证与导航。

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

关键词: 自动驾驶 安全验证 信号时序逻辑 模型预测控制 鲁棒性 sTaliro 安全导航

📋 核心要点

  1. 自动驾驶车辆的复杂性日益增加，安全验证变得至关重要，尤其是在导航等安全关键任务中。
  2. 论文提出了一种基于信号时序逻辑（STL）约束的模型预测控制（MPC）方法，以确保自动驾驶车辆的安全导航。
  3. 通过在不同测试场景下验证，证明了该控制器能够安全地导航自动驾驶车辆模型，并满足预设的STL安全规范。

📝 摘要（中文）

现代自动驾驶车辆(AV)的软件架构日趋复杂，因此安全验证成为大规模部署前的重要任务。对于导航中的安全关键任务，必须在部署前对规划算法提出的轨迹执行验证程序。信号时序逻辑(STL)约束可以规定AV的安全要求，多个STL约束的组合称为规范。STL与其他逻辑约束的关键区别在于，STL允许我们处理连续信号。我们通过计算规范内每个信号的鲁棒性值来验证STL规范的满足情况。较高的鲁棒性值表示系统更安全。模型预测控制(MPC)是控制AV导航最广泛使用的方法之一，它具有底层的状态和输入约束。本研究旨在制定和测试一个以STL规范作为约束的MPC控制器，该控制器可以安全地导航AV。成本函数的主要目标是最小化控制输入。STL约束将作为额外的约束层，根据手头的场景和任务而变化。我们建议使用sTaliro，一个基于MATLAB的STL规范鲁棒性计算器，以递推时域控制的方式用于AV导航任务。它输入一个简化的AV状态空间模型和一组STL规范，并据此构建一个闭环控制器。我们在不同的测试用例/场景中测试了我们的控制器，并验证了我们的AV模型的安全导航。

🔬 方法详解

问题定义：自动驾驶车辆的导航需要保证安全性，传统的MPC方法虽然常用，但缺乏对复杂安全规范的有效建模和验证手段。现有方法难以处理连续信号，并且难以将复杂的安全规则融入到控制过程中。因此，如何设计一个能够满足复杂安全规范，并能处理连续信号的自动驾驶车辆导航控制器是一个挑战。

核心思路：论文的核心思路是将信号时序逻辑（STL）作为MPC控制器的约束条件，利用STL能够描述连续信号和复杂时序逻辑的特点，将安全规范转化为可量化的约束，从而在优化过程中保证车辆的安全。通过最大化STL的鲁棒性值，确保车辆在满足安全规范的同时，尽可能地优化控制输入。

技术框架：该方法采用基于sTaliro的递推时域控制框架。首先，将自动驾驶车辆的状态空间模型和STL安全规范输入到sTaliro中。sTaliro计算当前状态下STL规范的鲁棒性值。然后，将鲁棒性值作为MPC控制器的约束条件，通过优化控制输入，使得车辆在满足安全规范的同时，尽可能地接近目标。最后，将计算得到的控制输入作用于车辆，并重复上述过程，实现递推时域控制。

关键创新：该方法的关键创新在于将STL规范直接融入到MPC控制器的设计中，从而能够显式地考虑安全约束。与传统的基于规则或人工势场的方法相比，该方法能够更灵活地处理复杂的安全规范，并能够保证车辆在满足安全规范的同时，尽可能地优化控制性能。此外，利用sTaliro进行鲁棒性计算，能够有效地处理连续信号，并提供量化的安全指标。

关键设计：该方法的关键设计包括：1) STL规范的选取，需要根据具体的应用场景和安全需求进行设计；2) MPC控制器的成本函数设计，需要在安全性和控制性能之间进行权衡；3) sTaliro的参数设置，需要根据车辆的动力学特性和计算资源进行调整。论文中成本函数主要目标是最小化控制输入。sTaliro作为MATLAB工具箱，其具体参数设置未知。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

论文通过在不同的测试用例/场景中测试了所提出的控制器，验证了自动驾驶车辆模型的安全导航。虽然论文中没有给出具体的性能数据和对比基线，但实验结果表明，该控制器能够有效地满足预设的STL安全规范，并能够安全地导航自动驾驶车辆。具体的性能提升幅度未知。

🎯 应用场景

该研究成果可应用于各种自动驾驶场景，例如城市道路自动驾驶、高速公路自动驾驶、以及特定区域的自动驾驶物流等。通过将安全规范转化为STL约束，可以提高自动驾驶系统的安全性和可靠性，降低事故风险。此外，该方法还可以应用于其他需要安全保障的控制系统，例如机器人控制、航空航天控制等。

📄 摘要（原文）

The software architecture behind modern autonomous vehicles (AV) is becoming more complex steadily. Safety verification is now an imminent task prior to the large-scale deployment of such convoluted models. For safety-critical tasks in navigation, it becomes imperative to perform a verification procedure on the trajectories proposed by the planning algorithm prior to deployment. Signal Temporal Logic (STL) constraints can dictate the safety requirements for an AV. A combination of STL constraints is called a specification. A key difference between STL and other logic constraints is that STL allows us to work on continuous signals. We verify the satisfaction of the STL specifications by calculating the robustness value for each signal within the specification. Higher robustness values indicate a safer system. Model Predictive Control (MPC) is one of the most widely used methods to control the navigation of an AV, with an underlying set of state and input constraints. Our research aims to formulate and test an MPC controller, with STL specifications as constraints, that can safely navigate an AV. The primary goal of the cost function is to minimize the control inputs. STL constraints will act as an additional layer of constraints that would change based on the scenario and task on hand. We propose using sTaliro, a MATLAB-based robustness calculator for STL specifications, formulated in a receding horizon control fashion for an AV navigation task. It inputs a simplified AV state space model and a set of STL specifications, for which it constructs a closed-loop controller. We test out our controller for different test cases/scenarios and verify the safe navigation of our AV model.