The Satisfiability and Validity Problems for Probabilistic CTL

Probabilistic CTL is obtained from the standard CTL (Computational Tree Logic) by replacing the existential and universal path quantifiers with the probabilistic operator where the probability of runs satisfying a given path formula is bounded by a rational constant. We survey the existing results about the satisfiability and validity problems for probabilistic CTL, and we also present some of the underlying proof techniques.