A Bisimulation-Invariance-Based Approach to the Separation of Polynomial Complexity Classes

技術要約：多項式時間計算量クラスの分離に向けた、双模倣不変性に基づくアプローチ

1. 問題設定
本論文は、$P = NP$（および、ひいては$P = PSPACE$）という根本的な未解決問題に取り組んでいる。記述計算量理論は、論理的定式化（例：$NP = \exists SO$, $PSPACE = FO + PFP$）を用いて、$NP$, $PSPACE$, $ExpTime$といった計算量クラスを特徴付けることに成功してきたが、一般的な、順序付けられていない構造におけるクラス$P$ の特徴付けは依然として困難なままである。この困難さは「順序問題（order problem）」として知られている。すなわち、$P$ の論理的特徴付けは通常、入力構造に対する明示的な全順序を必要とするが、計算量クラス $P$ に属する問題は本質的にそのような順序を持たないためである。

著者らは、これらの計算量クラスの双模倣不変な断片（$P/\sim$ 対 $NP/\sim$ および $P/\sim$ 対 $PSPACE/\sim$）を分離することが、$P = NP$という一般的な問題を解決するための実行可能な経路を提供し得るかどうかを調査している。彼らは、$P \neq NP$を証明することは、$P/\sim \neq NP/\sim$ を証明することと等価であると仮定している。ただし、これは対象となるクラスが、双模倣不変な困難な問題を含んでいることを前提としている。

2. 手法および理論的枠組み
本論文は、既存の文献における2つの確立された結果に基づいている：

1. Ottoの定理 [28]： 多項式時間で計算可能な双模倣不変なクエリのクラス（$P/\sim$）は、多項式 $\mu$-計算量（Polyadic $\mu$-Calculus, $L^\omega_\mu$）によって正確に捉えられる。
2. モデル検査の還元 [4, 23]： 多項式 $\mu$-計算量のモデル検査問題は、「パワーグラフ（power graphs）」として知られる特定の積構成を通じて、通常の（単項の）$\mu$-計算量（$L_\mu$）のモデル検査問題へと還元できる。

著者らはこれらを組み合わせ、**相対的規則性（relative regularity）**に基づく枠組みを構築している：

• 木言語への還元： グラフとその木の展開（unfolding）は双模倣（bisimilar）であるため、双模倣不変な論理における定義可能性は、木言語の定義可能性へと還元される。
• パワーグラフ： グラフ $G$ に対し、$G^d$ は、$d$ 個の $G$ の非同期積であり、コンポーネントをルートに戻す「リセット」遷移によって強化されている。
• モノフィケーション（Monofication）： 文法的変換により、多項式 $\mu$-計算量（$G$ 上の）の論理式を、通常の $\mu$-計算量（$G^d$ 上の）の論理式へと変換する。
• 相対的規則性： 木言語 $L$ が文脈言語 $R$ に対して相対的に規則的であるとは、ある $L_\mu$ 論理式が存在して、$L$ のメンバーと非メンバーを $R$ 内において正しく区別できる（ただし、$R$ の外側にある木については任意の主張が可能である）ことを指す。

3. 主な貢献と特徴付け
本論文は、計算量クラスの分離が、特定の木言語の相対的な非規則性を証明することへと還元されることを確立している。

• 分離の等価性（定理1）： 本論文は、$P = NP$であることと$P/\sim = NP/\sim$であることは同値であり、同様に$PSPACE$ についても成立することを証明している。これは、双模倣不変な困難な問題、具体的には、1文字アルファベット上の非決定性有限オートマトン（NFA）の非普遍性問題（$1NonUnivNFA$）および2文字アルファベット上の非普遍性問題（$2NonUnivNFA$）の存在に基づいている。
• パワーグラフの特徴付け（セクション4）： 著者らは、$d$-冪（$d$-powers）に双模倣であるグラフに関する2つの特徴付けを提供している：
  1. 代数的特徴付け： 「永続性（persistence）」（一つのコンポーネントでの動作が他のコンポーネントに影響を与えない）および「リセット特性（reset property）」を満たす、$d$ 次元非同期双模倣によるもの。
  2. 論理的特徴付け： 特定の論理式（$\phi_{per}, \phi_{rst}, \phi_{pow}$）を用いた、二項 $\mu$-計算量（$L^2_\mu$）による定義可能性によるもの。
• 相対的ポンピング補題（補題13）： 著者らは、通常の規則的な木言語のためのポンピング補題を、相対的規則性の文脈へと適応させている。もし言語 $L$ が $R$ に対して相対的に規則的であれば、$L \cap R$ に属する任意の木に対して、パスのセグメントをポンプアップした結果得られる木が、$R$ 内に留まる限り、$L$ に留まり続けることを示している。これにより、非規則性の証明は著しく困難になる。なぜなら、ポンピングはパワーグラフの構造的制約の範囲内に厳密に制限されなければならないからである。

4. 主な結果
核心となる結果は、NFA非普遍性問題から導かれる木言語の非規則性と、計算量分離を結びつけている：

• 定理26： $P \neq NP$ であることと、すべての $d \ge 1$ に対して、言語 $1NonUnivNFA_d$（$1NonUnivNFA$のグラフの$d$-冪の木の展開）が$Power_d$（$d$-冪のグラフに双模倣な木の言語）に対して相対的に非規則的であることは同値である。
• 定理30： $P \neq PSPACE$ であることと、すべての $d \ge 1$ に対して、言語 $2NonUnivNFA_d$ が $Power_d$ に対して相対的に非規則的であることは同値である。

著者らはこれらの言語を明示的に構成している。例えば、$1NonUnivNFA_d$ は、すべてのパスにおいて、特定のコンポーネントにおける一連のアクション（リセットを無視したもの）が、最終的に受理カラー $f$ を持たない状態へと至るような木からなる。

5. 意義と主張
本論文は、$P=NP$ 問題に対する解決策ではなく、新たな攻撃ラインを提示していると控えめに主張している。その意義は以下の点にある：

• 順序問題の緩和： 構造に対する全順序の必要性を回避し、双模倣不変なクエリに焦点を当てることで、以前の記述計算量における $P$ の特徴付けにおける主要な障壁を回避している。
• 論理的表現力： 計算量クラスの分離を、特定の木言語（パワーグラフに対する通常の $\mu$-計算量）の論理的不表現性の問題へと再構成している。
• 実現可能性と課題： 著者らは、理論的な還元は確立されているものの、実際の相対的非規則性の証明には「高度な組合せ論的複雑さ」が伴うことを認めている。標準的な非規則性の証明では不十分であり、パワーグラフの構造的特性を厳密に維持するようなポンピング引数を作成しなければならない。

結論として、パワーグラフのキャラクター化（代数的および論理的な両面）は、そのような証明を試みるための必要な道具を提供している。また、他の主要な計算量クラスとは異なり、$NP/\sim$ に対する論理的特徴付けが現在未知であることも指摘しており、これがこの双模倣不変なアプローチを十分に活用する上での障壁となっている。