研究概要

自動運転に代表されるような複雑なサイバーフィジカルシステムでは，車両の運動力学といった連続ダイナミクスで記述される「連続的」機構と，センサやカメラなどから得られたデータから（ニューラルネットワークなどの）機械学習，すなわち AI により離散的に意思決定を行う「離散的」機構が混在したハイブリッドシステムとなります。このような複雑な制御システムにおいて，制御システムの安全性を保証することは極めて困難であり，解決するべき重要課題となっています。
そこで本研究では，形式手法と呼ばれる概念に基づき，AI による意思決定機構を含む制御システムに対し，安全性といった設計仕様を満たすかどうかの検証や制御系設計の構築を行っています。具体的には，図4に示すように，検証したい項目を時相論理式（Linear Temporal Logic, Signal Temporal Logic など）で記述し，機械学習により学習されたモデル（図4: Xの部分）が含まれるシステムが論理式を満たしているかどうかを，形式手法の枠組みに基づき網羅的に検証（モニタリング）します。時相論理は，制御システムの安全性や可到達性など様々な設計仕様を表現できる論理体系です。そして，制御仕様が満たされていない場合は，制御仕様を満たすようなコントローラの設計及び学習を，最適制御理論や強化学習の枠組みを用いることで行います。
本研究は，JST CREST 日仏共同提案「AI 集約型サイバーフィジカルシステムの形式的解析設計手法」（研究代表者：京都大学 末永幸平先生）の支援を受けたものです。

図4. 形式的検証，制御系設計のイメージ図