Observational Equivalence for Synchronized Graph Rewriting with Mobility
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.
KeywordsGraph Transformation Monoidal Category Tile System Variable Node Parallel Composition
Unable to display preview. Download preview PDF.
- 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.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.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
- 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.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.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.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.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
- 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.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.Barbara Konig. Description and Verification of Mobile Processes with Graph Rewriting Techniques. PhD thesis, Technische Universitat Munchen, 1999.Google Scholar
- 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
- 21.Robin Milner. Communicating and Mobile Systems: the π-Calculus. Cambridge University Press, 1999.Google Scholar
- 22.Robin Milner and Davide Sangiorgi. Barbed bisimulation. In Proc. of ICALP’ 92. Springer-Verlag, 1992. LNCS 623.Google Scholar
- 24.Grzegorz Rozenberg, editor. Handbook of Graph Grammars and Computing by Graph Transformation, Vol.1: Foundations, volume 1. World Scientific, 1997.Google Scholar
- 25.Nobuko Yoshida. Graph notation for concurrent combinators. In Proc. of TPPP’ 94. Springer-Verlag, 1994. LNCS 907.Google Scholar