| 研究課題/領域番号 |
15J09877
|
|---|
| 研究種目 |
特別研究員奨励費
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 国内 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
赤崎 拓未 東京大学, 情報理工学系研究科, 特別研究員(DC1)
|
|---|
| 研究期間 (年度) |
2015-04-24 – 2018-03-31
|
| 研究課題ステータス |
完了 (2017年度)
|
| 配分額 *注記 |
2,800千円 (直接経費: 2,800千円)
2017年度: 900千円 (直接経費: 900千円)
2016年度: 900千円 (直接経費: 900千円)
2015年度: 1,000千円 (直接経費: 1,000千円)
|
|---|
| キーワード | falsification / temporal logic / reinforcement learning / Bayesian network / Gaussian process / 入力生成問題 / quantitative logic / サイバーフィジカルシステム / 時相論理 / ロバスト意味論 |
|---|
| 研究実績の概要 |
上半期は、昨年度から継続して、元の仕様と因果関係をもつ他の条件も考慮して入力生成問題を解く枠組みについての研究を行った。既存の入力生成問題アルゴリズムにおいては、時相論理式の形で与えられた仕様について、その論理式のロバスト意味論で与えられる値を目的関数として最小化問題を解くことで、よりロバストさの小さい、すなわち仕様に反するシステムへの入力を導出するのであった。しかし仕様によっては目的関数の形状が疎、あるいは多峰になり、最小化問題が上手く解けない場合があった。本手法では、この問題を解決するため、(1)元の仕様の他に、それと因果関係を持つ付帯条件をベイジアンネットとして与え、(2)仕様に反する入力の導出を、ロバスト意味論の値の最小化ではなく、仕様が偽であるときの付帯条件の真偽値の分布との距離の最小化として行った。これによって、元の目的関数の形状が最適化に適していなくとも、付帯条件のいずれかが適していれば、それをヒントに入力生成問題を解くことができる。本成果に基づく論文は2017年9月19日イタリア・トリノで行われた査読付き国際学会FVAV 2017で採択されている。
下半期は、深層強化学習によるサイバーフィジカルシステム設計の誤り発見手法の開発を行った。本研究は国立研究開発法人産業技術総合研究所の技術研修として行われた。既存手法が入力生成問題をロバスト意味論の最小化問題として解いたのに対して、本手法ではこれを強化学習の問題として解くことを提案した。最大の利点のひとつは、既存手法ではシステムへの入力を予めフィードフォワードとしてしか与えられなかったのに対し、強化学習では各時刻において現在の状態を観測しながらフィードバックとして決定できる点である。本成果に基づく論文は2018年7月にイギリス・オックスフォードで行われる査読付き国際学会FM2018において採択済みである。
|
| 現在までの達成度 (段落) |
29年度が最終年度であるため、記入しない。
|
| 今後の研究の推進方策 |
29年度が最終年度であるため、記入しない。
|
