Probabilistic models are widely used to analyze embedded, networked,
and more recently biological systems.  Existing analysis techniques
are limited to finite-state models and suffer from the state
explosion problem.  We propose predicate abstraction for
probabilistic models to tackle the state explosion problem and admit
infinite-state models.  We have implemented PASS, a predicate
abstraction model checker for probabilistic models supporting
unbounded integer and real arithmetic, as well as bit vectors.
We demonstrate the feasibility of our approach by verifying
properties of the Bounded Retransmission Protocol
for any file length and any number of retransmissions.
To the best of our knowledge, this is the first time
that properties of probabilistic infinite-state models
have been verified at this level of automation.