M2R Research Internship -  Encodings for Location Graphs

Scientific context

Location Graphs are a new formal model for component-based systems currently developed in the INRIA SPADES team,
that combines concurrent composition, dynamic reconfiguration and graph-like component structures [1].
The Location Graphs model subsumes previous computational models for mobile and distributed systems including
distributed or located variants of Milner's pi-calculus [2], and more abstract computational models such as Milner's bigraphs [3].
The psi-calculi is a process calculus framework recently developed by J. Parrow et al. [4] to facilitate the development of 
applied and extended variants of the pi-calculus.
The Synchronized Hyperedge Replacement (SHR) [5] is an hypergraph-based model of computation introduced to model dynamic distributed services.


Subject of the internship

The goal of this internship is to study encodings for Locations Graphs. Specifically, the intership will study 
whether faithful and non-trivial encodings are possible: (1) of the Location Graphs model in the psi-calculi framework, 
and (2) of the SHR model in a simple instance of the Location Graphs model. 
By 'faithful' we mean here an encoding which establishes some form of operational correspondence or simulation
between a term and its encoding , and by 'non-trivial' we mean here an encoding which respects certain well-formedness criteria
as studied e.g. by Gorla [6]. The internship will contribute to a more precise understanding of the Location Graphs semantics, 
and can lead to a publication and/or a PhD on the topic.


References

[1] J.B. Stefani : "Component as location graphs", in Proc. 11th Int. Symp. Formal Aspects of Component Software (FACS), 
LNCS 8997, Springer, 2015.

[2] R. Milner : "Communicating and Mobile Systems: The Pi Calculus", Cambridge University Press, 1999.

[3] R. Milner : "The Space and Motion of Communicating Agents", Cambridge University Press, 2009.

[4] J. Bengtson, M. Johansson,  J. Parrow, B. Victor: "Psi-calculi: a framework for mobile processes with nominal data and logic",
Logical Methods in Computer Science 7(1), 2011.

[5] G.L. Ferrari, D. Hirsch, I. Lanese, U. Montanari, and E. Tuosto : "Synchronized Hyperedge Replacement as a model for Service 
Oriented Computing", in Proc. 4th Int. Symp. Formal Methods for Components and Objects (FMCO), LNCS 2006.

[6] D. Gorla : "Towards a Unified Approach to Encodability and Separation Results for Process Calculi", in Proc. CONCUR 2008.


Contact

Jean-Bernard Stefani, INRIA SPADES team, jean-bernard.stefani@inria.fr