Abstract
Motivated by recent work on the derivation of labelled transitions and bisimulation congruences from unlabelled reaction rules, we show how to solve this problem in the DPO (double-pushout) approach to graph rewriting. Unlike in previous approaches, we consider graphs as objects, instead of arrows, of the category under consideration. This allows us to present a very simple way of deriving labelled transitions (called rewriting steps with borrowed context) which smoothly integrates with the DPO approach, has a very constructive nature and requires only a minimum of category theory. The core part of this paper is the proof sketch that the bisimilarity based on rewriting with borrowed contexts is a congruence relation.
Research partially supported by the BMBF project DACHIA, the TMR network SEGRAVIS and EPSRC grant R93346/01.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Bruni, R., Montanari, U., Sassone, V.: Open ended systems, dynamic bisimulation and tile logic. In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol. 1872, p. 440. Springer, Heidelberg (2000)
Corradini, A., Montanari, U., Rossi, F., Ehrig, H., Heckel, R., Löwe, M.: Algebraic approaches to graph transformation—part I: Basic concepts and double pushout approach. In: Rozenberg, G. (ed.) Handbook of Graph Grammars and Computing by Graph Transformation,Foundations, ch.3, vol.1. World Scientific, Singapore (1997)
Ehrig, H.: Bigraphs meet double pushouts. EATCS Bulletin 78, 72–85 (2002)
Ehrig, H., Gajewsky, M., Parisi-Presicce, F.: High-level replacement systems with applications to algebraic specifications and Petri nets. In: Ehrig, H., Kreowski, H.-J., Montanari, U., Rozenberg, G. (eds.) Handbook of Graph Grammars and Computing by Graph Transformation, Concurrency, Parallellism, and Distribution, ch. 6, vol. 3, pp. 341–400. World Scientific, Singapore (1999)
Ehrig, H., Heckel, R., Korff, M., Löwe, M., Ribeiro, L., Wagner, A., Corradini, A.: Algebraic approaches to graph transformation—part II: Single pushout approach and comparison with double pushout approach. In: Rozenberg, G. (ed.) Handbook of Graph Grammars and Computing by Graph Transformation, Foundations, ch. 4, vol. 1, World Scientific, Singapore (1997)
Ehrig, H., König, B.: Deriving bisimulation congruences in the DPO approach to graph rewriting. Technical report, Universität Stuttgart (2004) (to appear)
Gadducci, F., Heckel, R.: An inductive view of graph transformation. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 223–237. Springer, Heidelberg (1998)
Gadducci, F., Montanari, U.: A concurrent graph semantics for mobile ambients. In: Brookes, S., Mislove, M. (eds.) Proceedings of the 17th MFPS. Electronic Notes in Computer Science, vol. 45, Elsevier Science, Amsterdam (2001)
Gadducci, F., Montanari, U.: Comparing logics for rewriting: Rewriting logic, action calculi and tile logic. Theoretical Computer Science 285(2), 319–358 (2002)
Jensen, O.H., Milner, R.: Bigraphs and transitions. In: Proc. of POPL 2003, pp. 38–49. ACM, New York (2003)
König, B.: A graph rewriting semantics for the polyadic π-calculus. In: Workshop on Graph Transformation and Visual Modeling Techniques, ICALP Workshops 2000, Geneva, Switzerland, pp. 451–458. Carleton Scientific (2000)
Lack, S., Sobociński, P.: Adhesive categories. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 273–288. Springer, Heidelberg (2004)
Leifer, J.J.: Operational congruences for reactive systems. PhD thesis, University of Cambridge Computer Laboratory (September 2001)
Leifer, J.J., Milner, R.: Deriving bisimulation congruences for reactive systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, p. 243. Springer, Heidelberg (2000)
Lane, S.M.: Categories for the Working Mathematician. Springer, Heidelberg (1971)
Milner, R.: Bigraphical reactive systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 16–35. Springer, Heidelberg (2001)
Milner, R., Sangiorgi, D.: Barbed bisimulation. In: Proc. of ICALP 1992. LNCS, vol. 623. Springer, Heidelberg (1992)
Montanari, U., Sassone, V.: Dynamic congruence vs. progressing bisimulation for CCS. Fundamenta Informaticae 16, 171–196 (1992)
Montanari, U., Pistore, M.: Concurrent semantics for the π-calculus. Electronic Notes in Theoretical Computer Science 1 (1995)
Rozenberg, G.: Handbook of Graph Grammars and Computing by Graph Transformation, Foundations, vol. 1. World Scientific, Singapore (1997)
Sangiorgi, D.: On the proof method for bisimulation. In: Hájek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol. 969, pp. 479–488. Springer, Heidelberg (1995)
Sangiorgi, D., Walker, D.: The π-calculus—A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)
Sassone, V., Sobocinski, P.: Deriving bisimulation congruences: 2-categories vs precategories. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 409–424. Springer, Heidelberg (2003)
Sewell, P.: From rewrite rules to bisimulation congruences. Theoretical Computer Science 274(1-2), 183–230 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ehrig, H., König, B. (2004). Deriving Bisimulation Congruences in the DPO Approach to Graph Rewriting. In: Walukiewicz, I. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2004. Lecture Notes in Computer Science, vol 2987. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24727-2_12
Download citation
DOI: https://doi.org/10.1007/978-3-540-24727-2_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21298-0
Online ISBN: 978-3-540-24727-2
eBook Packages: Springer Book Archive