Published February 21, 2014
| Version v1
Publication
A behavioural theory for a π-calculus with preorders
Creators
Contributors
Others:
- Laboratoire de l'Informatique du Parallélisme (LIP) ; École normale supérieure de Lyon (ENS de Lyon) ; Université de Lyon-Université de Lyon-Université Claude Bernard Lyon 1 (UCBL) ; 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) ; Centre Inria d'Université Côte d'Azur (CRISAM) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)
- Preuves et Langages (PLUME) ; Laboratoire de l'Informatique du Parallélisme (LIP) ; École normale supérieure de Lyon (ENS de Lyon) ; Université de Lyon-Université de Lyon-Université Claude Bernard Lyon 1 (UCBL) ; Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon) ; Université de Lyon-Université de Lyon-Université Claude Bernard Lyon 1 (UCBL) ; Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)
- BASICS ; East China University of Science and Technology
- ANR-12-IS02-0001,PACE,Processus non-standard: Analyse, Coinduction, Expressivité(2012)
- ANR-10-LABX-0070,MILYON,Community of mathematics and fundamental computer science in Lyon(2010)
Description
We study the behavioural theory of piP, a pi-calculus featuring restriction as the only binder. In contrast with calculi such as Fusions and Chi, reduction in piP generates a preorder on names rather than an equivalence relation. We present two characterisations of barbed congruence in piP: the fi rst is based on a compositional LTS, and the second is an axiomatisation. The results in this paper bring out basic properties of piP, mostly related to the interplay between the restriction operator and the preorder on names
Additional details
Identifiers
- URL
- https://hal.science/hal-00949521
- URN
- urn:oai:HAL:hal-00949521v1
Origin repository
- Origin repository
- UNICA