Learning assumption for compositional verification of probabilistic systems

Probabilistic model checking provides a set of powerful formal techniques for analysing quantitative properties and establishing mathematically rigorous guarantees about the correctness of real-life systems that exhibit stochastic behaviour. A principal challenge for probabilistic model checking is scalability: the complexity of real-life systems often leads to models that are orders of magnitude larger than the capacity of current techniques. The work presented in this talk aims to solve this challenge, by developing fully-automated compositional verification techniques that decompose the analysis of large probabilistic systems into smaller sub-tasks. The contributions are novel approaches for automatically learning assumptions for compositional verification of both asynchronous and synchronous probabilistic systems.