 Probabilistic CTL

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