Published in Volume XXII, Issue 1, 2012, pages 105-145, doi: 10.7561/SACS.2012.1.105
Authors: A. Dorman, T. Heindel, B. König
Abstract
Process calculi and graph transformation systems provide models of reactive systems with labelled transition semantics (LTS). While the semantics for process calculi is compositional, this is not the case for graph transformation systems, in general. Hence, the goal of this article is to obtain a compositional semantics for graph transformation system in analogy to the structural operational semantics (SOS) for Milner’s Calculus of Communicating Systems (CCS).
The paper introduces an SOS style axiomatization of the standard labelled transition semantics for graph transformation systems that is based on the idea of minimal reaction contexts as labels, due to Leifer and Milner. In comparison to previous work on inductive definitions of similarly derived LTSs, the main feature of the proposed axiomatization is a composition rule that captures the communication of sub-systems so that it can feature as a counterpart to the communication rule of CCS.
Full Text (PDF)References
[1] P. Baldan, H. Ehrig, and B. König. Composition and decomposition of DPO transformations with borrowed context. In Proceedings of ICGT ’06, volume 4178 of Lecture Notes in Computer Science, pages 153-167. Springer, 2006.
[2] F. Bonchi, F. Gadducci, and B. König. Synthesising CCS bisimulation using graph rewriting. Information and Computation, 207(1):14-40, 2009. http://dx.doi.org/10.1016/j.ic.2008.10.005
[3] F. Bonchi, F. Gadducci, and G. V. Monreale. Labelled Transitions for Mobile Ambients (as Synthesized via a Graphical Encoding). Electronic Notes in Theoretical Computer Science, 242(1):73-98, 2009. http://dx.doi.org/10.1016/j.entcs.2009.06.014
[4] R. Bruni and E. Tuosto A. Lluch Lafuente, U. Montanari. Style-based architectural reconfigurations. Bulletin of the EATCS, 94:161-180, 2008.
[5] R. Bruni, F. Gadducci, and A. Lluch Lafuente. A graph syntax for processes and services. Web Services and Formal Methods, pages 46-60, 2010.
[6] R. Bruni, F. Gadducci, U. Montanari, and P. Sobociniski. Deriving weak bisimulation congruences from reduction systems. In Proceedings of CONCUR ’05, volume 3653 of Lecture Notes in Computer Science, pages 293-307. Springer, 2005.
[7] A. Corradini, R. Heckel, and U. Montanari. Graphical operational semantics. In Proceedings of GT-VMT ’00, pages 411-418. Carleton Scientic, Ottawa, 2000.
[8] R. de Simone. Higher level synchronizing devices in MEIJE-SCCS. Theoretical Computer Science, 37:245-267, 1985. http://dx.doi.org/10.1016/0304-3975(85)90093-3
[9] A. Dorman and T. Heindel. Structured operational semantics for graph rewriting. In Silva et al. [26], pages 37-51
[10] H. Ehrig and B. König. Deriving Bisimulation Congruences in the DPO Approach to Graph Rewriting with Borrowed Contexts. Mathematical Structures in Computer Science, 16(6):1133-1163, 2006. http://dx.doi.org/10.1017/S096012950600569X
[11] F. Gadducci. Graph rewriting for the pi-calculus. Mathematical Structures in Computer Science, 17(3):407-437, 2007. http://dx.doi.org/10.1017/S096012950700610X
[12] F. Gadducci and U. Montanari. The tile model. In Plotkin et al. [21], pages 133-166.
[13] D. Grohmann and M. Miculan. Graph algebras for bigraphs. Electronic Communications of the EASST, 29, 2010.
[14] J.F. Groote and F. Vaandrager. Structured operational semantics and bisimulation as a congruence. Information and Computation, 100:202-260, 1992. http://dx.doi.org/10.1016/0890-5401(92)90013-6
[15] D. Hirsch and U. Montanari. Synchronized hyperedge replacement with name mobility (a graphical calculus for mobile systems). In Proceedings of CONCUR ’01, volume 2154 of Lecture Notes in Computer Science, pages 121-136. Springer, 2001.
[16] D. Hirsch and U. Montanari. Shaped hierarchical architectural design. Electronic Notes in Theoretical Computer Science, 109:97-109, 2004. http://dx.doi.org/10.1016/j.entcs.2004.02.059
[17] Y. Lafont. Interaction nets. In Proceedings of POPL ’90, pages 95-108, New York, NY, USA, 1990. ACM.
[18] J. J. Leifer and R. Milner. Deriving bisimulation congruences for reactive systems. In Proceedings of CONCUR ’00, volume 1877 of Lecture Notes in Computer Science, pages 243-258, 2000.
[19] R. Milner. Bigraphical reactive systems. In Proceedings of CONCUR ’01, volume 2154 of Lecture Notes in Computer Science, pages 16-35. Springer, 2001.
[20] R. Milner. Pure bigraphs: Structure and dynamics. Information and Computation, 204(1):60-122, 2006. http://dx.doi.org/10.1016/j.ic.2005.07.003
[21] G. D. Plotkin, C. Stirling, and M. Tofte, editors. Proof, Language, and Interaction, Essays in Honour of Robin Milner. The MIT Press, 2000.
[22] J. Rathke and P. Sobocinski. Deriving structural labelled transitions for mobile ambients. Information and Computation, 208:1221-1242, 2010. http://dx.doi.org/10.1016/j.ic.2010.06.001
[23] A. Rensink. Compositionality in graph transformation. In Proceedings of ICALP ’10, volume 6199 of Lecture Notes in Computer Science, pages 309-320. Springer, 2010.
[24] V. Sassone and P. Sobocinski. Deriving bisimulation congruences using 2-categories. Nordic Journal of Computing, 10(2):163-183, 2003.
[25] V. Sassone and P. Sobocinski. A Congruence for Petri Nets. Electronic Notes in Theoretical Computer Science, 127(2):107-120, 2005. http://dx.doi.org/10.1016/j.entcs.2005.02.008
[26] A. Silva, S. Bliudze, R. Bruni, and M. Carbone, editors. Proceedings Fourth Interaction and Concurrency Experience, volume 59 of Electronic Proceedings in Theoretical Computer Science, 2011.
[27] A. Simpson. Sequent Calculi for Process Verification: Hennessy-Milner Logic for an Arbitrary GSOS. Journal of Logic and Algebraic Programming, 60-61:287 – 322, 2004. http://dx.doi.org/10.1016/j.jlap.2004.03.004
Bibtex
@article{sacscuza:dorman2013sosfgr,
title={Structured Operational Semantics for Graph Rewriting},
author={A. Dorman and T. Heindel and B. König},
journal={Scientific Annals of Computer Science},
volume={22},
number={1},
organization={``A.I. Cuza'' University, Iasi, Romania},
year={2013},
pages={105--145},
doi={10.7561/SACS.2012.1.105},
publisher={``A.I. Cuza'' University Press}
}