David Parker

Reader, Computer Science, University of Birmingham

I am interested in the construction, analysis and verification of mathematical models to study the behaviour of, for example:

- robotic systems
- security protocols
- biological systems

This might use techniques from a variety of different areas, e.g.:

- model checking
- game theory
- probabilistic model checking
- Monte Carlo simulation

I am happy to supervise projects in any of these areas. Typically, a project might involve implementing new techniques/functionality to support one of the above and then experimenting with it on some examples. This could, but does not have to, be done by extending or adapting parts of the PRISM tool, whose development I lead from here in Birmingham. A non-exhaustive list of suggestions is included below.

You can a get a feel for how PRISM has been used in some of the areas listed above by looking at the case studies section of the PRISM web site (example areas include security, planning, robotics and synthesis and biological systems)

Other related suggestions are welcome. Send me an email.

Model checking projects (PRISM)

Here are some project ideas that involve developing new functionality in the PRISM tool. PRISM supports analysis of both probabilistic and non-probabilistic models and the project could involve either. Furthermore, the first few projects below, do not assume any specific backround in terms of model checking or automated verification.

**Model checking for labelled transition systems**: PRISM is primarily a model checker for probabilistic systems. This project is will add dedicated model checking techniques for the simpler, non-probabilistic model of labelled transition systems. This will also allow the use of PRISM as a teaching tool to introduce such techniques, before moving to the probabilistic case.**Model visualisation and exploration**: PRISM builds state-based models. For small models, it can export the state graph to a Dot file using Graphviz, which can then be viewed externally. This project would integrate similar functionality cleanly into PRISM, allowing the user to easily view, or explore interactively, state graphs.**Model checking for two-player games**: PRISM has some support for model checking (non-probabilistic) labelled transition systems. This project will extend this to provide some model checking functionality for two-player games. These have many applications in the modelling and analysis of systems featuring competitive components, e.g. in security systems.**Property template language and wizard**: PRISM uses temporal logic to allow the user to express system properties that should be verified. This project will design and implement a property template language and accompanying "property wizard" for PRISM's GUI to make property specification easier for novice users. This could involve identifying commonly used*patterns*for temporal logics and translating to and from natural language descriptions.**Planning experiments**: One of the things PRISM can do is solve optimisation problems on Markov decision problems (MDPs). These are also widely used for planning problems, e.g. in the fields of robotics and AI. This project will implement connections between planning tools and languages (e.g. RDDL) and investigate how well PRISM performs in this field.**Efficient Monte Carlo simulation**: PRISM includes a discrete-event simulation engine for debugging models and for performing approximate/statistical model checking. But PRISM's guarded command based modelling language is rather inefficient to simulate. This project will implement more advanced techniques to perform efficient simulation.**Explicit-state model reductions**: PRISM's new explicit-state model checking engine will make it much easier to implement model reduction techniques such as symmetry reduction, bisimulation minimisation, partial order reduction and others, which can be difficult to do well with the existing symbolic engines. This project will investigate implementation of these techniques.**MDP analysis techniques**: For Markov decision processes (MDPs), PRISM mostly uses simple solution techniques such as value iteration. In other fields, alternative methods such as policy iteration are known to perform better. This project will implement such techniques and investigate their performance.**Enhanced statistical model checking**: PRISM has some support for approximate/statistical model checking, but only a relatively small number of properties are supported. This project will implement simulation-based analysis for other properties, such as those expressed in bounded LTL.