Skip to main content

Probabilistic Model Checking

Probability is an important component in the design and analysis of complex systems across a broad spectrum of application domains, including communication and multimedia protocols, randomised distributed algorithms, security protocols, dynamic power management and biological systems. Probabilistic model checking is a formal verification technique for the modelling and analysis of such systems. It provides efficient and rigorous methods for evaluating a wide range of quantitative properties, from performance and reliability to security and anonymity.

Our work on probabilistic model checking involves:

  • design and implementation of efficient tools and techniques, including the development of the state-of-the-art probabilistic model checker PRISM;
  • development of the underlying formalisms, theory and algorithms, including for example abstraction techniques, process calculi and probabilistic timed automata;
  • application of the techniques to real-world case studies, for example to the domains of ubiquitous and pervasive computing, to adaptive systems and to biological modelling.



Past Members

Radu Calinescu
Taolue Chen
Lu Feng
Vojtěch Forejt
Matthias Fruth
Liz Gresham
Tingting Han
Aleksandra Jovanovic
Mark Kattenbelt
Alexandru Mereacre
Hongyang Qu
Ashutosh Trivedi