A Behavioural Theory for a π-calculus with Preorders

Creators: Hirschkoff, Daniel; Madiot, Jean-Marie; Xu, Xian

Others:: Laboratoire de l'Informatique du Parallélisme (LIP) ; École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL) ; Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS); Preuves et Langages (PLUME) ; Laboratoire de l'Informatique du Parallélisme (LIP) ; École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL) ; Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL) ; Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS); Foundations of Component-based Ubiquitous Systems (FOCUS) ; Inria Sophia Antipolis - Méditerranée (CRISAM) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Dipartimento di Informatica - Scienza e Ingegneria [Bologna] (DISI) ; Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO)-Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO); East China University of Science and Technology; Mehdi Dastani; Marjan Sirjani; TC 2; WG 2.2

Description

We study the behavioural theory of πP, a π-calculus in the tradition of Fusions and Chi calculi. In contrast with such calculi, reduction in πP generates a preorder on names rather than an equivalence relation. We present two characterisations of barbed congruence in πP: the first is based on a compositional LTS, and the second is an axiomatisation. The results in this paper bring out basic properties of πP, mostly related to the interplay between the restriction operator and the preorder on names.Consequently, πP is a calculus in the tradition of Fusion calculi, in which both types and behavioural equivalences can be exploited in order to reason rigorously about concurrent and mobile systems.

Abstract

International audience

A Behavioural Theory for a π-calculus with Preorders

Description

Abstract

Additional details