用逻辑语言生成自动驾驶安全路径，兼顾安全性与计算效率。
Temporal Logic Guided Safe Navigation for Autonomous Vehicles
- 结合LTL与STL逻辑，先生成安全路径再求最优控制
- 在复杂场景下保持安全且计算时间可比传统方法
- 适合需要形式化安全保障的自动驾驶系统
自动驾驶车辆和地面机器人的安全验证对于其在不确定环境中的可靠运行至关重要。形式化语言工具为这类复杂人机系统提供了一种稳健且可靠的安全规则验证方法。本文提出一种混合方法，融合线性时序逻辑（LTL）和信号时序逻辑（STL）的优势，以生成自动驾驶车辆的安全轨迹和最优控制输入。采用基于LTL的符号路径规划生成形式化安全参考轨迹，随后利用混合整数线性规划（MILP）求解器在此轨迹基础上优化控制输入，同时满足由STL描述的状态、控制及安全约束。我们在两个环境中测试所提方案，并与主流路径规划算法进行对比。结果表明，相较于传统算法，该形式化安全方案在处理复杂规范场景时表现更优，同时保障了安全性并维持相近的计算时间。
原文摘要 · Abstract (English)
Safety verification for autonomous vehicles (AVs) and ground robots is crucial for ensuring reliable operation given their uncertain environments. Formal language tools provide a robust and sound method to verify safety rules for such complex cyber-physical systems. In this paper, we propose a hybrid approach that combines the strengths of formal verification languages like Linear Temporal Logic (LTL) and Signal Temporal Logic (STL) to generate safe trajectories and optimal control inputs for autonomous vehicle navigation. We implement a symbolic path planning approach using LTL to generate a formally safe reference trajectory. A mixed integer linear programming (MILP) solver is then used on this reference trajectory to solve for the control inputs while satisfying the state, control and safety constraints described by STL. We test our proposed solution on two environments and compare the results with popular path planning algorithms. In contrast to conventional path planning algorithms, our formally safe solution excels in handling complex specification scenarios while ensuring both safety and comparable computation times.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。