Formal Verification of Intersection Safety for Automated Driving

要約

私たちは、責任に敏感な安全性 (RSS) の形式化に関する最近の研究を基礎として、交差点シナリオにおける制御戦略の安全性の数学的証明を可能にする最初の形式的なフレームワークを提示します。
車両間の相互作用が複雑であるため、交差点のシナリオは困難です。
これに対処するために、前回の研究のプログラム ロジック dFHL を拡張し、安全性を確保する RSS 条件をアルゴリズムが自動的に検出できるハイブリッド制御フロー グラフの新しい形式を導入しました。
このように発見された RSS 条件は実験的に評価されます。
私たちは、それが安全であることを観察し (安全性の証明が示すように)、過度に保守的ではありません。

要約(オリジナル)

We build on our recent work on formalization of responsibility-sensitive safety (RSS) and present the first formal framework that enables mathematical proofs of the safety of control strategies in intersection scenarios. Intersection scenarios are challenging due to the complex interaction between vehicles; to cope with it, we extend the program logic dFHL in the previous work and introduce a novel formalism of hybrid control flow graphs on which our algorithm can automatically discover an RSS condition that ensures safety. An RSS condition thus discovered is experimentally evaluated; we observe that it is safe (as our safety proof says) and is not overly conservative.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google