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. ϕ ::= p ∣ ¬ p ∣ ϕ ∨ ϕ ∣ ϕ ∧ ϕ ∣ P ∼ λ ( ϕ U ϕ ) ∣ P ∼ λ ( ◻ ϕ ) {displaystyle phi ::=pmid eg pmid phi lor phi mid phi land phi mid {mathcal {P}}_{sim lambda }(phi {mathcal {U}}phi )mid {mathcal {P}}_{sim lambda }(square phi )} 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. 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.