Quantitative Analysis

Supervisor: Arnd Hartmanns

In the FMT group, we develop the probabilistic model checker mcsta as part of the Modest Toolset. Like all other probabilistic model checkers, it is a single-threaded implementation. As a Master's Final Project topic, you could develop the first parallel probabilistic model checker by multi-threading state space exploration (using the best algorithms and state set representations you can find in the literature, adapted to the probabilistic setting) and the iterative numerical algorithms like value iteration (devising and testing your own approaches after studying the scarce literature on this topic). In your implementation, you should carefully consider whether to use high-level (e.g. check multiple properties in parallel) or low-level parallelism (i.e. use a parallel implementation of a core algorithm), considering especially the impact on memory usage.

Supervisor: Milan Lopuhaä-Zwakenberg and Reza Soltani

Attack trees are a popular and useful tool to model a system's vulnerability to attackers. They are used in quantitative security analysis: they can be used to calculate security metrics such as the minimal time or resources an attacker needs to successfully compromise the system. As attack trees can grow quite large in practice, there is an ongoing need for algorithms that can calculate security metrics on a feasible timescale.

In this project, the student adds to this field of research by implementing proposed algorithms, inventing new ones, or analyzing the behaviour of existing methods. Some possible avenues for research are:

• Linear programming: many security metrics can be phrased as optimization problems (such as the minimal cost of a succesful attack). Therefore, a student could create new metric calculation algorithms based on optimization techniques such as linear programming.
• Multi-metric analysis: it often makes sense to consider the interplay between metrics: one attack may be more costly to the attacker than another, but do more damage in return. There are some ideas on how to co-analyze metrics, but these have hardly been implemented, and there is also plenty of room for new ideas.
• Attack tree properties: As the problem of calculating security metrics is NP-hard, many existing algorithms are of worst-case exponential complexity. However, it is unclear how these algorithms fare in practice, and what properties of the attack tree have an impact on algorithm complexity.
• Modular analysis: An underused idea in attack tree analysis is to split up the attack tree into so-called modules and analyze each module separately. This idea can be applied to many different algorithms, and it would be interesting to see what difference this makes on both a theoretical and an experimental level.

Of course, there are many other possibilities, and students are welcome to bring their own ideas to the table.

Supervisor: Ernst Moritz Hahn, Matthias Volk

State elimination is a method which works as follows: Starting with the original state-space or a Markov chain, states of the model are systematically removed, while making sure that the property (e.g. probability that a bad state is reached) is maintained. In the end, this way, the model reaches a form from which it is trivial to obtain the property one is interested in.

This project is about evaluating for which models state elimination works particulary well and in which order states shall be eliminated, and why. Depending on agreement with the candiate, the focus could be

• more on the theoretical side, considering structural properties of model classes for which state elimination works well as well as a good/optimal elimination order, or
• could be more on the practical side, implementing a tool in which one can either manually specify the order in which to eliminate states, use a scripting language (JavaScript, Lua, etc.) to decide about the order of elimination or integrate new elimination orders in existing tools.

Supervisors: Arnd Hartmanns, Bram Kohlen

Lightweight scheduler sampling (LSS) is a way to use Monte Carlo simulation/statistical model checking for Markov decision processes, i.e. for optimisation problems. It is currently limited in many ways, (e.g. to unbounded properties) and lacks many features (e.g. the ability to modify a scheduler identifier in a controlled way that results in a "small" change of the scheduler's decisions). There are many ways to improve it, randing from clever use of discretisation to genetic algorithms. As a Master's Final Project topic, you could thoroughly investigate where LSS is currently lacking – potentially starting from our current applications in satellite mesh routing – and improve it. This will involve devising, implementing, and benchmarking algorithms, and possibly modelling new case studies.

Supervisor: Rom Langerak

It is difficult to reason about medical diagnostics and treatment protocols: they usually consist of many processes, and timing, cost, effectiveness, and uncertainty play a complex role. We are therefore modelling and analysing such protocols using the timed-automata-based tool UPPAAL. Examples of past work include treatment of prostate cancer (with BMS), side effects of immunotherapy (with NKI), and tooth wear monitoring (with ACTA).

Assignments (to be formulated in agreement with the interests of the student) may include practical modelling and analysis, theoretical research, and tool development.

Supervisor: Ernst Moritz Hahn

For modelling many application areas, in particular in predictive maintenance, it is important to express two different types of timed behaviour: On the one hand, Events following the exponential distribution are useful to express the distribution of component failures or other unplanned events. On the other hand, fixed delays are used to express tasks which are planned, such as maintenance or scheduled downtime of a system. Classes of models which are able to comprise both exists (such as for instance piecewise-deterministic Markov processes (PDMPs)), but they are costly to analyse and their full expressive power is not always required. This proposed thesis targets at identifying relevant subclasses where the interaction of the two types of timed behaviour is more restricted, but which are easier to analyse. Depending on agreements with the BSc candidate, for this principle idea the project could focus on (not limited to) one or more of the following:

• Formal description of such models,
• Development of case studies,
• Development of analysis methods, and/or
• Implementation of solution algorithms.

Supervisors: Arnd Hartmanns, Bram Kohlen

Stochastic (timed) automata generalise continuous-time Markov chains (CTMC) or Markov automata (MA) by introducing delays that follow not only the exponential distribution, but arbitrary non-memoryless probability distributions instead. This makes the model checking problem hard. One way out is to approximate the non-memoryless distribution by a phase-type distribution. Phase-type distributions are constructed from exponential distributions – they are essentially small CTMCs – and thus allow standard CTMC/MA model checking algorithms to be applied. In this project, you will devise and implement such an approach, figuring out how to get efficiency (e.g. by minimising the representation of the phase-type distribution using an existing tool or your own implementation) and how to deal with the error that the approximation introduces (e.g. finding out whether we can quantify it, or make sure we only get safe over-/underapproximations).

Supervisors: Arnd Hartmanns, Bram Kohlen, Peter Lammich

We recently developed variants of the interval iteration algorithm, which is used for the iterative numerical computations in probabilistic model checking, that use correct rounding in all floating-point computations. Similar ideas should be applicable to similar algorithms like sound or optimistic value iteration; and they should work for expected rewards, too, where we so far only implemented them for reachability probabilities. We also think we should be able to round correctly in state elimination and when model checking Markov automata. In this project, you will augment all the probabilistic model checking algorithms you can find with correct rounding. To do so, you need to find out which rounding mode applies where, which operations need special care (e.g. due to not being covered by IEEE 754), implement what you find out, test your implementation, and benchmark it.