2016 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 |
ソフトウェア科学における諸手法のシステム工学への応用という最終目標に対して，研究内容面はもちろん，今後の研究体制の面でも大きな進展があった．
まず，ソフトウェア科学の諸手法（特にプログラム論理による推論およびモデル検査）について，この圏論的本質を明らかにする理論的成果を理論計算機科学分野の旗艦国際会議および並行システム分野のトップ国際会議において予稿集論文として発表した[日野・小林・蓮尾・Jacobs, LICS’16] [卜部・清水・蓮尾，CONCUR’16] [卜部・原・蓮尾，LICS’17]．
実際の工業製品はその複雑さゆえ既存の検証手法の直接の適用が困難であることが多い．しかしながら，既存の検証手法の基盤となる理論的アイデアを何らかのやり方で応用することは可能なはずである．この信念にもとづいた軽量形式手法の研究（検証や自動生成などの「高望み」でなく，たとえばテストやモニタリングの効率化を目指す）の一環として，時間つきオートマトンによって記述される仕様のパターンマッチ問題を高速に解くアルゴリズムの貢献を行った [和賀・赤崎・蓮尾，FORMATS’16]．
研究体制の面では，本科研費研究と同じ最終目標に向けてより大きな規模で研究を行うプロジェクト（JST ERATO）を開始した．ここで雇用する研究員はさまざまな学術的背景を持ち（制御理論，ソフトウェア工学など），彼らとの協働による研究の多面化の効果がすでに顕れつつある．研究代表者のハイブリッドシステム分野の主要国際会議HSCCにおける2年連続のプログラム委員経験も含め，本科研費研究において，今後想定より遥かに幅広い研究活動と成果が期待される．
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
研究計画に挙げた獲得目標に向けた成果はもちろん，当初想定を超えた多数の学術領域（ソフトウェア工学におけるテスト研究，数値最適化など）との協働が始まっており，今後これらの協働による多数の学術的成果が期待される．産業界との協働についても複数の企業と議論を行っているのみならず，より大規模の協働へ向けた体制が整いつつある．
|
| Strategy for Future Research Activity |
JST ERATO プロジェクトと緊密に連携しながら，1) 産業界の実問題からスタートする実際的な姿勢，2) その中でも常に数学的本質・抽象性・一般性を志向する姿勢，この両者を保持し，「現代の抽象数学だからこそ可能な数学の社会応用」という本研究のテーマを追求していく．
|
| Causes of Carryover |
研究の遂行にあたり少額の余剰が生じた．
|
| Expenditure Plan for Carryover Budget |
次年度の予算と合わせ執行する．
|
-
-
-
-
-
-
-
-
[Journal Article] The geometry of parallelism: classical, probabilistic, and quantum effects2017
Author(s)
Ugo Dal Lago, Claudia Faggian, Benoit Valiron, Akira Yoshimizu
-
Journal Title
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. ACM
Volume: なし
Pages: 833-845
DOI
Peer Reviewed / Int'l Joint Research
-
-
-
[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
-
-
[Journal Article] Coalgebraic Trace Semantics for Buechi and Parity Automata2016
Author(s)
Natsuki Urabe, Shunsuke Shimizu, Ichiro Hasuo
-
Journal Title
27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Quebec City, Canada. LIPIcs 59, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik
Volume: 59
Pages: 24:1-24:15
DOI
Peer Reviewed / Open Access / Acknowledgement Compliant
-
[Journal Article] A Boyer-Moore Type Algorithm for Timed Pattern Matching2016
Author(s)
Masaki Waga, Takumi Akazaki, Ichiro Hasuo
-
Journal Title
Formal Modeling and Analysis of Timed Systems - 14th International Conference, FORMATS 2016, Quebec, QC, Canada, August 24-26, 2016, Proceedings. Lecture Notes in Computer Science 9884, Springer
Volume: 9884
Pages: 121-139
DOI
Peer Reviewed / 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
-
-
-
-
