Amir Pnueli and Lenore D. Zuck, "Probabilistic
verification", <i> Information and Computation</I>, 1993, Vol. 103, No.
1, pp. 1-29.
<P>

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. 
<P>

(From the authors' abstract).