Amir Pnueli and Lenore D. Zuck, "Probabilistic verification", Information and Computation, 1993, Vol. 103, No. 1, pp. 1-29.

Probabilistic elements are often introduced in concurrent programs in order to solve problems that either cannot be solved efficiently or cannot be solved at all by deterministic programs. Interval-based temporal logic is often used to specify correctness conditions of concurrent programs. The paper presents a procedure that, given a probabilistic finite state program and a (restricted) temporal logic specification, decides whether the program satisfies its specification with probability 1.

(From the authors' abstract).