様相ミュー計算と確率ゲームへの逆数学的アプローチ：ハイブリッド検査法の創出と分析

点击翻译按钮获取中文摘要

本研究の目的は，モデル検査など論理学の応用技術において必要とされる論理や集合の公理が何かを探求し，異なる技法の間の類似性や相異性を顕在化することで，ハイブリッド技術の創出を目指すものである．初年度(令和３年度)においては５つの小領域におけるそれぞれの課題を探求し，得られた知見を統合して多角的な検討を加えることで，より高度な視点を得る計画であった．しかし，令和３年度，そして４年度も前半までは，コロナ禍の行動制限によりリアルな研究交流がほとんど行えず，個別課題ごとの研究を進めるに留まったが，以下のような顕著な進展が得られている．1. 様相μ計算の階層．様相μ計算の論理式は，演算子μ,νの入れ替わりが何回生じるかで分類される．μν型の論理式でもνμ型の論理式でも表現できる再帰的推移システムのクラスΔ2はμ型とν型の論理式の超限的な組合せによって表せることを示した論文を出版した．さらに，様相μ計算の階層の崩壊を認識論理学の視点で分析し，無知の形式化を行った．2. モデル検査法とゲーム意味論．様相μ計算の階層が様相の種類によってどう変わるかを，ゲーム意味論で調べる研究成果を得た．3. 確率的モデル検査．検査法もしく評価アルゴリムが非決定的でランダム化されているもので，Blackwellゲームの分析が究極の目的の一つである．確率アルゴリズムを逆数学的に分析する研究を開始した．4. ミニマックス定理を応用したYaoの原理は，どんな乱択アルゴリズムも，最悪の入力分布に対しては，決定性アルゴリズムの期待値よりも効率良くならないことを示すものである．決定木において最小コストを最大化する入力分布（固有分布）について，重みをもつ多分岐木について考察して，論文にまとめた．５. 確率的推論．真理値判定の確率アルゴリズムの視点から確率的推論を捕捉する独自の研究を目指しつつ，先行研究の成果を整理した．