• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2017 年度 実績報告書

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

研究課題

研究課題/領域番号 15J09877
研究機関東京大学

研究代表者

赤崎 拓未  東京大学, 情報理工学系研究科, 特別研究員(DC1)

研究期間 (年度) 2015-04-24 – 2018-03-31
キーワードfalsification / temporal logic / reinforcement learning / Bayesian network / Gaussian process
研究実績の概要

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

現在までの達成度 (段落)

29年度が最終年度であるため、記入しない。

今後の研究の推進方策

29年度が最終年度であるため、記入しない。

  • 研究成果

    (2件)

すべて 2017

すべて 雑誌論文 (1件) 学会発表 (1件) (うち国際学会 1件)

  • [雑誌論文] Causality-Aided Falsification2017

    • 著者名/発表者名
      Akazaki Takumi、Kumazawa Yoshihiro、Hasuo Ichiro
    • 雑誌名

      Electronic Proceedings in Theoretical Computer Science

      巻: 257 ページ: 3~18

    • DOI

      10.4204/EPTCS.257.2

  • [学会発表] Causality-Aided Falsification2017

    • 著者名/発表者名
      Takumi Akazaki
    • 学会等名
      First Workshop on Formal Verification of Autonomous Vehicles (FVAV 2017)
    • 国際学会

URL: 

公開日: 2018-12-17  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi