新パラダイム計算をねじふせる―多様な意味論的手法の合同・発展・応用

2015 年度 実績報告書

• 研究課題/領域番号: 24680001
• 研究機関: 東京大学
• 研究代表者: 蓮尾 一郎 東京大学, 情報理工学(系)研究科, 准教授 (60456762)
• 研究期間 (年度): 2012-04-01 – 2016-03-31
• キーワード: プログラム理論 / システム検証 / 形式検証 / 物理情報システム / ハイブリッドシステム / 関数型プログラミング / 量子計算 / 不動点論理

研究実績の概要

獲得目標１（ハイブリッドシステムの自動検証）については，超準アプローチにおけるスケーラビリティの課題を Cousot-Cousot の抽象解釈によって乗り越える試みについての論文が，抽象解釈とシステム検証に関する国際会議 VMCAI 2016 に採択された．また別に，産業界のモデルベース開発の現場における反例生成の重要性に鑑み，仕様記述言語（時相論理）に《平均化様相演算子》を導入して，確率的最適化による反例生成を効率化する研究について，論文がシステム検証分野のトップ国際会議 CAV 2015 に採択された．後者は特に優れた論文として，学術誌特集号への招待を受けた（現在査読中）．

獲得目標２（量子計算のための抽象機械）については，量子計算など（関数型計算における）一般の計算副作用について，GoI 式の抽象機械を一挙に与える圏論的枠組みについて研究を継続した．前年度得られた枠組み [Hoshino, Muroya & Hasuo, CSL-LICS 2014] に《再帰》を導入し，上記 GoI 抽象機械と（自然な，Plotkin & Power 式の）操作的意味論との間の関係性（妥当性 adequacy）を示した成果は，プログラミング言語分野のトップ国際会議 POPL 2016 に採択された．

さらに，上記獲得目標を含む具体的応用に通底する理論的基盤として，仕様記述のための不動点論理，特に最小不動点（活性）と最大不動点（安全性）が交替で現れる仕様の数学的基礎の研究に取り組んだ．この成果はプログラミング言語分野のトップ国際会議 POPL 2016 に採択された．このような交替性不動点論理式は，（様相μ計算で仕様が記述される）古典的なモデル検査においてはもちろん，近年では制御理論における recurrence や persistence など，より広いヘテロジニアス・システムの品質保証の文脈で重要視されており，今後上記成果の幅広い応用について研究を進めていく計画である．

現在までの達成度 (段落)

27年度が最終年度であるため、記入しない。

今後の研究の推進方策

27年度が最終年度であるため、記入しない。

次年度使用額が生じた理由

27年度が最終年度であるため、記入しない。

次年度使用額の使用計画

27年度が最終年度であるため、記入しない。

研究成果

• [国際共同研究] Univ. Bologna/INRIA Sophia Antipolis(イタリア)
  • 国名: イタリア
  • 外国機関名: Univ. Bologna/INRIA Sophia Antipolis
• [国際共同研究] University of Paris VII/Verimag(フランス)
  • 国名: フランス
  • 外国機関名: University of Paris VII/Verimag
• [国際共同研究] Radboud University(オランダ)
  • 国名: オランダ
  • 外国機関名: Radboud University
• [国際共同研究] Rice University(米国)
  • 国名: 米国
  • 外国機関名: Rice University
• [国際共同研究] University of Southampton/University of Bath(英国)
  • 国名: 英国
  • 外国機関名: University of Southampton/University of Bath
• [雑誌論文] Semantics of Higher-Order Quantum Computation via Geometry of Interaction (2016)
  • 著者名/発表者名: Ichiro Hasuo and Naohiko Hoshino
  • 雑誌名: Annals of Pure and Applied Logic 巻: 未定 ページ: 未定
  • 査読あり / 謝辞記載あり
• [雑誌論文] Healthiness from Duality (2016)
  • 著者名/発表者名: Wataru Hino, Hiroki Kobayashi, Ichiro Hasuo and Bart Jacobs
  • 雑誌名: Proc. Thirty-First Annual ACM/IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS 2016) 巻: なし ページ: 未定
  • 査読あり / 国際共著 / 謝辞記載あり
• [雑誌論文] Special Issue on Quantum Physics and Logic (QPL 2014) (2016)
  • 著者名/発表者名: Ichiro Hasuo and Prakash Panangaden, editors
  • 雑誌名: New Generation Computing 巻: 34 ページ: 1-152
  • DOI: 10.1007/s00354-016-0200-7
  • 国際共著
• [雑誌論文] Lattice-theoretic progress measures and coalgebraic model checking (2016)
  • 著者名/発表者名: Ichiro Hasuo, Shunsuke Shimizu, and Corina Cirstea
  • 雑誌名: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016 巻: なし ページ: 718-732
  • DOI: 10.1145/2837614.2837673
  • 査読あり / 国際共著 / 謝辞記載あり
• [雑誌論文] Memoryful Geometry of Interaction II: Recursion and Adequacy (2016)
  • 著者名/発表者名: Koko Muroya, Naohiko Hoshino and Ichiro Hasuo
  • 雑誌名: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016 巻: なし ページ: 748-760
  • DOI: 10.1145/2837614.2837672
  • 査読あり / 謝辞記載あり
