Quantitative Analysis

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

Grid-world Scenario Editor

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

Grid-world scenarios are a type of formal models which are often used to evaluate or demonstrate model checking or reinforcement learning algorithms. The scheme is such that one or agents are positioned in a cell of a fixed grid. Each step, they can move into one of four directions. Depending on the property under consideration, they might have to perform certain tasks there. For instance, in the scenario sketched below, we might ask whether it is possible for the robot to distribute coffee infinitely often from the coffee room to the other three rooms.

In this project, you are first going to perform a literature study about the common features of such grid-world scenarios. Afterwards, you are going to implement an editor supporting a well-justified set of such features. Your editor shall have an export functionality, so as to be able to export at least to the JANI format. The export shall be performed in such a way that model checkers reading the model can perform analyses efficiently and that you can compare results from the literature with your implementation.

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: Janusz Meylahn (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, 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).

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

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.

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

Hanoi Format Graphical Editor

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

The Hanoi format (HOA) is a textual description of automata which describe omega-regular languages, that is, languages over infinite words. HOA is a text-based format, which allows to specify automata with different so-called acceptance conditions. All these automata can describe the same class of languages, but they might be fit for different applications, or they might allow for a more or less compact representation.

In this project, you are going to implement a web-based graphical editor using the diagram editor UTML which is maintained at the University of Twente. The challenges here are to

• study the literature to design a tool which behaves according to user expectations,
• input and output of the HOA format,
• positioning the states when reading from the HOA format,
• simulating the automata, and
• performing simple conversions from one automaton class to another one, e.g. conversions from Büchi automata to 2-color parity games.

An appropriate level of formal methods as well as software engineering and GUI design is required. However, the focus of the project may be one one or several of the points discussed, following negotiations with the student.

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

Infinite Board Games

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

Infinite games are games in which a player wins if being able to fulfill an omega-regular property, that is to reproduce a certain behaviour infinitely often rather than fulfilling an objective which can be obtained in a finite number of steps. Such games often occur in the formal verification or synthesis of systems, e.g. when building a controller which is able to safely steer a system under possible behaviours of its environment. As an example, consider the situation below:

 Here, two robots operate on a grid-world. At each point of time, they can move to one of four directions. With probability 0.1, they move one field, and with probability 0.9 they move two fields. The objective of the first robot is to distribute coffee to all coffee rooms, which can be expressed as the LTL formula

Pmax [G (F coffee ∧ XF room1 ∧ XF room2 ∧ XF room3)]. The objective of the second robot is to prevent this.

The objective of this project is to develop a type of board game in which the player is given an omega-regular property and is supposed to steer the agent in such a way that the property is fulfilled. The assumed challenges here are to

• implement an algorithm to check omega-regular properties,
• design the user interface; in particular, allowing the user to specify infinite sequences with finitely many interactions,
• writing the game in such a way that it is challenging and interesting.

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

Supervisor: 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:

• Monopoly
• Game of the Goose
• The Quacks of Quedlinburg
• Lost Cities
• Incan Gold
• Royal game of Ur
• Snakes and Ladders

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.

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.

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:

• [1] David N. Jansen, Holger Hermanns: Dependability Checking with StoCharts: Is Train Radio Reliable Enough for Trains? QEST 2004: 250-259
• [2] Holger Hermanns, David N. Jansen, Yaroslav S. Usenko: From StoCharts to MoDeST: a comparative reliability analysis of train radio communications. WOSP 2005: 13-23
• [3] David N. Jansen, Holger Hermanns: QoS modelling and analysis with UML-statecharts: the StoCharts approach. SIGMETRICS Perform. Evaluation Rev. 32(4): 28-33 (2005)