CTL probabilístico

La lógica de árbol de computación probabilística (PCTL) es una extensión de la lógica de árbol de computación (CTL) que permite la cuantificación probabilística de propiedades descritas. Ha sido definida en el artículo de Hansson y Jonsson. ^{[ 1 ]}

PCTL es una lógica útil para definir propiedades de plazo flexible, por ejemplo, "tras una solicitud de servicio, existe al menos un 98 % de probabilidad de que el servicio se realice en 2 segundos". Similar a la idoneidad de CTL para la verificación de modelos, la extensión PCTL se utiliza ampliamente como lenguaje de especificación de propiedades para verificadores de modelos probabilísticos.

Una posible sintaxis de PCTL se puede definir de la siguiente manera:

En esto,${\displaystyle a\in A}$para algún conjunto finito${\displaystyle A}$de proposiciones atómicas,${\displaystyle \sim \in \{<,\leq,\geq,>\}}$es un operador de comparación y${\displaystyle \lambda }$es un umbral de probabilidad. Las fórmulas de PCTL se interpretan sobre cadenas de Markov discretas . Una estructura de interpretación es una cuádruple.${\displaystyle K=\langle S,s^{i},{\mathcal {T}},L\rangle }$, dónde

• ${\displaystyle S}$es un conjunto finito de estados,
• ${\displaystyle s^{i}\in S}$es un estado inicial,
• ${\displaystyle {\mathcal {T}}}$es una función de probabilidad de transición,${\displaystyle {\mathcal {T}}:S\times S\to [0,1]}$, de tal manera que para todo${\displaystyle s\in S}$tenemos${\displaystyle \sum _{s'\in S}{\mathcal {T}}(s,s')=1}$, y
• ${\displaystyle L}$es una función de etiquetado,${\displaystyle L:S\to 2^{A}}$, asignando proposiciones atómicas a los estados.

Un camino${\displaystyle \sigma }$de un estado${\displaystyle s_{0}}$es una secuencia infinita de estados ${\displaystyle s_{0}\to s_{1}\to \dots \to s_{n}\to \dots }$. El n-ésimo estado del camino se denota como${\displaystyle \sigma [n]}$ y el prefijo de${\displaystyle \sigma }$de longitud${\displaystyle n}$se denota como${\displaystyle \sigma \uparrow n}$.

Una medida de probabilidad${\displaystyle \mu _{m}}$en el conjunto de caminos con un prefijo común de longitud${\displaystyle n}$viene dado por el producto de las probabilidades de transición a lo largo del prefijo del camino:

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

Para${\displaystyle n=0}$La medida de probabilidad es igual a${\displaystyle \mu _{m}(\{\sigma \in X:\sigma \uparrow 0=s_{0}\})=1}$.

La relación de satisfacción${\displaystyle s\models _{K}f}$se define inductivamente de la siguiente manera:

• ${\displaystyle s\models _{K}a}$si y solo si${\displaystyle a\in L(s)}$,
• ${\displaystyle s\models _{K}\neg f}$si y solo si no${\displaystyle s\models _{K}f}$,
• ${\displaystyle s\models _{K}f_{1}\lor f_{2}}$si y solo si${\displaystyle s\models _{K}f_{1}}$o${\displaystyle s\models _{K}f_{2}}$,
• ${\displaystyle s\models _{K}f_{1}\land f_{2}}$si y solo si${\displaystyle s\models _{K}f_{1}}$y${\displaystyle s\models _{K}f_{2}}$,
• ${\displaystyle s\models _{K}{\mathcal {P}}_{\sim \lambda }(f_{1}{\mathcal {U}}f_{2})}$si y solo si${\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 } , y
• ${\displaystyle s\models _{K}{\mathcal {P}}_{\sim \lambda }(\square f)}$si y solo si${\displaystyle \mu _{m}(\{\sigma$ :\sigma [0]=s\land (\forall i\geq 0)\sigma [i]\models _{K}f\})\sim \lambda } .

• Lógica de árbol de computación
• Lógica temporal