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 investigate the use of the STARK tool [2,3] for the formal verification of AI. As a starting point, we can extend the feedback mechanism introduced in [4] for the shielding of AI agents. The developed theory can be supported by implementing the STARK shield for the reinforcement learning agents modelling autonomous vehicles presented in the ABZ 2025 case study track [1].
[1] https://abz-conf.org/site/2025/casestudy/
[2] 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.
https://doi.org/10.1007/978-3-031-35361-1_6
[3] V. Castiglioni, M. Loreti, S. TIni.
"STARK: A tool for the analysis of CPS robustness".
Science of Computation Programming, vol. 236, 2024.
https://doi.org/10.1016/j.scico.2024.103134
[4] V. Castiglioni, R. Lanotte, M. Loreti and S. Tini
"Evaluating the Effectiveness of Digital Twins through Statistical Model Checking with Feedback and Perturbations". Proceedings of FMICS 2024, LNCS 14952, pp 21--39, 2024. https://doi.org/10.1007/978-3-031-68150-9_2
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.
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.
https://doi.org/10.1007/978-3-031-15629-8_1
The first goal of this project is to use the STARK tool [2,3] to model the mechanical lung ventilator from the ABZ 2024 case study track [1], and to carry out an analysis of its robustness against perturbations. The second goal of the project is to carry out a comparative analysis of the expressiveness of the obtained STARK model with the mCRL2 [5] and UPPAAL [4] models of the mechanical lung ventilator.
[1] https://github.com/foselab/abz2024_casestudy_MLV
[2] 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.
https://doi.org/10.1007/978-3-031-35361-1_6
[3] V. Castiglioni, M. Loreti, S. TIni.
"STARK: A tool for the analysis of CPS robustness".
Science of Computation Programming, vol. 236, 2024.
https://doi.org/10.1016/j.scico.2024.103134
[4] J. Cuartas, D. Cortés, J.S. Betancourt, J. Aranda, J.I. Garcia, A.M. Valencia, J. Ortiz.
"Formal Verification of a Mechanical Ventilator using UPPAAL".
Proceedings of FTSCS 2023, pp 2--13, 2023.
https://doi.org/10.1145/3623503.3623536
[5] D. van Dortmont, J.J.A Keiren, T.A.C. Willemse.
"Modelling and Analysing a Mechanical Lung Ventilator in mCRL2".
Proceedings of ABZ 2024, LNCS 14759, pp 341--359, 2024.
https://doi.org/10.1007/978-3-031-63790-2_27
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∥.