技術要約：確率的双模倣類似性距離の連続性について

1. 問題提起

確率的双模倣類似性（Probabilistic bisimilarity）は、ラベル付きマルコフ連鎖（LMC）における標準的な振る舞いの同値性であり、状態空間の最小化やシステムの特性検証に使用される。しかし、厳密な双模倣類似性は脆弱である。遷移確率のわずかな摂動によって、状態間の同値性が完全に失われることがある。この問題に対処するため、振る舞いの差異の定量的尺度として確率的双模倣類似性距離（$\delta_\tau$）が導入された。ここで、$\delta_\tau(s, t) = 0$ であることは、$s$ と $t$ が双模倣類似であることを意味する。

この指標の決定的な制限は、その不連続性の可能性にある。Jaegerら [25] が指摘したように、遷移確率の小さな変化によって、状態間の距離に大きく、かつ急激な跳躍が生じることがある。このような連続性の欠如は、遷移確率が実験データからの近似値であることが多い経験的に導出されたモデルへの適用性を損なう。もし距離が不連続であれば、状態を統合したりモデル検査の結果を近似したりすることに依存するのは危険である。なぜなら、「見かけ上の類似性」が不確実性に対して頑健ではない可能性があるからである。

先行研究 [17] において、著者らは双模倣類似な状態ペアに対する双模倣距離の連続性のための十分条件として、ロバストな確率的双模倣類似性（$\simeq$）を導入した。しかし、以下の2つの根本的な問いが未解決のまま残されていた。

1. ロバストな双模倣類似性は、連続性のための必要条件でもあるのか？
2. 非双模倣な状態ペアに対して、どのように連続性を特徴付け、判定できるのか？

2. 手法および理論的枠組み

本論文は、積状態空間 $S \times S$ 上の結合（coupling）と方策（policy）の理論的枠組みを拡張することで、これらの問いに取り組む。

2.1 前提知識

著者らは、結合に基づく双模倣の標準的な定義（定義3）を利用する。双模倣類似距離 $\delta_\tau$ は、遷移分布のすべての結合に対して期待距離を最小化する関数 $\Delta_\tau$ の最小不動点として定義される。
極めて重要なことに、この距離は方策（定義10）を介して特徴付けられる。方策 $P$ は $S \times S$ 上のマルコフ連鎖を誘導する。距離 $\delta_\tau(s, t)$ は、誘導された連鎖において $(s, t)$ からラベルの異なるペアの集合（$S^2_1$）に到達する最小確率に対応する（命題11）。

2.2 ロバストな双模倣類似性と連続性

ロバストな双模倣類似性（$s \simeq t$）は、$(s, t)$ から対角集合 $S^2_\Delta$（状態が同一である集合）に到達する確率が1となるような方策 $P$ の存在として定義される。

• 既知の結果（定理13）： もし $s \simeq t$ ならば、$\delta_{(\cdot)}(s, t)$ は $\tau$ において連続である。
• 新たな貢献（定理14）： 著者らはその逆も成立することを証明した。すなわち、双模倣な状態（$s \sim t$）において、距離関数の連続性は、$s \simeq t$ であることと同値である。これにより、ロバストな双模倣類似性が、双模倣なペアの集合内における連続性のための必要十分条件であることが確立された。

2.3 任意のペアに対する一般的な特徴付け

本論文は、分析を任意の（非双模倣なものを含む）状態ペアへと拡張している。

• 定理17： 任意の $s, t \in S$ について、距離関数 $\delta_{(\cdot)}(s, t)$ が $\tau$ で連続であるための必要十分条件は、$(s, t)$ から $S^2_\Delta$ に到達する確率が正確に $1 - \delta_\tau(s, t)$ となるような方策 $P$ が存在することである。
  • この条件は、対角への到達における「損失」（これが距離を1に増大させる要因となる）が、距離の値自体によって正確に相殺されていることを意味する。
  • もしそのような方策が存在しない場合（すなわち、対角への最大到達確率が $1 - \delta_\tau(s, t)$ よりも厳密に小さい場合）、距離は不連続となる。

