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

2023 Fiscal Year Research-status Report

Declarative Distirbuted Programming based on Combinatorial Topology

Research Project

Project/Area Number 20K11678
Research InstitutionKyoto University

Principal Investigator

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

Project Period (FY) 2020-04-01 – 2025-03-31
Keywords並行分散計算 / 分散計算の数理論理モデル / 認識μ計算 / 宣言的プログラミング
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

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

Causes of Carryover

昨年度は予期せぬ海外出張旅費の高騰が主な理由で当年度予算を早期に使い果たす畏れがあったため助成金の前倒し請求を行ったものの、経費の抑制的な使用等に努めた結果、おおよそ予算通りの執行額に収めることができた。そのため見かけ上は相当の次年度使用額が生じたように見えるが、実際は当初の予算計画にほぼ戻っている。引き続き助成金の有効活用に努めていきたい。

  • Research Products

    (3 results)

All 2023 Other

All Journal Article (1 results) (of which Peer Reviewed: 1 results) Presentation (1 results) (of which Int'l Joint Research: 1 results) Remarks (1 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 Pages: オンライン出版

    • DOI

      10.1007/s41468-023-00151-8

    • Peer Reviewed
  • [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
    • Int'l Joint Research
  • [Remarks] Springer SharedIt: 雑誌論文1

    • URL

      https://rdcu.be/dq7fb

URL: 

Published: 2024-12-25  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi