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 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:



Therein, is comparison operator and is a probability threshold.


Formulas of PCTL are interpreted over discrete Markov chains. An interpretation structure
is a quadruple , where

• is a finite set of states,
• is an initial state,
• is a transition probability function, , such that for all we have , and
• is a labeling function, , assigning atomic propositions to states.

A path from a state is an infinite sequence of states
. The n-th state of the path is denoted as
and the prefix of of length is denoted as .

Probability Measure

A probability measure of the set of path with the common prefix of length is equal to the product of transitions probabilitites along the prefix of the path:

For the probability measure is equal to .

Satisfaction relations

Satisfaction relations , are inductively defined as follows:

• if and only if ,
• if and only if not ,
• if and only if or ,
• if and only if and ,
• if and only if , and
• if and only if .