Commutators for Stochastic Rewriting Systems: Theory and Implementation in Z3.

In the semantics of stochastic rewriting systems (SRSs) based on rule algebras, the evolution equations for average expected pattern counts are computed via so-called commutators counting the distinct sequential compositions of rules and observable patterns regarded as identity rules. In this paper, we consider the commutators for conditional SRS in the Sesqui-Pushout (SqPO) approach. However, graphs are often subject to constraints. To minimise the construction of spurious compositions prohibited by such constraints, we develop strategies for computing rule composition, both theoretically and using the SMT solver Z3 with its Python interface. Our two equivalent solutions for checking constraints include a straightforward generate-and-test approach based on forbidden graph patterns and a modular solution, where the patterns are decomposed as pushouts of monic spans into forbidden relation patterns. The implementation is based on a framework that allows a direct and modular representation of the categorical and logical theory in Python/Z3. For an example of SqPO rewriting of rigid multigraphs modelling polymer formation in organic chemistry, we assess and compare the performance of the two strategies.