Efficient Computation of Graph Overlaps for Rule Composition: Theory and Z3 Prototyping

Nicolas Behr
(Université de Paris, France)
Reiko Heckel
(University of Leicester, UK)
Maryam Ghaffari Saadat
(University of Leicester, UK)

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.

In Berthold Hoffmann and Mark Minas: Proceedings of the Eleventh International Workshop on Graph Computation Models (GCM 2020), Online-Workshop, 24th June 2020, Electronic Proceedings in Theoretical Computer Science 330, pp. 126–144.
Published: 3rd December 2020.

ArXived at: http://dx.doi.org/10.4204/EPTCS.330.8 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org