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

• Project/Area Number: 23K21641
• Project/Area Number (Other): 21H03392 (2021-2022)
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Multi-year Fund (2024); Single-year Grants (2021-2022)
• 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 – 2023-03-31
• Project Status: Ceased (Fiscal Year 2024)
• Budget Amount: ¥17,290,000 (Direct Cost: ¥13,300,000、Indirect Cost: ¥3,990,000); Fiscal Year 2026: ¥4,030,000 (Direct Cost: ¥3,100,000、Indirect Cost: ¥930,000); Fiscal Year 2025: ¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000); Fiscal Year 2024: ¥1,643,239 (Direct Cost: ¥1,264,030、Indirect Cost: ¥379,209); 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

本研究の目的は，モデル検査など論理学の応用技術において仮定される論理や集合の公理が何かを探査し，異なる技法の間の類似性や相異性を顕在化することで，ハイブリッド技術の創出を目指すものである．初年度(令和３年度)においては５つの領域に焦点を絞り，それぞれの課題を探求し，得られた知見を統合して多角的な検討を加えて，より高度な視点を得る計画であった．しかし，コロナ禍の行動制限により研究交流がほとんど行えず，とくに本研究で重要な役割を担う中国とシンガポールの協力者たちとの交流には長い空白ができてしまったので，代表者は北京の応用数学研究所に滞在して彼らとの交流基盤の回復に努め，体制が整うまで本研究を中断することにした．従って，本年度の研究も未完結であるが，個別課題ごとには次のような顕著な成果が得られた．
1. 様相μ計算の論理式は，演算子μ,νの入れ替わりが何回生じるかで分類される．μν型の論理式でもνμ型の論理式でも表現されるクラスΔ2はμ型とν型の論理式の超限的な組合せによって表せることを示す論文を出版した．さらに，様相μ計算の階層の崩壊を認識論理学の視点で分析し，無知の形式化を行った．2. 様相μ計算の階層が様相の種類によってどう変わるかを，真理値評価ゲームを用いて調べた．3. 確率的モデル検査は，検査法や評価アルゴリムがランダム化されたもので，ここではBlackwellゲームの一種として扱う．代表者が開発したWKLoの超準的手法を用いて，確率アルゴリズムを逆数学的に分析する研究を進めた．4. 決定木において，クエリの最小コストを最大化する入力分布（固有分布）について，より一般な木構造に対して固有分布を調べて論文にまとめた．さらにはグラフ構造への一般化を検討している．５. 確率アルゴリズムの視点から確率的推論を捕捉する独自の研究を目指しながら，先行研究の成果を整理した．

Current Status of Research Progress

3: Progress in research has been slightly delayed.

Reason

個別の小課題においては顕著な進展が得られたが，得られた知見を統合し多角的な検討を与える研究会等がコロナ禍で開催できなかった．

Strategy for Future Research Activity

コロナ禍で失われた国際研究協力体制を２年程度で取り戻す．研究代表者がほぼ毎年主催していた国際会議CTFMも2019年を最後に中断されている．行動制限は緩和されたが，このような会議を開くためにもまず代表者と関係者との協力関係の立て直しが必要であり，しばらく本研究を中断して海外の研究所に滞在しながら体制を整え，より一層ダイナミックな発展を目指して令和７年度内に研究を再開する．

Research Products

