Quantitative Analysis

Supervisors: Stefano Maria Nicoletti (s.m.nicoletti@utwente.nl) and Ernst Moritz Hahn (e.m.hahn@utwente.nl)

Description

BayesL is a logical query language for Bayesian networks. It is used to express probabilistic inference queries, such as marginal or conditional probabilities and most likely outcomes (MAP/MPE), as well as model-checking-style properties such as IDP and INFL. BayesL is supported by a model checker that parses a BN and evaluates the query, but BayesL itself is the query language.

This project is about building an explainable natural-language interface for a query language over Bayesian networks, such as the BayesL query language. The goal is to let users express an informal question in English and automatically translate it into a well-formed formal query, while also showing how each word or phrase of the question corresponds to each sub-expression of the generated formula.

Because the frontend is meant to be used interactively, it should also be lightweight: it must run locally on ordinary hardware, respond quickly, and avoid the energy and latency costs of calling a remote LLM.

A concrete example is a user asking:

"the probability that the most likely values of Intelligence and SAT given that the value of Letter is greater than Weak given that Letter is Strong"

This should be translated to a formula such as

P(MAP(Intelligence, SAT | Letter > Weak) | Letter = Strong).

The screenshot below is from the BayesL demonstrator, showing the same query and its natural-language paraphrase side by side. It is rather easy to turn a given BayesL into an English phrase using purely symbolic method; the other direction is less straightforward.

The figure below shows the two candidate architectures.

Encoder versus decoder pipeline

• Left (encoder / neuro-symbolic): tokenise the English input, run a bidirectional self-attention encoder, use a biaffine head arc-scorer to recover a maximum spanning tree (Chu–Liu–Edmonds), and render the formula tree deterministically. This gives one parallel forward pass and zero syntax errors by construction.
• Right (decoder / generative LM): feed the same English text as a prompt to an autoregressive language model that generates the target formula token by token, optionally constrained by a grammar mask. This is more flexible but requires one forward pass per output token and a mechanism to enforce grammar.

BSc and MSc variants

• BSc project: choose one of the two approaches, implement a working frontend for a well-defined fragment of the query language, and evaluate it on a small set of benchmark queries. A key part is also making the translation inspectable, so the user can see which words in the question generated which formula parts.
• MSc project: implement and compare both approaches. This includes designing a shared evaluation setup, analysing accuracy, latency, robustness, and explainability of the word-to-formula mapping, and deciding under which conditions the encoder or decoder approach is preferable.

Possible tasks

• Design a formal grammar for the target query language and the subset of natural language to be supported.
• Build or reuse a small dataset of natural-language queries paired with gold formal queries.
• For the chosen approach (BSc) or both approaches (MSc), implement parsing or generation and integrate it with an existing Bayesian network inference engine.
• Implement a mechanism that tracks or highlights which parts of the natural-language input map to which sub-expressions of the generated formula.
• Measure and compare the latency, memory footprint, and energy consumption of the chosen approach (or both approaches for MSc), and evaluate whether the frontend can run locally on modest hardware.
• Evaluate how well the system handles ambiguity, coreference, and paraphrasing, and how understandable the word-to-formula mapping is to the user.

Contact

If you are interested, please contact Stefano Maria Nicoletti or Ernst Moritz Hahn.

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.

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)