Probabilistic Model Checking and Strategy Synthesis

Dave Parker, University of Birmingham

Abstract:

Probabilistic model checking is an automated technique to verify whether a probabilistic system, e.g., a distributed network protocol which can exhibit failures, satisfies a temporal logic property, for example, "the minimum probability of the network recovering from a fault within 2 minutes is above 0.98". Dually, we can also synthesise, from a model and a property specification, a strategy for controlling the system in order to satisfy or optimise the property. This talk will give an overview of automated verification and strategy synthesis for probabilistic systems, focusing primarily on the model of Markov decision processes and temporal logics such as PCTL, LTL and their extensions with costs/rewards. I will also describe recent advances in multi-objective model checking, to investigate trade-offs between several conflicting properties, and extensions to stochastic multi-player games, used to model competitive or collaborative behaviour.

Bio:

Dave Parker is a Lecturer in Computer Science at the University of Birmingham and a Visiting Lecturer at the University of Oxford. His main research interests are in the area of formal verification, with a particular focus on the analysis of quantitative aspects such as probabilistic and real-time behaviour, and he has published over 90 papers in this area. Recent work includes efficient techniques for scalable verification (e.g. abstraction, compositionality), game-theoretic verification methods, and applications of these approaches to areas such as systems biology, DNA computing and computer security. He leads development of the widely used probabilistic verification tool PRISM, regularly serves on the programme committees of international conferences such as CONCUR, QEST, CMSB and SAC, and frequently gives invited tutorials at summer-schools and workshops.

http://www.cs.bham.ac.uk/~parkerdx/