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 robot operating in an unknown environment, satisfies a temporal logic property, e.g., "the minimum probability of completing the task within 15 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, and present some recent advances in this area, including: multi-objective model checking (to investigate trade-offs between several conflicting properties), extensions to stochastic game models (to model competitive or collaborative behaviour) and permissive strategy synthesis (to generate flexible and robust controllers). I will describe the tool support for these techniques, in the form of the probabilistic model checker PRISM and its extensions, and present results from the application of these techniques to examples such as robotic motion planning, dynamic power management controllers and task scheduling.

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 robotics, computer security and DNA computing. He leads development of the widely used probabilistic verification tool PRISM, regularly serves on the programme committees of international conferences (e.g. TACAS, CAV, SEFM, CONCUR, QEST) and frequently gives invited tutorials at summer-schools and workshops.

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