| 研究課題/領域番号 |
21J13334
|
|---|
| 研究種目 |
特別研究員奨励費
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 国内 |
|---|
| 審査区分 |
小区分60010:情報学基礎論関連
|
|---|
| 研究機関 | 総合研究大学院大学 |
|---|
研究代表者 |
小森田 祐一 総合研究大学院大学, 複合科学研究科, 特別研究員(DC2)
|
|---|
| 研究期間 (年度) |
2021-04-28 – 2023-03-31
|
| 研究課題ステータス |
完了 (2022年度)
|
| 配分額 *注記 |
1,000千円 (直接経費: 1,000千円)
2022年度: 600千円 (直接経費: 600千円)
2021年度: 400千円 (直接経費: 400千円)
|
|---|
| キーワード | モデル検査 / 確率的システム / 圏論 / 余代数 / ファイバー圏 / 無限ゲーム |
|---|
| 研究開始時の研究の概要 |
計算機のプログラムが二つ与えられたとき，「それらが同じ振る舞いをするかどうか」は理論・実用の両面で重要な問題の一つであり，その定式化の一つとして双模倣関係がある．また，近年では「それらがどの程度似通っているか」を表す双模倣距離というものも広く使われ始めている．
本研究では，双模倣関係と双模倣距離を統合し，これらを扱う統一的なアルゴリズムを導出することを目指す．ファイバー圏と呼ばれる数学的な概念がその鍵となる．
|
| 研究実績の概要 |
本研究では、状態遷移システムの分析に関し、同値関係、距離などの観測モードに依らない形での理論の定式化・実証コードの実装を目指している。令和4年度は、主に以下の2つの、すでに存在するアルゴリズムを圏論的に解釈し、一般化することを目指して研究を行った。
1つ目は、無限ゲームに基づいたアルゴリズムである。これは主に、[Tang & van Breugel, CONCUR 2016]、[Bacci+, CONCUR 2019]などの論文で扱われているものである。本研究においてはすでに、LICS2019論文ジャーナル版において、状態遷移システムの無限ゲームによる分析を取り扱っているが、先に述べた論文で扱われているゲームはそれとは大きく異なる性質を持つ。特に、LICS2019論文ジャーナル版におけるゲームは常に決定論的であるが、先に述べた論文で扱われるものは、確率的システムについては確率的ゲームになるのである。本研究ではこの違いを圏論的に、「関手の持ち上げの表式の違い」として定式化した。特に先に述べた論文で扱うものは Wasserstein Lifting と呼ばれるものでとらえられ、これを用いてアルゴリズムの一般化ができる可能性がある。
2つ目は、partition refinementと呼ばれる一群のアルゴリズムである。これは観測モードとしては同値関係を扱うものであり、距離などの他の観測モードでは類似のアルゴリズムは提案されていない。そこで、このアルゴリズムを抽象的・圏論的に分析することにより、逆に、観測モードとしての同値関係の持つどのような性質が、このアルゴリズムを成立させているのかの分析を試み、一定の成果を得た。
どちらについても、京都大学数理解析研究所の計算機科学チームの複数の研究者と共同研究を行った。現在論文化に向けて研究を進めている。
|
| 現在までの達成度 (段落) |
令和4年度が最終年度であるため、記入しない。
|
| 今後の研究の推進方策 |
令和4年度が最終年度であるため、記入しない。
|
