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.

Supervisor: Ernst Moritz Hahn

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.

Genetic Algorithms for Controller Generation of Markov Decision Processes

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

Markov decision processes (MDPs) are a modeling formalism which applies to a wide range of systems. MDPs feature both control as well as stochastic behavior. For instance, consider the robot scenario below.

At each point of time, the robot can move in one of four directions. With a probability of 0.3, it moves up two fields, and with a probability of 0.7, it moves up one field. Assume that we want to steer the robot in such a way that it distributes coffee from the coffee room to all the other three rooms. For doing so, we have to resolve the nondeterministic choices in such a way that the property is fulfilled. We can obtain controllers which do so, by using methods such as reinforcement learning or model checking. These methods often work well, but they have the disadvantage that the decisions made are often hard to understand.

In this project, we target at synthesizing understandable controllers in terms of guarded command programs (GCP). A GCP consists of multiple commands, each with a certain guard. A command can be executed in a situation in which its guard is fulfilled. For instance, a controller such as

[ ] blocked_up ∧ right_free → move_right

[ ] blocked_down ∧ left_free → move_left

…

would try to move right if the robot can move right but not up, and move left if the left field is free but the field down is blocked. We aim at automatically deriving such controllers using genetic algorithms. The challenges are

• Implementing the infrastructure to work with guarded commands,
• implementing the connection to a model checker, e.g. the Modest model checker,
• developing good selection criteria, and
• developing ways to mutate a given GCP.

If you are interested in this project, please contact Ernst Moritz Hahn (e.m.hahn@utwente.nl). If the implementation for this project is going to be integrated into the Modest model checker, you can consult Arnd Hartmanns (a.hartmanns@utwente.nl) for implementation-related questions.

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

Evaluating Student Solutions for Automata

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

As part of the module Languages & Machines (L&M), students are required to design automata with a given language. For instance, they might be given the regular expression E = (ab)* and be asked to design a finite automaton the language of which is L(E). A possible correct solution is the following automaton:

However, students might come up with incorrect solutions such as the following one, in which the accepting and non-accepting states are switched:

In this project, you are going to evaluate a tool to provide feedback - formative and/or summative - to student solutions, so as to improve the understanding of automata constructions for the L&M module. The challenges here are

• How good or how bad is an incorrect solution - in terms of points?
• How to demonstrate to the student how an incorrect solution could be fixed?
• How to take into account that there is no unique solution, but infinitely many ones?

The technical realisation of the tool is up to you. However, we require the tool to be web-based, so as to be easily accessible to the target audience. We suggest to base it on the diagram editor UTML which is developed at the University of Twente.

If you are interested in this project, 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.