Probabilistic CTL

Probabilistic Computation Tree Logic is an extension of CTL which allows for probabilistic quantification of described properties. It has been defined in the paper by [http://citeseer.ist.psu.edu/hansson94logic.html 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

One of the possible syntax of PCTL is defined as follows:
$phi\; ::=\; p\; |\; eg\; p\; |\; phi\; lor\; phi\; |\; phi\; land\; phi\; |\; mathcal\{P\}\_\{simlambda\}(phi\; mathcal\{U\}\; phi)$
mathcal{P}_{simlambda}(squarephi)
Therein, is comparison operator and $lambda$ is a probability threshold.
Formulas of PCTL are interpreted over discrete Markov chains. An interpretation structureis a quadruple $K\; =\; langle\; S,\; s^i,\; mathcal\{T\},\; L\; angle$, where
*$S$ is a finite set of states,
*$s^i\; in\; S$ is an initial state,
*$mathcal\{T\}$ is a transition probability function, $mathcal\{T\}\; :\; S\; imes\; S\; o\; [0,1]$, such that for all $s\; in\; S$ we have $sum\_\{s\text{'}in\; S\}\; mathcal\{T\}(s,s\text{'})=1$, and
*$L$ is a labeling function, $L:S\; o2^A$, assigning atomic propositions to states.
A path $sigma$ from a state $s\_0$ is an inifite sequence of states $s\_0\; o\; s\_1\; o\; dots\; o\; s\_n\; o\; dots$. The n-th state of the path is denoted as $sigma\; [n]$and the prefix of $sigma$ of length $n$ is denoted as $sigmauparrow\; n$.

Probability Measure

A probability measure $mu\_m$ of the set of path with the common prefix of length $n$ is equal to the product of transitions probabilitites along the prefix of the path:
$mu\_m(\{sigma\; in\; X\; :\; sigmauparrow\; n\; =\; s\_0\; o\; dots\; o\; s\_n\; \})\; =\; mathcal\{T\}(s\_0,s\_1)\; imesdots\; imesmathcal\{T\}(s\_\{n-1\},s\_n)$
For $n\; =\; 0$ the probability measure is equal to $mu\_m(\{sigma\; in\; X\; :\; sigmauparrow\; 0\; =\; s\_0\; \})\; =\; 1$.

Satisfaction relations

Satisfaction relations $s\; models\_K\; f$, $sigma\; models\_K\; f$ are inductively defined as follows:
* $s\; models\_K\; a$ if and only if $a\; in\; L(s)$,
* $s\; models\_K\; eg\; f$ if and only if not $s\; models\_K\; f$,
* $s\; models\_K\; f\_1\; lor\; f\_2$ if and only if $s\; models\_K\; f\_1$ or $s\; models\_K\; f\_2$,
* $s\; models\_K\; f\_1\; land\; f\_2$ if and only if $s\; models\_K\; f\_1$ and $s\; models\_K\; f\_2$,
* $s\; models\_K\; mathcal\{P\}\_\{simlambda\}(f\_1\; mathcal\{U\}\; f\_2)$ if and only if , and
* $s\; models\_K\; mathcal\{P\}\_\{simlambda\}(square\; f)$ if and only if $mu\_m(\{sigma\; :\; sigma\; [0]\; =\; s\; land\; (forall\; i\; geq\; 0)sigma\; [i]\; models\_K\; f\})\; sim\; lambda$.