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.
[1] 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.
A possible syntax of PCTL can be defined as follows:
is a comparison operator and
is a probability threshold.
Formulas of PCTL are interpreted over discrete Markov chains.
An interpretation structure is a quadruple
is an infinite sequence of states
The n-th state of the path is denoted as
A probability measure
on the set of paths with a common prefix of length
is given by the product of transition probabilities along the prefix of the path: For
the probability measure is equal to
The satisfaction relation
is inductively defined as follows: