技術要約：様相論理における不動点論理式の定義と分離の複雑性

1. 問題設定

本論文は、命題様相論理（ML）に対する様相 $\mu$-計算量（$\mu$ML）の**様相分離可能性（modal separability）**問題を調査している。2つの矛盾する $\mu$ML 論理式 $\phi$ と $\phi'$ が与えられたとき、問題は、$\phi \models \psi$ かつ $\psi \models \neg \phi'$ を満たす ML 論理式 $\psi$（「セパレーター（分離子）」）が存在するかどうかを問うものである。

この問題は、**様相定義可能性（modal definability）**を一般化したものである。定義可能性とは、特定の $\mu$ML 論理式が ML 論理式と等価であるかどうかを判定することである（ここで $\phi' = \neg \phi$ である）。この研究は、コンピュータサイエンスに関連する様々なモデルのクラスにわたって実施されている：

• 任意のモデル（無制限の出次数）。
• 単語（出次数 $\le 1$ のモデル、これを $T_1$ とする）。
• 二分木（出次数 $\le 2$ のモデル、これを $T_2$ とする）。
• 有界な出次数 $d \ge 3$ の木（これを $T_d$ とする）。
• 有限モデルおよび無限単語。

著者らはまた、クレイグ補間存在問題（セパレーターが $\phi$ と $\phi'$ の共通の記号のみを使用しなければならないという、分離可能性の特殊なケース）およびセパレーターの有効な構成についても調査している。

2. 手法

著者らは、モデル理論的な特徴付けとオートマトン理論的な手法を組み合わせて用いている：

• モデル理論的な特徴付け: 決定手続きの核となるのは**結合一貫性（joint consistency）**である。2つの論理式が分離不可能であることは、特定の双模倣関係（bisimulation relations）に関してそれらが「結合的に一貫している」ことと同値である。具体的には、$\phi$ と $\phi'$ がすべての $n$ に対して $(\sigma, n)$-双模倣に関して結合的に一貫している場合、それらは ML で分離不可能である。

  • 単語 ($T_1$) および二分木 ($T_2$) について、著者らは双模倣性が同型性（isomorphism）を意味する（あるいは同型性に還元できる）という事実を利用し、結合双模倣一貫性を結合同型一貫性と等置している。
  • $d \ge 3$ の場合、この等価性は成立しないため、**双模倣商（bisimulation quotients）**を用いたより複雑な分析が必要となる。

• オートマトン理論: 本論文は、$\mu$ML と**非決定性パリティ木オートマトン（NPTA）**との間のよく知られた対応関係を利用している。

  • $\mu$ML 論理式は NPTA に翻訳される。
  • 結合一貫性のチェックという問題は、これらのオートマトンが受理する言語の共通部分のチェックへと還元される。
  • 重要な技術的ツールは、元のオートマトンが受理する言語の双模倣商を認識するオートマトンの構成である。これにより、著者らは有界な出次数の木における分離可能性を、これらの商の同型性チェックへと還元することで決定することができる。

• セパレーターの構成: 分離可能性が確立された場合、著者らはセパレーターを構成するためのアルゴリズムを提供する。これらの構成は、多くの場合、入力された論理式の一貫した型の選言である、入力論理式の**ML 一様帰結（ML-uniform consequences）**を生成することを含む。

3. 主な貢献と結果

3.1. 分離可能性と定義可能性の複雑性

本論文は、$\mu$ML 論理式の ML 分離可能性および ML 定義可能性に関する精密な複雑性のランドスケープを確立しており、それは論文内の表1にまとめられている：

モデルクラス	ML 定義可能性	ML 分離可能性	セパレーター構成サイズ
単語 ($T_1$)	PSpace-complete	PSpace-complete	単一指数関数的
二分木 ($T_2$)	ExpTime-complete	ExpTime-complete	二重指数関数的
無制限のモデル	ExpTime-complete	ExpTime-complete	二重指数関数的
木 ($T_d, d \ge 3$)	ExpTime-complete	2-ExpTime-complete	三重指数関数的

