Process Bisimulation Via a Graphical Encoding

  • Filippo Bonchi
  • Fabio Gadducci
  • Barbara König
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4178)


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 König (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.


Inference Rule Boundary Node Graph Transformation Label Transition System Recursive Process 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Baldan, P., Corradini, A., Ehrig, H., Löwe, M., Montanari, U., Rossi, F.: Concurrent semantics of algebraic graph transformation. In: Ehrig, H., Kreowski, H.-J., Montanari, U., Rozenberg, G. (eds.) Handbook of Graph Grammars and Computing by Graph Transformation, vol. 3, pp. 107–187. World Scientific, Singapore (1999)Google Scholar
  2. 2.
    Baldan, P., Corradini, A., Heindel, T., König, B., Sobociński, P.: Processes for adhesive rewriting systems. In: Aceto, L., Ingólfsdóttir, A. (eds.) FOSSACS 2006. LNCS, vol. 3921, pp. 202–216. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  3. 3.
    Baldan, P., Ehrig, H., König, B.: Composition and decomposition of DPO transformations with borrowed context. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 153–167. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  4. 4.
    Berry, G., Boudol, G.: The chemical abstract machine. Theor. Comp. Sci. 96, 217–248 (1992)CrossRefMathSciNetzbMATHGoogle Scholar
  5. 5.
    Bonchi, F., Gadducci, F., König, B.: Process bisimulation via a graphical encoding. Technical Report TR-06-07, Dipartimento di Informatica, Università di Pisa (2006)Google Scholar
  6. 6.
    Corradini, A., Gadducci, F.: An algebraic presentation of term graphs, via gs-monoidal categories. Applied Categorical Structures 7, 299–331 (1999)CrossRefMathSciNetzbMATHGoogle Scholar
  7. 7.
    Corradini, A., Montanari, U., Rossi, F.: Graph processes. Fundamenta Informaticae 26, 241–265 (1996)MathSciNetzbMATHGoogle Scholar
  8. 8.
    Ehrig, H., König, B.: Deriving bisimulation congruences in the DPO approach to graph rewriting. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 151–166. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  9. 9.
    Engelfriet, J., Gelsema, T.: Multisets and structural congruence of the π-calculus with replication. Theor. Comp. Sci. 211, 311–337 (1999)CrossRefMathSciNetzbMATHGoogle Scholar
  10. 10.
    Gadducci, F.: Term graph rewriting and the π-calculus. In: Ohori, A. (ed.) APLAS 2003. LNCS, vol. 2895, pp. 37–54. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  11. 11.
    Gadducci, F., Heckel, R.: An inductive view of graph transformation. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 219–233. Springer, Heidelberg (1998)Google Scholar
  12. 12.
    Gadducci, F., Montanari, U.: A concurrent graph semantics for mobile ambients. In: Brookes, S., Mislove, M. (eds.) Mathematical Foundations of Programming Semantics. Electr. Notes in Theor. Comp. Sci., vol. 45. Elsevier Science, Amsterdam (2001)Google Scholar
  13. 13.
    Gadducci, F., Montanari, U.: Observing reductions in nominal calculi via a graphical encoding of processes. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds.) Processes, Terms and Cycles: Steps on the Road to Infinity. LNCS, vol. 3838, pp. 106–126. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  14. 14.
    Jensen, O.H., Milner, R.: Bigraphs and transitions. In: Morriset, G. (ed.) Principles of Programming Languages, pp. 38–49. ACM Press, New York (2003)Google Scholar
  15. 15.
    Leifer, J., Milner, R.: Deriving bisimulation congruences for reactive systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 243–258. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  16. 16.
    Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)zbMATHGoogle Scholar
  17. 17.
    Milner, R.: The polyadic π-calculus: A tutorial. In: Bauer, F.L., Brauer, W., Schwichtenberg, H. (eds.) Logic and Algebra of Specification. Nato ASI Series F, vol. 94, pp. 203–246. Springer, Heidelberg (1993)Google Scholar
  18. 18.
    Milner, R.: Pure bigraphs: Structure and dynamics. Information and Computation 204, 60–122 (2006)CrossRefMathSciNetzbMATHGoogle Scholar
  19. 19.
    Parrow, J., Victor, B.: The fusion calculus: Expressiveness and simmetry in mobile processes. In: Pratt, V. (ed.) Logic in Computer Science, pp. 176–185. IEEE Computer Society Press, Los Alamitos (1998)Google Scholar
  20. 20.
    Sassone, V., Sobociński, P.: Deriving bisimulation congruences using 2-categories. Nordic Journal of Computing 10, 163–183 (2003)MathSciNetzbMATHGoogle Scholar
  21. 21.
    Sassone, V., Sobociński, P.: Reactive systems over cospans. In: Logic in Computer Science, pp. 311–320. IEEE Computer Society Press, Los Alamitos (2005)Google Scholar
  22. 22.
    Sewell, P.: From rewrite rules to bisimulation congruences. Theor. Comp. Sci. 274, 183–230 (2004)CrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Filippo Bonchi
    • 1
  • Fabio Gadducci
    • 1
  • Barbara König
    • 2
  1. 1.Dipartimento di InformaticaUniversità di Pisa 
  2. 2.Institut für Informatik und Interaktive SystemeUniversität Duisburg-Essen 

Personalised recommendations