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