• 単語 ($T_1$): 分離可能性は PSpace-complete である。これは最も容易なケースであり、単語上の $\mu$ML の充足可能性の複雑さと一致する。
• 二分木 ($T_2$) および無制限: 分離可能性は ExpTime-complete である。著者らは、二分木の構造的性質（双模倣性が同型性を意味する）により、無制限モデルとの共通のアルゴリズム的扱いが可能であることを示している。
• 木 ($d \ge 3$): これが最も重要な発見である。ML 定義可能性は ExpTime-complete のままであるが、ML 分離可能性は 2-ExpTime-complete へと跳ね上がる。
  • 著者らは、この複雑性の増加が、単に二分木へ高次の出次数をエンコードすること（これは複雑性を維持する）によるものではないことを示している。
  • 困難さは、ML が $d \ge 3$ の $T_d$ 上で**クレイグ補間特性（Craig Interpolation Property, CIP）**を欠いていることに起因する。

3.2. クレイグ補間と補間存在

• CIP の失敗: 本論文は、ML がすべてのモデル、単語、および二分木の上では CIP を享受するが、出次数 $d \ge 3$ の木の上では失敗することを証明している。
• 補間存在: CIP の失敗を受けて、著者らは $T_d$ ($d \ge 3$) 上での ML に関するクレイグ補間存在問題（共通の記号のみを使用するセパレーターが存在するか？）を研究している。彼らは、この問題が coNExpTime-complete であり、これらクラスにおける ML の妥当性問題（PSpace-complete）よりも厳密に難しいことを示している。

3.3. 有効な構成

論文は、セパレーターが存在する場合の構成アルゴリズムを提供している：

• 単語: 指数時間での構成が可能である（単語上の ML に対し $\mu$ML は指数関数的に簡潔であるため、これは最適である）。
• 二分木／無制限: 二重指数時間での構成が可能である。
• $d \ge 3$: 三重指数時間での構成が可能である。
• 著者らは、$d \ge 3$ の場合、構成されたセパレーターはサイズに関して最適であると推測されるが、構成サイズに対する形式的な下界は未解決のままであると述べている。

3.4. 段階的様相（ケーススタディ）

著者らは、結果を**段階的様相論理（graded Modal Logic, grML）および段階的 $\mu$-計算量（graded $\mu$ML, gr$\mu$ML）**へと拡張している。これらには、後続者の数を数える様相（例：「少なくとも $k$ 個の子が……を満たす」）が含まれる。

• セパレーターに段階が含まれる場合: 定義可能性と分離可能性はともに ExpTime-complete である。
• セパレーターに段階が含まれない場合:
  • 定義可能性: gr$\mu$ML 論理式の ML 定義可能性は ExpTime-complete である。
  • 分離可能性: gr$\mu$ML 論理式の ML 分離可能性は 2-ExpTime-complete である。
  • 著者らは、分離可能性の複雑性が（定義可能性と比較して）高くなる理由を、有界な次数の木が gr$\mu$ML で定義可能であり、これにより一般的な $d \ge 3$ のケースを段階的な設定に還元できるという事実に求めている。

4. 重要性と主張

本論文は、不動点論理の複雑性について「かなり完全で興味深い全体像」を提供すると主張している。その主な意義は以下の通りである：

1. 複雑性のギャップの特定: これは、標準的なモデルクラス上の自然な論理において、**分離可能性が定義可能性よりも明らかに難しい（具体的には 2-ExpTime 対 ExpTime）**ことが証明された、この分野における最初の既知の事例である。これは、分離可能性が定義可能性と同等か、あるいはそれよりも容易であったこれまでの結果とは対照的である。
2. 補間と複雑性の接続: 本研究は、クレイグ補間特性の失敗と、分離可能性問題の計算複雑性の増大との間の直接的な関連性を確立している。$d \ge 3$ の木における CIP の欠如が、2-ExpTime の困難さの根源であることが示されている。
3. 様相論理のランドスケープの精緻化: 結果は、様相推論の複雑さが木構造（出次数）によって一様ではないことを明確にしている。二分木から三分木への移行は、論理的性質（特に補間）および分離可能性のような推論タスクの計算コストを根本的に変化させる。
4. 構成的な結果: 決定手続きを超えて、論文はセパレーターのサイズ（例：二分木では二重指数、$d \ge 3$ では三重指数）に関する境界を提供し、セパレーターの有効な構成法を提示している。

著者らは、彼らの知見が、モデルの構造的性質（出次数）、言語の論理的性質（補間）、および推論問題の計算複雑性の間の微妙な相互作用を浮き彫りにしていると結論づけている。また、$d \ge 3$ におけるセパレーターサイズの最適性や、他の断片または演算子への結果の拡張に関する未解決の問いを残している。