We present and compare P-PRISMA and F-PRISMA, two parametric calculi that can be instantiated with different interaction policies, defined as synchronization algebras with mobility of names (SAMs). In particular, P-PRISMA is based on name transmission (P-SAM), like pi-calculus, and thus exploits directional (input-output) communication only, while F-PRISMA is based on name fusion (F-SAM), like Fusion calculus, and thus exploits a more symmetric form of communication. However, P-PRISMA and F-PRISMA can easily accommodate many other high-level synchronization mechanisms than the basic ones available in pi-calculus and Fusion, hence allowing for the development of a general meta-theory of mobile calculi. We define for both the labeled operational semantics and a form of strong bisimilarity, showing that the latter is compositional for any SAM. We also discuss reduction semantics and weak bisimilarity. We give several examples based on heterogeneous SAMs, we investigate the case studies of pi-calculus and Fusion calculus giving correspondence theorems, and we show how P-PRISMA can be encoded in F-PRISMA. Finally, we show that basic categorical tools can help to relate and to compose SAMs and PRISMA processes in an elegant way.

Parametric synchronizations in mobile nominal calculi

BRUNI, ROBERTO;
2008-01-01

Abstract

We present and compare P-PRISMA and F-PRISMA, two parametric calculi that can be instantiated with different interaction policies, defined as synchronization algebras with mobility of names (SAMs). In particular, P-PRISMA is based on name transmission (P-SAM), like pi-calculus, and thus exploits directional (input-output) communication only, while F-PRISMA is based on name fusion (F-SAM), like Fusion calculus, and thus exploits a more symmetric form of communication. However, P-PRISMA and F-PRISMA can easily accommodate many other high-level synchronization mechanisms than the basic ones available in pi-calculus and Fusion, hence allowing for the development of a general meta-theory of mobile calculi. We define for both the labeled operational semantics and a form of strong bisimilarity, showing that the latter is compositional for any SAM. We also discuss reduction semantics and weak bisimilarity. We give several examples based on heterogeneous SAMs, we investigate the case studies of pi-calculus and Fusion calculus giving correspondence theorems, and we show how P-PRISMA can be encoded in F-PRISMA. Finally, we show that basic categorical tools can help to relate and to compose SAMs and PRISMA processes in an elegant way.
2008
Bruni, Roberto; Lanese, I.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11568/118566
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? 4
social impact