Abstraction in Quantitative Probabilistic Model Checking

Gethin Norman

Probabilistic model checking is an established technique for formal modelling and analysis of systems that exhibit stochastic behaviour. It has been used to study quantitative properties of a wide range of systems, from communication protocols to biological pathways. In practice, however, scalability quickly becomes a major issue even when employing efficient model checking algorithms and state-of-the-art data structures. Abstraction is an approach to reduce the complexity of the model and/or verification procedure and therefore combat this issue. This talk will consider a number of different approaches which apply abstraction techniques to quantitative probabilistic model checking. This will including surveying both precise and approximate approaches, as well as methods that are based on the model checking algorithm and those that are based on abstracting the model.