Probabilistic Model Checking: Advances and Applications

ABSTRACT. Probabilistic model checking is a technique for formally verifying quantitative properties of systems that exhibit stochastic behavior. It can provide formal guarantees on a wide range of system properties, such as safety, reliability, energy efficiency or security, and can be used to investigate trade-offs between them. This talk will give an overview of the probabilistic model checking tool PRISM, and describe some of the current advances being made in its development. This includes techniques for controller synthesis and multi-objective verification, as well as support for new probabilistic models such as stochastic games and partially observable Markov decision processes. These will be illustrated with applications from various domains including robotics, energy management and task scheduling.

Authors

• David Parker

Keywords

No keywords are indexed for this paper.