Probabilistic CTL

Template:More footnotes Probabilistic Computation Tree Logic (PCTL) is an extension of computation tree logic (CTL) that allows for probabilistic quantification of described properties. It has been defined in the paper by Hansson and Jonsson.

PCTL is a useful logic for stating soft deadline properties, e.g. "after a request for a service, there is at least a 98% probability that the service will be carried out within 2 seconds". Akin CTL suitability for model-checking PCTL extension is widely used as a property specification language for probabilistic model checkers.

PCTL syntax

A possible syntax of PCTL can be defined as follows:

$\varphi ::=p\mid \mathrm{\neg }\varphi \mid \varphi \vee \varphi \mid \varphi \wedge \varphi \mid {𝒫}_{\sim \lambda }(\varphi 𝒰\varphi )\mid {𝒫}_{\sim \lambda }(◻\varphi )$

Therein, $\sim \in \{<,\le ,\ge ,>\}$ is a comparison operator and $\lambda$ is a probability threshold.
Formulas of PCTL are interpreted over discrete Markov chains. An interpretation structure is a quadruple $K=⟨S,s^i,𝒯,L⟩$, where

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

A path $\sigma$ from a state $s_0$ is an infinite sequence of states $s_0\to s_1\to \dots \to s_n\to \dots$. The n-th state of the path is denoted as $\sigma [n]$ and the prefix of $\sigma$ of length $n$ is denoted as $\sigma \uparrow n$.

Probability measure

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

${\mu }_m(\{\sigma \in X:\sigma \uparrow n=s_0\to \dots \to s_n\})=𝒯(s_0,s_1)\times \dots \times 𝒯(s_{n-1},s_n)$

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

Satisfaction relation

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

• $s{\models }_{K}a$ if and only if $a\in L(s)$,
• $s{\models }_K\mathrm{\neg }f$ if and only if not $s{\models }_{K}f$,
• $s{\models }_K{f}_1\vee f_2$ if and only if $s{\models }_K{f}_1$ or $s{\models }_K{f}_2$,
• $s{\models }_K{f}_1\wedge f_2$ if and only if $s{\models }_K{f}_1$ and $s{\models }_K{f}_2$,
• $s{\models }_K{𝒫}_{\sim \lambda }(f_1𝒰f_2)$ if and only if ${\mu }_m(\{\sigma :\sigma [0]=s\wedge (\mathrm{\exists }i)\sigma [i]{\models }_K{f}_2\wedge (\mathrm{\forall }0\le j<i)\sigma [j]{\models }_K{f}_1\})\sim \lambda$, and
• $s{\models }_K{𝒫}_{\sim \lambda }(◻f)$ if and only if ${\mu }_m(\{\sigma :\sigma [0]=s\wedge (\mathrm{\forall }i\ge 0)\sigma [i]{\models }_{K}f\})\sim \lambda$.

See also

• Computation tree logic
• Temporal logic