Below, you can find a few examples of topics for Master's projects. Feel free to contact me to discuss these, or similar, proposals.
The goal of this project is to extend the modelling of agents in STARK with actions beyond read/write on the data states and with nondeterminism. Specifically, we want to
establish whether the distributions should include the nondeterministic choices, or if the resolution should end up in a set of distributions
find an efficient data structure to handle nondeterministic choices in both cases
investigate how we need to change RobTL and DisTL to accomodate nondeterministic behaviour
In [1] we proved that CCS parallel composition operator cannot be finitely axiomatised modulo any of the four weak bisimulation-based congruences for van Glabbeek's spectrum: rooted branching bisimilarity, rooted eta-bisimilarity, rooted delay bisimilarity and rooted weak bisimilarity. In [2], we investigated the use of the auxiliary operators left merge and communication merge towards obtaining finite axiomatisability results. Unfortunately, we only managed to prove such positive results under the assumption that the set of actions is infinite.
The aim of this project is to try to extend the results from [2], by investigating the existence of a finite axiomatisation of rooted branching bisimilarity over CCS with full, left and communication merge operators, defined over a finite set of actions.
[1] L. Aceto, V. Castiglioni, A. Ingolfsdottir, B. Luttik.
Non finite axiomatisability of weak bisimulation-based congruences.
TCS 1054, 2025
https://doi.org/10.1016/j.tcs.2025.115453
[2] L. Aceto, V. Castiglioni, A. Ingolfsdottir, B. Luttik.
Axiomatising weak bisimulation congruences over {CCS} with left merge and communication merge
TCS 1047, 2025.
https://doi.org/10.1016/j.tcs.2025.115325
In [1] we investigated the existence of finite axiomatisations of the interleaving parallel composition operator modulo the various semantics in van Glabbeek's linear time - branching time spectrum.
The aim of this project is to investigate the same problem modulo a semantics that was left out of the original spectrum: impossible futures semantics.
[1] L. Aceto, V. Castiglioni, A. Ingolfsdottir, B. Luttik, M.R. Pedersen.
On the Axiomatisability of Parallel Composition.
LMCS 18(1), 2022
https://doi.org/10.46298/lmcs-18(1:15)2022
In [1] we exploited a reduction technique, designed to lift negative results across process algebras, to prove the non-finite axiomatisability of various extensions of BCCSP modulo bisimilarity. There are however a number of theoretical questions that are still open. For instance, we proved that, when we consider BCCSP enriched with a CSP-style parallel composition operator |_A for each subset A of the set of actions, the reduction technique cannot be applied. Hence, to complete the study of the axiomatisability of CSP-style parallel composition operator modulo bisimilarity, a direct proof of the non existence of a finite, ground-complete axiomatisation over that language should be provided. Another direction, could be to study the axiomatisations modulo failure semantics, the classic semantics associated to the process algebra CSP.
[1] L. Aceto, E. Anastasiadi, V. Castiglioni, A. Ingolfsdottir.
"Non-finite axiomatisability results via reductions: CSP parallel composition and CCS restriction".
LNCS 13560, pp. 1--26, 2022.
Details will be shared at the end of the project.
Collective adaptive systems (CAS) are characterised by a large number of agents that have to coordinate their activities in a decentralised, and often implicit way, in order to achieve a common goal while being subject to a dynamic and unpredictable enviroment. Specifically, in CAS the behaviour of each agent can change dynamically in time due to either its interaction with the other agents; or to the fact that an agent can freely join or leave the system at any time; or to failures and/or conflicts that may occur in the interactions. While in the literature we can find several proposals of formal specification and static verification techniques for CAS, the paper [1] is the only attempt, to the best of our knowledge, to use a metric to analyse CAS performance. However, the proposed metric compares the behaviour of the agents in the systems, rather than the overall behaviour of different systems. This makes it unfeasible to account for the effects of external perturbations on system performance.
The aim of this project is to extend and enhance the techniques proposed in [1] by using the evolution sequence model [2,3], and the STARK tool [4], to model and analyse the performance of CAS, and their robustness against failures and/or perturbations.
[1] C. Feng, M. Gribaudo, J. Hillston.
"Performance analysis of collective adaptive behaviour in time and space".
ENTCS 318, pp 53--68, 2015.
https://doi.org/doi:10.1016/j.entcs.2015.10.019
[2] V. Castiglioni, M. Loreti, S. Tini.
"A framework to measure the robustness of programs in the unpredictable environment".
LMCS 19(3), 2023.
https://doi.org/10.46298/lmcs-19(3:2)2023
[3] V. Castiglioni, M. Loreti, S. Tini.
"RobTL: A temporal logic for the robustness of cyber-physical systems".
Available at https://doi.org/10.48550/arXiv.2212.11158
[4] V. Castiglioni, M. Loreti, S. TIni.
"STARK: A Software Tool for the Analysis of Robustness in the unKnown environment".
Proceedings of COORDINATION 2023, LNCS 13908, pp 115--132, 2023.
Details will be shared at the end of the project.
Our goal is to expand the CSLib of Lean with the axiomatisation of CCS modulo bisimilarity due to Faron Moller (https://link.springer.com/chapter/10.1007/BFb0032072) and formalised for CCS by Aceto et al (https://dl.acm.org/doi/10.1145/1459010.1459016). If time permits, after bisimilarity we will also consider the axiomatisations of the other equivalences in the linear time branching time spectrum presented in (https://lmcs.episciences.org/8979).
Our goal is to use STARK to model tumor growth and to investigate optimisation techniques for drug administration.
Sander van Heesch, On the Axiomatisability of Weak Decorated Trace Semantics over BCCS||
Defended on 28 May 2025.
Abstract: This thesis investigates the axiomatisability of weak decorated trace semantics over the process algebra BCCS extended with the interleaving parallel composition operator, denoted as BCCS∥. Weak semantics consider the silent action τ as an invisible action to abstract away from internal behaviour. The weak decorated trace semantics consist of weak trace, weak completed trace, weak failure, weak ready, weak failure trace and weak ready trace equivalences. We start our investigation by considering how different formalisations of the set of initial actions of a process affect the expressive power of the considered semantics. We show that for weak completed trace and weak failure semantics the choice of the set of initials (I(p) or I′(p)) does not affect their expressive power, while for weak ready, weak failure trace and weak ready trace semantics this choice is fundamental to their expressive power. We proceed by studying if the considered equivalences are congruences with respect to BCCS∥, and if any restrictions are necessary to ensure that. We show that each of the equivalences are congruences with respect to BCCS∥, and specifically, that weak ready, weak failure trace and weak ready trace equivalences with I(p) are congruences only when the set of actions is restricted to a single action (|A| = 1). Finally, we investigate the axiomatisability of the considered equivalences over both BCCS and BCCS∥. For each considered weak decorated trace equivalence, we establish finite, sound, and ground-complete axiomatisations over both BCCS and BCCS∥.
Wietske de Bondt, Modelling a Mechanical Lung Ventilator in STARK
Defended on 8 June 2026.
Abstract: In this Master Thesis a STARK model of a Mechanical Lung Ventilator (MLV) is presented. In particular, the specification document of the MLV from the ABZ 2024 case study is used. Requirements from the case study have been transformed into DisTL (Distribution Temporal Logic) and RobTL (Robustness Temporal Logic) formulas and have been verified to show the robustness of the model against perturbations. Additionally, a comparison with an already existing mCRL2 model of the MLV has been done, which showcased a difference in modeling the breathing dynamics. Lastly, another comparison is done with a UPPAAL model of a general mechanical lung ventilator. This comparison highlighted that properties verifiable by UPPAAL, are, to some extent, also verifiable by the STARK tool.
Huaze Xu, Shielding for Autonomous Highway Driving with STARK
Defended on 1 October 2026.
Abstract: Reinforcement-learning-based autonomous driving agents can achieve effective driving behaviours, but their decisions are difficult to verify and may lead to unsafe situations. This thesis studies runtime safety shielding for the ABZ 2025 autonomous highway driving case study, focusing on a three-lane highway setting in which pre-trained AI agents control an ego vehicle. This thesis uses STARK to construct runtime shields for these AI agents. Before each AI-proposed action is applied, the shield evaluates it against predicted future traffic evolution and rejects it if the prediction indicates an unsafe outcome. The safety requirements are expressed using DisTL formulae, which compare predicted behaviours with desired safety-related behaviours. Two shield designs are implemented. The first shield uses a heuristic prediction model based on simple assumptions about surrounding vehicles. The second shield uses randomized IDM–MOBIL-based prediction to model possible future reactions of nearby vehicles. Experimental results show that both shields substantially reduce the collision rate of the adversarial AI agent. The recoverability-based shield achieves a better balance between safety and operational performance than the heuristic shield in our experiment setting. These results suggest that STARK can provide a useful framework for constructing runtime shields that combine predicted future behaviours with formal temporal-logic evaluation.
Agnes Vulpescu, Issues encountered when proving that BCCSP∥ modulo possible future equivalence has no finite, ground-complete axiomatization when the set of actions is a singleton
This report studies whether the process algebra BCCSP extended with the purely interleaving parallel composition operator admits a finite, ground-complete equational axiomatization modulo possible futures equivalence when the set of actions is a singleton. The natural approach is to use the general technique introduced by Moller, namely to produce an infinite family of valid equations together with a witness property that is preserved by derivations from any finite sound axiom system but distinguishes the two sides of each equation. However, an axiom, namely p ∥(a.q +a.r) ≈p ∥a.q +p ∥a.r, is sound modulo possible futures when the set of actions is a singleton. This axioms allows sound derivations distribute parallel composition across summands in a way that defeats the explored witness properties. We present the candidate witness families of equations together with the investigated witness properties and identify where the distributivity axiom obstructs the preservation argument in each case.
Benjamin Softic, Safety Analysis of Sensors Attacks with STARK (co-supervised by Nicola Zannone)
Autonomous driving vehicles depend on a suite of sensors to perceive their environment and make safety-critical decisions, which makes them attractive targets for adversaries who manipulate sensor readings. In this paper we investigate the robustness of an autonomous vehicle controller against cyber-physical attacks using the STARK tool. Building on a two-lane, two-car highway scenario, we model three classes of sensor attacks as perturbations of the vehicle’s evolution sequence: a LiDAR attack that dazzles or blacks out the distance sensor, a coordinated attack that simultaneously spoofs the sensed speed and inter-vehicle distance to mislead the controller, and a phantom attack that injects fabricated obstacles. Using Robustness Temporal Logic, we express safety, lane-keeping, and overtaking properties as Wasserstein distances between the nominal and perturbed behaviours, and verify them across repeated simulations. Our results show that each attack measurably degrades controller safety, and we discuss controller improvements that harden the vehicle against these threats.