形式的手法とサイバーフィジカルシステム設計開発との相互拡張

点击翻译按钮获取中文摘要

上半期は、昨年度から継続して、元の仕様と因果関係をもつ他の条件も考慮して入力生成問題を解く枠組みについての研究を行った。既存の入力生成問題アルゴリズムにおいては、時相論理式の形で与えられた仕様について、その論理式のロバスト意味論で与えられる値を目的関数として最小化問題を解くことで、よりロバストさの小さい、すなわち仕様に反するシステムへの入力を導出するのであった。しかし仕様によっては目的関数の形状が疎、あるいは多峰になり、最小化問題が上手く解けない場合があった。本手法では、この問題を解決するため、(1)元の仕様の他に、それと因果関係を持つ付帯条件をベイジアンネットとして与え、(2)仕様に反する入力の導出を、ロバスト意味論の値の最小化ではなく、仕様が偽であるときの付帯条件の真偽値の分布との距離の最小化として行った。これによって、元の目的関数の形状が最適化に適していなくとも、付帯条件のいずれかが適していれば、それをヒントに入力生成問題を解くことができる。本成果に基づく論文は2017年9月19日イタリア・トリノで行われた査読付き国際学会FVAV 2017で採択されている。下半期は、深層強化学習によるサイバーフィジカルシステム設計の誤り発見手法の開発を行った。本研究は国立研究開発法人産業技術総合研究所の技術研修として行われた。既存手法が入力生成問題をロバスト意味論の最小化問題として解いたのに対して、本手法ではこれを強化学習の問題として解くことを提案した。最大の利点のひとつは、既存手法ではシステムへの入力を予めフィードフォワードとしてしか与えられなかったのに対し、強化学習では各時刻において現在の状態を観測しながらフィードバックとして決定できる点である。本成果に基づく論文は2018年7月にイギリス・オックスフォードで行われる査読付き国際学会FM2018において採択済みである。