Automated Compositional Verification for Probabilistic Systems 
 
Probabilistic automata are a natural formalism for modelling and verifying systems that exhibit both stochastic and nondeterministic behaviour. Scalability of these techniques, however, represents a major challenge. This talk describes a compositional verification framework for such systems, based on assume-guarantee reasoning. Assumptions and guarantees are captured by probabilistic safety properties, represented as finite automata. These can be verified efficiently, using a reduction to the problem of multi-objective probabilistic model checking.  Furthermore, we address the problem of automatically generating suitable assumptions, using the well-known L* algorithm for algorithmic learning of regular languages. A prototype tool implementing these techniques has been used to perform compositional probabilistic verification of several large case studies, including instances where conventional, non-compositional approaches are infeasible.