技術要約：シミュレーション同値性における最小および標準的商

問題提起

ラベル付き遷移系（LTS）は、様々な高次仕様言語の基礎となる意味論的モデルとして機能する。状態空間爆発問題を管理するための一般的な手法は、**商（quotienting）**であり、これは等価な状態を統合することで、意味的に同等な、より小さなシステムを生成するものである。強双模倣性（strong bisimilarity）、分岐双模倣性（branching bisimulation）、およびトレース同値性（trace equivalence）については、商関数とその性質（標準性と最小性）が確立されているが、**弱シミュレーション同値性（weak simulation equivalence）および結合類似性（coupled similarity）**に関する挙動については、未だ十分に探求されていない。

他の同値性に関する既存の研究では、成功の度合いが異なることが示されている：

• 双模倣性については、商は標準的（同型を除いて一意的）であり、かつ最小である。
• トレース同値性については、最小の商が一意的ではない場合があり、その計算はPSPACE完全である。
• 弱シミュレーションおよび結合類似性については、標準的な商や最小の商が存在するかどうかは不明であり、それらを計算する複雑性も確立されていない。

本論文は、弱シミュレーション同値性（$\equiv_S$）および結合類似性（$\equiv_{CS}$）に対する標準的および最小の商の存在を調査し、それらを見つけるための計算複雑性を分析する。

手法

著者らは、任意のLTSをその同値類の代表元へと変換するための抽象的な手順を開発している。この手法は、シミュレーション前順序の性質と、特定の$\tau$-法則（観測不能なアクションを制御する公理）に基づく一連の変換に依存している。

1. 普遍的商と冗長性の除去

プロセスは、すべての等価な状態を統合する$\forall$-商から始まる。しかし、これだけでは不十分であり、それは「慣性的（inert）」な遷移（等価な状態間の遷移）や「重複」遷移を導入する可能性がある。

• 被覆された遷移（Covered Transitions）: 著者らは、重複遷移の概念を被覆された遷移へと一般化している。遷移 $p \xrightarrow{\alpha} q$ が「被覆されている」とは、別の遷移 $p' \xrightarrow{\alpha} q'$ が存在し、$p$ が $\tau$-ステップを経て $p'$ に到達可能であり、かつ $q$ が $q'$ によってシミュレートされる（$q \sqsubseteq_x q'$）ことを指す。
• 被覆された遷移を除去することは、同値性を保持しながら状態空間を削減するが、得られるLTSは必ずしも標準的でも最小でもない。

2. $\tau$-脱飽和（標準性のために）

標準性を達成するために、著者らは $\tau.x = x$ および $\tau.(\tau.x + y) = \tau.x + y$ という公理に基づく**$\tau$-脱飽和（$\tau$-desaturation）**を導入する。

• 操作: もし状態 $p$ が $q$ への $\tau$-遷移を持つ場合（$p \xrightarrow{\tau} q$）、その遷移は除去され、$p$ は $q$ のすべての出力遷移で「飽和」される。結合類似性の場合は、これに加えて $q$ が出力 $\tau$-遷移を持つ必要がある。
• 効果: この変換は連続する $\tau$-遷移を排除し、状態への入力遷移を減少させる。繰り返し適用することで終了し、**脱飽和された（desaturated）**LTSが得られる。
• 結果: $\forall$-商、$\tau$-脱飽和、被覆された遷移の除去、および到達不能な状態の除去を組み合わせることで、著者らは**簡約された（reduced）LTSを定義する。彼らは、同値な2つの簡約されたLTSは互いに同型であることを証明し、これにより標準的な商（canonical quotient）**の存在を確立した。

3. $\tau$-飽和（最小性のために）

最小性を達成するために、著者らは逆の操作である**$\tau$-飽和（$\tau$-saturation）**を導入する。

• 操作: もし $q \sqsubseteq_x p$ であれば、$\tau$-遷移 $p \xrightarrow{\tau} q$ を追加できる。これにより、既存の遷移が「被覆可能（coverable）」になり、それらを除去できるようになる。
• 最適化の課題: どの $\tau$-飽和ステップを追加するかという選択は非決定論的である。異なる選択は異なる削減をもたらす。最大級の削減を行うための最適な $\tau$-飽和ステップの集合を選択する問題は、**集合被覆問題（Set Cover Problem）**と等価であることが示されている。
• アルゴリズム: 最小の商手順は、まず標準的な商を計算し、次に各状態に対して「被覆可能な」遷移を特定する。そして、各状態に対して集合被覆問題のインスタンスを解くことで、他の遷移を最大限に除去することを可能にする最小の $\tau$-遷移の集合を決定する。

主な貢献と結果

1. 標準的な商の存在

本論文は、弱シミュレーション同値性と結合類似性の両方について、標準的な商が存在することを証明している。

• 定理 4.4: 2つの簡約されたLTS（脱飽和され、被覆された遷移がなく、到達不能な状態がなく、慣性的遷移がなく、等価な状態がないもの）は、互いに同型であることと、それらが同値であることは同値である。
• アルゴリズム 1: この標準的な商を計算するための多項式時間のプロシージャが提供されている。

2. 最小の商の複雑性

本論文は、最小の商（状態数と遷移数のレキシコグラフィカルに最小の商）を計算することがNP完全であることを確立している。

• 定理 5.5: $\equiv_x$ に関する最小化はNP困難である。これは集合被覆問題からの帰着によって証明されている。
• 含意: 双模倣性最小化（多項式時間で可能）とは異なり、シミュレーション同値性のための絶対的に最小の等価なLTSを見つけることは、一般的なケースにおいて計算量的に困難である。
• アルゴリズム 2: 集合被覆問題のオラクルを利用して最小の商を計算する手順が記述されている。このアルゴリズム自体は（NP困難な部分問題のために）多項式時間ではないが、最新の集合被覆ソルバーを利用することを可能にする。これらのソルバーに生成されるインスタンスは、通常、状態の出次数によって制限されるほど小さい。

3. 双模倣性との相違

これらの結果は、双模倣性からの根本的な乖離を浮き彫りにしている：

• 双模倣性の場合、最小の商は一意的であり、多項式時間で計算可能である。
• シミュレーション同値性の場合、最小の商は一意的ではない可能性があり（同じ同値類に対して複数の非同型な最小LTSが存在し得る）、その探索はNP完全である。

意義と主張

本論文は、研究が進んでいる双模倣性とトレース同値性を超えて、商化の理論的理解を拡張することを主張している。

• 一般化: 本アプローチは「重複遷移」の概念を一般化し、シミュレーション前順序に特有の $\tau$-法則を利用して標準形を導出する。
• 実用性: 絶対的な最小の商を見つけることはNP完全であるが、提案された手法により、LTSの最小化において生じる具体的なインスタンスは小さいため、効率的な集合被覆ソルバーを活用して大幅な状態空間の削減を実現できる。
• 謙虚な姿勢: 著者らは、自らの結果が弱シミュレーションおよび結合類似性の特定の $\tau$-法則に依存していることを明記している。彼らは、これらの結果が線形時間・分岐時間（LBT）スペクトル全体に一般化できるとは主張しておらず、異なる同値性には異なる $\tau$-法則と変換戦略が必要であることを示唆している。

結論として、本論文は、弱シミュレーションおよび結合類似性に対して、標準的な商および最小の商の両方を得るための初めての抽象的な手順を提供しており、前者を多項式時間で計算可能、後者をNP完全として特徴付けている。