2018 Fiscal Year Research-status Report
圏論と数理論理学によるものづくりサポート―ソフトウェア科学のシステム工学への移転
| Project/Area Number |
15KT0012
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
蓮尾 一郎 国立情報学研究所, アーキテクチャ科学研究系, 准教授 (60456762)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
|
|---|
| Project Period (FY) |
2015-07-10 – 2020-03-31
|
| Keywords | 物理情報システム / 形式検証 / テスト / ハイブリッドシステム / 数理論理学 / 統計的機械学習 / 圏論 / プログラム理論 |
|---|
| Outline of Annual Research Achievements |
ソフトウェア科学における諸手法のシステム工学への応用という最終目標に対して，多様なトピックにおいて大きな進展があった．
まず，実システムに適用可能とするためのスケーラビリティの向上のため，確率的最適化をはじめとする統計的機械学習の活用に取り組んだ．具体的にはハイブリッドシステムの反例生成のための効率的アルゴリズムの研究に取り組み，既存の連続量最適化ベースの手法の実効性をモンテカルロ木探索により向上させた成果を，組込みシステム分野のトップ国際会議 EMSOFT'18 にて発表した．また，同種のアイデアを用いて，仕様における論理結合子の解釈という当該分野でよく知られた問題を解決した成果は，システム検証分野の旗艦国際会議 CAV'19に採択された．
昨年度から引き続き取り組んだ実行時モニタリングの研究においても，顕著な成果を上げた．具体的成果は以下の通り．1) ネットワークを介したモニタリングのための通信量圧縮のためのフィルタリング手法を考案し，EMSOFT'18（上述）に同じく採択された．この成果については特許出願中である．2) パリ13大学の研究者を長期滞在者として迎え，特にパラメータを許す仕様に対するモニタリング手法の研究が大きく進展した．この成果は，トップ国際会議 ICECCS'18 で最優秀論文賞を受けたのみならず，CAV'19（上述）や NFM'19 にも採択された．
その他，より理論的なトピックとして，確率的システムの静的解析手法としてのマルチンゲールの研究に取り組み，その成果をトップ国際会議 ATVA'18, TACAS'19 にて発表した．これらの手法を含む多様なシステム検証手法の論理的・圏論的基礎の研究もあわせて推進し，その成果の一つは理論計算機科学の旗艦国際会議である LICS'19 に採択された．
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
CAV, EMSOFT, LICS, TACAS, ATVA 等のトップ国際会議において論文を出版し，学術界におけるインパクトの高い成果を上げることができた．さらに，これらの研究進展は理論から産業応用へ急速に裾野を広げつつあり，産業界の5社あまりと協働を行っている．
|
| Strategy for Future Research Activity |
引き続き，メタ理論と産業応用の両輪を推進力とした形式手法研究を推進する．特に，統計的機械学習との協働をより強力に推進する．
|
| Causes of Carryover |
（理由）
予定していた海外出張でとりやめたものがあった．
（使用計画）
次年度の予算と合わせ使用する．
|
-
-
-
-
-
[Journal Article] Codensity Games for Bisimilarity2019
Author(s)
Yuichi Komorida, Shin-ya Katsumata, Nick Hu, Bartek Klin, Ichiro Hasuo
-
Journal Title
Proc. LICS 2019, Thirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science
Volume: -
Pages: -
DOI
Peer Reviewed / Int'l Joint Research
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
