| Project/Area Number |
21J13334
|
|---|
| Research Category |
Grant-in-Aid for JSPS Fellows
|
| Allocation Type | Single-year Grants |
|---|
| Section | 国内 |
|---|
| Review Section |
Basic Section 60010:Theory of informatics-related
|
|---|
| Research Institution | The Graduate University for Advanced Studies |
|---|
Principal Investigator |
小森田 祐一 総合研究大学院大学, 複合科学研究科, 特別研究員(DC2)
|
|---|
| Project Period (FY) |
2021-04-28 – 2023-03-31
|
| Project Status |
Completed (Fiscal Year 2022)
|
| Budget Amount *help |
¥1,000,000 (Direct Cost: ¥1,000,000)
Fiscal Year 2022: ¥600,000 (Direct Cost: ¥600,000)
Fiscal Year 2021: ¥400,000 (Direct Cost: ¥400,000)
|
|---|
| Keywords | モデル検査 / 確率的システム / 圏論 / 余代数 / ファイバー圏 / 無限ゲーム |
|---|
| Outline of Research at the Start |
計算機のプログラムが二つ与えられたとき，「それらが同じ振る舞いをするかどうか」は理論・実用の両面で重要な問題の一つであり，その定式化の一つとして双模倣関係がある．また，近年では「それらがどの程度似通っているか」を表す双模倣距離というものも広く使われ始めている．
本研究では，双模倣関係と双模倣距離を統合し，これらを扱う統一的なアルゴリズムを導出することを目指す．ファイバー圏と呼ばれる数学的な概念がその鍵となる．
|
| Outline of Annual Research Achievements |
本研究では、状態遷移システムの分析に関し、同値関係、距離などの観測モードに依らない形での理論の定式化・実証コードの実装を目指している。令和4年度は、主に以下の2つの、すでに存在するアルゴリズムを圏論的に解釈し、一般化することを目指して研究を行った。
1つ目は、無限ゲームに基づいたアルゴリズムである。これは主に、[Tang & van Breugel, CONCUR 2016]、[Bacci+, CONCUR 2019]などの論文で扱われているものである。本研究においてはすでに、LICS2019論文ジャーナル版において、状態遷移システムの無限ゲームによる分析を取り扱っているが、先に述べた論文で扱われているゲームはそれとは大きく異なる性質を持つ。特に、LICS2019論文ジャーナル版におけるゲームは常に決定論的であるが、先に述べた論文で扱われるものは、確率的システムについては確率的ゲームになるのである。本研究ではこの違いを圏論的に、「関手の持ち上げの表式の違い」として定式化した。特に先に述べた論文で扱うものは Wasserstein Lifting と呼ばれるものでとらえられ、これを用いてアルゴリズムの一般化ができる可能性がある。
2つ目は、partition refinementと呼ばれる一群のアルゴリズムである。これは観測モードとしては同値関係を扱うものであり、距離などの他の観測モードでは類似のアルゴリズムは提案されていない。そこで、このアルゴリズムを抽象的・圏論的に分析することにより、逆に、観測モードとしての同値関係の持つどのような性質が、このアルゴリズムを成立させているのかの分析を試み、一定の成果を得た。
どちらについても、京都大学数理解析研究所の計算機科学チームの複数の研究者と共同研究を行った。現在論文化に向けて研究を進めている。
|
| Research Progress Status |
令和4年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
令和4年度が最終年度であるため、記入しない。
|
