Quantitative Analysis

Probability is everywhere in our daily lives and IT systems: as games of chance, as random events like device failures, or in randomised algorithms. Other systems show time-dependent behaviour or need to satisfy real-time requirements. Sometimes, timing and probabilities are intertwined, like in communication protocols, or we even need to consider quantities evolving according to physical laws such as a room's temperature or the water level in a buffer tank.

In FMT, we work with (extensions of) Markov chains, Markov decision processes, stochastic games, and timed automata to model such systems. We model real-life systems with UPPAAL, use fault trees as a graphical tool to think about failure probabilities, and develop the Modest Toolset to create, simulate, and verify formal models that include probabilities and timing.

We offer B.Sc. research projects related to probabilistic, timed, and hybrid verification topics: on case studies, modelling language and compiler improvements, algorithms for model checking and simulation, and connections with other languages or tools.

Prerequisites

Related Modules

Available Project Proposals

If you are interested in the general topic of Quantitative Verification, or if you have your own project idea related to the topic, please contact us directly. Alternatively, you can also work on one of the following concrete project proposals in various subfields of quantitative analysis:

Modelling Language Technology

Modelling languages are similar to programming languages, yet different. We offer topics related to various aspects of our modelling language compilers.

(There are currently no open topic proposals in this area.)

    Probabilistic Verification

    Probabilistic model checking and statistical model checking compute optimal probabilities, expected values, and strategies for Markov models. You can implement new algorithms, combinations of methods, or improve performance.

    • Increase Your Floating-Point Precision When Stuck

      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. Now these algorithms are free of floating-point errors, but now they sometimes tend to get "stuck" at a fixpoint due to rounding before reaching the desired error specified by the user. In this project, you will investigate – devise, implement, and benchmark – modifications of this approach that, instead of giving up, increase the floating-point precision (in hardware or in software, e.g. via the MPFR library).

    • Learning Decision Trees from Lightweight Scheduler Simulation

      Supervisors: Arnd Hartmanns, Bram Kohlen

      Lightweight scheduler sampling (LSS) is a technique to obtain near-optimal decisions for the choices available in a Markov decision process in a simulation-based approach, using O(1) memory. At this point, however, the result is an opaque "scheduler ID" that offers no information on what the optimal decisions are. You will devise and implement, in the Modest Toolset, methods to extract those choices and present them to the user in an appropriate way, potentially by connecting to the dtControl tool developed by our colleagues in Munich.

    • Safe Rounding in Iterative Numeric Algorithms

      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. In this project, you will pick one or two algorithms that do not yet have a correctly rounding implementation, think about which rounding mode needs to be applied at which places, implement the result, and benchmark it.

    • Speeding Up Iterative Numeric Algorithms

      Supervisors: Arnd Hartmanns, Bram Kohlen, Peter Lammich

      The fastest algorithms used for computing probabilities and expected rewards in probabilistic model checking are all based on value iteration: they iteratively approximate the desired solution (which is a fixpoint of the algorithm) and stop when the error is small enough. Current implementations are simple nested loops with double-precision floating-point computations. In this project, you will investigate – devise, implement, and benchmark – ways to speed up these implementations, e.g. by parallelisation (multi-threading) or vectorisation (using SIMD instruction sets such as SSE/AVX). The implementation part will be in C and/or C#.

    (Probabilistic) Timed Automata

    Timed automata are an established way to model hard real-time systems. Probabilistic timed automata capture the combination of randomisation and real-time behaviour.

    • Diagonal Digital Clocks

      Supervisors: Bram Kohlen, Arnd Hartmanns

      The digitals clocks technique is one way to model-check probabilistic timed automata (PTA): models of real-time systems with randomised choices. It is commonly applied to diagonal-free PTA only, where clock variables cannot be compared to each other. However, the underlying correctness proof does not require this restriction. You will devise an approach that preserves all the information necessary to decide diagonal clock constraints and implement it in the Modest Toolset.

    • Modelling medical protocols with UPPAAL

      Supervisor: Rom Langerak

      It is difficult to reason about medical diagnostic and treatment protocols: they usually consist of many processes, and timing, cost, effectiveness, and uncertainty play a complex role. We are therefore modelling and analyzing 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.

    • Non-Convexity in Backwards Reachability

      Supervisor: Bram Kohlen

      Backwards reachability is an efficient model checking algorithm for probabilistic timed automata. It manipulates sets of time points symbolically. Currently, these sets must be convex. However, we developed an idea for an algorithm which might support non-convex sets, too. We would like to know whether this idea it is feasible: You will implement and benchmark it, and try to break it.

    • Non-Divergence in Digital Clocks

      Supervisor: Bram Kohlen

      Probabilistic timed automata capture the combination of randomisation and real-time behaviour. However, they allow infinitely many actions to happen in finite time, which is physically impossible. You will find out if existing case studies are affected by non-divergence, implement techniques to exclude such behaviour in model checking, and benchmark the performance impact.

    Other Topics

    • Reproducing StoCharts

      Supervisor: Ernst Moritz Hahn

      Statecharts are a widely known flexible graphical modelling mechanism to describe behavioural aspects of models in UML. StoCharts [1-3] are a mechanism to enrich Statecharts with stochastic behavours, such as failure rates, unforseeable delays in actions performed, etc. In previous works, StoCharts have been used to analyse safety properties of train radio systems.

      Statechart [1]

      StoChart [1]

      UTML is an editor developed at the FMT group of the University of Twente which allows draw graphs which have a formal semantics, such as deterministic finite automata, or fault trees. In particular, models created by UTML are easy to parse, because they are stored as JSON data.

      The purpose of this thesis is to reproduce the results obtained from these works. For this, the idea is to

      • Parse the UTML data to StoCharts
      • Transform these StoCharts into the (also JSON-based) stochastic modelling language JANI
      • Analyse these models with the Modest model checker
      • Compare the results to the ones provided in the existing publications

      References:

    • Attack tree metrics

      Supervisor: Milan Lopuhaä-Zwakenberg

      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.

    • Evaluating state elimination

      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.
    • Modelling board games

      Supervisor: Matthias Volk, Milan Lopuhaä-Zwakenberg

      Board games are an easy-to-understand model of stochastic systems as they naturally contain sources of randomization (throwing dice, drawing cards, etc.). Existing work has already modelled some board games and puzzles as Markov models.

      Research directions:

      In this project, we aim to model a selection of popular board games as probabilistic models and analyse them via model checkers such as Storm. Possible candidates include:

      You are free to consider board games or puzzles with randomization of your own liking.

      Requirements

      Interest in board games is very beneficial. It is useful but not required to have knowledge on Markov chains.

    Contact