Probabilistic Model Checking and Strategy Synthesis for Robot Navigation

Dave Parker, University of Birmingham
http://www.cs.bham.ac.uk/~parkerdx/

Probabilistic model checking is an automated technique to verify whether a probabilistic system satisfies a formally specified quantitative correctness property (e.g. "with probability at least 0.999, the airbag successfully deploys within 20 milliseconds of a crash"). The same techniques can also be used to synthesise a strategy (e.g. a controller for a robot) which then guarantees satisfaction of a correctness property (e.g. "the minimum probability of patrolling all rooms within 15 minutes is above 0.98"). This talk will give an overview of probabilistic model checking and strategy synthesis, including some recent directions such as multi-objective model checking (to investigate trade-offs between several conflicting properties) and permissive strategy synthesis (to generate flexible and robust controllers). I will also describe how these techniques have been applied to the problem of robot navigation, using the probabilistic model checker PRISM, and deployed on a mobile service robot.

Bio:

Dave Parker is a Senior Lecturer in Computer Science at the University of Birmingham. 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. CAV, TACAS, SEFM, CONCUR, QEST) and frequently gives invited tutorials at summer-schools and workshops.