2019 Fiscal Year Annual Research Report
物理情報システムに対する軽量検証の、オートマトン的技法を用いた実用的発展
| Project/Area Number |
18J22498
|
|---|
| Research Institution | The Graduate University for Advanced Studies |
|---|
Principal Investigator |
和賀 正樹 総合研究大学院大学, 複合科学研究科, 特別研究員(DC1)
|
|---|
| Project Period (FY) |
2018-04-25 – 2021-03-31
|
| Keywords | モニタリング / 反例生成 / 軽量形式検証 / 物理情報システム / 時間オートマトン / パラメタ同定 / オートマトン学習 / 回帰型ニューラルネットワーク |
|---|
| Outline of Annual Research Achievements |
まず前年度に提案したモニタリング問題のためのアルゴリズムの高速化のために、アルゴリズムの開発及びツール実装を行った。国際会議予稿集論文として今年度発表した論文[Waga & Andre NFM'19]はこの方向の成果であり、文字列探索における「スキッピング」の技術を パラメタ付き時間パターンマッチング問題に応用したものである。また、モニタリング問題の更なる拡張のために、アルゴリズムの開発及びツール実装を行った。国際会議予稿集論文として今年度発表した論文 [Waga, Andre, & Hasuo, CAV'19] [Waga, FORMATS'19] はこの方向の成果であり、データや意味論を代数的に一般化したものである。特に、実時間システムの主要国際会議で発表された後者の論文においては、危険・安全の二値を出力する代わりに危険度合いを出力する、量的意味論を半環を用いて一般化した。本研究は国際会議 FORMATS 2019 において Oded Maler賞 (最優秀論文賞) を受賞した。
また、オートマトン学習を用いたテスト手法についてもアルゴリズムの開発や要素技術の研究を行った。国際会議予稿集論文として今年度採択された論文[Waga HSCC'20]においては物理情報システムについての反例生成問題を、オートマトン学習を経由して解く手法について研究を行った。国際会議予稿集論文として今年度発表または採択された論文[Okudono, Waga, Sekiyama, & Hasuo, AAAI'20] [Gutierrez, Okudono, Waga, & Hasuo, GECCO'20]においては重みつきオートマトンへの近似を介した、回帰型ニューラルネットワークのテストについての要素技術の研究を行った。
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
当初の計画について、計画以上の進展が得られた。CAVやAAAIといったトップ国際会議において論文を出版しつつFORMATSという実時間システム研究の主要国際会議にて最優秀論文賞を受賞するという、学術界におけるインパクトの高い成果を挙げることができた。特に今年度はオートマトン学習を用いたテストの研究成果という、物理情報システムの分野では新しい方向性の成果も挙げることができており、現在特許出願中である。さらに、これらの研究進展は理論から産業応用へ急速に裾野を広げつつあり、産業界とも協働を行っている。
|
| Strategy for Future Research Activity |
前年度はモニタリング問題を解くアルゴリズムの改良に加えて、物理情報システムや深層学習のテストについても取り組んだ。本年度も引き続き、モニタリング問題を解くアルゴリズムの改良に加えて、特に物理情報システムのテストの性能向上についても研究を進める。また、組込みシステムにおける軽量検証技術についても引き続き改良を進めていく。
|
