Commutators for Stochastic Rewriting Systems: Theory and Implementation in Z3
Commutators for Stochastic Rewriting Systems: Theory and Implementation in Z3
复制标题
随机重写系统的换向器：Z3 中的理论与实现
DOI：
--
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
R. Heckel
中科院分区：
文献类型：
--
作者：
Nicolas Behr;Maryam Ghaffari Saadat;R. Heckel
在基于规则代数的随机重写系统（SRS）语义中，平均期望模式数的演化方程是通过对规则和可观察模式的不同序列组合进行计数的所谓的计数器来计算的.在本文中，我们考虑条件SRS的Sesqui-Pushout（SqPO）方法的分解器。然而，图常常受到约束。为了最大限度地减少这种约束所禁止的虚假组合物的建设，我们制定了计算规则组合物的策略，无论是理论上还是使用SMT求解器Z3与Python接口。我们的两个等价的解决方案检查约束包括一个简单的生成和测试方法的基础上禁止的图形模式和模块化的解决方案，其中的模式被分解为推出的monic跨度到禁止的关系模式。该实现基于一个框架，该框架允许在Python/Z3中直接和模块化地表示分类和逻辑理论。对于一个例子的SqPO重写刚性多重图建模聚合物形成在有机化学中，我们评估和比较这两种策略的性能。
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.