nach oben

Erschienen in:

2021 | OriginalPaper | Buchkapitel

Concurrency Theorems for Non-linear Rewriting Theories

verfasst von : Nicolas Behr, Russ Harmer, Jean Krivine

Erschienen in: Graph Transformation

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Sesqui-pushout (SqPO) rewriting along non-linear rules and for monic matches is well-known to permit the modeling of fusing and cloning of vertices and edges, yet to date, no construction of a suitable concurrency theorem was available. The lack of such a theorem, in turn, rendered compositional reasoning for such rewriting systems largely infeasible. We develop in this paper a suitable concurrency theorem for non-linear SqPO-rewriting in categories that are quasi-topoi (subsuming the example of adhesive categories) and with matches required to be regular monomorphisms of the given category. Our construction reveals an interesting “backpropagation effect” in computing rule compositions. We derive in addition a concurrency theorem for non-linear double pushout (DPO) rewriting in rm-adhesive categories. Our results open non-linear SqPO and DPO semantics to the rich static analysis techniques available from concurrency, rule algebra and tracelet theory.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Nächstes Kapitel A Generalized Concurrent Rule Construction for Double-Pushout Rewriting

In this paper, we follow the conventions of compositional rewriting theory [9], i.e., we speak of “input”/“output” motifs of rules, as opposed to “left”/“right” motifs in the traditional literature [22].

Some authors prefer to not consider directly the category \(\mathbf {BRel}\), but rather define \(\mathbf {SGraph}\) as some category equivalent to \(\mathbf {BRel}\), where simple graphs are of the form \(\langle V,E\rangle \) with \(E\subseteq V\times V\). This is evidently equivalent to directly considering \(\mathbf {BRel}\), whence we chose to not make this distinction in this paper.

As demonstrated in [26, Fact 3.4], every finitary \(\mathcal {M}\)-adhesive category \(\mathbf{C}\) possesses an (extremal \(\mathcal {E}\), \(\mathcal {M}\))-factorization, so if \(\mathbf{C}\) is known to possess FPCs as required by the construction, this might allow to generalize the \(\mathcal {M}\)-FPC-PO-augmentation construction to this setting.

Note that square (1) pasted with the pullback square formed by the morphisms \(\overline{\alpha }, id_B,e,e\circ \bar{\alpha }\) yields a pullback square that is indeed of the right form to warrant the existence of a morphism n into the FPC square \((1)\,+\,(2)\).

Note that this part of the definition of general SqPO-semantics coincides precisely with the original definition of [17].

Note that we have drawn the rule from right to left so that the input, sometimes called the left-hand side, of the rule is the topmost rightmost graph. Note also that the structure of the homomorphisms may be inferred from the node positions, with the exception of the vertex clonings that are explicitly mentioned in the text.

Adamek, J., Herrlich, H., Strecker, G.: Abstract and concrete categories: the joy of cats. Reprints Theory Appl. Categ. (17), 1–507 (2006). http://www.tac.mta.ca/tac/reprints/articles/17/tr17.pdf

Behr, N.: Sesqui-pushout rewriting: concurrency, associativity and rule algebra framework. In: Proceedings of GCM 2019. EPTCS, vol. 309, pp. 23–52 (2019). https://doi.org/10.4204/eptcs.309.2

Behr, N.: Tracelets and tracelet analysis of compositional rewriting systems. In: Proceedings of ACT 2019. EPTCS, vol. 323, pp. 44–71 (2020). https://doi.org/10.4204/EPTCS.323.4

Behr, N.: On stochastic rewriting and combinatorics via rule-algebraic methods. In: Proceedings of TERMGRAPH 2020, vol. 334, pp. 11–28 (2021). https://doi.org/10.4204/eptcs.334.2

Behr, N., Danos, V., Garnier, I.: Stochastic mechanics of graph rewriting. In: Proceedings of LiCS 2016. ACM Press (2016). https://doi.org/10.1145/2933575.2934537

Behr, N., Danos, V., Garnier, I.: Combinatorial conversion and moment bisimulation for stochastic rewriting systems. LMCS 16(3), 3:1–3:45 (2020). https://lmcs.episciences.org/6628

Behr, N., Harmer, R., Krivine, J.: Concurrency theorems for non-linear rewriting theories (long version). CoRR (2021). https://arxiv.org/abs/2105.02842

