Student projects
Below, you can find a few examples of topics for Master's projects. Feel free to contact me to discuss these, or similar, proposals.
Axiomatisability of CSP parallel composition operator
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.
Collective adaptive systems
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.
Ongoing projects
Axiomatising the weak spectrum
We have recently studied the axiomatisability of weak bisimulation-based congruences over the recursion, relabelling, and restriction free fragment of CCS [1,2,3]. The aim of this project is to extend those studies to other congruences in the divergence-free weak linear time-branching time spectrum.
[1] L. Aceto, V. Castiglioni, A. Ingolfsdottir, B. Luttik.
"On the axiomatisation of branching bisimulation congruence over CCS".
Proceedings of CONCUR 2022, LIPIcs vol 243, pp 6:1--6:18, 2022.
https://doi.org/10.4230/LIPIcs.CONCUR.2022.6
[2] L. Aceto, V. Castiglioni, A. Ingolfsdottir, B. Luttik.
"Non finite axiomatisability of weak bisimulation-based congruences".
Available at https://drive.google.com/file/d/1Sf-kX8TTS-eDx9K1Cfh-uxx1h3LCxfDT/view?usp=drive_link
[3] L. Aceto, V. Castiglioni, A. Ingolfsdottir, B. Luttik.
"Axiomatising weak bisimulation congruences pver CCS with left merge and communication merge".
Available at https://drive.google.com/file/d/1rHUnTP9ensKk57IcJnL8d7Ilkgp8r7a4/view?usp=drive_link