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

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.

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.

Supervisors: Stefano 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: Ernst Moritz Hahn (e.m.hahn@utwente.nl) with Mariëlle Stoelinga as second supervisor

Description

Why does one meme disappear while another suddenly goes viral? Why can a football team unexpectedly gain collective momentum, even though no single player controls the match? And how can an opinion that starts in a small online community rapidly become dominant?

Agent-based models (ABMs) help analyse and predict such collective behaviour. They simulate many individual agents — people, players, consumers, traders, or AI agents — each following relatively simple rules. Their interactions can nevertheless produce surprising behaviour at the level of the whole system: viral cascades, collective momentum, tipping points, polarization, booms, or sudden collapse. These emergent phenomena are visible in simulation runs but hard to state precisely — which pattern of agent behaviour, exactly, marks the onset of a "speculative boom" in a simulated market?

This project investigates whether machine learning can automatically discover the different behavioural regimes of such a system and learn simple rules describing how the system moves between them. Can we recognize that a trend is starting to go viral? Can we distinguish a stable phase from a tipping point? And can we express such discoveries in a way that humans can understand?

A simulation produces a huge amount of detailed information: what every agent does, how agents interact, and how the overall system evolves. The challenge is to turn all this detail into a compact description of what is happening at the collective level. The project therefore trains a model that compresses each simulation state into a short list of numbers — an embedding. A complete simulation run then becomes a trajectory through this compressed space, and similar situations group into a small number of regimes — for example quiet, emerging, viral, fading in a model of online virality, or stable prices, speculative boom, crash in an agent-based market.

From many simulation runs, we then learn how the system moves between these regimes. Because only finitely many runs are available, we do not assume that transition probabilities are known exactly. Instead, we estimate probability ranges, resulting in a compact probabilistic map of the emergent behaviour — formally, an interval Markov chain.

This map can answer questions such as:

• How likely is an emerging trend to become viral?
• How long does collective momentum typically last?
• Which regimes tend to precede a tipping point?
• How does changing the behaviour of individual agents affect the collective outcome?

The final step is to turn these patterns into short, interpretable rules, such as

read "from a stable market, a speculative boom follows within 30 steps with probability at least 0.7". Such rules provide compact explanations of the emergent dynamics rather than merely predicting what happens next. They are tested on fresh simulation runs and compared across different parameter settings, and the regimes are related back to the real macro variables they encode.

Pipeline of the project. A simulation produces logged runs of agent-level states and macro-level quantities; a learned model compresses each state; grouping the compressed run reveals regimes; the regimes yield a map of transitions with probability ranges; the map is analysed and mined for short rules, yielding explanations of the emergent dynamics that are validated on fresh runs and compared across parameter settings.

What you will do

You will choose or develop an agent-based case study with interesting emergent behaviour — for example online virality, sports, collective climate action, opinion dynamics, or another topic that interests you; a NetLogo market or segregation model is a good starting point. You will then:

• generate and log simulation data, recording agent-level events and macro-level quantities;
• train a machine-learning model that compresses complex agent states into a low-dimensional representation;
• identify meaningful collective regimes in this representation and check them against expert knowledge and the logged quantities;
• learn a probabilistic map describing transitions between regimes — formally, an interval Markov chain, with a probability range for each pair of regimes derived from the observed frequencies;
• analyse this map and automatically derive simple explanatory rules;
• validate whether the discovered regimes and rules correspond to meaningful real-world quantities and remain valid on new simulation runs.

Optional extensions

Depending on your interests, the project can be extended in several directions — for example by comparing different learning architectures for the compression step, asking a language model to propose names and interpretations for the discovered regimes, evaluating the learned rules live during a simulation as an "emergence alarm", or running additional simulations automatically wherever the regime map is still too uncertain to answer a question.

The central challenge is simple to state, but harder to answer:
Can we turn millions of small interactions into a few simple rules explaining when collective behaviour emerges?