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

Declarative Distirbuted Programming based on Combinatorial Topology

Research Project

Project/Area Number 20K11678
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeMulti-year Fund
Section一般
Review Section Basic Section 60010:Theory of informatics-related
Research InstitutionKyoto University

Principal Investigator

西村 進  京都大学, 理学研究科, 准教授 (10283681)

Project Period (FY) 2020-04-01 – 2025-03-31
Project Status Granted (Fiscal Year 2023)
Budget Amount *help
¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000)
Fiscal Year 2024: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2023: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2022: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2021: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2020: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Keywords並行分散計算 / 分散計算の数理論理モデル / 認識μ計算 / 宣言的プログラミング / 数理論理モデル / 並行分散システム / 組合せトポロジー
Outline of Research at the Start

並行分散計算の組合せトポロジー論は、幾何的モデルを用いて並行分散システムの振舞いについて理解を得るための手法である。本研究は、この組合せトポロジー論の適用範囲を従来より強力な計算モデルにまで拡張し、並行分散システムの計算構造を宣言的に記述するプログラミング手法を提案する。これによって並行分散システムを、並行プロセス毎の逐次プログラムの寄せ集めではなく、一体のシステムとして宣言的にプログラミングすることを可能にする。また、このような宣言的記述から、実行可能なプログラムを自動的に導出する手法を与える。導出されたプログラムが効率よく実行されるような最適化の技法も合わせて開発する。

Outline of Annual Research Achievements

本年度は、前年度終わりに行った大学院生2名との共同研究について、2023年初夏に独DagstuhlのLiebniz Center for Informaticsで開催された研究集会で発表を行った。この研究集会はインフォーマルなものではあるが、分散並列計算の組合せ幾何的モデルから派生して近年注目を集めている分散並列計算の認識論理モデルについて先導的な仕事を行っている研究者が集まって行われたものである。発表の具体的な内容としては、故障が起こり得る分散システムで同期メッセージ通信プロトコルによって分散合意問題が不可解であることを認識論理モデルを用いて示すために、分散同期メッセージ通信の単体的複体モデルに適合した認識論理モデルの構成方法を与え、さらに不可解性を示すための障害論理式を与えることができたことを報告した。
また、前年度の研究結果である、並列分散システム中のプロセスが何度でも情報を交換できる複ラウンド計算モデルに対してk集合合意問題の不可解性を示すための障害論理式を認識μ計算を用いて定義する手法に関する論文が国際学術誌に採録された。
これらは、Goubaultらによって提起された並列分散計算の認識論理モデルが種々の分散合意問題の不可解に対して適用可能であることを示すと同時に、単体的複体モデルと比べたときの限界を示すことを示唆する重要な成果である。
これまでの研究により得られた、並列分散計算の組合せトポロジーモデルと認識論理モデルの間の対応から、分散並行計算を宣言的に記述するためのプログラミング手法についての重要な着想を得ることができ、その着想を具体的な形にするため研究を進めているところである。

Current Status of Research Progress
Current Status of Research Progress

3: Progress in research has been slightly delayed.

Reason

当該年度までの研究により、分散計算の認識論理モデルにおいて、分散計算問題の不可解性を具体的な障害論理式を用いて証明することが可能であることを示すことができた。認識論理モデルと障害論理式はもともとGoubaultらにより提唱されたものであったが、その理論的枠組みがどのような状況で具体的に適用可能かは検証されていなかった。本研究により、分散計算の多ラウンド実行については認識μ計算による認識論理の拡張で、プロセス間で互いの故障が関知可能であるような分散同期メッセージ通信プロトコルについては故障を加味した積更新モデルの拡張で対応できることが示され、それぞれに対する適切な障害論理式を具体的に与えることに成功した。これらは、分散計算の単体的複体モデルと比べたときの認識論理モデルの有効性と限界を示すと同時に、単体的複体モデルによって表される計算現象の本質を示唆する重要な成果であると考える。
その一方で、宣言的分散並列プログラミングについてはまだ大きな成果を出せていない。しかしながら、上述の計算モデルに関する根源的な理解を元に、重要な着想を最近になって受け、その考えに基づいて研究を初めたところである。

