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.

For the iterative numerical algorithms, previous attempts have been made on low-level parallelism with limited success; we would still be interested in exploring higher-level parallelism options for this part, and parallelisation of the state space exploration.

Supervisors: Arnd Hartmanns

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

to be added

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

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, 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.

Gamification for Deductive Systems

Supervisor: Ernst Moritz Hahn (e.m.hahn@utwente.nl)

Deductive systems are a proof method to show that a formula of a formal logic is valid. That is, if it is possible to prove that a formula is true using a correct deductive system, the formula is true under any interpretation. The proofs constructed using deductive systems are trees, such as the following one for the formula (∀ x. p(x) ∨ ∀ x. q(x)) → ∀ x. (p(x) ∨ q(x)):

Using deductive systems is an important learning goal in the MSc course Advanced Logic. Unfortunately, students find using such systems to prove a concrete formula very hard. This holds in particular for those of the so-called Hilbert type.

In this project, you are going to develop a video game in which students build such trees interactively, such that future students have a better way of training on a larger number of examples than doing them purely by pen-and-paper on a limited example set. The objectives and challenges for this thesis are thus

• How to automatically generate formulae with an appropriate difficulty level?
• How to let the student input proofs in an efficient way?
• How to grade partial solutions?
• How to provide motivating feedback to the student?

The technical implementation of such a game is up to you. We would however be able to provide some Lua-based infrastructure for working with formulae, such as parsing them, etc. If you are interested in this topic, please contact Ernst Moritz Hahn (e.m.hahn@utwente.nl).

Adventure Games with Formal Guarantees

Supervisor: Ernst Moritz Hahn (e.m.hahn@utwente.nl)

Adventure games are strongly story-based video games. The player controls the protagonist, steering its actions, so as to drive forward the story. The user interface often allows interactions of the form “do <verb> with <object 1> together with <object 2>” or similar. This type of game has been quite popular for a while, but faced a decline by factors such as lack of motivation to for the player to play a game more than once, high effort of drawing graphics, and high cost of developing the storyline. The latter results because the designers have to take into account the many different ways in which a player might interact with the environment. Typically, it is considered a design error if it is possible to reach a situation in which the player is stuck and not able to reach the goal of the game anymore.

(https://www.gog.com/en/game/flight_of_the_amazon_queen)

In this project, you are going to apply formal methods to ease the development of adventure games. The idea is to develop a domain-specific language (SDL) which describes the possible interactions of the protagonist with the environment. The SDL shall be transformed into the input languages of general model checkers, such as e.g. the input language of SPIN. Desirable properties shall be expressed by a property specification language, which could be translated into a formal logic. For instance, never reaching a situation in which one is stuck could be expressed as the CTL formula “AG (EF won)”. This way, it will be possible to check whether the desired properties indeed hold.

If you are interested in this project, please contact Ernst Moritz Hahn (e.m.hahn@utwente.nl).

Algorithmic collusion for omega-regular properties
in grid-world scenarios

Supervisor: Moritz Hahn (j.m.meylahn@utwente.nl), Ernst Moritz Hahn (e.m.hahn@utwente.nl)

Consider a scenario of multiple agents, each of which is following their own interest and is using reinforcement learning (RL) to maximize their profit. Under certain conditions, collusion may occur, that is, the RL algorithms might implicitly negotiate contracts with other agents.

In this proposed thesis, you are going to research collusion in scenarios where agents operate on a grid-world and follow an omega-regular objective. Omega-regular properties are properties which can be described using omega-regular automata or logics. They can describe more complex behaviours than reward signals. For instance, consider the example below:

The first robot tries to distribute coffee from the coffee room to the other three rooms. This behaviour can be described as Pmax [G (F coffee ∧ XF room1 ∧ XF room2 ∧ XF room3)]. The second robot wants to move between two rooms, expressible as

Pmax [G (F room1 ∧ F room2)]. To efficiently perform these tasks, profit from negotiating with each other, so as to avoid each other’s path. It would be convenient for each robot to ignore the other robot completely rather than moving out of the way, because in this way it might be able to distribute coffee more quickly. However, in this case, the other robot would reciprocally do the same, if according RL algorithms are used.

There is an active area of using RL for handling omega-regular properties. The novel aspect of this thesis is the combination with collusion. The challenges of this thesis are

• implementing appropriate transformations from omega-regular properties to rewards,
• implementing appropriate 2-player RL algorithms on top of the above,
• evaluating the results, and
• providing an outlook for a theoretical foundation of these results.

Supervisors: Arnd Hartmanns, Mark van Wijk

Both probabilistic model checking and reinforcement learning use Markov decision processes to model systems. However, the formats used to store these models differ significantly, making reinforcement learning benchmarks to be unavailable to probabilistic model checkers. With the newly introduced explicit state space format UMB, modern probabilistic model checkers such as Storm, PRISM, and mcsta can take in an explicit state space to analyse. This means that if the state space can be extracted from models used in the reinforcement literature, such as the Gymnasium benchmark set, they can be analysed by probabilistic model checkers. This helps better understand the differences between the approaches and allows for a wider set of benchmark models.

Extracting the explicit state space is nontrivial since the underlying probabilities cannot always be extracted from the model directly. These need to be extracted or approached in some other way, for example using simulation to approximate the model. In this research, we aim to find a way to extract these models and turn them into the UMB format such that they can be used by probabilistic model checkers.