確率的CTL

確率的計算ツリー論理(PCTL) は、記述された特性の確率的定量化を可能にする計算ツリー論理(CTL)の拡張です。これは、Hansson と Jonsson の論文で定義されています。^{[ 1 ]}

PCTLは、例えば「サービス要求後、サービスが2秒以内に実行される確率は少なくとも98%である」といった、緩やかな期限に関する特性を記述するのに便利な論理体系です。CTLと同様に、PCTL拡張は確率的モデルチェッカーの特性記述言語として広く用いられ、モデル検査に適しています。

PCTLの構文は、以下のように定義できる。

その中で、${\displaystyle a\in A}$ある有限集合に対して${\displaystyle A}$原子命題の、${\displaystyle \sim \in \{<,\leq ,\geq ,>\}}$は比較演算子であり、${\displaystyle \lambda }$は確率閾値です。PCTL の式は離散マルコフ連鎖上で解釈されます。解釈構造は四つ組です。${\displaystyle K=\langle S,s^{i},{\mathcal {T}},L\rangle }$、 どこ

• ${\displaystyle S}$は有限の状態の集合であり、
• $\displaystyle s^{i}\in S$初期状態です。
• $\displaystyle {\mathcal {T}}}$は遷移確率関数であり、${\displaystyle {\mathcal {T}}:S\times S\to [0,1]}$、すべてのに対して${\displaystyle s\in S}$我々は持っています${\displaystyle \sum _{s'\in S}{\mathcal {T}}(s,s')=1}$、 そして
• ${\displaystyle L}$これはラベル付け関数です。${\displaystyle L:S\to 2^{A}}$原子命題を状態に割り当てる。

道${\displaystyle \sigma }$ある州から$s0$無限の状態列 $\displaystyle s_{0}\to s_{1}\to \dots \to s_{n}\to \dots }$パスのn番目の状態は次のように表される。${\displaystyle \sigma [n]}$ そして接頭辞${\displaystyle \sigma }$長さ${\displaystyle n}$と表記される${\displaystyle \sigma \uparrow n}$。

確率尺度${\displaystyle \mu _{m}}$長さが共通の接頭辞を持つパスの集合について${\displaystyle n}$これは、パスの接頭辞に沿った遷移確率の積によって与えられる。

${\displaystyle \mu _{m}(\{\sigma \in X:\sigma \uparrow n=s_{0}\to \dots \to s_{n}\})={\mathcal {T}}(s_{0},s_{1})\times \dots \times {\mathcal {T}}(s_{n-1},s_{n})}$

のために${\displaystyle n=0}$確率測度は${\displaystyle \mu _{m}(\{\sigma \in X:\sigma \uparrow 0=s_{0}\})=1}$。

満足度関係${\displaystyle s\models _{K}f}$は、以下のように帰納的に定義される。

• ${\displaystyle s\models _{K}a}$かつその場合に限り${\displaystyle a\in L(s)}$、
• ${\displaystyle s\models _{K}\neg f}$の場合のみ、${\displaystyle s\models _{K}f}$、
• ${\displaystyle s\models _{K}f_{1}\lor f_{2}}$かつその場合に限り$\displaystyle s\models _{K}f_{1}}$または$s\models_Kf2$、
• $\displaystyle s\models _{K}f_{1}\land f_{2}}$かつその場合に限り$\displaystyle s\models _{K}f_{1}}$そして$s\models_Kf2$、
• ${\displaystyle s\models _{K}{\mathcal {P}}_{\sim \lambda }(f_{1}{\mathcal {U}}f_{2})}$かつその場合に限り${\displaystyle \mu _{m}(\{\sigma$ :\sigma [0]=s\land (\exists i)\sigma [i]\models _{K}f_{2}\land (\forall 0\leq j<i)\sigma [j]\models _{K}f_{1}\})\sim \lambda } 、および
• ${\displaystyle s\models _{K}{\mathcal {P}}_{\sim \lambda }(\square f)}$かつその場合に限り${\displaystyle \mu _{m}(\{\sigma$ :\sigma [0]=s\land (\forall i\geq 0)\sigma [i]\models _{K}f\})\sim \lambda } .

• 計算ツリーロジック
• 時間論理