×

Efficient computation of graph overlaps for rule composition: theory and Z3 prototyping. (English) Zbl 07456054

Hoffmann, Berthold (ed.) et al., Proceedings of the eleventh international workshop on graph computation models, GCM 2020, online-workshop, June 24, 2020. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 330, 126-144 (2020).
Summary: Graph transformation theory relies upon the composition of rules to express the effects of sequences of rules. In practice, graphs are often subject to constraints, ruling out many candidates for composed rules. Focusing on the case of sesqui-pushout (SqPO) semantics, we develop a number of alternative strategies for computing compositions, each theoretically and with an implementation via the Python API of the Z3 theorem prover. The strategies comprise a straightforward generate-and-test strategy based on forbidden graph patterns, a variant with a more implicit logical encoding of the negative constraints, and a modular strategy, where the patterns are decomposed as forbidden relation patterns. For a toy model of polymer formation in organic chemistry, we compare the performance of the three strategies in terms of execution times and memory consumption.
For the entire collection see [Zbl 1466.68017].

MSC:

68Qxx Theory of computing

Software:

z3; Grez; MedOlDatschgerl
PDFBibTeX XMLCite
Full Text: arXiv Link

References:

[1] Jakob L. Andersen, Christoph Flamm, Daniel Merkle & Peter F. Stadler (2016): A Software Package for Chemically Inspired Graph Transformation. In: Graph Transformation (ICGT 2016), LNCS 9761, Springer International Publishing, pp. 73-88, doi:10.1007/978-3-319-40530-8 5. · Zbl 1344.68105 · doi:10.1007/978-3-319-40530-8_5
[2] Mayur Bapodra & Reiko Heckel (2010): From Graph Transformations to Differential Equations. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 30, doi:10.14279/tuj.eceasst.30.431. · doi:10.14279/tuj.eceasst.30.431
[3] Nicolas Behr (2019): Sesqui-Pushout Rewriting: Concurrency, Associativity and Rule Algebra Framework. In: Workshop on Graph Computation (GCM 2019), EPTCS 309, Open Publishing Association, pp. 23-52, doi:10.4204/eptcs.309.2. · Zbl 07453087 · doi:10.4204/eptcs.309.2
[4] Nicolas Behr, Vincent Danos & Ilias Garnier (2016): Stochastic mechanics of graph rewriting. In: Proceed-ings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016), ACM Press, doi:10.1145/2933575.2934537. · Zbl 1401.68132 · doi:10.1145/2933575.2934537
[5] Nicolas Behr, Vincent Danos & Ilias Garnier (2020): Combinatorial Conversion and Moment Bisimulation for Stochastic Rewriting Systems. Logical Methods in Computer Science Volume 16, Issue 3. Available at https://lmcs.episciences.org/6628. · Zbl 1528.68153
[6] Nicolas Behr & Jean Krivine (2019): Compositionality of Rewriting Rules with Conditions. Available at arXiv:1904.09322 [cs.LO] .
[7] Nicolas Behr & Jean Krivine (2020): Rewriting theory for the life sciences: A unifying framework for CTMC semantics. In: Graph Transformation (ICGT 2020), LNCS 12150, Springer International Publishing, pp. 185-202, doi:10.1007/978-3-030-51372-6 11. · Zbl 1502.68146 · doi:10.1007/978-3-030-51372-6_11
[8] Nicolas Behr & Pawel Sobocinski (2018): Rule Algebras for Adhesive Categories. In: 27th EACSL Annual Conference on Computer Science Logic (CSL 2018), LIPIcs 119, Schloss Dagstuhl-Leibniz-Zentrum für Informatik, pp. 11:1-11:21, doi:10.4230/LIPIcs.CSL.2018.11. · Zbl 1528.68154 · doi:10.4230/LIPIcs.CSL.2018.11
[9] Nicolas Behr & Pawel Sobocinski (2020): Rule Algebras for Adhesive Categories. Logical Methods in Computer Science Volume 16, Issue 3. Available at https://lmcs.episciences.org/6615. · Zbl 1444.68083
[10] Gil Benkö, Christoph Flamm & Peter F. Stadler (2003): A Graph-Based Toy Model of Chemistry. J. Chem. Inf. Comput. Sci. 43(4), pp. 1085-1093, doi:10.1021/ci0200570. · doi:10.1021/ci0200570
[11] Nikolaj Bjørner, Leonardo de Moura, Lev Nachmanson & Christoph M. Wintersteiger (2019): Program-ming Z3. In: Engineering Trustworthy Software Systems, Springer International Publishing, pp. 148-201, doi:10.1007/978-3-030-17601-3 4. · doi:10.1007/978-3-030-17601-3_4
[12] Pierre Boutillier, Mutaamba Maasha, Xing Li, Héctor F Medina-Abarca, Jean Krivine, Jérôme Feret, Ioana Cristescu, Angus G Forbes & Walter Fontana (2018): The Kappa platform for rule-based modeling. Bioin-formatics 34(13), pp. i583-i592, doi:10.1093/bioinformatics/bty272. · doi:10.1093/bioinformatics/bty272
[13] Harrie Jan Sander Bruggink (2015): Grez user manual. Available at http://www.ti.inf.uni-due.de/research/ tools/grez/.
[14] Andrea Corradini, Tobias Heindel, Frank Hermann & Barbara König (2006): Sesqui-Pushout Rewrit-ing. In: Graph Transformations (ICGT 2006), LNCS 4178, Springer Berlin Heidelberg, pp. 30-45, doi:10.1007/11841883 4. · Zbl 1156.68423 · doi:10.1007/11841883_4
[15] Andrea Corradini, Barbara König & Dennis Nolte (2017): Specifying Graph Languages with Type Graphs. In: Graph Transformation (ICGT 2017), LNCS 10373, Springer International Publishing, pp. 73-89, doi:10.1007/978-3-319-61470-0 5. · Zbl 1425.68191 · doi:10.1007/978-3-319-61470-0_5
[16] Andrea Corradini, Barbara König & Dennis Nolte (2019): Specifying graph languages with type graphs. J. Log. Algebr. Methods Program. 104, pp. 176-200, doi:10.1016/j.jlamp.2019.01.005. · Zbl 1423.68248 · doi:10.1016/j.jlamp.2019.01.005
[17] Vincent Danos, Jerome Feret, Walter Fontana, Russell Harmer, Jonathan Hayman, Jean Krivine, Chris Thompson-Walsh & Glynn Winskel (2012): Graphs, Rewriting and Pathway Reconstruction for Rule-Based Models. In: Foundations of Software Technology and Theoretical Computer Sci-ence (FSTTCS 2012), LIPIcs 18, Schloss Dagstuhl-Leibniz-Zentrum für Informatik, pp. 276-288, doi:10.4230/LIPIcs.FSTTCS.2012.276. · Zbl 1354.68193 · doi:10.4230/LIPIcs.FSTTCS.2012.276
[18] Vincent Danos, Jérôme Feret, Walter Fontana, Russell Harmer & Jean Krivine (2008): Rule-Based Modelling, Symmetries, Refinements. In: Formal Methods in Systems Biology (FMSB 2008), LNCS 5054, Springer, pp. 103-122, doi:10.1007/978-3-540-68413-8 8. · Zbl 1348.92070 · doi:10.1007/978-3-540-68413-8_8
[19] Vincent Danos, Reiko Heckel & Pawel Sobocinski (2014): Transformation and Refinement of Rigid Struc-tures. In: Graph Transformation (ICGT 2014), LNCS 8571, Springer International Publishing, pp. 146-160, doi:10.1007/978-3-319-09108-2 10. · Zbl 1425.68157 · doi:10.1007/978-3-319-09108-2_10
[20] Vincent Danos & Cosimo Laneve (2004): Formal molecular biology. TCS 325(1), pp. 69-110, doi:10.1016/j.tcs.2004.03.065. · Zbl 1071.68041 · doi:10.1016/j.tcs.2004.03.065
[21] Vincent Danos & Vincent Schachter, editors (2004): Computational Methods in Systems Biology (CMSB 2004). LNCS 3082, Springer Berlin Heidelberg, doi:10.1007/b107287. · Zbl 1088.68659 · doi:10.1007/b107287
[22] Hartmut Ehrig, Ulrike Golas, Annegret Habel, Leen Lambers & Fernando Orejas (2012): M -Adhesive Trans-formation Systems with Nested Application Conditions. Part 2: Embedding, Critical Pairs and Local Conflu-ence. Fundam. Inform. 118(1-2), pp. 35-63, doi:10.3233/FI-2012-705. · Zbl 1242.68128 · doi:10.3233/FI-2012-705
[23] Hartmut Ehrig, Ulrike Golas, Annegret Habel, Leen Lambers & Fernando Orejas (2014): M -adhesive trans-formation systems with nested application conditions. Part 1: parallelism, concurrency and amalgamation. Math. Struct. Comput. Sci. 24(04), doi:10.1017/s0960129512000357. · Zbl 1342.68176 · doi:10.1017/s0960129512000357
[24] Marcus Ermler, Hans-Jörg Kreowski, Sabine Kuske & Caroline von Totth (2011): From Graph Transforma-tion Units via MiniSat to GrGen.NET. In: International Symposium on Applications of Graph Transforma-tions with Industrial Relevance, LNCS 7233, Springer, Berlin, Heidelberg, pp. 153-168, doi:10.1007/978-3-642-34176-2 14. · doi:10.1007/978-3-642-34176-2_14
[25] Philippe Flajolet & Robert Sedgewick (2009): Analytic Combinatorics. Cambridge University Press, doi:10.1017/CBO9780511801655. · Zbl 1165.05001 · doi:10.1017/CBO9780511801655
[26] Karsten Gabriel, Benjamin Braatz, Hartmut Ehrig & Ulrike Golas (2014): Finitary M -adhesive categories. Math. Struct. Comput. Sci. 24(04), doi:10.1017/S0960129512000321. · Zbl 1342.68177 · doi:10.1017/S0960129512000321
[27] Annegret Habel & Karl-Heinz Pennemann (2009): Correctness of high-level transformation systems relative to nested conditions. Math. Struct. Comput. Sci. 19(02), pp. 245-296, doi:10.1017/s0960129508007202. · Zbl 1168.68022 · doi:10.1017/s0960129508007202
[28] Russ Harmer, Vincent Danos, Jérôme Feret, Jean Krivine & Walter Fontana (2010): Intrinsic information carriers in combinatorial dynamical systems. Chaos: An Interdisciplinary Journal of Nonlinear Science 20(3), p. 037108, doi:10.1063/1.3491100. · Zbl 1311.92202 · doi:10.1063/1.3491100
[29] Reiko Heckel, Andrea Corradini, Hartmut Ehrig & Michael Löwe (1996): Horizontal and Vertical Structuring of Typed Graph Transformation Systems. Math. Struct. Comput. Sci. 6(6), pp. 613-648, doi:10.1017/S0960129500070110. · Zbl 0866.68056 · doi:10.1017/S0960129500070110
[30] Reiko Heckel, Jochen Malte Küster & Gabriele Taentzer (2002): Confluence of Typed Attributed Graph Transformation Systems. In: Graph Transformation (ICGT 2002), LNCS 2505, Springer, pp. 161-176, doi:10.1007/3-540-45832-8 14. · Zbl 1028.68031 · doi:10.1007/3-540-45832-8_14
[31] Reiko Heckel, Leen Lambers & Maryam Ghaffari Saadat (2019): Analysis of Graph Transformation Systems: Native vs Translation-based Techniques. In: Workshop on Graph Computation (GCM 2019), EPTCS 309, Open Publishing Association, pp. 1-22, doi:10.4204/EPTCS.309.1. · Zbl 07453086 · doi:10.4204/EPTCS.309.1
[32] Tobias Isenberg, Dominik Steenken & Heike Wehrheim (2013): Bounded Model Checking of Graph Trans-formation Systems via SMT Solving. In: Formal Techniques for Distributed Systems (FMOODS/FORTE 2013), LNCS 7892, Springer, Berlin, Heidelberg, pp. 178-192, doi:10.1007/978-3-642-38592-6 13. · doi:10.1007/978-3-642-38592-6_13
[33] Hans-Jörg Kreowski, Sabine Kuske & Robert Wille (2010): Graph transformation units guided by a SAT solver. In: Graph Transformations (ICGT 2010), LNCS 6372, Springer, Berlin, Heidelberg, pp. 27-42, doi:10.1007/978-3-642-15928-2 3. · Zbl 1306.68080 · doi:10.1007/978-3-642-15928-2_3
[34] Stephen Lack & Paweł Sobociński (2005): Adhesive and quasiadhesive categories. RAIRO -Theoretical Informatics and Applications 39(3), pp. 511-545, doi:10.1051/ita:2005028. · Zbl 1078.18010 · doi:10.1051/ita:2005028
[35] Leen Lambers, Daniel Strüber, Gabriele Taentzer, Kristopher Born & Jevgenij Huebert (2018): Multi-granular conflict and dependency analysis in software engineering based on graph transfor-mation. In: International Conference on Software Engineering (ICSE 2018), ACM, pp. 716-727, doi:10.1145/3180155.3180258. · doi:10.1145/3180155.3180258
[36] Tihamer Levendovszky, Ulrike Prange & Hartmut Ehrig (2007): Termination Criteria for DPO Transformations with Injective Matches. Electron. Notes Theor. Comput. Sci. 175(4), pp. 87-100, doi:10.1016/j.entcs.2007.04.019. · Zbl 1278.68123 · doi:10.1016/j.entcs.2007.04.019
[37] Leonardo de Moura & Nikolaj Bjørner (2008): Z3: An Efficient SMT Solver. In: Tools and Algorithms for the Construction and Analysis of Systems, Springer Berlin Heidelberg, pp. 337-340, doi:10.1007/978-3-540-78800-3 24. · doi:10.1007/978-3-540-78800-3_24
[38] Nebras Nassar, Jens Kosiol, Thorsten Arendt & Gabriele Taentzer (2019): Constructing Optimized Validity-Preserving Application Conditions for Graph Transformation Rules. In: Graph Transformation (ICGT 2019), LNCS 11629, Springer, pp. 177-194, doi:10.1007/978-3-030-23611-3 11. · Zbl 1429.68092 · doi:10.1007/978-3-030-23611-3_11
[39] Guilherme Rangel, Leen Lambers, Barbara König, Hartmut Ehrig & Paolo Baldan (2008): Behavior Preser-vation in Model Refactoring Using DPO Transformations with Borrowed Contexts. In: Graph Transforma-tions (ICGT 2008), LNCS 5214, Springer, pp. 242-256, doi:10.1007/978-3-540-87405-8 17. · Zbl 1175.68231 · doi:10.1007/978-3-540-87405-8_17
[40] Dominik Steenken (2015): Verification of infinite-state graph transformation systems via abstraction. Ph.D. thesis, University of Paderborn. Available at https://digital.ub.uni-paderborn.de/ubpb/urn/urn:nbn:de:hbz: 466:2-15768.
[41] Dominik Steenken, Heike Wehrheim & Daniel Wonisch (2011): Sound and complete abstract graph trans-formation. In: Brazilian Symposium on Formal Methods, Springer, pp. 92-107, doi:10.1007/978-3-642-25032-3 7. · Zbl 1349.68106 · doi:10.1007/978-3-642-25032-3_7
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.