Reader, Computer Science, University of Birmingham
Student Project Ideas
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
planning, robotics and synthesis
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
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.