Assume-Guarantee Verification for Probabilistic Systems 
 
 Probabilistic automata are a natural formalism for modelling and verification of network protocols. Scalability of these techniques, however, represents a major challenge. We present a compositional verification technique for such systems, based on assume-guarantee reasoning. We model assumptions and guarantees as probabilistic safety properties, represented by finite automata. Our techniques are efficient and fully automated, based on a reduction to the problem of multi-objective probabilistic model checking. Using a prototype tool, we illustrate probabilistic verification of several large case studies, including instances where conventional, non-compositional approaches are infeasible.