Advertisement

Observational Equivalence for Synchronized Graph Rewriting with Mobility

  • Barbara König
  • Ugo Montanari
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2215)

Abstract

We introduce a notion of bisimulation for graph rewriting systems, allowing us to prove observational equivalence for dynamically evolving graphs and networks.

We use the framework of synchronized graph rewriting with mobility which we describe in two different, but operationally equivalent ways: on graphs defined as syntactic judgements and by using tile logic. One of the main results of the paper says that bisimilarity for synchronized graph rewriting is a congruence whenever the rewriting rules satisfy the basic source property. Furthermore we introduce an up-to technique simplifying bisimilarity proofs and use it in an example to show the equivalence of a communication network and its specification.

Keywords

Graph Transformation Monoidal Category Tile System Variable Node Parallel Composition 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    R. Bruni, D. Frutos-Escrig, N. Martí-Oliet, and U. Montanari. Bisimilarity congruences for open terms and term graphs via tile logic. In Proc. of CONCUR 2000, pages 259–274. Springer-Verlag, 2000. LNCS 1877.CrossRefGoogle Scholar
  2. 2.
    R. Bruni, D. Frutos-Escrig, N. Martí-Oliet, and U. Montanari. Tile bisimilarity congruences for open terms and term graphs. Technical Report TR-00-06, Dipartimento di Informatica, Università di Pisa, 2000.Google Scholar
  3. 3.
    Roberto Bruni, Fabio Gadducci, and Ugo Montanari. Normal forms for partitions and relations. In Recents Trends in Algebraic Development Techniques, 12th International Workshop, WADT’ 98, pages 31–47. Springer-Verlag, 1998. LNCS 1589, full version to appear in TCS.Google Scholar
  4. 4.
    Gnanamalar David, Frank Drewes, and Hans-Jörg Kreowski. Hyperedge replacement with rendezvous. In Proc. of TAPSOFT (Theory and Practice of Software Development), pages 167–181. Springer-Verlag, 1993. LNCS 668.Google Scholar
  5. 5.
    Roberto de Simone. Higher level synchronizing devices in MEIJE-SCCS. Theoretical Computer Science, 37:245–267, 1985.zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    P. Degano and U. Montanari. A model of distributed systems based on graph rewriting. Journal of the ACM, 2(34):411–449, 1987.CrossRefMathSciNetGoogle Scholar
  7. 7.
    H. Ehrig. Introduction to the algebraic theory of graphs. In Proc. 1st International Workshop on Graph Grammars, pages 1–69. Springer-Verlag, 1979. LNCS 73.Google Scholar
  8. 8.
    H. Ehrig, H.-J. Kreowski, U. Montanari, and G. Rozenberg, editors. Handbook of Graph Grammars and Computing by Graph Transformation, Vol.3: Concurrency, Parallellism, and Distribution. World Scientific, 1999.Google Scholar
  9. 9.
    Maribel Fernández and Ian Mackie. Coinductive techniques for operational equivalence of interaction nets. In Proc. of LICS’ 98. IEEE Computer Society Press, 1998.Google Scholar
  10. 10.
    F. Gadducci and R. Heckel. An inductive view of graph transformation. In Recent Trends in Algebraic Development Techniques, 12th International Workshop, WADT’ 97, pages 223–237. Springer-Verlag, 1997. LNCS 1376.Google Scholar
  11. 11.
    F. Gadducci and U. Montanari. The tile model. In Gordon Plotkin, Colin Stirling, and Mads Tofte, editors, Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press, 1999.Google Scholar
  12. 12.
    J.F. Groote and F. Vaandrager. Structured operational semantics and bisimulation as a congruence. Information and Computation, 100:202–260, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    Dan Hirsch, Paola Inverardi, and Ugo Montanari. Reconfiguration of software architecture styles with name mobility. In António Porto and Gruia-Catalin Roman, editors, Proc. of COORDINATION 2000, pages 148–163. Springer-Verlag, 2000. LNCS 1906.Google Scholar
  14. 14.
    Dan Hirsch and Ugo Montanari. Synchronized hyperedge replacement with name mobility (a graphical calculus for mobile systems). In Proc. of CONCUR’ 01. Springer-Verlag, 2001. to appear.Google Scholar
  15. 15.
    Barbara Konig. Description and Verification of Mobile Processes with Graph Rewriting Techniques. PhD thesis, Technische Universitat Munchen, 1999.Google Scholar
  16. 16.
    Barbara Konig. A graph rewriting semantics for the polyadic pi-calculus. In Workshop on Graph Transformation and Visual Modeling Techniques (Geneva, Switzerland), ICALP Workshops’ 00, pages 451–458. Carleton Scientific, 2000.Google Scholar
  17. 17.
    James J. Leifer and Robin Milner. Deriving bisimulation congruences for reactive systems. In Proc. of CONCUR 2000, 2000. LNCS 1877.CrossRefGoogle Scholar
  18. 18.
    R. Milner and D. Sangiorgi. Techniques of weak bisimulation up-to. In Proc. of CONCUR’ 92. Springer-Verlag, 1992. LNCS 630.CrossRefGoogle Scholar
  19. 19.
    Robin Milner. A Calculus of Communicating Systems. Springer-Verlag, 1980. LNCS 92.zbMATHGoogle Scholar
  20. 20.
    Robin Milner. Calculi for interaction. Acta Informatica, 33(8):707–737, 1996.CrossRefMathSciNetGoogle Scholar
  21. 21.
    Robin Milner. Communicating and Mobile Systems: the π-Calculus. Cambridge University Press, 1999.Google Scholar
  22. 22.
    Robin Milner and Davide Sangiorgi. Barbed bisimulation. In Proc. of ICALP’ 92. Springer-Verlag, 1992. LNCS 623.Google Scholar
  23. 23.
    U. Montanari and F. Rossi. Graph rewriting, constraint solving and tiles for coordinating distributed systems. Applied Categorical Structures, 7:333–370, 1999.zbMATHCrossRefMathSciNetGoogle Scholar
  24. 24.
    Grzegorz Rozenberg, editor. Handbook of Graph Grammars and Computing by Graph Transformation, Vol.1: Foundations, volume 1. World Scientific, 1997.Google Scholar
  25. 25.
    Nobuko Yoshida. Graph notation for concurrent combinators. In Proc. of TPPP’ 94. Springer-Verlag, 1994. LNCS 907.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Barbara König
    • 1
  • Ugo Montanari
    • 1
  1. 1.Dipartimento di InformaticaUniversità di PisaItalia

Personalised recommendations