Parameterized verification by probabilistic abstraction

Abstract

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 γ-faimess, a notion of fairness that is sound and complete for verifying simple temporal properties (whose only temporal operators are ◇ and □) over finite-state systems. The paper presents a symbolic model checker based on γ-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 γ-faimess with network invariants is demonstrated on Lehman and Rabin's Courteous Philosophers algorithm. © Springer-Verlag Berlin Heidelberg 2003.