David Parker Lecturer School of Computer Science University of Birmingham Edgbaston, Birmingham, B15 2TT Email: d.a.parker@cs.bham.ac.uk Tel: +44 (0) 121 41 47264 Office: 107 Office hours: Wed 12.30-1.30, Thu 3-4

<< NEWS >> Postdoc position at Birmingham on "Automated Game-Theoretic Verification of Security Systems". Applications close 4 Sep 2013.

Student Project Ideas

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

• biological systems;
• DNA computing;
• security protocols;
• robotic 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 which involve:

1. building/analysing a model of a real-life system;
   and/or
2. implementing new techniques/functionality to support this.

For (i), I can provide suggestions, or see this site for some examples in the areas of security, biological systems, planning, robotics and synthesis. For (ii), see below for some specific suggestions for features that could be implemented for the PRISM software tool, which is developed here in Birmingham.

Other related suggestions are welcome. Send me an email.

Here are some project ideas that involve developing new functionality for the state-of-the-art software tool PRISM. This first list of projects requires no background about what PRISM is or how it works, but you will need good Java programming skills.

• 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.
• 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.
• Eclipse-plugin: PRISM has a standalone GUI for editing, debugging, exploring and analysing models, described in the PRISM modelling language. This project will create an Eclipse plugin to provide an alternative way for users to work with PRISM.

Here are some project ideas that involve developing new functionality and efficient techniques for PRISM. These projects are more advanced than those above and would require some background knowledge in topics such as probabilistic models , ... As above, you will need good programming skills (typically Java).

• 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.
• 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.
• Compiler optimisations for PRISM models: The efficiency of model checking depends on many factors, but often small changes can made to the model, which do not affect its behaviour, yet improve performance. This project will implement automatic optimisation of PRISM language models with the goal of optimising model checking.
• 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.
• Differential equation solution techniques: PRISM analyses transient (timed) properties of continuous-time Markov chains (CTMCs), primarily using techniques like uniformisation. This project will investigate incorporating alternative methods, based on differential equation solvers.
• Instantaneous transitions: PRISM supports modelling and analysis of continuous-time Markov chains, but it does not allow instantaneous transitions, which can be a useful modelling tool. This project will add this ability. A related extension would be to add support for analysis of continuous-time Markov decision processes (CTMDPs) to PRISM's explicit engine.
• Efficient automata-based probabilistic model checking: PRISM uses deterministic Rabin automata to implement probabilistic LTL model checking (see e.g. the lectures here). But these automata can be very inefficient in some cases. This projet will implement improved automata-based model checking 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.