情報・システム研究機構 国立情報学研究所（以下：NII）の蓮尾一郎教授らは、車の自動運転システムの安全性に強い数学的保証を与える技術と基礎理論を明示した。
背景
自動運転のような複雑なシステムの安全性を数学的に証明することは一般的に困難だが、RSSは交通安全のためのルールを数式で書き表すことによって、自動運転車の安全性を数学的に証明するという。RSSで示した論理的安全ルールは、メーカー・車種問わず、国際規格や業界標準・交通法規として活用できるため、自動運転の社会受容を大きく加速すると期待されている。
研究手法・成果
RSSは技術的な基盤が発達しておらず、単純な運転シナリオに対する衝突回避のみをターゲットとしていたが、新たな拡張であるGA-RSSを提案した。GA-RSSは、dFHL（differential Floyd-Hoare logic、微分フロイド・ホーア論理）を提案し、論理的安全ルールの導出ワークフローとソフトウェアサポートを設計・実装。「車との衝突を回避しながら安全な地点で非常停止する」といった目標のある複雑な運転シナリオに対しても、論理的安全ルールを策定し、正しさを証明できたという。
今後の展望
GA-RSSは、産業界での安全性保証の取り組みや国際規格策定に向けた動きに大きく貢献できると確信したという。GA-RSSの活用で、RSSの考え方が広く適用できるようになり、自動運転の様々な状況下での安全性に数学的証明ができれば、自動運転に対する不安を払拭でき、社会普及と産業発展へ向けた大きな弾みになるとしている。
情報・システム研究機構 国立情報学研究所 アーキテクチャ科学研究系教授 蓮尾 一郎 氏のコメント
証明を書くための言語（論理体系）を設計し、証明を書く営みにソフトウェアによるサポートを与えるのが、形式論理学の研究を行ってきた我々の社会貢献のミッションです。今回は、マツダ株式会社の皆様との協働の機会を得て、自動運転という重要な応用分野に対し貢献を行うことができました。
長年研ぎ澄ましてきた理論的研究が今回（応用上の）日の目を見たと思っていますし、また同時に、数学的・理論的な基礎研究の重要性を示す一例でもあると考えています。
ERATO MMSDプロジェクトは、他プロジェクト（MIRAI eAIプロジェクト、CREST CyPhAIプロジェクト、CREST ZT-IoTプロジェクト等）とともに、NIIの包括的ソフトウェア研究拠点としての活動の一翼を担っています。
ERATO MMSDプロジェクトは、特にソフトウェア科学の理論的・数学的基盤の追究を通じて、物理情報システム・人工知能システム・システムセキュリティなど、新たな応用分野への貢献を行っていきます。
