Automated Verification and Strategy Synthesis for Probabilistic Systems

Marta Kwiatkowska
University of Oxford
Friday, 29 November, 2013 - 14:00
NO Solvay (5th floor)

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 in a given
time period is above 0.98. One can also generate, given a model and a
temporal property, a strategy for controlling the system in order to
achieve or optimise the property, but this aspect has received less
attention to date. In this paper, we give an overview of methods for
automated verification and strategy synthesis, focusing on Markov
decision process models and temporal logics PCTL and LTL. We also
describe how to apply multi-objective model checking to investigate
trade-offs between the properties. We illustrate these techniques by
means of several case studies analysed in the PRISM model checker (www.prismmodelchecker.org). The lecture concludes with a summary of future challenges in this area.