M2 Internship

Created on October 09, 2026

2026

Open Automata meet Choreographies

General Information

Advisors: Rabéa Ameur-Boulifa (Télécom Paris – Sophia), Cinzia Di Giusto (UCA – Sophia) and Ludovic Henrio (CNRS – ENS Lyon)

Contacts:

Who: Master 2 Computer Science students

Where: Eurecom/Laboratoire I3S or Lyon

Topic

Context. Over the past years, we have developed a theoretical framework for open systems, introducing the notion of open automata [6, 3, 5] — labelled transition systems (LTSs) extended with parameters and holes representing unspecified components. Each transition is enriched with guards and assignments that capture complex data and behavioural dependencies between the automaton and its open interfaces. These models preserve key compositional properties such as bisimulation when composed.

Composition in open automata consists of filling holes with other automata, provided their interfaces are compatible. Currently, compatibility relies mainly on the syntactic matching of action labels and arities. However, this approach fails to capture the structured interactions — the sequences of inputs and outputs — occurring between components.

To overcome this limitation, we aim to annotate open automata with typing information, that is, a “local” description of their interaction protocols. These local views, expressed through behavioural types, capture how multiple participants cooperate. By linking open automata to choreographies, we can reason compositionally about interaction correctness, ensuring that local behaviours collectively conform to a coherent global protocol.

Hence, the central question becomes:

Can we synthesise a choreography (global type) from a set of interacting open automata to ensure safe and deadlock-free composition?

Objectives. Depending on the candidate’s profile and interests, the project may evolve along two complementary directions. A first, more foundational direction will focus on the development of new theoretical results, including formal models, correctness proofs, and the study of behavioural equivalences and compositional properties. A second, more applied direction will focus on implementing the proposed framework by extending existing tools or developing new software prototypes to support the modelling, synthesis, and verification of choreographic compatibility for open automata. These two directions are complementary and may also be combined within the internship. The precise orientation will be chosen together with the student, depending on their interests and skills. Concretely, several contributions are possible:

  • Choreographic Compatibility: Design a compatibility condition for composing open automata based on choreographic specifications. This involves linking the local transitions of automata with the corresponding projections of a global type.
  • Foundational contributions: (with possible mechanisation on theorem provers)
    1. Introduce a configurable scheduler: i.e., define a master whose behaviour spans from allowing all possible actions of its slaves or deciding the order of each single interaction.
    2. Show correctness and safety properties by using the choreographic structure to prove deadlock freedom and communication safety for the composed systems.
    3. Study the expressive power of the framework by integrating variables and parameters (e.g., showing bisimulation results).
  • Applied contributions:
    1. Implement an execution environment for open automata and/or establish connections with existing model-checking tools, such as CADP [7].
    2. Develop techniques for extracting choreographies from Erlang programs.
    3. Integrate SAT solvers to support the synthesis and verification of choreographic specifications that include variables and parameters.

We envisage this internship as the first step of a longer research project and expect that it will naturally continue as a PhD thesis, allowing the selected candidate to further develop and consolidate the theoretical and/or practical contributions initiated during the internship.

References

  1. Hans Hüttel, Ivan Lanese, Vasco T. Vasconcelos, Luìs Caires, Marco Carbone, Pierre-Malo Deniélou, Dimitris Mostrous, Luca Padovani, Antònio Ravara, Emilio Tuosto, Hugo Torres Vieira, Gianluigi Zavattaro: Foundations of Session Types and Behavioural Contracts. ACM Comput. Surv. 49(1): 3:1-3:36 (2016)
  2. Gay, Simon J. and Vasconcelos, Vasco T. Session Types. Cambridge University Press, 2025
  3. Ludovic Henrio, Eric Madelaine, Min Zhang: A Theory for the Composition of Concurrent Processes. In Albert, E., Lanese, I., eds.: 36th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE). Volume LNCS-9688, Heraklion, Greece (June 2016) 175–194. hal-01299562
  4. Alessandro Fantechi, Elie Najm, Jean-Bernard Stefani: From Behavioural Contracts to Session Types. Models, Languages, and Tools for Concurrent and Distributed Programming 2019: 278-297
  5. Zechen Hou, Eric Madelaine: Symbolic Bisimulation for Open and Parameterized Systems. In: PEPM 2020 - ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, New-Orleans, United States (January 2020). hal-02406098
  6. Rabéa Ameur-Boulifa, Ludovic Henrio, Eric Madelaine: Compositional equivalences based on Open pNets. Journal of Logical and Algebraic Methods in Programming, In press. (hal-03894031)
  7. Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe: CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes. cadp.inria.fr International Journal on Software Tools for Technology Transfer (STTT), 15(2):89-107, April 2013