Supervisors

Suitable for

Abstract

Prerequisites:  Computational Complexity

 

Background

Multiparty Session Types (MST) [1] are formal models of asynchronous distributed computation in which local processes exchange messages through communication channels.
The fact that communication channels implement unbounded memory entails that these models are as expressive as Turing machines, making all non-trivial properties undecidable.
As a consequence, classical problems in the area of distributed computing, such as configuration reachability or coverability have not yet been thoroughly studied.
On the other hand, the many variants of Petri nets (PN) [2] have different expressive powers, and there are well-known results regarding the complexity of relevant problems,

Focus

In this project, you will investigate which restrictions on the MST models make these problems decidable, by studying  their complexities either by means of many-to-one reductions between MST and PN , or in the more general framework of well-structured transition systems [3]. The objective of this project is to draw a landscape of complexity results relating MST with two classes of PN, namely P/T and elementary systems. You should address both upper and lower complexity bounds, which will determine the direction of the reductions, and formally define the subclasses of MST models to which these reductions apply. An outstanding outcome of this project would integrate these results in the theory of well-structured transition systems and also extend to analyses of global types [4].

References:

[1] Coppo, Mario, Mariangiola Dezani-Ciancaglini, Luca Padovani, and Nobuko Yoshida. "A Gentle Introduction to Multiparty Asynchronous Session Types". In Formal Methods for Multicore Programming, edited by Marco Bernardo and Einar Broch Johnsen, 9104:146–78. Lecture Notes in Computer Science. Cham: Springer International Publishing, 2015. https://doi.org/10.1007/978-3-319-18941-3_4.
[2] T. Murata, "Petri nets: Properties, analysis and applications," in Proceedings of the IEEE, vol. 77, no. 4, pp. 541-580, April 1989, doi: 10.1109/5.24143.
[3] Alain Finkel and Philippe Schnoebelen, "Well-Structured Transition Systems Everywhere!", Theoretical Computer Science 256(1–2), pages 63–92, 2001.

[4] Thien Udomsrirungruang, Nobuko Yoshida: Top-Down or Bottom-Up? Complexity Analyses of Synchronous Multiparty Session Types. POPL 2025

Essential goals: To describe reductions from the coverability, and/or the reachability problems between two classes of PN models (P/T and elementary systems) and restrictions of Multiparty Session Types. To formally define the restrictions of MST for which these reductions make sense.

Stretch-goals: To integrate and generalise these results according to the theory of well-structured transition systems.