Вероятностный CTL

Логика вероятностного дерева вычислений (PCTL) — это расширение логики дерева вычислений (CTL), которое позволяет проводить вероятностную количественную оценку описанных свойств. Это было определено в статье Ханссона и Йонссона. ^[1]

PCTL — это полезная логика для указания свойств мягкого срока, например «после запроса на услугу существует по крайней мере 98% вероятность того, что услуга будет выполнена в течение 2 секунд». Пригодность Akin CTL для проверки моделей Расширение PCTL широко используется в качестве языка спецификации свойств для средств проверки вероятностных моделей.

Синтаксис PCTL

Возможный синтаксис PCTL можно определить следующим образом:

$\phi ::=p\mid \neg \phi \mid \phi \lor \phi \mid \phi \land \phi \mid {\mathcal {P}}_{\sim \lambda }(\phi {\mathcal {U}}\phi )\mid {\mathcal {P}}_{\sim \lambda }(\square \phi )$

В этом, $\sim \in \{<,\leq ,\geq ,>\}$ является оператором сравнения и $\lambda$ является порогом вероятности.
Формулы PCTL интерпретируются над дискретными цепями Маркова . Структура интерпретации четверка $K=\langle S,s^{i},{\mathcal {T}},L\rangle$ , где

$S$ представляет собой конечное множество состояний,
$s^{i}\in S$ это начальное состояние,
${\mathcal {T}}$ — функция вероятности перехода, ${\mathcal {T}}:S\times S\to [0,1]$ , такой, что для всех $s\in S$ у нас есть $\sum _{s'\in S}{\mathcal {T}}(s,s')=1$ , и
$L$ это функция маркировки, $L:S\to 2^{A}$ , присваивая состояниям атомарные предложения.

Путь $\sigma$ из штата $s_{0}$ это бесконечная последовательность состояний $s_{0}\to s_{1}\to \dots \to s_{n}\to \dots$ . n-е состояние пути обозначается как $\sigma [n]$ и префикс $\sigma$ длины $n$ обозначается как $\sigma \uparrow n$ .

Вероятностная мера

Вероятностная мера $\mu _{m}$ на множестве путей с общим префиксом длины $n$ определяется произведением вероятностей перехода по префиксу пути:

\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})

Для $n=0$ вероятностная мера равна $\mu _{m}(\{\sigma \in X:\sigma \uparrow 0=s_{0}\})=1$ .

Отношение удовлетворенности

Отношение удовлетворения $s\models _{K}f$ индуктивно определяется следующим образом:

$s\models _{K}a$ тогда и только тогда, когда $a\in L(s)$ ,
$s\models _{K}\neg f$ тогда и только тогда, когда нет $s\models _{K}f$ ,
$s\models _{K}f_{1}\lor f_{2}$ тогда и только тогда, когда $s\models _{K}f_{1}$ или $s\models _{K}f_{2}$ ,
$s\models _{K}f_{1}\land f_{2}$ тогда и только тогда, когда $s\models _{K}f_{1}$ и $s\models _{K}f_{2}$ ,
$s\models _{K}{\mathcal {P}}_{\sim \lambda }(f_{1}{\mathcal {U}}f_{2})$ тогда и только тогда, когда $\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$ , и
$s\models _{K}{\mathcal {P}}_{\sim \lambda }(\square f)$ тогда и только тогда, когда $\mu _{m}(\{\sigma :\sigma [0]=s\land (\forall i\geq 0)\sigma [i]\models _{K}f\})\sim \lambda$ .