| 研究課題/領域番号 |
20K11678
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
西村 進 京都大学, 理学研究科, 准教授 (10283681)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2025-03-31
|
| キーワード | 並行分散計算 / 分散計算の数理論理モデル / 認識μ計算 / 宣言的プログラミング |
|---|
| 研究実績の概要 |
近年、分散並列計算の組合せ幾何的モデルと、動的認識論理のKripkeモデルが相互に深く関連していることが明らかとなり、この2つの分野の交流による研究が盛んになってきている。組合せ幾何的モデルでは、分散計算問題の可解性を単体的複体モデルにおける高次元の連結性に帰着して議論するが、一定の条件の下で同様の議論を単体的複体モデルと同型なKripkeモデル上で認識論理を用いて行うことができる。特にGoubaultらは、障害論理式、すなわち分散並列システムに対応するKripkeモデルでは成り立つが実現したい分散並列計算に対応するKripkeモデルでは成り立たないような認識論理式をひとつ発見することによって、分散計算問題の不可解性を立証できることを示した。しかしながら、認識論理を用いる方法は基礎的な適用例が少し明らかになったばかりであり、計算モデルの精密化や適用範囲を拡張するための研究が進行しているところである。
本年度は、前年度から継続の、並列分散システム中のプロセスが何度でも情報を交換できる複ラウンド計算モデルに対して認識論理の拡張である認識μ計算を用いてk集合合意問題の不可解性を示す研究を完成させ、2022年初夏にパリで開催された研究集会で発表した。その内容をまとめた論文を現在国際誌に投稿中である。
さらに、分散同期メッセージ通信プロトコルによって分散合意問題が不可解であることを障害論理式を用いて示した。(大学院生2名との共同研究) この不可解性自体はすでに組合せ幾何的モデルで知られた結果であったが、認識論理の枠組みでは示されていなかった。本研究において、Goubaultらが示した分散同期メッセージ通信の単体的複体モデルに適合したKripkeモデルに対して、障害論理式を適用するのに必要な動的認識モデルの構成に必要な積更新モデルの構成方法を与えることによってこれを達成した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
本年度の研究では、並行分散計算モデルが純粋でない単体的複体モデルによって表される場合について、Goubaultらによる提案を拡張し、分散計算問題の不可解性を障害論理式を用いて示すための枠組みを与えることに成功した。動的認識論理を用いる手法は、提案当初は計算モデルとして純粋な単体的複体モデルのみを想定しており、このことは並行分散システムで発生するプロセス故障を捉えにくいという問題があった。Goubaultらの最近の研究で、純粋でない単体的複体モデルと対応するKripkeモデルのクラスが明らかにされたが、本研究ではこれにふさわしい積更新モデルの概念を与え、プロセス間で互いの故障が関知可能であるような分散同期メッセージ通信プロトコルについてこれに対応する積更新モデルを構成し、合意問題の不可解性を示す障害論理式を与えることに成功した。
以上の結果は、プロセス故障のある並行分散計算の計算構造について重要な知見を与えるものであるとともに、さらに精緻な並行分散計算のためのモデルの提案につながる成果である。このような知見は、プロセス故障を前提とした分散計算モデルに関してより本質的な洞察を与えるものであり、以降の研究において分散計算プログラムの宣言的記述に大きく寄与すると考えられる。
|
| 今後の研究の推進方策 |
純粋でない単体的複体モデルに対する手法を深化させ、たとえば複ラウンドの分散同期メッセージ通信プロトコルについてのk集合合意問題の不可解性を示す障害論理式の構成などを通して、純粋でないモデルのもつ計算構造について洞察を深めたい。純粋でない単体的複体モデルに対応するKripkeモデルについては、最近研究が活発に行われており、より精緻なモデルに対して障害論理式を用いた手法を適用可能とするのも興味深いテーマである。この方面の研究推進に関しては、関連する国外の研究グループとの交流・情報交換も行っていきたい。
純粋でないモデルに対する新たな知見を、並行分散プログラムの宣言的記述にフィードバックしていきたい。特に、これまでに得られた知見は、単体的複体モデルのファセット(最大次元面、故障していない並行プロセスの集合を表す)が並行分散計算で本質的な情報であることを示唆しており、ファセットを中心とした宣言的記述により、従来のプロセス毎に動作を記述する方法とは異なるプログラミングパラダイムの提案を目指して研究を進めていく予定である。
|
| 次年度使用額が生じた理由 |
昨年度も、新型コロナ感染症の流行が予想していたよりも沈静化が遅く、学会出席等の出張を伴うが困難であったために旅費をあまり執行できなかったのが主たる理由である。これから新型コロナ感染症の流行も収束の方向に向かっていくと考えられるので、国際研究集会への参加等を通して、関連研究分野の研究者と議論・情報交換を行うなどして助成金を有効活用していきたい。
|
