様相ミュー計算と確率ゲームへの逆数学的アプローチ:ハイブリッド検査法の創出と分析
Project/Area Number |
21H03392
|
Research Category |
Grant-in-Aid for Scientific Research (B)
|
Allocation Type | Single-year Grants |
Section | 一般 |
Review Section |
Basic Section 60010:Theory of informatics-related
|
Research Institution | Tohoku University |
Principal Investigator |
田中 一之 東北大学, 理学研究科, 名誉教授 (70188291)
|
Co-Investigator(Kenkyū-buntansha) |
宮部 賢志 明治大学, 理工学部, 専任准教授 (00583866)
鹿島 亮 東京工業大学, 情報理工学院, 准教授 (10240756)
木原 貴行 名古屋大学, 情報学研究科, 准教授 (80722701)
|
Project Period (FY) |
2021-04-01 – 2025-03-31
|
Project Status |
Granted (Fiscal Year 2022)
|
Budget Amount *help |
¥17,290,000 (Direct Cost: ¥13,300,000、Indirect Cost: ¥3,990,000)
Fiscal Year 2023: ¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2022: ¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000)
Fiscal Year 2021: ¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000)
|
Keywords | 数理論理学 / モデル検査 / 様相ミュー計算 / 逆数学 / 確率ゲーム / 様相μ計算 / 無限ゲーム / 確率的推論 |
Outline of Research at the Start |
本研究は,モデル検査のような応用論理学にとって必要な数学の理論的仮定が何かを探求することで、異なる技法の間の類似性や相異性を発見し,ハイブリッドな新技法の開発を目標とするものである.モデル検査問題の多くは,それを表現する様相μ計算に対するゲーム意味論の決定問題に置き換わるが,逆にゲームの視点から様相μ計算で表せない問題も作れ,より強い表現手法を創出する指針となる.また,確率的モデル検査は Blackwell ゲームとみなせるが,その逆数学的分析は進んでいないため,その有限版であるブール木のクエリ複雑さの議論から始めて一般化を試みる.こうした知見を統合して,数理論理学の新しい応用領域を切り拓く.
|
Outline of Annual Research Achievements |
本研究の目的は,モデル検査など論理学の応用技術において必要とされる論理や集合の公理が何かを探求し,異なる技法の間の類似性や相異性を顕在化することで,ハイブリッド技術の創出を目指すものである.初年度(令和3年度)においては5つの小領域におけるそれぞれの課題を探求し,得られた知見を統合して多角的な検討を加えることで,より高度な視点を得る計画であった.しかし,令和3年度,そして4年度も前半までは,コロナ禍の行動制限によりリアルな研究交流がほとんど行えず,個別課題ごとの研究を進めるに留まったが,以下のような顕著な進展が得られている. 1. 様相μ計算の階層.様相μ計算の論理式は,演算子μ,νの入れ替わりが何回生じるかで分類される.μν型の論理式でもνμ型の論理式でも表現できる再帰的推移システムのクラスΔ2はμ型とν型の論理式の超限的な組合せによって表せることを示した論文を出版した.さらに,様相μ計算の階層の崩壊を認識論理学の視点で分析し,無知の形式化を行った.2. モデル検査法とゲーム意味論.様相μ計算の階層が様相の種類によってどう変わるかを,ゲーム意味論で調べる研究成果を得た.3. 確率的モデル検査.検査法もしく評価アルゴリムが非決定的でランダム化されているもので,Blackwellゲームの分析が究極の目的の一つである.確率アルゴリズムを逆数学的に分析する研究を開始した.4. ミニマックス定理を応用したYaoの原理は,どんな乱択アルゴリズムも,最悪の入力分布に対しては,決定性アルゴリズムの期待値よりも効率良くならないことを示すものである.決定木において最小コストを最大化する入力分布(固有分布)について,重みをもつ多分岐木について考察して,論文にまとめた.5. 確率的推論.真理値判定の確率アルゴリズムの視点から確率的推論を捕捉する独自の研究を目指しつつ,先行研究の成果を整理した.
|
Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
個別の小領域における課題に対しては顕著な進展が得られているが,全体を討議するような研究会が開催できていない.
|
Strategy for Future Research Activity |
コロナ禍で失われた研究実施体制を2年程度で取り戻す.研究代表者がほぼ毎年主催共催していた国際会議CTFMも2019年を最後に中断されており,2025年年度を目処に徐々に復活させる.小領域間の交流や合流の可能性を検討しながら,研究全体の一層ダイナミックな発展を目指す.
|
Report
(1 results)
Research Products
(8 results)