Behr, N., Krivine, J.: Rewriting theory for the life sciences: a unifying theory of CTMC semantics. In: Gadducci, F., Kehrer, T. (eds.) ICGT 2020. LNCS, vol. 12150, pp. 185–202. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-51372-6_11CrossRef

Behr, N., Krivine, J.: Compositionality of rewriting rules with conditions. Compositionality 3, 2 (2021). https://doi.org/10.32408/compositionality-3-2CrossRef

10.

Behr, N., Sobocinski, P.: Rule algebras for adhesive categories (extended journal version). LMCS 16(3), 2:1–2:38 (2020). https://lmcs.episciences.org/6615

11.

Bonifati, A., Furniss, P., Green, A., Harmer, R., Oshurko, E., Voigt, H.: Schema validation and evolution for graph databases. In: Laender, A.H.F., Pernici, B., Lim, E.-P., de Oliveira, J.P.M. (eds.) ER 2019. LNCS, vol. 11788, pp. 448–456. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-33223-5_37CrossRef

12.

Bousquet-Mélou, M.: Counting planar maps, coloured or uncoloured. London Mathematical Society Lecture Note Series. Cambridge University Press, pp. 1–50 (2011). https://doi.org/10.1017/CBO9781139004114.002

13.

Boutillier, P., et al.: The Kappa platform for rule-based modeling. Bioinformatics 34(13), i583–i592 (2018). https://doi.org/10.1093/bioinformatics/bty272CrossRef

14.

Braatz, B., Golas, U., Soboll, T.: How to delete categorically—two pushout complement constructions. J. Symb. Comput. 46(3), 246–271 (2011). https://doi.org/10.1016/j.jsc.2010.09.007MathSciNetCrossRefMATH

15.

Cockett, J., Lack, S.: Restriction categories I: categories of partial maps. Theor. Comput. Sci. 270(1), 223–259 (2002). https://doi.org/10.1016/S0304-3975(00)00382-0MathSciNetCrossRefMATH

16.

Cockett, J., Lack, S.: Restriction categories II: partial map classification. Theor. Comput. Sci. 294(1), 61–102 (2003). https://doi.org/10.1016/S0304-3975(01)00245-6MathSciNetCrossRefMATH

17.

Corradini, A., Heindel, T., Hermann, F., König, B.: Sesqui-pushout rewriting. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 30–45. Springer, Heidelberg (2006). https://doi.org/10.1007/11841883_4CrossRef

18.

Corradini, A., Duval, D., Echahed, R., Prost, F., Ribeiro, L.: AGREE – algebraic graph rewriting with controlled embedding. In: Parisi-Presicce, F., Westfechtel, B. (eds.) ICGT 2015. LNCS, vol. 9151, pp. 35–51. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21145-9_3CrossRefMATH

19.

Danos, V., Heindel, T., Honorato-Zimmer, R., Stucki, S.: Reversible Sesqui-pushout rewriting. In: Giese, H., König, B. (eds.) ICGT 2014. LNCS, vol. 8571, pp. 161–176. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-09108-2_11CrossRef

20.

Diers, Y.: Familles universelles de morphismes, Publications de l’U.E.R. mathématiques pures et appliquées, vol. 145. Université des sciences et techniques de Lille I (1978)

21.

Dyckhoff, R., Tholen, W.: Exponentiable morphisms, partial products and pullback complements. J. Pure Appl. Algebra 49(1–2), 103–116 (1987)MathSciNetCrossRef

22.

Ehrig, H., et al.: Fundamentals of Algebraic Graph Transformation. Monographs in Theoretical Computer Science. Springer, Heidelberg (2006). https://doi.org/10.1007/3-540-31188-2

23.

Ehrig, H., Golas, U., Hermann, F.: Categorical frameworks for graph transformation and HLR systems based on the DPO approach. Bull. EATCS 102, 111–121 (2010)MathSciNetMATH

24.

Ehrig, H., Habel, A., Padberg, J., Prange, U.: Adhesive high-level replacement categories and systems. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) ICGT 2004. LNCS, vol. 3256, pp. 144–160. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30203-2_12CrossRef

25.

