2015 Fiscal Year Research-status Report
圏論と数理論理学によるものづくりサポート―ソフトウェア科学のシステム工学への移転
| Project/Area Number |
15KT0012
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
蓮尾 一郎 東京大学, 大学院情報理工学系研究科, 講師 (60456762)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
|
|---|
| Project Period (FY) |
2015-07-10 – 2019-03-31
|
| Keywords | 物理情報システム / モデルベース開発 / 形式検証 / ハイブリッドシステム / 数理論理学 / 圏論 / プログラム理論 / 不動点論理 |
|---|
| Outline of Annual Research Achievements |
具体的研究項目(A1-B2)に加え，それらに通底する理論的基盤について研究を進め，（いくつかのトップ国際会議論文を含む）複数の論文として成果を発表した．
[中川・蓮尾，TGC'16]においては，「できるだけ早く何かを実現したい」等の仕様を表現できる線形時相論理の割引付き解釈に対して，近最適スケジューラを求める方法を与えた．これは研究項目(A1,A2)に寄与する成果である．
プログラミング言語分野のトップ国際会議での論文[蓮尾・清水・Cirstea, POPL'16]においては，不動点論理，特に最小不動点（活性）と最大不動点（安全性）が交替で現れる仕様の数学的基礎の研究に取り組んだ．このような交替性不動点論理式は，モデル検査においてはもちろん，近年では制御理論など，より広いヘテロジニアス・システムの品質保証の文脈で重要視されており，この成果は研究項目(A1,A2,B2)に寄与する重要な成果である．今後この成果の応用を追求する予定であるが，特に(A1)に関して，Buechi 受理条件付き確率的システムの間の模倣関係について成果を得て，論文を投稿した[卜部・清水・蓮尾, 投稿中]．
システム検証分野のトップ国際会議での論文[赤崎・蓮尾, CAV'15]においては，モデルベース開発の現場における反例生成の重要性に鑑み，仕様記述言語（時相論理）に《平均化様相演算子》を導入して，確率的最適化による反例生成を効率化する研究を行った．これは特に優れた論文として学術誌特集号への招待を受けた（現在査読中）．この成果は産業界の現場において形式論理の果たしうる役割を示唆するものとして，本研究において重要なものと考える．
論文[木戸・蓮尾・Chaudhuri, VMCAI'16]においては，超準アプローチ（研究項目(B2)の基盤）におけるスケーラビリティの課題を抽象解釈によって乗り越える試みを行った．ここでは抽象領域として凸多面体を用いたが，楕円等を用いる拡張について現在研究を推進している．
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
研究計画に挙げた理論的獲得目標(A1-B2)に関する着実な研究成果はもちろん，それら研究目標のうちの複数に通底するような数学的知見，ブレイクスルーが得られており（たとえば[蓮尾・清水・Cirstea, POPL’16]の成果），理論的進捗は想定以上と言える．実践上の獲得目標についても，各論文に付随するツール実装はもとより，研究進展に伴う産業界との新たな協働が生まれつつあり，来年度以降の実践的な研究の体制づくりが順調に進んでいる．
|
| Strategy for Future Research Activity |
[蓮尾・清水・Cirstea, POPL’16] に得られた基本的成果について，理論面での拡張および応用面での活用を戦略的に進めていく．この際，隣接する諸領域（特にソフトウェア工学・システム工学・制御工学）とのより大規模な協働を模索する．産業界との新たな共同研究を研究遂行において活用する．
|
Research Products
(24 results)
-
-
-
-
-
-
[Journal Article] Healthiness from Duality2016
Author(s)
Wataru Hino, Hiroki Kobayashi, Ichiro Hasuo and Bart Jacobs
-
Journal Title
Proc. Thirty-First Annual ACM/IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS 2016)
Volume: なし
Pages: 682-691
DOI
Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
-
-
-
-
-
-
-
-
-
[Presentation] Healthiness from Duality2016
Author(s)
Wataru Hino, Hiroki Kobayashi, Ichiro Hasuo and Bart Jacobs
Organizer
Thirty-First Annual ACM/IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS 2016)
Place of Presentation
New York City, USA
Year and Date
2016-07-05 – 2016-07-08
Int'l Joint Research
-
-
-
-
-
-
-
-
-