2.4 アルゴリズムによる決定手順

定理17に基づき、著者らはすべての状態ペアに対して連続性を多項式時間で判定するアルゴリズム1を開発した。

• メカニズム： このアルゴリズムは、「悪い」集合（双模倣であるがロバストではないペア、または必然的にラベルの不一致を招くペア）を通過することなく、ロバストな集合に到達できないペアを反復的に特定することで、不連続なペアを計算する。
• 不動点の計算： アルゴリズムは、状態ペアの格子上の単調関数 $A$ および $B$ を使用する。最小不動点 $\alpha$（不連続なペア）と最大不動点 $\beta$（連続なペア）を計算する。
• 計算量： 最適な結合のチェック（アルゴリズム1の6行目）は、最小費用最大流問題（命題25）に帰着され、多項式時間で解ける。アルゴリズム全体の実行時間は、状態空間のサイズに対して多項式時間である。

3. 主な貢献

1. ロバストな双模倣類似性の必要性の証明： 本論文は、ロバストな双模倣類似性が、双模倣な状態における双模倣類似距離の連続性のための十分条件であるだけでなく、必要条件でもあることを証明し、[17] の予想を解決した。
2. 完全な特徴付け： 著者らは、定理17を通じて、すべての ペア（双模倣および非双模倣の両方）に対する連続性の完全な理論的特徴付けを提供し、連続性を対角への到達を最大化する特定の方策の存在へと結びつけた。
3. 多項式時間の決定アルゴリズム： すべての状態ペアに対して連続性を判定する新しいアルゴリズムが提示された。
4. 実験的検証： アルゴリズムはPRISMモデルチェッカーに実装された。Quantitative Verification Benchmark Set (QVBS) およびランダム化されたJavaアルゴリズム（jpf-probabilistic経由）を用いた実験により、連続性の判定が、距離自体の計算と比較して最小限のオーバーヘッドしか発生しないことが示された。多くの場合、連続性のチェックは距離の計算よりも大幅に高速であった。

4. 結果および実験的評価

実験的評価は、従来の双模倣類似性とロバスト双模倣類似性の下で最小化されたモデルが異なるベンチマーク（不連続性の可能性を示すもの）に焦点を当てた。

• 効率性： ほとんどのベンチマークにおいて、連続性を判定するために必要な時間は、双模倣類似距離を計算するために必要な時間と同等か、それよりも短かった。例えば、oscillators ベンチマークでは、距離計算に約5秒かかったのに対し、連続性チェックは約0.002秒であった。
• 自明なケース： 距離がすべてのペアに対して連続である場合（例：従来の双模倣類似とロバスト双模倣類似が一致する場合）、アルゴリズムはほぼ即座に終了する。
• 実用性： 実験結果は、連続性の検証という「追加のステップ」が計算量的に実行可能であり、遷移確率に不確実性があるモデルに対して頑健性の保証を提供することを確認した。

5. 意義および主張

本論文は、確率的双模倣類似性距離の連続性に関する理論的空白を埋めるものである。ロバストな双模倣類似性が双模倣の場合の連続性のための正確な条件であることを証明し、すべてのペアに対する一般的な特徴付けを提供することで、本研究は実務家が以下を行うことを可能にする：

• 頑健性の評価： 2つの状態間の振る舞いの類似性が、遷移確率の小さな摂動に対して安定しているかどうかを判断する。
• 安全なモデル簡約： 連続性が保証されている場合にのみ、経験的に導出されたモデルにおいて状態を安全に統合し、モデル検査の結果を無効にする「距離の跳躍」のリスクを回避する。
• 効率的な検証： 連続性のチェックを、無視できるほどのパフォーマンスコストで既存の検証ワークフローに統合する。

著者らは、現在の研究は決定可能性と特徴付けを確立するものであるが、将来的には、摂動の下で距離がどの程度増加するかについての定量的境界を提供し、グラフ構造を保存する摂動の下での連続性を調査することを目指すと述べている。