The paper introduces a novel approach to the synthesis of labelled transition systems for calculi with name mobility. The proposal is based on a graphical encoding: Each process is mapped into a (ranked) graph, such that the denotation is fully abstract with respect to the usual structural congruence (i.e., two processes are equivalent exactly when the corresponding encodings yield the same graph). Ranked graphs are naturally equipped with a few algebraic operations, and they are proved to form a suitable (bi)category of cospans. Then, as proved by Sassone and Sobocinski, the synthesis mechanism based on relative pushout, originally proposed by Milner and Leifer, can be applied. The resulting labelled transition system has ranked graphs as both states and labels, and it induces on (encodings of) processes an observational equivalence that is reminiscent of early bisimilarity.

Observing reductions in nominal calculi via a graphical encoding of processes

GADDUCCI, FABIO;MONTANARI, UGO GIOVANNI ERASMO
2005-01-01

Abstract

The paper introduces a novel approach to the synthesis of labelled transition systems for calculi with name mobility. The proposal is based on a graphical encoding: Each process is mapped into a (ranked) graph, such that the denotation is fully abstract with respect to the usual structural congruence (i.e., two processes are equivalent exactly when the corresponding encodings yield the same graph). Ranked graphs are naturally equipped with a few algebraic operations, and they are proved to form a suitable (bi)category of cospans. Then, as proved by Sassone and Sobocinski, the synthesis mechanism based on relative pushout, originally proposed by Milner and Leifer, can be applied. The resulting labelled transition system has ranked graphs as both states and labels, and it induces on (encodings of) processes an observational equivalence that is reminiscent of early bisimilarity.
2005
Gadducci, Fabio; Montanari, UGO GIOVANNI ERASMO
File in questo prodotto:
File Dimensione Formato  
klop.pdf

solo utenti autorizzati

Tipologia: Versione finale editoriale
Licenza: NON PUBBLICO - Accesso privato/ristretto
Dimensione 1.24 MB
Formato Adobe PDF
1.24 MB Adobe PDF   Visualizza/Apri   Richiedi una copia

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/92016
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 10
  • ???jsp.display-item.citation.isi??? 9
social impact