We present the link-calculus, an extension of π-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.
Scheda prodotto non validato
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo
|Titolo:||The link-calculus for open multiparty interactions|
BRODO, Linda (Corresponding)
|Data di pubblicazione:||2020|
|Appare nelle tipologie:||1.1 Articolo in rivista|