We present the link-calculus, an extension of pi-calculus, that models interactions that are multiparty, i.e. that may involve more than two processes, mutually exchanging data. Communications are seen as chains of suitably combined links (which record the source and the target ends of each hop of interactions), each contributed by one party. Values are exchanged by means of message tuples, still provided by each party. We develop semantic theories and proof techniques for link-calculus and apply them in reasoning about complex distributing computing scenarios, where more than two participants need to synchronise in order to perform a task. In particular, we introduce the notion of linked bisimilarity in analogy with the early bisimilarity of the π-calculus. Differently from the π-calculus case, we can show that it is a congruence with respect to all the link-calculus operators and that is also closed under name substitution.

The link-calculus for open multiparty interactions

Chiara Bodei;Roberto Bruni
2020-01-01

Abstract

We present the link-calculus, an extension of pi-calculus, that models interactions that are multiparty, i.e. that may involve more than two processes, mutually exchanging data. Communications are seen as chains of suitably combined links (which record the source and the target ends of each hop of interactions), each contributed by one party. Values are exchanged by means of message tuples, still provided by each party. We develop semantic theories and proof techniques for link-calculus and apply them in reasoning about complex distributing computing scenarios, where more than two participants need to synchronise in order to perform a task. In particular, we introduce the notion of linked bisimilarity in analogy with the early bisimilarity of the π-calculus. Differently from the π-calculus case, we can show that it is a congruence with respect to all the link-calculus operators and that is also closed under name substitution.
2020
Bodei, Chiara; Brodo, Linda; Bruni, Roberto
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/1048308
 Attenzione

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

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