技術要約：ラベル付きマルコフ連鎖におけるロバストな確率的双シミラリティ

問題提起

確率的双シミラリティ（probabilistic bisimilarity）は、確率システムの検証における基礎的な概念であり、振る舞いが区別できない状態を統合することで状態空間の最小化を可能にする。しかし、標準的な確率的双シミラリティは、遷移確率の微小な摂動に対してロバストではない。確率的双シミラリティ距離関数（振る舞いの擬距離）は状態間の類似性を定量化するが、これはしばしば不連続である。つまり、遷移確率の極めて小さな変化によって、2つの状態間の距離が0（双シミラ）から大きな値（例：1）へ、あるいはその逆に、不連続に跳ね上がる可能性がある。

この不連続性は、遷移確率が実験データから導出されており、本質的に近似的である実用的なアプリケーションにおいて、重大な信頼性の問題を引き起こす。本論文の例が示すように、2つの状態は公称モデル（$\varepsilon = 0$）では双シミラであるが、無限小の摂動（$\varepsilon > 0$）の下では、最大級に異なる長期的な振る舞い（例：到達可能性特性）を示すことがある。したがって、このような状態を最小化モデルにおいて統合することは、正確な遷移確率が未知である場合には安全ではない可能性がある。

手法

著者らは、標準的な確率的双シミラリティ（$\sim$）よりも厳格な部分集合として、ロバストな確率的双シミラリティ（$\simeq$）を導入している。その核心となる手法は以下の通りである：

1. 方策に基づく特徴付け: 本論文では、状態の積空間 $S \times S$ 上の「方策（policies）」（結合/couplings）の概念を利用する。方策 $P$ は、状態のペアを $S \times S$ 上の分布へと写像する。
2. ロバスト性の定義: 2つの状態 $s$ と $t$ がロバストに双シミラである（$s \simeq t$）とは、誘導されたマルコフ連鎖 $\langle S \times S, P \rangle$ において、ペア $(s, t)$ が対角集合 $S^2_\Delta = \{(s, s) \mid s \in S\}$ に確率1で到達するような方策 $P$ が存在することを意味する。
3. 連続性の保証: 著者らは、$s \simeq t$ であれば、確率的双シミラリティ距離関数 $\delta(s, t)$ は遷移関数 $\tau$ の摂動に対して連続であることを証明している。具体的には、$\tau$ に収束する遷移関数の列 $\tau_n$ に対して、$s \simeq t$ ならば $\lim_{n \to \infty} \delta_{\tau_n}(s, t) = 0$ が成立する。これは、標準的な双シミラリティにおいて、極限が公称点での距離と一致しない場合があることとは対照的である。
4. アルゴリズムによる計算: 本論文では、最大のロバスト双シミラ関係を計算するための多項式時間アルゴリズム（Algorithm 1）を提示している。このアルゴリズムは、以下の3つの関数を用いて、初期の双シミラな状態の集合を反復的に洗練させる：
   • Filter（フィルタ）: 現在の関係によって支持されるある方策の下で、対角集合 $S^2_\Delta$ に到達可能なペアを特定する。
   • Prune（除去）: 関係が「近傍」の定義に関して対称性と推移性を維持するようにする。
   • Bisim（双シミラ）: 現在の関係に含まれる最大の双シミラ関係を計算する。
     アルゴリズムは、これらの関数の合成の最大不動点において停止する。

主な貢献

• 形式的定義: 積空間における対角集合へのほとんど確実な到達を保証する方策を通じて定義される、ロバストな確率的双シミラリティの導入。
• 理論的保証: ロバストな確率的双シミラリティが、遷移確率の任意の摂動下における確率的双シミラリティ距離関数の連続性の十分条件であることを示す証明（定理2）。
• 効率的なアルゴリズム: ロバストな確率的双シミラリティを計算するための $O(n^6)$ アルゴリズム（$n$ は状態数）の開発。これにより、大規模な検証タスクへの適用が可能となる。
• 経験的検証: アルゴリズムを PRISM モデルチェッカー内に実装し、QVBS（Quantitative Verification Benchmark Set）および jpf-probabilistic 拡張からのベンチマークを用いて評価を行った。

実験結果

著者らは、170のモデルに対して実装の評価を行った。主な知見は以下の通りである：

• 実現可能性: ロバストな双シミラリティは、152のモデル（約89%）において1分未満で正常に計算された。
• 状態空間の差異: 最小化されたモデルが異なるケースにおいて、ロバストなアプローチは、従来の双シミラリティと比較して、感度のために統合すべきではないと判断された状態のペアを正しく識別し、結果として著しく大きな状態空間をもたらすことが多かった。
• パフォーマンスのオーバーヘッド: ロバストな双シミラリティは従来の双シミラリティよりも低速であり（ベンチマークに応じて平均28%から140,000%以上の時間増加、例：crowds ベンチマーク）、計算時間は標準的なモデルの多くについては実用的な範囲内に留まった。
• 限界: 10のモデル（約6%）において、従来の双シミラリティは成功したものの、ロバストなアルゴリズムはメモリ制約（OutOfMemoryError）により失敗した。これは nand および egl ベンチマークの特定のインスタンスで観察された。

意義と主張

本論文は、遷移確率が近似値である確率システムにおいて、状態の同値性を決定するためのより信頼性の高い方法として、ロバストな確率的双シミラリティを提供すると主張している。距離関数の連続性を保証することで、パラメータのわずかな変動下で振る舞いが異なる状態を誤って統合するリスクを軽減する。

著者らは、本研究を、高精度を必要とするミッションクリティカルなシステムへの実用的なステップとして位置づけている。彼らは、ロバストな双シミラリティは連続性の十分条件であるが、双シミラな状態に対する必要条件でもあるのではないかと推測している。最後に、論理的なロバスト双シミラリティの特性付けや、グラフ構造を保持する摂動と新しい遷移を導入する摂動の区別に関する調査など、今後の方向性を提示して締めくくっている。