研究課題
ソフトウェア科学における諸手法のシステム工学への応用という最終目標に対して，研究内容面はもちろん，今後の研究体制の面でも大きな進展があった．まず，ソフトウェア科学の諸手法（特にプログラム論理による推論およびモデル検査）について，この圏論的本質を明らかにする理論的成果を理論計算機科学分野の旗艦国際会議および並行システム分野のトップ国際会議において予稿集論文として発表した[日野・小林・蓮尾・Jacobs, LICS’16] [卜部・清水・蓮尾，CONCUR’16] [卜部・原・蓮尾，LICS’17]．実際の工業製品はその複雑さゆえ既存の検証手法の直接の適用が困難であることが多い．しかしながら，既存の検証手法の基盤となる理論的アイデアを何らかのやり方で応用することは可能なはずである．この信念にもとづいた軽量形式手法の研究（検証や自動生成などの「高望み」でなく，たとえばテストやモニタリングの効率化を目指す）の一環として，時間つきオートマトンによって記述される仕様のパターンマッチ問題を高速に解くアルゴリズムの貢献を行った [和賀・赤崎・蓮尾，FORMATS’16]．研究体制の面では，本科研費研究と同じ最終目標に向けてより大きな規模で研究を行うプロジェクト（JST ERATO）を開始した．ここで雇用する研究員はさまざまな学術的背景を持ち（制御理論，ソフトウェア工学など），彼らとの協働による研究の多面化の効果がすでに顕れつつある．研究代表者のハイブリッドシステム分野の主要国際会議HSCCにおける2年連続のプログラム委員経験も含め，本科研費研究において，今後想定より遥かに幅広い研究活動と成果が期待される．
1: 当初の計画以上に進展している
研究計画に挙げた獲得目標に向けた成果はもちろん，当初想定を超えた多数の学術領域（ソフトウェア工学におけるテスト研究，数値最適化など）との協働が始まっており，今後これらの協働による多数の学術的成果が期待される．産業界との協働についても複数の企業と議論を行っているのみならず，より大規模の協働へ向けた体制が整いつつある．
JST ERATO プロジェクトと緊密に連携しながら，1) 産業界の実問題からスタートする実際的な姿勢，2) その中でも常に数学的本質・抽象性・一般性を志向する姿勢，この両者を保持し，「現代の抽象数学だからこそ可能な数学の社会応用」という本研究のテーマを追求していく．
研究の遂行にあたり少額の余剰が生じた．
次年度の予算と合わせ執行する．
すべて 2017 2016 その他
すべて 国際共同研究 (5件) 雑誌論文 (9件) (うち国際共著 3件、 査読あり 8件、 謝辞記載あり 5件、 オープンアクセス 2件) 学会発表 (7件) (うち国際学会 7件、 招待講演 1件) 備考 (2件)
Information and Computation
巻: 252 ページ: 110-137
https://doi.org/10.1016/j.ic.2016.03.007
Annals of Pure and Applied Logic
巻: 168 ページ: 404-469
https://doi.org/10.1016/j.apal.2016.10.010
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. ACM
巻: なし ページ: 833-845
10.1145/3009837.3009859
To appear in Proceedings of the Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) 2017
巻: なし ページ: 印刷中
Proc. Thirty-First Annual ACM/IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS 2016)
巻: なし ページ: 682-691
10.1145/2933575.2935319
Proc. 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal. LIPIcs 52, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik
巻: 52 ページ: 2:1-2:2
10.4230/LIPIcs.FSCD.2016.2
27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Quebec City, Canada. LIPIcs 59, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik
巻: 59 ページ: 24:1-24:15
10.4230/LIPIcs.CONCUR.2016.24
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
巻: 9884 ページ: 121-139
10.1007/978-3-319-44878-7_8
group-mmm.org/~ichiro
http://www.fos.kuis.kyoto-u.ac.jp/~ksuenaga/
