Advertisement

Rewriting Theory for the Life Sciences: A Unifying Theory of CTMC Semantics

  • Nicolas BehrEmail author
  • Jean Krivine
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 12150)

Abstract

The Kappa biochemistry and the MØD organo-chemistry frameworks are amongst the most intensely developed applications of rewriting theoretical methods in the life sciences to date. A typical feature of these types of rewriting theories is the necessity to implement certain structural constraints on the objects to be rewritten (a protein is empirically found to have a certain signature of sites, a carbon atom can form at most four bonds, ...). In this paper, we contribute to the theoretical foundations of these types of rewriting theory a number of conceptual and technical developments that permit to implement a universal theory of continuous-time Markov chains (CTMCs) for stochastic rewriting systems. Our core mathematical concepts are a novel rule algebra construction for the relevant setting of rewriting rules with conditions, both in Double- and in Sesqui-Pushout semantics, augmented by a suitable stochastic mechanics formalism extension that permits to derive dynamical evolution equations for pattern-counting statistics.

Keywords

Double-pushout rewriting Sesqui-pushout rewriting Rule algebra Stochastic mechanics Biochemistry Organic chemistry 

1 Motivation

One of the key applications that rewriting theory may be considered for in the life sciences is the theory of continuous-time Markov chains (CTMCs) modeling complex systems. In fact, since Delbrück’s seminal work on autocatalytic reaction systems in the 1940s [20], the mathematical theory of chemical reaction systems has effectively been formulated as a rewriting theory in disguise, namely via the rule algebra of discrete graph rewriting [11]. In the present paper, we provide the necessary technical constructions in order to consider the CTMCs and analysis methods of relevance for more general types of compositional rewriting theories with conditions, with key examples provided in the form of biochemical graph rewriting in the sense of the Kappa framework (https://kappalanguage.org) [12], and (organo-) chemical graph rewriting in the sense of the MØD framework (https://cheminf.imada.sdu.dk/mod/) [1]. The present paper aims to serve two main purposes: the first consists in providing an extension of the existing category-theoretical rule-algebra frameworks [4, 10, 11] by the rewriting theoretical design feature of incorporating rules with conditions as well as constraints on objects (Sect. 3). Based upon these technical developments, we then investigate to which extent it is possible to utilize the rule-algebraic stochastic mechanics frameworks of the relevant types (Sect. 4) in order to compute evolution equations for the moments of pattern-count observables within the Kappa and MØD frameworks (Sect. 5 and 6).

2 Compositional Rewriting Theories with Conditions

The well-established Double-Pushout (DPO) [21] and Sesqui-Pushout (SqPO) [13] frameworks for rewriting systems over categories with suitable adhesivity properties [23, 24, 26, 30] provide a principled and very general foundation for rewriting theories. In practice, many applications require the rewriting of objects that are not part of an adhesive category themselves, but which may be obtained from a suitable “ambient” category via the notion of conditions on objects. Together with a corresponding notion of constraints on rewriting rules, this yields a versatile extension of rewriting theory. In the DPO setting, this modification had been well-known [21, 22, 23, 27], while it has been only very recently introduced for the SqPO setting [8]. For the rule algebra constructions presented in the main part of this contribution, we require in addition a certain compositionality property of our rewriting theories (established for the DPO case in [10, 11], for the SqPO case in [4], and for both settings augmented with conditions in [8]).

2.1 Category-Theoretical Prerequisites

Throughout this paper, we will make the following assumptions1:

Assumption 1

 Open image in new window is a finitary Open image in new window-adhesive category with Open image in new window-initial object, Open image in new window-effective unions and epi-Open image in new window-factorization. In the setting of Sesqui-Pushout (SqPO) rewriting, we assume in addition that all final pullback complements (FPCs) along composable pairs of Open image in new window-morphisms exist, and that Open image in new window-morphisms are stable under FPCs.

Both of the main application examples presented within this paper rely upon typed variants of undirected multigraphs.

Definition 1

Let Open image in new window be the restricted powerset functor (mapping a set S to the set of its subsets \(P\subset S\) with \(1\le |P|\le 2\)). The category \(\mathbf {uGraph}\) [11] of finite undirected multigraphs is defined as the finitary restriction of the comma category Open image in new window. Thus an undirected multigraph is specified as \(G=(E_G,V_G,i_G)\), where \(E_G\) and \(V_G\) are (finite) sets of edges and vertices, respectively, and where Open image in new window is the edge-incidence map.

Theorem 1

\(\mathbf {uGraph}\) satisfies Assumption 1, both for the DPO- and for the extended SqPO-variant.

Proof

As demonstrated in [11], \(\mathbf {uGraph}\) is indeed a finitary Open image in new window-adhesive category with Open image in new window-initial object and Open image in new window-effective unions, for Open image in new window the class of component-wise monic \(\mathbf {uGraph}\)-morphisms. It thus remains to prove the existence of an epi-Open image in new window-factorization as well as the properties related to FPCs. To this end, utilizing the fact that the category \(\mathbf {Set}\) upon which the comma category \(\mathbf {uGraph}\) is based possesses an epi-mono-factorization, we may construct the following diagram from a \(\mathbf {uGraph}\)-morphism Open image in new window (for component morphisms \(\varphi _E:E\rightarrow E'\) and \(\varphi _V:V\rightarrow V'\)):The diagram is constructed as follows:
  1. 1.

    Perform the epi-mono-factorizations \(\varphi _E=m_E\circ e_E\) and \(\varphi _V=m_V\circ e_V\), and apply the functor Open image in new window in order to obtain the morphisms Open image in new window and Open image in new window; since the functor Open image in new window preserves monomorphisms [31], Open image in new window.

     
  2. 2.
    Construct the pullback Since monomorphisms are stable under pullback in \(\mathbf {Set}\), having proved that Open image in new window implies Open image in new window.
     
  3. 3.

    By the universal property of pullbacks, there exists a morphism Open image in new window. Let Open image in new window be the epi-mono-factorization of this morphism.

     
  4. 4.

    By stability of monomorphisms under composition in \(\mathbf {Set}\), we find that Open image in new window, and consequently Open image in new window yields an alternative epi-mono-factorization of \(\varphi _E\). Then by uniqueness of epi-mono-factorizations up to isomorphism, there must exist an isomorphism Open image in new window.

     
We have thus demonstrated that both Open image in new window and Open image in new window are morphisms in \(\mathbf {uGraph}\). Since morphisms in comma categories are mono-, epi- or iso-morphisms if they are so componentwise [21], we conclude thatwhich finally entails that we have explicitly constructed an epi-mono-factorization of the \(\mathbf {uGraph}\)-morphism Open image in new window.
In order to demonstrate that FPCs along pairs of composable Open image in new window-morphisms Open image in new window in \(\mathbf {uGraph}\) exist (for Open image in new window the class of component-wise monomomophic \(\mathbf {uGraph}\) morphisms), we provide the following explicit construction:

2.2 Conditions

Referring to [9, Appendix A.2] for further details and technical definitions, we will utilize as a notational convention the standard shorthand notations
$$\begin{aligned} \exists (X\hookrightarrow Y):=\exists (X\hookrightarrow Y,\mathsf {true}_Y),\quad \forall (X\hookrightarrow Y,\mathsf {c}_Y):=\lnot \exists (X\hookrightarrow Y,\lnot \mathsf {c}_Y). \end{aligned}$$
(3)
For example, the constraints
express for a given object Open image in new window that Z contains at least two vertices (if \(Z\vDash \mathsf {c}_{\mathop {\varnothing }}^{(1)}\)), that Z does not contain parallel pairs of directed edges (if \(Z\vDash \mathsf {c}_{\mathop {\varnothing }}^{(2)}\)), and that for every directed edge in Z there also exists a directed edge between the same endpoints with opposite direction (if \(Z\vDash \mathsf {c}_{\mathop {\varnothing }}^{(3)}\)), respectively.

2.3 Compositional Rewriting with Conditions

Throughout this section, we assume that we are given a type Open image in new window of rewriting semantics and an Open image in new window-adhesive category Open image in new window satisfying the respective variant of Assumption 1. In categorical rewriting theories, the universal constructions utilized such as pushouts, pullbacks, pushout complements and final pullback complements are unique only up to universal isomorphisms. This motivates specifying a suitable notion of equivalence classes of rules with conditions:

Definition 2

(Rules with conditions). Let Open image in new window denote the class of (linear) rules with conditions, defined asWe define two rules with conditions \(R_j=(r_j,\mathsf {c}_{I_j})\) (\(j=1,2\)) equivalent, denoted \(R_2\sim R_1\), iff \(\mathsf {c}_{I_1}\equiv \mathsf {c}_{I_2}\) and if there exist isomorphisms Open image in new window such that the diagram on the right commutes. We denote by Open image in new window the set of equivalence classes under \(\sim \) of rules with conditions.

Definition 3

(Direct derivations). Let Open image in new window and Open image in new window be concrete representatives of some equivalence class Open image in new window, and let Open image in new window be objects. Then a type Open image in new window direct derivation is defined as a commutative diagram such as below right, where all morphism are in Open image in new window (and with the left representation a shorthand notation)with the following pieces of information required relative to the type:
  1. 1.

    Open image in new window: given Open image in new window, m is a DPO-admissible match of R into X, denoted Open image in new window, if \(m\vDash \mathsf {c}_I\) and (A) is constructable as a pushout complement, in which case (B) is constructed as a pushout.

     
  2. 2.

    Open image in new window: given Open image in new window, m is a SqPO-admissible match of R into X, denoted Open image in new window, if \(m\vDash \mathsf {c}_I\), in which case (A) is constructed as a final pullback complement and (B) as a pushout.

     
  3. 3.

    Open image in new window: given just the “plain rule” r and Open image in new window, \(m^{*}\) is a DPO\({}^{\dag }\)-admissible match of r into X, denoted Open image in new window, if (B) is constructable as a pushout complement, in which case (B) is constructed as a pushout.

     

For types Open image in new window, we will sometimes employ the notation \(R_m(X)\) for the object Y.

Note that at this point, we have not yet resolved a conceptual issue that arises from the non-uniqueness of a direct derivation given a rule and an admissible match. Concretely, the pushout complement, pushout and FPC constructions are only unique up to isomorphisms. This issue will ultimately be resolved as part of the rule algebraic theory. We next consider a certain composition operation on rules with conditions that is quintessential to our main constructions:

Definition 4

(Rule compositions). Let Open image in new window be two equivalence classes of rules with conditions, and let Open image in new window and \(\mathsf {c}_{I_j}\) be concrete representatives of \(R_j\) (for \(j=1,2\)). For Open image in new window, an Open image in new window-span \(\mu =(I_2\hookleftarrow M_{21}\hookrightarrow O_1)\) (i.e. with Open image in new window) is a Open image in new window -admissible match of \(R_2\) into \(R_1\) if the diagram below is constructable (with \(N_{21}\) constructed by taking pushout)and if Open image in new window. Here, the condition \(\mathsf {c}_{I_{21}}\) is computed as
$$\begin{aligned} \mathsf {c}_{I_{21}}:=\mathsf {Shift}(I_1\hookrightarrow I_{21},\mathsf {c}_{I_1})\;\wedge \; \mathsf {Trans}(N_{21}\leftharpoonup I_{21},\mathsf {Shift}(I_2\hookrightarrow N_{21},\mathsf {c}_{I_2})). \end{aligned}$$
(8)
In this case, we define the type Open image in new window composition of \(R_2\) with \(R_1\) along \(\mu \), denoted Open image in new window, aswhere \((O_{21}\leftharpoonup I_{21}):=(O_{21}\leftharpoonup N_{21})\circ (N_{21}\leftharpoonup I_{21})\) (with \(\circ \) the span composition operation).

We refer the interested readers to [9, Appendix A.3] for a summary of the relevant technical results on two variants of concurrency theorems following [8] (where the DPO-type concurrency theorem is of course classical, cf. e.g. [21]).

3 Rule Algebras for Compositional Rewriting with Conditions

The associativity property of rule compositions in both DPO- and SqPO-type semantics for rewriting with conditions as proved in [8] may be fruitfully exploited within rule algebra theory. One possibility to encode the non-determinism in sequential applications of rules to objects is given by lifting each possible configuration Open image in new window (i.e. isomorphism class of objects) to a basis vector \(\left| X\right\rangle \) of a vector space Open image in new window; then a rule r is lifted to a linear operator acting on Open image in new window, with the idea that this operator acting upon a basis vector \(\left| X\right\rangle \) should evaluate to the “sum over all possibilities to act with r on X”. We will extend here the general rule algebra framework [4, 6, 10] to the present setting of rewriting rules with conditions.

We will first lift the notion of rule composition into the setting of a composition operation on a certain abstract vector space over rules, thus realizing the heuristic concept of “summing over all possibilities to compose rules”.

Definition 5

Let Open image in new window be the rewriting type, and let Open image in new window be a category satisfying the relevant variant of Assumption 1. Let Open image in new window be an Open image in new window-vector space, defined via a bijection Open image in new window from the set of equivalence classes of linear rules with conditions to the set of basis vectors of Open image in new window. Let Open image in new window denote the type Open image in new window rule algebra product, a binary operation defined via its action on basis elements Open image in new window (for Open image in new window) asWe refer to Open image in new window as the Open image in new window -type rule algebra over Open image in new window.

Theorem 2

For type Open image in new window over a category Open image in new window satisfying Assumption 1, the rule algebra Open image in new window is an associative unital algebra, with unit element \(\delta (R_{\mathop {\varnothing }})\), where \(R_{\mathop {\varnothing }}:=(\mathop {\varnothing }\hookleftarrow \mathop {\varnothing }\hookrightarrow \mathop {\varnothing };\mathsf {true})\).

Proof

Associativity follows from [9, Theorem 7], while unitality, i.e. thatfollows directly from an explicit computation of the relevant rule compositions.

As alluded to in the introduction, the prototypical example of rule algebras are those of DPO- or (in this case equivalently) SqPO-type over discrete graphs, giving rise as a special case to the famous Heisenberg-Weyl algebra of key importance in mathematical chemistry, combinatorics and quantum physics (see [11] for further details). We will now illustrate the rule algebra concept in an example involving a more general base category.

Example 1

For the category \(\mathbf {uGraph}\) and DPO-type rewriting semantics, consider as an example the following two rules with conditions:The first rule is a typical example of a rule with application conditions, i.e. here stating that the rule may only link two vertices if they were previously not already linked to each other. The second rule, owing to DPO semantics, can in effect only be applied to vertices without any incident edges. The utility of the rule-algebraic composition operation then consists in reasoning about sequential compositions of these rules, for example (letting \(*:= \star _{DPO}{}\)):To provide some intuition: the first computation encodes the causal information that the two rules may either be composed along a trivial overlap, or rule \(R_C\) may overlap on one of the vertices in the output of \(R_V\); in the latter case, any vertex to which first \(R_V\) and then \(R_C\) applies must not have had any incident edges, i.e. in particular no edge violating the constraint of \(R_C\), which is why the composite rule \(R_C'\) does not feature any non-trivial constraint. In the other order of composition, the two vertices in the output of \(R_C\) are linked by an edge, so \(R_V\) cannot be applied to any of these two vertices (leaving just the trivial overlap contribution).

Just as the rule algebra construction encodes the compositional associativity property of rule compositions, the following representation construction encodes in a certain sense the properties described by the concurrency theorem:

Definition 6

Let Open image in new window be an Open image in new window-adhesive category satisfying Assumption 1. Let Open image in new window be defined as the Open image in new window -vector space whose set of basis vectors is isomorphic to the set2 of iso-classes of objects of Open image in new window via a bijection Open image in new window. Then the Open image in new window -type canonical representation of the Open image in new window -type rule algebra over Open image in new window, denoted Open image in new window, is defined as the morphism Open image in new window specified via

Theorem 3

Open image in new window as defined above is an algebra homomorphism (and thus in particular a well defined representation).

Proof

The proof that we provide in [9, Appendix B.1] is entirely analogous to the one for the case without application conditions [4, 10].

4 Stochastic Mechanics Formalism

Referring to [6, 7, 11] for further details and derivations, suffice it here to highlight the key role played by the algebraic concept of commutators in stochastic mechanics. Let us first provide the constructions of continuous-time Markov chains (CTMCs) and observables in stochastic rewriting systems.

Definition 7

Let Open image in new window (referred to as dual projection vector) be defined via its action on basis vectors of Open image in new window as Open image in new window.

Theorem 4

Let Open image in new window be a category satisfying the relevant variant of Assumption 1, and let Open image in new window be the Open image in new window-type rule algebra of linear rules with conditions over Open image in new window. Let Open image in new window denote the Open image in new window-type canonical representation of Open image in new window. Then the following results hold:
  1. 1.
    The basis elements of the space Open image in new window of Open image in new window -type observables, i.e. the diagonal linear operators that arise as (linear combinations of) Open image in new window-type canonical representations of rewriting rules with conditions, have the following structure (Open image in new window in the DPO case, Open image in new window in the SqPO case):
     
  2. 2.
    DPO-type jump closure property: for every linear rule with condition Open image in new window, we find that where Open image in new window is the homomorphism defined via its action on basis elements \(\delta (R)\) for Open image in new window as
     
  3. 3.
    SqPO-type jump closure property: for every linear rule with condition Open image in new window, we find that where3 Open image in new window is the homomorphism defined via
     
  4. 4.
    CTMCs via stochastic rewriting systems: Let Open image in new window be the space of (sub-)probability distributions over Open image in new window (i.e. Open image in new window). Let Open image in new window be a collection of N pairs of positive real-valued parameters \(\kappa _j\) (referred to as base rates) and linear rules \(R_j\) with application conditions, Then given an initial state Open image in new window, the Open image in new window-type stochastic rewriting system based upon the transitions Open image in new window gives rise to the CTMC Open image in new window with time-dependent state Open image in new window (for \(t\ge 0\)) and evolution equation Here, the infinitesimal generator Open image in new window of the CTMC is given by
     

Proof

See [9, Appendix B.2].

Remark 1

The operation Open image in new window featuring in the DPO- and SqPO-type jump-closure properties has a very intuitive interpretation: given a linear rule with condition Open image in new window, the linear operator Open image in new window is an observable that evaluates on a basis vector Open image in new window as Open image in new window = (# of ways to apply R to X)Open image in new window.

As for the concrete computational techniques offered by the stochastic mechanics formalism, one of the key advantages of this rule-algebraic framework is the possibility to reason about expectation values (and higher moments) of pattern-count observables in a principled and universal manner. The precise formulation is given by the following generalization of results from [7] to the setting of DPO- and SqPO-type rewriting for rules with conditions:

Theorem 5

Given a CTMC Open image in new window with time-dependent state Open image in new window (for \(t\ge 0\)), a set of observables Open image in new window and n formal variables \(\lambda _1,\dotsc ,\lambda _n\), define the exponential moment-generating function (EMGF) \(M(t;\underline{\lambda })\) asThen \(M(t;\underline{\lambda })\) satisfies the following formal evolution equation (for \(t\ge 0\)):

Proof

In full analogy to the case of rules without conditions [7], the proof follows from the BCH formula \(e^{\lambda A}Be^{-\lambda A}=e^{ ad_{\lambda A}}(B)\) (for Open image in new window). Here, \(ad_A^{\circ 0}(B):=B\), \(ad_A(B):=AB-BA\) (also referred to as the commutator [AB] of A and B), and \(ad_A^{\circ (q+1)}(B):=ad_A(ad_A^{\circ q}(B))\) for \(q\ge 1\). Finally, the \(q=0\) term in the above expression evaluates identically to 0 due to Open image in new window.

Combining this theorem with the notion of Open image in new window-type jump-closure, one can in favorable cases express the EMGF evolution equation as a PDE on formal power series in \(\lambda _1,\dotsc ,\lambda _n\) and with t-dependent real-valued coefficients. Referring the interested readers to [7] for further details on this technique, let us provide here a simple non-trivial example of such a calculation.

Example 2

Let us consider a stochastic rewriting system over the category Open image in new window of finite undirected multigraphs, with objects further constrained by the structure constraint Open image in new window that prohibits multiedges. Let us consider for type Open image in new window the four rules with conditions \(R_{E_{\pm }}\) (edge-creation/-deletion) and \(R_{V_{\pm }}\) (vertex creation/deletion), defined as

Here, the prefactors \(\tfrac{1}{2}\) for \(R_{E_{\pm }}\) are chosen purely for convenience. Note that \(R_{E_{+}}\) is the only rule requiring a non-trivial application condition, since linking two vertices with an edge might create a multiedge (precisely when the two vertices were already linked). Introducing base rates Open image in new window and letting Open image in new window, we may assemble the infinitesimal generator Open image in new window of a CTMC asOne might now ask whether there is any interesting dynamical structure e.g. in the evolution of the moments of the observables that count the number of times each of the transitions of this system is applicable,The algebraic data necessary in order to formulate EMGF evolution equations are all commutators of the observables with the contributions Open image in new window to the “off-diagonal part” Open image in new window of the infinitesimal generator Open image in new window. We will present here for brevity just those commutators necessary in order to compute the evolution equations for the averages of the three observables:
$$\begin{aligned} \begin{aligned}{}[O_{\bullet },\hat{V}_{\pm }]&=\pm \hat{V}_{\pm },\;&[O_{\bullet },\hat{E}_{\pm }]&=0&\\ [O_{\bullet \vert \bullet },\hat{V}_{+}]&= \hat{A},&[O_{\bullet \vert \bullet },\hat{V}_{-}]&= -\hat{B},\;&[O_{\bullet \vert \bullet },\hat{E}_{\pm }]&= \mp \hat{E}_{\pm }\\ [O_{\bullet \!-\! \bullet },\hat{V}_{+}]&=0,&[O_{\bullet \!-\! \bullet },\hat{V}_{-}]&= -\hat{C},\;&[O_{\bullet \!-\! \bullet },\hat{E}_{\pm }]&= \pm \hat{E}_{\pm } \end{aligned} \end{aligned}$$
(26)
As typical in these types of commutator computations, we find a number of contributions (here \(\hat{A}\), \(\hat{B}\) and \(\hat{C}\)) that were not either observables or based upon rules of the SRS:
Picking for simplicity as an initial state Open image in new window just the empty graph, and invoking the SqPO-type jump-closure property (cf. Theorem 4) repeatedly in order to evaluate Open image in new window, the moment EGF evolution equation (23) specializes to the following “Ehrenfest-like” [7] ODE system:
$$\begin{aligned} \begin{aligned} \tfrac{d}{dt}\langle O_{\bullet }\rangle (t)&=\langle [O_{\bullet },H]\rangle (t)=\nu _{+}-\nu _{-}\langle O_{\bullet }\rangle (t)\\ \tfrac{d}{dt}\langle O_{\bullet \vert \bullet }\rangle (t)&=\langle [O_{\bullet \vert \bullet },H]\rangle (t) =\nu _{+}\langle O_{\bullet }\rangle (t) -(2\nu _{-}+\varepsilon _{+})\langle O_{\bullet \vert \bullet }\rangle (t) +\varepsilon _{-}\langle O_{\bullet \!-\!\bullet }\rangle (t)\\ \tfrac{d}{dt}\langle O_{\bullet \!-\!\bullet }\rangle (t)&=\langle [\langle O_{\bullet \!-\!\bullet }\rangle (t),H]\rangle (t) =\varepsilon _{+}\langle O_{\bullet \vert \bullet }\rangle (t) -(2\nu _{-}+\varepsilon _{-})\langle O_{\bullet \!-\!\bullet }\rangle (t)\\ \langle O_{\bullet }\rangle (0)&=\langle O_{\bullet \vert \bullet }\rangle (t)=\langle O_{\bullet \!-\!\bullet }\rangle (t)=0. \end{aligned} \end{aligned}$$
This ODE system may be solved exactly (see [9, Appendix C]). We depict in Fig. 1 two exemplary evolutions of the three average pattern counts for different choices of parameters. Since due to SqPO-semantics the vertex deletion and creation transitions are entirely independent of the edge creation and deletion transitions, the vertex counts stabilize on a Poisson distribution of parameter \(\nu _{+}/\nu _{-}\) (where we only present the average vertex count value here). As for the non-linked vertex pair and edge patter counts, the precise average values are sensitive to the parameter choices (i.e. whether or not vertices tend to be linked by an edge or not may be freely tuned in this model via adjusting the parameters).
Fig. 1.

Time-evolutions of pattern count observables for different parameter choices.

While the example presented was chosen mainly to illustrate the computational techniques, it highlights the typical feature of the emergence of contributions in the relevant (nested) commutator calculations that may not have been included in the non-diagonal part \(\hat{H}\) of the infinitesimal generator of the CTMC. We refer the interested readers to [7] for an extended discussion of this phenomenon, and for computation strategies for higher-order moment evolution equations.

5 Application Scenario 1: Biochemistry with Kappa

The Kappa platform [18, 19] for rule-based modeling of biochemical reaction systems is based upon the notion of so-called site-graphs that abstract proteins and other complex macro-molecules into agents (with sites representing interaction capacities of the molecules). This open source platform offers a variety of high-performance simulation algorithms (for CTMCs based upon Kappa rewriting rules) as well as several variants of static analysis tools to analyze and verify biochemical models [12]. In view of the present paper, it is interesting to note that since the start of the Kappa development, the simulation-based algorithms have been augmented by differential semantics modules aimed at deriving ODE systems for the evolution of pattern-count observable average values [14, 15, 17, 29]. In this section, we will experiment with a (re-)encoding of Kappa in terms of typed undirected graphs with certain structural constraints that permits to express such moment statistics ODEs via our general rule-algebraic stochastic mechanics formalism. We will then provide an illustrative exemplary computation of ODEs in order to point out certain intrinsic intricacies (notably non-closure properties) typical of such calculations. One of the key theoretical features of Kappa is its foundation upon the notion of rigidity [16]. In practice, the construction involves an ambient category Open image in new window (which possesses suitable adhesivity properties), a pattern category Open image in new window (obtained from Open image in new window via certain negative constraints) and finally a state category Open image in new window (obtained from Open image in new window via additional positive constraints). We will now present one possible realization of Kappa based upon the Open image in new window-adhesive category of typed undirected multigraphs:

Definition 8

For a Kappa model K, let Open image in new window be the category of finite undirected multigraphs typed over \(T_K\), where \(T_K\) distinguishes agent vertex types, site vertex types and three forms of edge types: agent-site, site-site and loops on sites. For each agent type vertex \(X\in \{A,B,\ldots \}\), the type graph contains the site type vertices \(x_1:X,\dotsc ,x_{n_X}:X\) (incident to the X-type vertex via an edge, and where \(n_X<\infty \)). \(T_K\) also contains link type edges between sites that encode which sites can be linked, and loops on site type vertices that represent dynamic attributes, such as the phosphorylation state of a site. Indicating the three different edge types by wavy lines (agent-site), solid lines (site-site) and dotted lines (property loops), the agent vertices with filled circles Open image in new window and the site vertices by open circles Open image in new window , and using the placeholder \(\bullet \) for a vertex and a dashed line for an edge of any type, we may introduce the negative constraints defining the pattern category Open image in new window as Open image in new window, with the set Open image in new window of “forbidden subgraphs” defined asFinally, the state category Open image in new window is obtained from Open image in new window via imposing a positive constraint Open image in new window that ensures that each agent X is linked to exactly one of each of its site vertices x : X, and if a site x : X can carry a property or alternative variants thereof, it also carries a loop that signifies one of these properties (see the example below for further details). Moreover, a given site x : X must be linked to an agent X (i.e. cannot occur in isolation).

Example 3

Consider a simple Kappa model with a type graph as below left that introduces two agent types \(\mathsf {K}\) (for “kinase”) and \(\mathsf {P}\) (for “protein”), where \(\mathsf {K}\) has a site \(k:\mathsf {K}\), and where \(\mathsf {P}\) has sites \(p_t,p_l,p_b:\mathsf {P}\). Moreover, the sites \(p_t\) and \(p_b\) can carry properties \(\mathsf {u}\) (“unphosphorylated”) and \(\mathsf {p}\) (“phosphorylated”), depicted as dotted loops in the type graph. Sites \(k:\mathsf {K}\) and \(p_l:\mathsf {P}\) can bind (as indicated by the solid line in the type graph).

As a prototypical example of a Kappa stochastic rewriting system, consider a system based upon the rewriting rules \(k_{\pm }\), \(l_{\pm }\), \(t_{\pm }\) and \(b_{\pm }\). Here, for the rule \(l_{+}\), we have indicated that it must be equipped with an application condition that ensures that the site of the \(\mathsf {K}\)-type agent and the left site of the \(\mathsf {P}\)-type agent must be free before binding. As common practice also in the standard Kappa theory, we otherwise leave in the graphical depictions those application conditions necessary to ensure consistent matches implicit as much as possible. Consider then for a concrete computational example the time-evolution of the average count of the pattern described in the identity rule \(r_{obs_P}\). As typical in Kappa rule specifications \(r_{obs_P}\) as well as several of the other rules depicted only explicitly involve patterns, but not necessarily states, since e.g. in \(r_{obs_P}\) the left site of the \(\mathsf {P}\)-type agent is not mentioned. In complete analogy to the computation presented in Example 2, let us first compute the commutators of the observable \(O_{\mathsf {K}}=\rho (\delta (r_{obs_K};\mathsf {c}_{obs_K}))\) with the operators \(\hat{X}:=\rho (\delta (r_X;\mathsf {c}_X))\):
$$\begin{aligned} \begin{aligned}{}[O_{\mathsf {K}},\hat{K}_{\pm }]&=\pm \hat{K}_{\pm },\; [O_{\mathsf {K}},\hat{L}_{\pm }]=[O_{\mathsf {K}},\hat{T}_{\pm }]=[O_{\mathsf {K}},\hat{B}_{\pm }]=0 \end{aligned} \end{aligned}$$
(28)
However, letting \(O^{(\mathsf {x},\mathsf {y})}_{P}\), \(O^{(\mathsf {x},\mathsf {y})}_{link}\) and \(O^{(\mathsf {x},\mathsf {y})}_{free}\) denote the observables for the patterns
one may easily demonstrate that even a comparatively simple observable such as \(O^{(\mathsf {p},\mathsf {p})}_{P}\) already leads to an infinite cascade of contributions to the ODEs for the averages of pattern counts. As typical in these sorts of computations, the discovery of a new pattern observable via applying SqPO-type jump-closure (Theorem 4) to the commutator contributions to \(\tfrac{d}{dt}\langle O^{(\mathsf {p},\mathsf {p})}_{P}\rangle (t)\) leads to the discovery of new pattern observables yet again, such as inIn particular the last observable \(O^{(\mathsf {u},\mathsf {p})}_{free}\) is found to lead to an infinite tower of other observables (i.e. “ODE non-closure”), starting from

This exemplary and preliminary analysis reveals that while the rule-algebraic CTMC implementation is in principle applicable to the formulation and analysis Kappa systems, further algorithmic and theoretical developments will be necessary (including possibly ideas of fragments and refinements as in [14, 15, 29]) in order to obtain a computationally useful alternative rewriting-theoretic implementation of Kappa.

6 Application Scenario 2: Organic Chemistry with MØD

The MØD platform [1] for organo-chemical reaction systems is a prominent example of a DPO-type rewriting theory of high relevance to the life sciences. From a theoretical perspective, MØD has been designed [3] as a rewriting system over so-called chemical graphs, a certain typed and undirected variant of the category \(\mathbf {PLG}\) of partially labelled directed graphs. While the latter category had been introduced in [28] as a key example of an Open image in new window-Open image in new window-adhesive category, with the motivation of permitting label-changes in rewriting rules, it was also demonstrated in loc cit. that \(\mathbf {PLG}\) is not Open image in new window-adhesive. Since moreover no concrete construction of a tentative variant \(\mathbf {uPLG}\) of \(\mathbf {PLG}\) for undirected graphs, let alone results on the possible adhesivity properties of such a category are known in the literature, we propose here an alternative and equivalent encoding of chemical graphs. We mirror the constructions of [1, 3] in that chemical graphs will be a certain typed variant of undirected graphs, with vertex types representing atom types, edge types ranging over the types \(\{\mathtt {-},\mathtt {=},\mathtt {\#},\mathtt {:}\}\) representing single, double, triple and aromatic bonds, respectively, and with the graphs being required to not contain multiedges. Inspired by the Kappa constructions in the previous section, we opt to represent properties (such as e.g. charges on atoms) as typed loop edges on vertices representing atoms, whence the change of a property (which was the main motivation in [3] for utilizing a variant of \(\mathbf {PLG}\)) may be encoded in a rewriting rule simply via deletion/creation of property-encoding loops. Unfortunately, while the heuristics presented thus far would suggest that chemical graphs in the alternative categorical setting should be just simple typed undirected graphs, the full specification of chemical graphs would also have to include additional, empirical information from the chemistry literature. Concretely, atoms such as e.g. carbon only support a limited variety of bond types and configurations of incident bonds (referred to as valencies), with additional complications such as poly-valencies possible for some types of atoms as illustrated by the following example.

Example 4

The Meisenheimer-2-3-rearrangement reaction [32] (cf. also [2]) constitutes an example4 of a reaction where polyvalence is encountered:Upon matching this rule into a chemically valid mixture, the N atom on the input of the rule will have valence 5, while on the output it will have valence 3. This type of information is evidently in no way contained in the chemical graphs alone, and must therefore be encoded in terms of suitable additional typing on the graphs and application conditions.

While thus at present no encoding of chemical graphs into a categorical framework with suitable adhesivity properties is available, we posit that it would be highly fruitful in light of the stochastic mechanics framework presented in this paper to develop such an encoding (joint work in progress with J.L. Andersen, W. Fontana and D. Merkle).

7 Conclusion and Outlook

Rewriting theories of DPO- and SqPO-type for rules with conditions over Open image in new window-adhesive categories are poised to provide a rich theoretical and algorithmic framework for modeling stochastic dynamical systems in the life sciences. The main result of the present paper consists in the introduction of a rule algebra framework that extends the pre-existing constructions [4, 6, 10] precisely via incorporating the notion of conditions. The sophisticated Kappa [12] and MØD [1] bio-/organo-chemistry platforms and related developments have posed one of the main motivations for this work. For both of these platforms, we present a first analysis and stepping stones towards bridging category-theoretical rewriting theories and stochastic mechanics computations. Especially for the organo-chemistry setting, our work motivates the development of a full encoding of (at least a reasonable fragment of) organic chemistry in terms of chemical graphs and rewriting rules thereof, which to date is still unavailable. This encoding will be beneficial also in the development of tracelet-based techniques [5], and is current work in progress.

An intriguing perspective for future developments in categorical rewriting theory consists in developing a robust and versatile methodology for the analysis of ODE systems of pattern-counting observables in stochastic rewriting systems. While the results of this paper permit to formulate dynamical evolution equations for arbitrary higher moments of such observables, in general cases (as illustrated in Sect. 5) the non-closure of the resulting ODE systems remains a fundamental technical challenge. In the Kappa literature, sophisticated conceptual and algorithmic approaches to tackle this problem have been developed such as refinements [14, 16], model reduction techniques [15] and stochastic fragments [25] (see also [7] for an extended discussion). We envision that a detailed understanding of these approaches from within the setting of categorical rewriting and of rule algebra theory could provide a very fruitful enrichment of the methodology of rewriting theory.

Footnotes

  1. 1.

    We review in Appendix A.1 of [9] (an extended version of the present paper) some of the salient background material on Open image in new window-adhesive categories and the relevant notational conventions.

  2. 2.

    We assume here that the isomorphism classes of objects of Open image in new window form a set (i.e. not a proper class).

  3. 3.

    Since in applications we will always fix the type of rewriting to either DPO or SqPO, we will use the same symbol for the jump-closure operator in both cases.

  4. 4.

    This example reaction was typeset directly via MØD (cf. [9, Appendix D]).

References

  1. 1.
    Andersen, J.L., Flamm, C., Merkle, D., Stadler, P.F.: A software package for chemically inspired graph transformation. In: Echahed, R., Minas, M. (eds.) ICGT 2016. LNCS, vol. 9761, pp. 73–88. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-40530-8_5CrossRefzbMATHGoogle Scholar
  2. 2.
    Andersen, J.L., Flamm, C., Merkle, D., Stadler, P.F.: An intermediate level of abstraction for computational systems chemistry. Philos. Trans. R. Soc. A: Math. Phys. Eng. Sci. 375(2109), 20160354 (2017).  https://doi.org/10.1098/rsta.2016.0354CrossRefGoogle Scholar
  3. 3.
    Andersen, J.L., Flamm, C., Merkle, D., Stadler, P.F.: Rule composition in graph transformation models of chemical reactions. Match 80(3), 661–704 (2018)MathSciNetGoogle Scholar
  4. 4.
    Behr, N.: Sesqui-pushout rewriting: concurrency, associativity and rule algebra framework. In: Echahed, R., Plump, D. (eds.) Proceedings of the Tenth International Workshop on Graph Computation Models (GCM 2019) in Eindhoven, The Netherlands. Electronic Proceedings in Theoretical Computer Science, vol. 309, pp. 23–52. Open Publishing Association (2019).  https://doi.org/10.4204/eptcs.309.2
  5. 5.
    Behr, N.: Tracelets and tracelet analysis of compositional rewriting systems (accepted for ACT2019 in Oxford). arXiv:1904.12829 (2019)
  6. 6.
    Behr, N., Danos, V., Garnier, I.: Stochastic mechanics of graph rewriting. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science - LICS 2016. ACM Press (2016).  https://doi.org/10.1145/2933575.2934537
  7. 7.
    Behr, N., Danos, V., Garnier, I.: Combinatorial conversion and moment bisimulation for stochastic rewriting systems. arXiv:1904.07313 (2019)
  8. 8.
    Behr, N., Krivine, J.: Compositionality of rewriting rules with conditions. arXiv:1904.09322 (2019)
  9. 9.
    Behr, N., Krivine, J.: Rewriting theory for the life sciences: a unifying theory of CTMC semantics (extended version). arXiv:2003.09395 (2020)
  10. 10.
    Behr, N., Sobocinski, P.: Rule algebras for adhesive categories. In: Ghica, D., Jung, A. (eds.) 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), vol. 119, pp. 11:1–11:21. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2018).  https://doi.org/10.4230/LIPIcs.CSL.2018.11
  11. 11.
    Behr, N., Sobocinski, P.: Rule algebras for adhesive categories (invited extended journal version). arXiv:1807.00785 (2019)
  12. 12.
    Boutillier, P., et al.: The kappa platform for rule-based modeling. Bioinformatics 34(13), i583–i592 (2018).  https://doi.org/10.1093/bioinformatics/bty272CrossRefGoogle Scholar
  13. 13.
    Corradini, A., Heindel, T., Hermann, F., König, B.: Sesqui-pushout rewriting. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) Graph Transformations. Lecture Notes in Computer Science, vol. 4178, pp. 30–45. Springer, Berlin and Heidelberg (2006)CrossRefGoogle Scholar
  14. 14.
    Danos, V., Feret, J., Fontana, W., Harmer, R., Krivine, J.: Rule-based modelling, symmetries, refinements. In: Fisher, J. (ed.) FMSB 2008. LNCS, vol. 5054, pp. 103–122. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-68413-8_8CrossRefzbMATHGoogle Scholar
  15. 15.
    Danos, V., Feret, J., Fontana, W., Harmer, R., Krivine, J.: Abstracting the differential semantics of rule-based models: exact and automated model reduction. In: 2010 25th Annual IEEE Symposium on Logic in Computer Science. IEEE (2010).  https://doi.org/10.1109/lics.2010.44
  16. 16.
    Danos, V., Heckel, R., Sobocinski, P.: Transformation and refinement of rigid structures. In: Giese, H., König, B. (eds.) ICGT 2014. LNCS, vol. 8571, pp. 146–160. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-09108-2_10CrossRefzbMATHGoogle Scholar
  17. 17.
    Danos, V., Heindel, T., Honorato-Zimmer, R., Stucki, S.: Moment semantics for reversible rule-based systems. In: Krivine, J., Stefani, J.-B. (eds.) RC 2015. LNCS, vol. 9138, pp. 3–26. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-20860-2_1CrossRefzbMATHGoogle Scholar
  18. 18.
    Danos, V., Laneve, C.: Formal molecular biology. Theoret. Comput. Sci. 325(1), 69–110 (2004).  https://doi.org/10.1016/j.tcs.2004.03.065MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Danos, V., Schachter, V. (eds.): CMSB 2004. LNCS, vol. 3082. Springer, Heidelberg (2005).  https://doi.org/10.1007/b107287CrossRefzbMATHGoogle Scholar
  20. 20.
    Delbrück, M.: Statistical fluctuations in autocatalytic reactions. J. Chem. Phys. 8(1), 120–124 (1940).  https://doi.org/10.1063/1.1750549CrossRefGoogle Scholar
  21. 21.
    Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. MTCSAES. Springer, Heidelberg (2006).  https://doi.org/10.1007/3-540-31188-2CrossRefzbMATHGoogle Scholar
  22. 22.
    Ehrig, H., Golas, U., Habel, A., Lambers, L., Orejas, F.: \(\cal{M}\)-adhesive transformation systems with nested application conditions. Part 2: embedding, critical pairs and local confluence. Fundamenta Informaticae 118(1–2), 35–63 (2012).  https://doi.org/10.3233/FI-2012-705MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    Ehrig, H., Golas, U., Habel, A., Lambers, L., Orejas, F.: \(\cal{M}\)-adhesive transformation systems with nested application conditions. Part 1: parallelism, concurrency and amalgamation. Math. Struct. Comput. Sci. 24(04) (2014).  https://doi.org/10.1017/s0960129512000357
  24. 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_12CrossRefGoogle Scholar
  25. 25.
    Feret, J., Koeppl, H., Petrov, T.: Stochastic fragments: a framework for the exact reduction of the stochastic semantics of rule-based models. Int. J. Softw. Inf. (IJSI) 7(4), 527–604 (2014)Google Scholar
  26. 26.
    Gabriel, K., Braatz, B., Ehrig, H., Golas, U.: Finitary \(\cal{M}\)-adhesive categories. Math. Struct. Comput. Sci. 24(04) (2014).  https://doi.org/10.1017/S0960129512000321
  27. 27.
    Habel, A., Pennemann, K.H.: Correctness of high-level transformation systems relative to nested conditions. Math. Struct. Comput. Sci. 19(02), 245 (2009).  https://doi.org/10.1017/s0960129508007202MathSciNetCrossRefzbMATHGoogle Scholar
  28. 28.
    Habel, A., Plump, D.: \(\cal{M}, \cal{N}\)-adhesive transformation systems. In: Ehrig, H., Engels, G., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2012. LNCS, vol. 7562, pp. 218–233. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-33654-6_15CrossRefGoogle Scholar
  29. 29.
    Harmer, R., Danos, V., Feret, J., Krivine, J., Fontana, W.: Intrinsic information carriers in combinatorial dynamical systems. Chaos: Interdisc. J. Nonlinear Sci. 20(3), 037108 (2010).  https://doi.org/10.1063/1.3491100MathSciNetCrossRefzbMATHGoogle Scholar
  30. 30.
    Lack, S., Sobociński, P.: Adhesive and quasiadhesive categories. RAIRO - Theoret. Inf. Appl. 39(3), 511–545 (2005).  https://doi.org/10.1051/ita:2005028MathSciNetCrossRefzbMATHGoogle Scholar
  31. 31.
    Padberg, J.: Towards M-adhesive categories based on coalgebras and comma categories. arXiv:1702.04650 (2017)
  32. 32.
    Smith, M.B., March, J.: March’s Advanced Organic Chemistry. Wiley, Hoboken (2006).  https://doi.org/10.1002/0470084960CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.Center for Research and Interdisciplinarity (CRI), Université de Paris, INSERM U1284ParisFrance
  2. 2.Institut de Recherche en Informatique Fondamentale (IRIF)Université de Paris, CNRS UMR 8243Paris Cedex 13France

Personalised recommendations