• [Int'l Joint Research] シンガポール国立大学(シンガポール)
• [Int'l Joint Research] 武漢理工大学(中国)
• [Journal Article] Lawvere-Tierney topologies for computability theorists (2023)
  • Author(s): Kihara Takayuki
  • Journal Title: Transactions of the American Mathematical Society, Series B Volume: 10 Issue: 2 Pages: 48-85
  • DOI: 10.1090/btran/134
  • Peer Reviewed / Open Access
• [Journal Article] On One-Variable Fragments of Modal μ-Calculus (2022)
  • Author(s): Pacheco Leonardo、Li Wenjuan、Tanaka Kazuyuki
  • Journal Title: Proc. of Computability Theory and Foundations of Mathematics 2019 (Wuhan) Volume: - Pages: 17-45
  • DOI: 10.1142/9789811259296_0002
  • Peer Reviewed / Int'l Joint Research
• [Journal Article] Infinite Games, Inductive Definitions and Transfinite Recursion (2022)
  • Author(s): Tanaka Kazuyuki、Yoshii Keisuke
  • Journal Title: Proc. of Computability Theory and Foundations of Mathematics 2019 (Wuhan) Volume: - Pages: 47-78
  • DOI: 10.1142/9789811259296_0003
  • Peer Reviewed
• [Journal Article] On the Degrees of Ignorance: via Epistemic Logic and μ-Calculus (2022)
  • Author(s): Leonard Pacheco, Kazuyuki Tanaka
  • Journal Title: Proc. of SOCREAL2022 Volume: - Pages: 74-78
  • Peer Reviewed / Int'l Joint Research
• [Journal Article] The Alternation Hierarchy of the $\mu $-calculus over Weakly Transitive Frames (2022)
  • Author(s): Pacheco Leonardo、Tanaka Kazuyuki
  • Journal Title: WoLLIC 2022, LNCS Volume: 13468 Pages: 207-220
  • DOI: 10.1007/978-3-031-15298-6_13
  • ISBN: 9783031152979, 9783031152986
  • Peer Reviewed / Int'l Joint Research
• [Journal Article] Second-order logic and related systems: a game-semantical perspective (2022)
  • Author(s): Wenjuan Li, Kazuyuki Tanaka
  • Journal Title: RIMS Kokyuroku Volume: 2233 Pages: 1-19
  • Int'l Joint Research
• [Journal Article] 様相ミュー計算のタブロー法の完全性と無限ゲームの決定性について (2022)
  • Author(s): 鹿島亮
  • Journal Title: RIMS Kokyuroku Volume: 2233 Pages: 65-81
• [Journal Article] Rational Sequences Converging to Left-c.e. Reals of Positive Effective Hausdorff Dimension (2022)
  • Author(s): Hiroyuki Imai, Masahiro Kumabe, Kenshi Miyabe, Yuki Mizusawa and Toshio Suzuki
  • Journal Title: Proc. of Computability Theory and Foundations of Mathematics 2019 (Wuhan) Volume: - Pages: 97-121
  • Peer Reviewed
• [Journal Article] Topological reducibilities for discontinuous functions and their structures (2022)
  • Author(s): Kihara Takayuki
  • Journal Title: Israel Journal of Mathematics Volume: 252 Issue: 1 Pages: 461-500
  • DOI: 10.1007/s11856-022-2367-6
  • Peer Reviewed / Open Access
• [Journal Article] Wadge-like degrees of Borel bqo-valued functions (2022)
  • Author(s): Kihara Takayuki、Selivanov Victor
  • Journal Title: Proceedings of the American Mathematical Society Volume: 150 Issue: 9 Pages: 3989-4003
  • DOI: 10.1090/proc/15930
  • Peer Reviewed / Int'l Joint Research
• [Journal Article] Enumerating Classes of Effective Quasi-Polish Spaces (2022)
  • Author(s): M. de Brecht, T. Kihara, & V. Selivanov
  • Journal Title: Revolutions and Revelations in Computability (CiE 2022), Lecture Notes in Computer Science Volume: 13359 Pages: 88-102
  • DOI: 10.1007/978-3-031-08740-0_8
  • ISBN: 9783031087394, 9783031087400
  • Peer Reviewed / Int'l Joint Research
• [Journal Article] 汎用的学習理論 (2022)
  • Author(s): 宮部賢志
  • Journal Title: 数理解析研究所講究録 Volume: 2228 Pages: 215-225
• [Journal Article] The Eigen-Distribution for Multi-Branching Weighted Trees on Independent Distributions (2021)
  • Author(s): Peng Weiguang、Peng NingNing、Tanaka Kazuyuki
  • Journal Title: Methodology and Computing in Applied Probability Volume: 24 Issue: 1 Pages: 277-287
  • DOI: 10.1007/s11009-021-09849-7
  • Peer Reviewed / Int'l Joint Research
• [Journal Article] A COMPARISON OF VARIOUS ANALYTIC CHOICE PRINCIPLES (2021)
  • Author(s): D’AURIAC PAUL-ELLIOT ANGLES、KIHARA TAKAYUKI
  • Journal Title: The Journal of Symbolic Logic Volume: 86 Issue: 4 Pages: 1452-1485
  • DOI: 10.1017/jsl.2021.37
  • Peer Reviewed / Int'l Joint Research
• [Journal Article] Turing degrees in Polish spaces and decomposability of Borel functions (2020)
  • Author(s): Gregoriades Vassilios、Kihara Takayuki、Ng Keng Meng
  • Journal Title: Journal of Mathematical Logic Volume: 21 Issue: 01 Pages: 1-41
  • DOI: 10.1142/s021906132050021x
  • Peer Reviewed / Int'l Joint Research
• [Presentation] Computability Theory and Reverse Mathematics via Lawvere-Tierney topologies (2022)
  • Author(s): Takayuki Kihara
  • Organizer: Computability in Europe 2022
  • Int'l Joint Research / Invited
• [Presentation] 計算可能性と定義可能性による階層構造／この１０年で何が起こったか (2021)
  • Author(s): 木原貴行
  • Organizer: 日本数学会 秋季総合分科会
  • Invited
• [Book] 計算理論と数理論理学 (2022)
  • Author(s): 田中 一之
  • Total Pages: 312
  • Publisher: 共立出版
  • ISBN: 4320114728
• [Book] コンピュータサイエンスにおける様相論理 (2022)
  • Author(s): 鹿島 亮
  • Total Pages: 176
  • Publisher: 森北出版
  • ISBN: 4627856415