Team : APR
Departure date : 09/30/2010
Supervision : Amal EL FALLAH SEGHROUCHNI Co-supervision : PESCHANSKI Frédéric
Towards A Denotational Semantics for Mobility
The semantics of concurrent systems has been studied extensively. Even though several avenues have been explored, there are two main schools of thought in the matter. The first promotes the π-calculus, a process algebra defined by extending its ancestor CCS. Its semantic point of view is operational, as processes are represented as labelled transition systems. Its main asset is that it allows to intuitively express mobility, the ability of processes to move with respect to one another. This is possible by allowing to make the scope of communication channels vary. The second rests on CSP, a process algebra which was built from a denota- tional point of view, as a value-passing concurrent language whose processes are translated into a set-theoretic augmented trace system which was refined through- out the years. Although CSP has no native support for mobility, it was recently shown that it is expressive enough to encode the π-calculus. The main purpose of this thesis was and still is to build a bridge between both worlds, by contributing a process algebra that is both fully mobile like the π- calculus, with the full expressive power of dynamic channel name scoping, but also fully denotational like CSP, with a set-theoretic compositional denotation defined for each process rather than just an operational characterisation. This last goal was not fully reached. In order to retain the native mobility of the π-calculus, part of its syntax and constructs had to be retained, specifically its concept of scope restriction that, together with the ability to send scope-restricted channels through public channels, allow to make channel scope truly dynamic. This imposed to introduce locations in order to link each observation to the potential of the process for further interaction at that point, using the unique spatial identification of the relevant node within the process branching structure.
The contributions of this thesis are as follows. First, a process algebra that is a xxvii variant of the π-calculus which is inspired by CSP, and is both compositional and mobile, is introduced. It is compositional because such models can be composed without regard for context, and a context-independent equivalence relation could be designed. It is mobile because it shares the whole of the π-calculus mobile prop- erties, not only channel passing but also scope extrusion. Despite its weaknesses, it is a significant step towards a denotational model. Second, full abstraction was achieved: an axiomatic semantics is also provided and proved to strictly corre- spond to the finite part of the denotational semantics. Due to its properties, the process algebra behaves in an elegant way even with the mismatch operator, which is not a given for many variants of the π-calculus. Third, a refinement theory is provided for the language. Although still very perfectible, it is unheard of in a mobile setting. Fourth, a logic was designed, following the CSP world model.
Defence : 01/10/2011 - 10h Jury members : Mme EL FALLAH SEGHROUCHNI Amal
M. ROSCOE Andrew William [Rapporteur]
M. GOLDSMITH Michael [Rapporteur]
Mme CASTELLANI Ilaria
M. HIRSCHKOFF Daniel
Mme BERARD Béatrice
M. PESCHANSKI Frédéric Encadrant
J.‑A. Bialkiewicz, F. Peschanski : “A Denotational Study of Mobility”, Communicating Process Architectures, vol. 67, Concurrent Systems Engineering Series, Eindhoven, Netherlands, pp. 239-261, (IOS Press), (ISBN: 978-1-60750-065-0) (2009)
F. Peschanski, J.‑A. Bialkiewicz : “Modelling and Verifying Mobile Systems Using Pi-Graphs”, 35th International Conference on Current Trends in Theory and Practice of Computer Science (Sofsem 2009), vol. 5404, Lecture Notes in Computer Science, Špindlerův Mlýn, Czech Republic, pp. 437-442, (Springer) (2009)