The paper presents a case study on the synthesis of labelled transition systems (LTSs) for process calculi, choosing as testbed Milner's Calculus of Communicating System (CCS). The proposal is based on a graphical encoding: each CCS process is mapped into a graph equipped with suitable interfaces, such that the denotation is fully abstract with respect to the usual structural congruence. Graphs with interfaces are amenable to the synthesis mechanism proposed by Ehrig and Koenig and based on borrowed contexts (BCs), an instance of relative pushouts originally introduced by Milner and Leifer. The BC mechanism allows the effective construction of an LTS that has graphs with interfaces as both states and labels, and such that the associated bisimilarity is automatically a congruence. Our paper focuses on the analysis of the LTS distilled by exploiting the encoding of CCS processes: besides offering major technical contributions towards the simplification of the BC mechanism, a key result of our work is the proof that the bisimilarity on processes obtained via BCs coincides with the standard strong bisimilarity for CCS.

Synthesising CCS bisimulation using graph rewriting

Bonchi F.;GADDUCCI, FABIO;
2009

Abstract

The paper presents a case study on the synthesis of labelled transition systems (LTSs) for process calculi, choosing as testbed Milner's Calculus of Communicating System (CCS). The proposal is based on a graphical encoding: each CCS process is mapped into a graph equipped with suitable interfaces, such that the denotation is fully abstract with respect to the usual structural congruence. Graphs with interfaces are amenable to the synthesis mechanism proposed by Ehrig and Koenig and based on borrowed contexts (BCs), an instance of relative pushouts originally introduced by Milner and Leifer. The BC mechanism allows the effective construction of an LTS that has graphs with interfaces as both states and labels, and such that the associated bisimilarity is automatically a congruence. Our paper focuses on the analysis of the LTS distilled by exploiting the encoding of CCS processes: besides offering major technical contributions towards the simplification of the BC mechanism, a key result of our work is the proof that the bisimilarity on processes obtained via BCs coincides with the standard strong bisimilarity for CCS.
Bonchi, F.; Gadducci, Fabio; König, B.
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: http://hdl.handle.net/11568/130139
 Attenzione

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

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