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