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.

  • Bit Packing: Use Less Memory and also Run Faster? (reserved)

    Supervisors: Arnd Hartmanns, Bram Kohlen

    A state stored by our probabilistic model checker mcsta consists of the values of many model variables, each taking up 2n bits with n ≥ 3 in memory right now. What happens if we bit-pack them, i.e. use the lowest sufficient number of bits for each variable: Clearly we use less memory, but will the overhead make the tool slower, or will we run faster due to fewer memory accesses?

  • Performance Impact of Hash Functions in Explicit-State Model Checking (reserved)

    Supervisors: Arnd Hartmanns, Bram Kohlen

    Our explicit-state probabilistic model checker mcsta relies heavily on hash sets and tables to store (sub)sets of states and map them to other data. Significant runtime is thus spent computing state hashes. You will investigate the performance impact of different state hash functions and the tradeoff between hash quality (e.g. likelihood of collisions in practice) and hashing speed.

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

  • Automatic evaluation of fault-tree-based for student exercises

    Supervisor: Ernst Moritz Hahn

    The objective of this project is to allow an automatic evaluation of exercises in which students draw (variants of) fault trees by comparing them to a given sample solution. Depending on agreement with the BSc candidate, the focus of this project could be on one (but is not limited to) one or more of the following:

    • drawing of the fault trees (a project which could be the technical base to do so has recently been finished),
    • integration into learning platforms such as Canvas,
    • evaluation and (semi) automatic grading of the diagrams according to specified criteria (correctness, minimality, etc.)
  • Modular analysis on attack tree metrics

    Supervisor: Milan Lopuhaä-Zwakenberg

    Attack trees (ATs) are used throughout the cybersecurity industry to model a system’s vulnerability to an attacker. This vulnerability can then be expressed via AT metrics, that are calculated based on the AT. Calculating AT metrics is a time-consuming problem for large ATs. However, modular analysis, in which an AT is split up into smaller sub-ATs which are handled one at a time, has been used in several cases to speed up computation. In this project, the student implements modular analysis and performs experiments to assess its impact on performance.

  • 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.
  • Fuzzy Markov chains

    Supervisor: Ernst Moritz Hahn

    Fuzzy Markov chains are extensions of Markov chains in which probabilities are associated with a function expressing the belief in this value. Being able to express belief in probability values rather than single values for probabilities is important, because in many applications, exact probabilities are not known. This project is centred around improving the analysis of such models. It could be centred around or more of the following topics:

    • Developing a graphical editor for fuzzy Markov chains,
    • extending the modelling language JANI so as to handle this model class,
    • model checking or simulation of fuzzy Markov chains.
  • Queueing System Editor

    Supervisor: Ernst Moritz Hahn

    "Because of corona, a restaurant uses the following method to limit the number of customers. Outside the restaurant, there are 5 waiting queues Q1,...,Q5 which can hold a maximum of 2 customers each. However, only 1 customers is actually allowed to be waiting at each queue. As long as there are fewer than 2 customers, at each of these queues, customers arrive with an average of 2 customers per time unit (per queue). [...]"

    Queueing systems are models which consist of the concatenation of multiple waiting queues, between which customers are transferred according to certain rules. Queueing systems have many important applications, such as the one seen above. This project focusses implementing a graphical editor for these types of models. It shall also be possible to export the models to the modelling language JANI and/or the input language of the probabilistic model checker PRISM, such that the performance of a queueing system (throughput, average waiting time, etc.) can be faithfully evaluated.

  • Restricted interactions of exponential distributions and timed delays

    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.
  • Scenario editor for probabilistic model checking

    Supervisor: Ernst Moritz Hahn

    This project targets at developing an editor for spacial models which can be used for performance evaluation of new model checking methods. As an example, consider the example at https://core.ac.uk/download/pdf/80780059.pdf, Section 2. Here, a new model checking method is evaluated using scenarios where we have two robots operating in a grid world with antagonistic behaviours. Using the editor developed in this project, it shall be possible to develop similar spacial models. It shall be possible to load models, store models, and to export them to either the language of the probabilistic model checker PRISM (http://www.prismmodelchecker.org/) or in JANI (https://pure.qub.ac.uk/portal/files/161670364/paper.pdf).

    Other details: The implementation language is the choice of the student. It would be useful if the student knew about modelling languages, but this is not a strict requirement.

  • Speeding up parametric model checking using GPGPU computation

    Supervisor: Ernst Moritz Hahn

    Parametric Markov chains occur quite naturally in various applications. In a recent paper (https://arxiv.org/abs/1805.05672), we have discussed how we can speed up the analysis of such models. The idea is to represent measures such as reachability probabilities, expected rewards, etc. as algebraic circuits, that is, as DAG-like structures. Once one has such an algebraic circuit, one can efficiently obtain the concrete value for a given instantiation of the parameter values. Using interval arithmetic, it is also possible to obtain lower and upper bounds for such values for regions of parameters. This can thus be used to decide for which parameter regions the value is guaranteed to be above or below a given threshold. Using GPGPU-based frameworks such as CUDA or OpenCL, the evaluation of parameter regions could be parallelised efficiently. Doing so, one can thus efficiently divide the parameter space into regions for which a given safety or performance measure is guaranteed to be above or below a given threshold.

    A student wanting to do this project should be able to understand the cited paper, at least the basic ideas. Good programming skills are required. They should also know either CUDA or OpenCL, or at least be willing to learn the concepts of one of these frameworks very quickly. They should also either know or be willing to learn about interval arithmetic.

  • Visualisation of quantum superoperators

    Supervisor: Ernst Moritz Hahn

    Superoperator-labelled quantum Markov chains (QMCs) are extensions of Markov chains in which transitions are not labelled with probabilities but with superoperators. These superoperators manipulate operators, which correspond to states of quantum systems. When analysing such a QMC, the result is in turn again a superoperator which describes how the system the QMC describes manipulates a given quantum state.

    As quantum superoperators are represented in matrix form, which are rather unintuitive, this project focusses on visualising them so as to provide an intuition of their meaning.

Contact