The paper studies automatic verification of liveness properties with probability 1 over parameterized programs that include probabilistic transitions, and proposes two novel approaches to the problem. The first approach is based on a Planner that occasionally determines the outcome of a finite sequence of ``random'' choices, while the other random choices are performed non-deterministically. Using a Planner, a probabilistic protocol can be treated just like a non-probabilistic one and verified as such. The second approach is based on $\gamma$-fairness, a notion of fairness that is sound and complete for verifying simple temporal properties (whose only temporal operators are $\Diamond$ and $\Box$) over finite-state systems. The paper presents a symbolic model checker based on $\gamma$-fairness. We then show how the network invariant approach can be adapted to accommodate probabilistic protocols. The utility of the Planner approach is demonstrated on a probabilistic mutual exclusion protocol. The utility of the approach of $\gamma$-fairness with network invariants is demonstrated on Lehman and Rabin's Courteous Philosophers algorithm.
FOSSACS 2003