Strategy for Future Research Activity

宣言的並行分散プログラミングを実現するための理論的枠組みを構築する予定である。
通常の並行分散プログラミングでは、個別のプロセス毎にその動作をプログラムで規定する。これは、単体的複体モデルにおいて単体的複体が含む各点をどのように変換するかを規定することに相当する。一方、これまで行ってきた並行分散システムの認識論理モデルの研究が示唆するのは、各点の変換ではなく、単体的複体モデルのファセット(によって表される並行プロセスの集合)の変換こそが並行分散計算で本質的だということである。この考え方に基づいて、従来とはまったく異なるプログラミングパラダイムの提案を見ざして研究を進めていく。これを実現するための課題としては、単体的複体モデルの各ファセットを一意に特定するための効率的な方法や、ファセットの数の組合せ爆発への対応などが考えられるが、これらに対処する方法へのいくつかのアイディアに関して有効性を確かめていく予定である。
これらの研究の推進に際しては、関連するトピックの研究者とのコミュニケーションや研究集会への参加等により情報収集を行っていきたい。

Report

(4 results)
  • 2023 Research-status Report
  • 2022 Research-status Report
  • 2021 Research-status Report
  • 2020 Research-status Report
  • Research Products

    (8 results)

All 2023 2022 2020 Other

All Journal Article (2 results) (of which Peer Reviewed: 1 results,  Open Access: 1 results) Presentation (4 results) (of which Int'l Joint Research: 2 results,  Invited: 1 results) Remarks (2 results)

  • [Journal Article] Defining logical obstruction with fixpoints in epistemic logic2023

    • Author(s)
      Nishimura Susumu
    • Journal Title

      Journal of Applied and Computational Topology

      Volume: Novermber Issue: 4 Pages: 941-970

    • DOI

      10.1007/s41468-023-00151-8

    • Related Report
      2023 Research-status Report
    • Peer Reviewed
  • [Journal Article] Partial Product Updates for Agents of Detectable Failure and Logical Obstruction to Task Solvability2023

    • Author(s)
      Daisuke Nakai, Masaki Muramatsu, Susumu Nishimura
    • Journal Title

      arXiv.org

      Volume: arXiv:2303.16437

    • Related Report
      2022 Research-status Report
    • Open Access
  • [Presentation] Product Updates for Partial Epistemic Models and Logical Obstruction to Task Solvability2023

    • Author(s)
      Susumu Nishimura
    • Organizer
      Epistemic and Topological Reasoning in Distributed Systems
    • Related Report
      2023 Research-status Report
    • Int'l Joint Research
  • [Presentation] 認識論理による分散タスク不可解性とその証明能力について2022

    • Author(s)
      西村進
    • Organizer
      第三十三回 ALGI 代数,論理,幾何と情報科学研究集会
    • Related Report
      2022 Research-status Report
  • [Presentation] On the Power of Epistemic Logic for Defining Obstructions to Distributed Agreement Tasks2022

    • Author(s)
      Susumu Nishimura
    • Organizer
      CELT2022: Connections between Epistemic Logic and Topology
    • Related Report
      2022 Research-status Report
    • Int'l Joint Research / Invited
  • [Presentation] 動的認識論理を用いた分散計算タスクの不可解性証明について2020

    • Author(s)
      西村進
    • Organizer
      第37回 記号論理と情報科学 研究集会 (SLACS2020)
    • Related Report
      2020 Research-status Report
  • [Remarks] Springer SharedIt: 雑誌論文1

    • URL

      https://rdcu.be/dq7fb

    • Related Report
      2023 Research-status Report
  • [Remarks] arXiv 論文(共著)

    • URL

      https://arxiv.org/abs/2011.13630

    • Related Report
      2020 Research-status Report

URL: 

Published: 2020-04-28   Modified: 2024-12-25  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi