• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

2016 Fiscal Year Research-status Report

圏論と数理論理学によるものづくりサポート―ソフトウェア科学のシステム工学への移転

Research Project

Project/Area Number 15KT0012
Research InstitutionThe 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

次年度の予算と合わせ執行する.

  • Research Products

    (23 results)

All 2017 2016 Other

All Int'l Joint Research (5 results) Journal Article (9 results) (of which Int'l Joint Research: 3 results,  Peer Reviewed: 8 results,  Acknowledgement Compliant: 5 results,  Open Access: 2 results) Presentation (7 results) (of which Int'l Joint Research: 7 results,  Invited: 1 results) Remarks (2 results)

  • [Int'l Joint Research] Univ. Bologna/INRIA Sophia Antipolis(イタリア)

    • Country Name
      ITALY
    • Counterpart Institution
      Univ. Bologna/INRIA Sophia Antipolis
  • [Int'l Joint Research] Univ. Paris VII/CentraleSupelec(フランス)

    • Country Name
      FRANCE
    • Counterpart Institution
      Univ. Paris VII/CentraleSupelec
  • [Int'l Joint Research] Radboud University(オランダ)

    • Country Name
      NETHERLANDS
    • Counterpart Institution
      Radboud University
  • [Int'l Joint Research] Univ. Bath/Univ. Southampton(英国)

    • Country Name
      UNITED KINGDOM
    • Counterpart Institution
      Univ. Bath/Univ. Southampton
  • [Int'l Joint Research] Arizona State Univ.(米国)

    • Country Name
      U.S.A.
    • Counterpart Institution
      Arizona State Univ.
  • [Journal Article] Quantitative simulations by matrices2017

    • Author(s)
      Natsuki Urabe, Ichiro Hasuo
    • Journal Title

      Information and Computation

      Volume: 252 Pages: 110-137

    • DOI

      https://doi.org/10.1016/j.ic.2016.03.007

    • Peer Reviewed
  • [Journal Article] Semantics of higher-order quantum computation via geometry of interaction2017

    • Author(s)
      Ichiro Hasuo, Naohiko Hoshino
    • Journal Title

      Annals of Pure and Applied Logic

      Volume: 168 Pages: 404-469

    • DOI

      https://doi.org/10.1016/j.apal.2016.10.010

    • Peer Reviewed
  • [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

      10.1145/3009837.3009859

    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] The Geometry of Concurrent Interaction: Handling Multiple Ports by Way of Multiple Tokens2017

    • Author(s)
      Ugo Dal Lago, Ryo Tanaka and Akira Yoshimizu
    • Journal Title

      To appear in Proceedings of the Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) 2017

      Volume: なし Pages: 印刷中

    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] Categorical Liveness Checking by Corecursive Algebras2017

    • Author(s)
      Natsuki Urabe, Masaki Hara and Ichiro Hasuo
    • Journal Title

      To appear in Proceedings of the Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) 2017

      Volume: なし Pages: 印刷中

    • Peer Reviewed / Acknowledgement Compliant
  • [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

      10.1145/2933575.2935319

    • Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
  • [Journal Article] Coalgebras and Higher-Order Computation: a GoI Approach2016

    • Author(s)
      Ichiro Hasuo
    • Journal Title

      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

      Volume: 52 Pages: 2:1-2:2

    • DOI

      10.4230/LIPIcs.FSCD.2016.2

    • Open Access / 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

      10.4230/LIPIcs.CONCUR.2016.24

    • 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

      10.1007/978-3-319-44878-7_8

    • Peer Reviewed / Acknowledgement Compliant
  • [Presentation] The Geometry of Concurrent Interaction: Handling Multiple Ports by Way of Multiple Tokens2017

    • Author(s)
      Ugo Dal Lago, Ryo Tanaka and Akira Yoshimizu
    • Organizer
      Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) 2017
    • Place of Presentation
      Reykjavik, Iceland
    • Year and Date
      2017-06-20 – 2017-06-23
    • Int'l Joint Research
  • [Presentation] The geometry of parallelism: classical, probabilistic, and quantum effects2017

    • Author(s)
      Ugo Dal Lago, Claudia Faggian, Benoit Valiron, Akira Yoshimizu
    • Organizer
      44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017
    • Place of Presentation
      Paris, France
    • Year and Date
      2017-01-15 – 2017-01-21
    • Int'l Joint Research
  • [Presentation] A Boyer-Moore Type Algorithm for Timed Pattern Matching2016

    • Author(s)
      Masaki Waga, Takumi Akazaki, Ichiro Hasuo
    • Organizer
      Formal Modeling and Analysis of Timed Systems - 14th International Conference, FORMATS 2016
    • Place of Presentation
      Quebec City, Canada
    • Year and Date
      2016-08-24 – 2016-08-26
    • Int'l Joint Research
  • [Presentation] Coalgebraic Trace Semantics for Buechi and Parity Automata2016

    • Author(s)
      Natsuki Urabe, Shunsuke Shimizu, Ichiro Hasuo
    • Organizer
      27th International Conference on Concurrency Theory, CONCUR 2016
    • Place of Presentation
      Quebec City, Canada
    • Year and Date
      2016-08-23 – 2016-08-26
    • Int'l Joint Research
  • [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
  • [Presentation] Coalgebras and Higher-Order Computation: a GoI Approach2016

    • Author(s)
      Ichiro Hasuo
    • Organizer
      1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
    • Place of Presentation
      Porto, Portugal
    • Year and Date
      2016-06-22 – 2016-06-26
    • Int'l Joint Research / Invited
  • [Presentation] Categorical Liveness Checking by Corecursive Algebras2016

    • Author(s)
      Natsuki Urabe, Masaki Hara, Ichiro Hasuo
    • Organizer
      Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) 2017
    • Place of Presentation
      Reykjavik, Iceland
    • Year and Date
      2016-06-20 – 2016-06-23
    • Int'l Joint Research
  • [Remarks] 研究代表者個人ウェブページ

    • URL

      group-mmm.org/~ichiro

  • [Remarks] 研究分担者個人ウェブページ

    • URL

      http://www.fos.kuis.kyoto-u.ac.jp/~ksuenaga/

URL: 

Published: 2018-01-16   Modified: 2022-10-18  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi