Dave Parker: Probabilistic Model Checking and Controller Synthesis

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 controller (e.g. for a robot or a power management system) 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 controller 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 some applications of these techniques to real-world problems using the probabilistic model checker PRISM.