Temporal Logic Guided Safe Navigation for Autonomous Vehicles

要約

自動運転車（AVS）と地上ロボットの安全検証は、不確実な環境を考慮して信頼できる操作を確保するために重要です。
正式な言語ツールは、このような複雑なサイバー物理システムの安全規則を検証するための堅牢で健全な方法を提供します。
この論文では、線形時間論理（LTL）や信号時間論的論理（STL）などの正式な検証言語の強度を組み合わせて、自律車両ナビゲーションの安全な軌跡と最適な制御入力を生成するハイブリッドアプローチを提案します。
LTLを使用してシンボリックパス計画アプローチを実装して、正式に安全な参照軌道を生成します。
次に、この参照軌道で混合整数線形プログラミング（MILP）ソルバーを使用して、STLによって記述された状態、制御、および安全上の制約を満たしながら、制御入力を解決します。
提案されたソリューションを2つの環境でテストし、結果を一般的なパス計画アルゴリズムと比較します。
従来のパス計画アルゴリズムとは対照的に、当社の正式に安全なソリューションは、安全性と同等の計算時間の両方を確保しながら、複雑な仕様シナリオの処理に優れています。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google