Copyright Information
The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of
scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other
copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying
this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without
the explicit permission of the copyright holder.
show main publications
Process Bisimulation via a Graphical Encoding @INPROCEEDINGS{BGK:ICGT2006:PBGE, title = {{Process Bisimulation via a Graphical Encoding}}, author = {{Filippo} {Bonchi} and {Fabio} {Gadducci} and {Barbara} {Koenig}}, booktitle = {Proceedings of ICGT 2006, 3rd International Conference on Graph Transformation}, editor = {Andrea Corradini and Hartmut Ehrig and Ugo Montanari and Leila Ribeiro and Grzegorz Rozenberg}, pages = {168-183}, 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 based on borrowed contexts (BCs), proposed by Ehrig and Koenig (which are 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 some technical contributions towards the simplification of the BC mechanism, the key result of our work is the proof that the bisimilarity on processes obtained via BCs coincides with the standard strong bisimilarity for CCS.}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {4178}, year = {2006}, url = {http://rap.dsi.unifi.it/sensoriasite/icgt06Pippo.pdf}, partner = {PISA}, status = {public}, task = {T7.1}, }
|