Probabilistic CTL

A possible syntax of PCTL can be defined as follows:

Therein, ${\displaystyle \sim \in \{<,\leq ,\geq ,>\}}$ is a comparison operator and ${\displaystyle \lambda }$ is a probability threshold.
Formulas of PCTL are interpreted over discrete Markov chains. An interpretation structure is a quadruple ${\displaystyle K=\langle S,s^{i},{\mathcal {T}},L\rangle }$, where

• ${\displaystyle S}$ is a finite set of states,
• ${\displaystyle s^{i}\in S}$ is an initial state,
• ${\displaystyle {\mathcal {T}}}$ is a transition probability function, ${\displaystyle {\mathcal {T}}:S\times S\to [0,1]}$, such that for all ${\displaystyle s\in S}$ we have ${\displaystyle \sum _{s'\in S}{\mathcal {T}}(s,s')=1}$, and
• ${\displaystyle L}$ is a labeling function, ${\displaystyle L:S\to 2^{A}}$, assigning atomic propositions to states.

A path ${\displaystyle \sigma }$ from a state ${\displaystyle s_{0}}$ is an infinite sequence of states ${\displaystyle s_{0}\to s_{1}\to \dots \to s_{n}\to \dots }$. The n-th state of the path is denoted as ${\displaystyle \sigma [n]}$ and the prefix of ${\displaystyle \sigma }$ of length ${\displaystyle n}$ is denoted as ${\displaystyle \sigma \uparrow n}$.

A probability measure ${\displaystyle \mu _{m}}$ on the set of paths with a common prefix of length ${\displaystyle n}$ is given by the product of transition probabilities along the prefix of the path:

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

For ${\displaystyle n=0}$ the probability measure is equal to ${\displaystyle \mu _{m}(\{\sigma \in X:\sigma \uparrow 0=s_{0}\})=1}$.

The satisfaction relation ${\displaystyle s\models _{K}f}$ is inductively defined as follows:

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

• Computation tree logic
• Temporal logic