Verification of Parametric Markov Automata under Time-bounded Reachability

技術要約：時間限定到達可能性におけるパラメトリック・マルコフ・オートマトン（pMA）の検証

問題設定
マルコフ・オートマトン（MA）は、非決定論的かつ連続的な時間を持つ確率的システムの構成的モデルであり、一般化確率的ペトリネットや動的故障木などのモデルのセマンティクスとして機能する。しかし、既存のモデル検査アルゴリズムは、すべての遷移率と確率が正確に既知である、完全に指定されたモデルを必要とする。この仮定は、パラメータが環境の不確実性や未知の要素に左右される可能性がある現実世界のシステムにおいては、しばしば非現実的である。

本論文は、遷移率および確率的な後続分布が固定された定数ではなく、パラメトリックな関数によって定義される**パラメトリック・マルコフ・オートマトン（pMA）**の検証に取り組む。著者らは、時間限定到達可能性特性（例：「時刻 $t$ 以内にゴール状態に到達する確率が $\theta$ を超えるか？」）に焦点を当てている。具体的には、以下の2つの問題を扱う：

1. 充足性の検証（Satisfaction Verification）： 与えられた領域内に、特性を充足または違反するパラメータ値が存在するかどうかを判定する。
2. 合成（Synthesis）： パラメータ空間を、特性を充足する領域と違反する領域に分割する。

この解析は、システムのスケジューラ（非決定論的な選択を行う）と「自然（Nature）」（パラメータ値を割り当てる）の相互作用に基づく、4つの異なる充足関係（Feasibility, Angelic-aid, Robust, Demonic）を考慮しなければならない。

手法
提案手法は、連続的なパラメトリック・モデルを、既存の合成技術が適用可能な離散モデルへと変換する2段階のプロセスを通じて、これらの問題を解決する。その際、導入される誤差を制御する。

1. 離散化と変換：

   • pMAはまずステップサイズ $\delta$ を用いて離散化され、連続時間モデルから**パラメトリック・マルコフ決定過程（pMDP）**へと変換される。このステップは、非パラメトリックなMAに関する従来の離散化結果を一般化したものである。
   • 確率的状態（PS）における即時遷移（時間の経過なしに発生するもの）を処理するために、著者らは状態消去法を採用し、確率的状態をマルコフ状態（MS）へと集約することで、モデルを標準的なステップ限定到達可能性問題（pMDP上の）へと変換する。
   • 離散化によって指数項（$e^{-\lambda \delta}$）が導入されるが、これは記号的なパラメータ合成において扱うのが困難であるため、著者らはこれらの項を部分テイラー展開を用いて近似する。これにより、「近似離散化pMA」が得られ、遷移確率は有理関数によって表現され、過大近似および過小近似によって制御される。

2. パラメータ・リフティング（PL）と検証：

   • 変換されたpMDPは、**パラメータ・リフティング（PL）**を用いて解析される。PL法は、パラメータの選択を、第2のプレイヤーである「自然」による非決定論的な選択として扱うことで、状態間の依存関係を抽象化する。これは確率的ゲームにおける手法である。
   • PL法は、到達確率の上限および下限を計算する。これらの境界値は、ユーザーが指定した閾値 $\theta$ と比較される。
   • 本手法は、精緻化スキームを利用する。もし境界値が決定不能な場合（すなわち、区間が閾値を跨いでいる場合）、パラメータ領域を分割し、プロセスを繰り返す。
   • 総誤差は、離散化誤差（$\epsilon_\delta$）、テイラー近似による誤差、およびPL抽象化によって導入される誤差の3つの項によって決定される。著者らは、離散化誤差が支配的な要因であることを示している。

主な貢献

• pMAの定義： パラメータ化されたレートおよび確率関数をMAに拡張した、パラメトリック・マルコフ・オートマトンを正式に導入した。
• 時間限定到達可能性のためのアルゴリズム： 時間限定到達可能性の制約下で、pMAの充足性検証およびパラメータ合成を実行可能な初のアルゴリズムを提示した。
• 一般化された離散化： Guckら[17]による離散化結果をパラメトリックな設定へと一般化し、離散化されたpMAが真のpMAの到達確率を境界付けることを証明した。
• 近似離散化： 指数項を扱うためにテイラー展開を用いた手法を導入し、有理関数ベースの合成ツールの利用を可能にした。
• 実装： 本手法は、Storm モデルチェッカー（Stormpy インターフェース経由）を用いて実装されており、pMAおよびパラメトリックCTMCの両方をサポートしている。

実験結果
著者らは、flexible-manufacturing、polling、kanban などのQCOMPベンチマークセットのモデルを含む一連のベンチマークを用いて実装を評価した。

• 検証： 充足性の検証において、ツールはテストされたすべてのベンチマークに対して決定的な回答を提示することに成功し、多くの場合、数秒以内で完了した。
• 合成： パラメータ合成において、ツールは小規模なモデルに対してパラメータ空間の分割に成功した。しかし、より大規模または複雑なモデルについては、頻繁に15分のタイムアウトに達した。
• 性能のボトルネック： 実験的解析により、離散化が主要な性能ボトルネックであることが特定された。計算コストは、誤差を減らすために離散化ステップ $\delta$ を小さくする場合、あるいはモデル内の最大滞在率が増加する場合に著しく増大する。
• 比較： パラメトリックCTMCに対するPRISM-PSYとの比較では、提案手法は（離散化を必要としないため）PRISM-PSYよりも低速であった。しかし、提案手法はPRISM-PSYが失敗する場面でも成功する。すなわち、pMAや、遷移率だけでなくパラメトリックな遷移確率（例：tandem ベンチマーク）を持つモデルを解析できる点である。

意義と主張
本論文は、信頼性工学において広く利用されているが、以前は完全に指定されたインスタンスに限定されていたモデルクラスであるマルコフ・オートマトンの解析を可能にすることで、形式検証における空白を埋めるものであると主張している。著者らは、離散化ステップが十分に小さい限り、本アプローチが任意の精度まで検証および合成の問題を解決できることを強調している。

著者らはスケーラビリティに関して謙虚な姿勢を維持しており、現在の実装が離散化のコストによって制限されていることを認めている。彼らは、性能の主なボトルネックがpMAの離散化に起因することを明示的に述べている。したがって、将来の研究として、離散化を完全に回避するアプローチ（例えば、連続時間確率的ゲームを直接解析するか、ユニフォーミゼーション技術を利用する手法）を調査すべきであると示唆しているが、これらの代替案も独自の計算上の課題をもたらす可能性があることも指摘している。本研究は、連続時間非決定論的システムのパラメトリック解析のための基礎的な枠組みを確立し、Stormのような既存のツールの能力を、より広いクラスのモデルにおけるパラメトリックな不確実性を扱う方向へと拡張するものである。