Ehrig, H., et al.: \(\cal{M}\)-adhesive transformation systems with nested application conditions. Part 1: parallelism, concurrency and amalgamation. MSCS 24(04), 1–48 (2014). https://doi.org/10.1017/s0960129512000357

26.

Braatz, B., Ehrig, H., Gabriel, K., Golas, U.: Finitary \(\cal{M}\)-adhesive categories. In: Ehrig, H., Rensink, A., Rozenberg, G., Schürr, A. (eds.) ICGT 2010. LNCS, vol. 6372, pp. 234–249. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15928-2_16CrossRef

27.

Garner, R., Lack, S.: On the axioms for adhesive and quasiadhesive categories. TAC 27(3), 27–46 (2012)MathSciNetMATH

28.

Harmer, R., Le Cornec, Y.S., Légaré, S., Oshurko, E.: Bio-curation for cellular signalling: the kami project. IEEE/ACM Trans. Comput. Biol. Bioinform. 16(5), 1562–1573 (2019). https://doi.org/10.1109/TCBB.2019.2906164CrossRef

29.

Harmer, R., Oshurko, E.: Knowledge representation and update in hierarchies of graphs. JLAMP 114, 100559 (2020)MathSciNetMATH

30.

Harmer, R., Oshurko, E.: Reversibility and composition of rewriting in hierarchies. EPTCS 330, 145–162 (2020). https://doi.org/10.4204/eptcs.330.9CrossRefMATH

31.

Heindel, T.: Hereditary pushouts reconsidered. In: Ehrig, H., Rensink, A., Rozenberg, G., Schürr, A. (eds.) ICGT 2010. LNCS, vol. 6372, pp. 250–265. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15928-2_17CrossRef

32.

Johnstone, P.T.: Sketches of an Elephant - A Topos Theory Compendium, vol. 1. Oxford University Press, Oxford (2002)MATH

33.

Johnstone, P.T., Lack, S., Sobociński, P.: Quasitoposes, quasiadhesive categories and artin glueing. In: Mossakowski, T., Montanari, U., Haveraaen, M. (eds.) CALCO 2007. LNCS, vol. 4624, pp. 312–326. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73859-6_21CrossRefMATH

34.

Lack, S., Sobociński, P.: Adhesive categories. In: Walukiewicz, I. (ed.) FoSSaCS 2004. LNCS, vol. 2987, pp. 273–288. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24727-2_20CrossRef

35.

Lack, S., Sobociński, P.: Adhesive and quasiadhesive categories. RAIRO - Theor. Inform. Appl. 39(3), 511–545 (2005). https://doi.org/10.1051/ita:2005028MathSciNetCrossRefMATH

36.

Löwe, M.: Polymorphic Sesqui-pushout graph rewriting. In: Parisi-Presicce, F., Westfechtel, B. (eds.) ICGT 2015. LNCS, vol. 9151, pp. 3–18. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21145-9_1CrossRefMATH

37.

Monro, G.: Quasitopoi, logic and heyting-valued models. J. Pure Appl. Algebra 42(2), 141–164 (1986). https://doi.org/10.1016/0022-4049(86)90077-0MathSciNetCrossRefMATH

Titel: Concurrency Theorems for Non-linear Rewriting Theories
verfasst von: Nicolas Behr
Russ Harmer
Jean Krivine
Verlag: Springer International Publishing
Buch: Graph Transformation
Print ISBN: 978-3-030-78945-9

Electronic ISBN: 978-3-030-78946-6

Copyright-Jahr: 2021
DOI: https://doi.org/10.1007/978-3-030-78946-6_1

Premium Partner

Bildnachweise

Rittal/© Rittal, NTT Data/© NTT Data, Wildix/© Wildix, Ceyoniq Technology GmbH/© Ceyoniq Technology GmbH, arvato Systems GmbH/© arvato Systems GmbH, Ninox Software GmbH/© Ninox Software GmbH, Everyday Software S.L./© Everyday Software S.L., Redgate/© Redgate, CELONIS Labs GmbH, DC-Datacenter-Group GmbH/© DC-Datacenter-Group GmbH, all for one/© all for one, G Data CyberDefense/© G Data CyberDefense, FAST LTA/© FAST LTA, Vendosoft/© Vendosoft, Kumavision/© Kumavision, Noriis Network AG/© Noriis Network AG, WSW Software GmbH/© WSW Software GmbH

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"