• [雑誌論文] Abstract Interpretation with Infinitesimals: Towards Scalability in Nonstandard Static Analysis (2016)
  • 著者名/発表者名: Kengo Kido, Swarat Chaudhuri and Ichiro Hasuo
  • 雑誌名: Proc. Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016, Lecture Notes in Computer Science 巻: 9583 ページ: 229-249
  • DOI: 10.1007/978-3-662-49122-5_11
  • 査読あり / 国際共著 / 謝辞記載あり
• [雑誌論文] Near-Optimal Scheduling for LTL with Future Discounting (2016)
  • 著者名/発表者名: Shota Nakagawa and Ichiro Hasuo
  • 雑誌名: Proc. Trustworthy Global Computing - 10th International Symposium, TGC 2015, Lecture Notes in Computer Science 巻: 9533 ページ: 112-130
  • DOI: 10.1007/978-3-319-28766-9_8
  • 査読あり / 謝辞記載あり
• [雑誌論文] Coalgebraic Infinite Traces and Kleisli Simulations (2015)
  • 著者名/発表者名: Natsuki Urabe and Ichiro Hasuo
  • 雑誌名: Proc. 6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015, LIPIcs 巻: 35 ページ: 320-335
  • DOI: 10.4230/LIPIcs.CALCO.2015.320
  • 査読あり / オープンアクセス / 謝辞記載あり
• [雑誌論文] Generic Weakest Precondition Semantics from Monads Enriched with Order (2015)
  • 著者名/発表者名: Ichiro Hasuo
  • 雑誌名: Theoretical Computer Science 巻: 604 ページ: 2-29
  • DOI: 10.1016/j.tcs.2015.03.047
  • 査読あり
• [雑誌論文] Time Robustness in MTL and Expressivity in Hybrid System Falsification (2015)
  • 著者名/発表者名: Takumi Akazaki and Ichiro Hasuo
  • 雑誌名: Proc. Computer Aided Verification - 27th International Conference, CAV 2015, Lecture Notes in Computer Science 巻: 9207 ページ: 356-374
  • DOI: 10.1007/978-3-319-21668-3_21
  • 査読あり / 謝辞記載あり
• [学会発表] Healthiness from Duality (2016)
  • 著者名/発表者名: Wataru Hino, Hiroki Kobayashi, Ichiro Hasuo and Bart Jacobs
  • 学会等名: Thirty-First Annual ACM/IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS 2016)
  • 発表場所: New York City, USA
  • 年月日: 2016-07-05 – 2016-07-08
  • 国際学会
• [学会発表] Coalgebras and Higher-Order Computation: a GoI Approach (2016)
  • 著者名/発表者名: Ichiro Hasuo
  • 学会等名: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
  • 発表場所: Porto, Portugal
  • 年月日: 2016-06-22 – 2016-06-26
  • 国際学会 / 招待講演
• [学会発表] Lattice-theoretic progress measures and coalgebraic model checking (2016)
  • 著者名/発表者名: Ichiro Hasuo, Shunsuke Shimizu, and Corina Cirstea
  • 学会等名: The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016
  • 発表場所: St. Petersburg, Florida, United States
  • 年月日: 2016-01-20 – 2016-01-23
  • 国際学会
• [学会発表] Memoryful Geometry of Interaction II: Recursion and Adequacy (2016)
  • 著者名/発表者名: Koko Muroya, Naohiko Hoshino and Ichiro Hasuo
  • 学会等名: The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016
  • 発表場所: St. Petersburg, Florida, United States
  • 年月日: 2016-01-20 – 2016-01-23
  • 国際学会
• [学会発表] Abstract Interpretation with Infinitesimals: Towards Scalability in Nonstandard Static Analysis (2016)
  • 著者名/発表者名: Kengo Kido, Swarat Chaudhuri and Ichiro Hasuo
  • 学会等名: Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016
  • 発表場所: St. Petersburg, Florida, United States
  • 年月日: 2016-01-17 – 2016-01-19
  • 国際学会
• [学会発表] Near-Optimal Scheduling for LTL with Future Discounting (2015)
  • 著者名/発表者名: Shota Nakagawa and Ichiro Hasuo
  • 学会等名: Trustworthy Global Computing - 10th International Symposium, TGC 2015
  • 発表場所: Madrid, Spain
  • 年月日: 2015-08-31 – 2015-09-01
  • 国際学会
• [学会発表] Time Robustness in MTL and Expressivity in Hybrid System Falsification (2015)
  • 著者名/発表者名: Takumi Akazaki and Ichiro Hasuo
  • 学会等名: Computer Aided Verification - 27th International Conference, CAV 2015
  • 発表場所: San Fransisco, CA, USA
  • 年月日: 2015-07-18 – 2015-07-24
  • 国際学会
• [学会発表] Coalgebraic Infinite Traces and Kleisli Simulations (2015)
  • 著者名/発表者名: Natsuki Urabe and Ichiro Hasuo
  • 学会等名: 6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015
  • 発表場所: Nijmegen, the Netherlands
  • 年月日: 2015-06-24 – 2015-06-26
  • 国際学会
• [図書] 圏論の歩き方 (2015)
  • 著者名/発表者名: 圏論の歩き方委員会 (編集)
  • 総ページ数: 295
  • 出版者: 日本評論社
• [備考] 東京大学蓮尾研ウェブページ
  • URL: http://www-mmm.is.s.u-tokyo.ac.jp/
• [備考] 研究代表者個人ウェブページ
  • URL: http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/