国立情報学研究所（ＮＩＩ）の蓮尾一郎教授らは、自動運転車の安全性を数学的に証明する手法を開発した。車間距離を衝突回避可能な距離に保ちつつ、複数車の間を縫って車線を変更し非常停車するという複雑な運転シナリオに対応できた。このルールを順守する限り事故を起こさないことが数学的に証明される。自動車メーカーは事故時の責任問題に一定の答えを出せる。

自動車専用道で他車が前後や隣の車線を走っている状況で論理的安全を保証する手法を開発した。他車が急ブレーキをかけるなどしたら衝突不可避な可能性がある領域に入り込まないように車両を制御する。ただこのルールだけでは直進時の車間距離維持などの単純なシーンしか対応できなかった。

そこで微分フロイド・ホーア論理という形式論理の体系を提案した。微分方程式で表現される自動車のダイナミクスとプログラムを組み合わせる。自動運転の走行計画を分割してシーンごとに逐次的に解析できる。

シミュレーションでは車の間を縫って安全な路側帯に非常停車できた。周囲の車の状況など、シーンが変わる度に論理的安全を確かめて走行する。移動効率や乗り心地を追求するプログラムと並列させると安全を担保しながら走れる。