Probabilistic Model Checking and PRISM
|
Supervisor |
|
|
Suitable for |
Abstract
I can offer a range of projects on the topics of probabilistic model checking. In particular, there are a number of possibilities to extend or enhance the probabilistic model checker PRISM. Proposals include:
- explicit-state model construction and reduction techniques;
- integration of differential equation solution techniques;
- adding support for instantaneous transitions/nondeterminism to continuous-time models;
- explicit-state model construction and reduction techniques;
- investigation of numerical accuracy and stability for probabilistic model checking;
- design and implementation of a property template language;
- compiler optimisations for PRISM models;
- efficient techniques for Monte Carlo simulation of PRISM models;
- efficient automata-based probabilistic model checking;
- investigation of arbitrary precision arithmetic for probabilistic model checking.
I am also happy to discuss your own suggestions. Please send me an email or come and talk to me.
Another possibility is to undertake a modelling and verification case study in PRISM. Suitable application areas include:
- probabilistic security protocols;
- biological process modelling;
- randomised communication and multimedia protocols;
- randomised distributed algorithms.