Probabilistic CTL

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.
One of the possible syntax of PCTL is defined as follows:
formula_1
Therein, formula_2 is comparison operator and formula_3 is a probability threshold.
<br>
Formulas of PCTL are interpreted over discrete Markov chains. An interpretation structure
is a quadruple formula_4, where 
<br>
A path formula_13 from a state formula_14 is an infinite sequence of states 
formula_15. The n-th state of the path is denoted as formula_16
and the prefix of formula_13 of length formula_18 is denoted as formula_19.
Probability measure.
A probability measure formula_20 of the set of path with the common prefix of length formula_18 is equal to the product of transitions probabilities along the prefix of the path:
formula_22
For formula_23 the probability measure is equal to formula_24.
Satisfaction relation.
The satisfaction relation formula_25 is inductively defined as follows: