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

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

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

Синтаксис PCTL

Один из возможных синтаксисов PCTL определяется следующим образом:

${displaystyle phi ::=pmid eg pmid phi lor phi mid phi land phi mid {mathcal {P}}_{sim lambda }(phi {mathcal {U}}phi )mid {mathcal {P}}_{sim lambda }(square phi )}$

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

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

Тропинка ${displaystyle sigma }$ из государства ${displaystyle s_{0}}$ бесконечная последовательность состояний ${displaystyle s_{0} o s_{1} o dots o s_{n} o 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} o dots o s_{n}})={mathcal {T}}(s_{0},s_{1}) imes dots imes {mathcal {T}}(s_{n-1},s_{n})}$

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

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

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

• ${displaystyle smodels _{K}a}$ если и только если ${displaystyle ain L(s)}$,
• ${displaystyle smodels _{K}eg f}$ если и только если нет ${displaystyle smodels _{K}f}$,
• ${displaystyle smodels _{K}f_{1}lor f_{2}}$ если и только если ${displaystyle smodels _{K}f_{1}}$ или же ${displaystyle smodels _{K}f_{2}}$,
• ${displaystyle smodels _{K}f_{1}land f_{2}}$ если и только если ${displaystyle smodels _{K}f_{1}}$ и ${displaystyle smodels _{K}f_{2}}$,
• ${displaystyle smodels _{K}{mathcal {P}}_{sim lambda }(f_{1}{mathcal {U}}f_{2})}$ если и только если ${displaystyle mu _{m}({sigma :sigma [0]=sland (exists i)sigma [i]models _{K}f_{2}land (forall 0leq j<i)sigma [j]models _{K}f_{1}})sim lambda }$, и
• ${displaystyle smodels _{K}{mathcal {P}}_{sim lambda }(square f)}$ если и только если ${displaystyle mu _{m}({sigma :sigma [0]=sland (forall igeq 0)sigma [i]models _{K}f})sim lambda }$.

Смотрите также

• Логика дерева вычислений
• Временная логика

Рекомендации

1. Ханссон, Ханс и Бенгт Йонссон. «Логика рассуждений о времени и надежности». Формальные аспекты вычислений 6.5 (1994): 512-535.