Vincent Danos

Russ Harmer
email: russ.harmer@pps.jussieu.fr

Glynn Winskel

Constraining rule-based dynamics with types

A generalized framework of site graphs is introduced in order to provide the first fully semantic definition of the side-effect-free core of the rule-based language Kappa. This formalization allows for the use of types either to confirm that a rule respects a certain invariant or to guide a restricted refinement process that allows us to constrain its run-time applicability.

Introduction

Rule-based modelling [START_REF] Danos | Rule-based Modelling of Cellular Signalling[END_REF][START_REF] Hlavacek | Rules for Modeling Signal-Transduction Systems[END_REF] has been proposed as one possible solution to the problem of defining and investigating highly combinatorial microscopic transition systems found in cellular signalling networks and various models in statistical physics. Specifically, rules define rewrites of partially-specified macroscopic patterns that can match a variety of fully-specified microscopic entities. In this way, different instances of a rule may induce differing kinds of microscopic transition.

In previous work, we have introduced a mathematical framework of site graphs and embeddings in order to analyze how patterns can be refined to more specific patterns that match fewer microscopic entities. This led to the theory of rule refinement [START_REF] Murphy | Rule-based modelling and model refinement[END_REF] that explains how to split a rule into subcases which can then, if desired, be distinguished kinetically.

The present contribution extends this previous work in several ways. Firstly, by tweaking some of the basic definitions, we obtain a larger class of site graphs and homomorphisms that allows for a fully general expression of the binding, unbinding and state change actions fundamental to the rulebased framework. In particular, unlike in our previous work, we allow a site to have internal states which can be tested and modified independently of its binding state, i.e. whether the site is bound or not.

Secondly, unlike our previous treatment which uses a syntactic definition of actions as lists of rewrite instructions called 'action scripts', we introduce here a purely semantic definition of actions, as appropriate spans of monos, and an associated site graph rewriting in the double-push-out style [START_REF] Ehrig | Graph-grammars: an algebraic approach[END_REF]. This provides the first fully semantic definition of a rule-based language that, in particular, captures precisely the side-effect-free fragment of Kappa.

Finally, we formalize the idea of typing site graphs with homomorphisms into some fixed site graph, the contact graph, whose structure specifies all the admissible links and states. This is reminiscent of categories of bundles and, indeed, we find an adjunction associated with changing contact graph analogous to the familiar adjunction arising from a change of base.

This leads to our main conceptual point: types can be used to constrain the dynamics engendered by a collection of rules. Indeed, types can be used in both a static and a dynamic manner. On the one hand, a rule may or may not be compatible with a given contact graph so that a type can be used statically to enforce certain invariants. On the other hand, an action can be tagged with a type which will only be checked dynamically, via the change of contact graph adjunction, in order to reject potential events if they do not satisfy the properties demanded by the type.

The category of site graphs

In this section, we introduce the category of site graphs and homomorphisms and the important subcategory of realizable site graphs and matchings.

Basic definitions

A site graph G is specified by a tuple A G , S G , E G , σ G , ε G , λ G where • A G , S G
and E G are finite sets (of agents, sites and states);

• σ G : S G → A G assigns sites to agents and ε G : E G → S G assigns states to sites; • λ G is a symmetric relation on ((S G ) × (S G ) ) -{ , }.
The relation λ G encodes the link, or edge, structure of the graph:

• if s, s ∈ λ G , where s, s ∈ S G , then there is a link between them;

• if s, ∈ λ G , so that s ∈ S G , then s has a stub.

A site s ∈ S G may have neither an incident edge nor a stub; this means that its binding status is unspecified. We write this as s ∈ λ G . We use a Kappa-like syntax [START_REF] Danos | Rule-based Modelling of Cellular Signalling[END_REF] to denote site graphs textually: each node has an interface consisting of an agent name and a set of site names; the two ends of a link are represented by equal numerical superscripts to the sites in question; a stub is represented by a superscript; states are represented as subscripts to their sites. So

A(s 0,1 , t 1 ), B(s 1,2, ), C(t 2 p , s ), D(s )
represents a graph with four agents: A has a site s with unspecified binding status but two states 0 and 1, plus a site t bound to site s of B which has a stub and is also bound to site t of C, et c. Note that, unlike in usual Kappa syntax, a site can have multiple links and a stub so we cannot represent a stub implicitly by the mere absence of a link; we must note it explicitly.

A homomorphism f : G 1 → G 2 of site graphs is specified by a tuple of functions

f A : A G 1 → A G 2 , f S : S G 1 → S G 2 , f E : E G 1 → E G 2 such that A G 1 f A S G 1 σ G 1 o o f S S G 1 f S E G 1 ε G 1 o o f E A G 2 S G 2 σ G 2 o o S G 2 E G 2 ε G 2 o o
commute and the link structure of G 1 is preserved:

• if s, s ∈ λ G 1 , for s, s ∈ S G 1 , then f S (s), f S (s ) ∈ λ G 2 ; • if s, ∈ λ G 1 , so s ∈ S G 1 , then f S (s), ∈ λ G 2 .
The existence of a homomorphism f from G 1 to G 2 is more general than our previous notion of embedding since a site with unspecified binding status may be mapped to a site with a stub and/or links.

Basic categorical structure

We write SGrph for the category of site graphs and homomorphisms with composition defined in the obvious component-wise fashion. The empty site graph 0 where A 0 = S 0 = E 0 = ∅ is an initial object; and the singleton site graph 1 with A 1 = S 1 = E 1 = ∅ and where the unique site has both a stub and a self-loop is a terminal object. An arrow f is a mono if, and only if, its three constituent functions-f A , f S and f E -are all injective; and is an epi if, and only if, the three functions are all surjective.

Given a co-span

G 1 f 13 / / G 3 G 2 f 23 o o
, we take pull-backs in Set

A G 0 f 02A / / f 01A A G 2 f 23A S G 0 f 02S / / f 01S S G 2 f 23S E G 0 f 02E / / f 01E E G 2 f 23E A G 1 f 13A / / A G 3 S G 1 f 13S / / S G 3 E G 1 f 13E / / E G 3 to define the span G 1 G 0 f 01 o o f 02 / / G 2 ,
where the link structure of G 0 is defined by:

• s 1 , s 2 λ G 0 s 1 , s 2 iff s 1 λ G 1 s 1 and s 2 λ G 2 s 2 ; • s 1 , s 2 λ G 0 iff s 1 λ G 1 and s 2 λ G 2 .
The span

G 1 G 0 f 01 o o f 02 / / G 2 is
G 0 f 01 o o f 02 / / G 2 , define G 1 f 13 / / G 3 G 2 f 23 o o
with the push-outs in Set, analogous to the above pull-backs, and defining the link structure of G 3 as:

• [s] λ G 3 [s ] iff either, for some s 1 , s 1 ∈ S G 1 , inl(s 1 ) ∈ [s] and inl(s 1 ) ∈ [s ]
and s 1 λ G 1 s 1 ; or, for some s 2 , s 2 ∈ S G 2 , inr(s 2 ) ∈ [s] and inr(s 2 ) ∈ [s ] and s 2 λ G 2 s 2 ;

• [s] λ G 3 iff either, for some s 1 ∈ S G 1 , inl(s 1 ) ∈ [s] and s 1 λ G 1 ; or, for some s 2 ∈ S G 2 , inr(s 2 ) ∈ [s] and s 2 λ G 2 .
The co-span

G 1 f 13 / / G 3 G 2 f 23 o o
is our choice of push-out in SGrph; intuitively, it is a 'union' of G 1 and G 2 , i.e. the smallest, and so most general, site graph that can map to any site graph that both G 1 and G 2 can map to-relative to the given span from G 0 . This means that SGrph has finite co-products, obtained by taking push-outs from its initial object.

Realizable site graphs

The structure of a site graph can be interpreted in two different ways: either its links and stubs specify possibilities, i.e. admissible bonds and free sites; or they describe an actuality, i.e. a real configuration of agents.

For our purposes, this latter interpretation only makes sense for site graphs whose link/stub and state structure is 'deterministic' in the following natural sense:

• for all s ∈ S G , if s, s 1 ∈ λ G and s, s 2 ∈ λ G then s 1 = s 2 ; • the state map ε G is injective.
The idea is that each site is a resource that, at any given time, can have at most one state and be dedicated to at most one task, i.e. it can be free (a stub) or bound (linked) but not both and, if bound, then only to one thing. We call such site graphs realizable.

If f : G 1 → G 2
and G 2 is realizable then G 1 need not be realizable, e.g. there is an obvious homomorphism mapping G 1 := A(s 1,2 ), B(t 1 , t 2 ) to G 2 := A(s 1 ), B(t 1 ). (We are implicitly defining the homomorphism with our choice of 'names' for nodes and sites: the node named A in G 1 is mapped to the node named A in G 2 , the sites named t in G 1 are both mapped to the site named t in G 2 , et c.) However, if f S and f E are injective then G 1 must be realizable since f S being injective would force any link non-determinism in G 1 to be propagated to G 2 and f E does likewise for states. We say that f is a matching iff f S and f E are injective.

We write rSGrph for the subcategory of SGrph with objects realizable site graphs and arrows matchings. This category inherits pull-backs from

SGrph: given a co-span G 1 f 13 / / G 3 G 2 f 23 o o
, the pull-back of f 13 and

f 23 , considered as arrows of SGrph, yields a span G 1 G 0 f 01 o o f 02 / / G 2
where f 01 and f 02 are matchings, since pull-backs preserve monos, so that G 0 is realizable. This span is also the pull-back in rSGrph.

The situation is more complicated with regard to push-outs. Firstly, push-outs need not exist since the construction in SGrph does not guarantee that G 3 is realizable, even if G 0 , G 1 and G 2 all are, e.g. if a site has different states in G 1 and G 2 . Secondly, even if a push-out exists, it may not be the same as in SGrph, e.g. if G 0 = A(s) and

G 1 = G 2 = A(s 1 ), B(t 1 ) then G 3 = A(s 1 ), B(t 1 ) in rSGrph but G 3 = A(s 1,2 ), B(t 1 ), B(t 2 ) in SGrph.

Typing site graphs

In rule-based modelling, our main interest is in realizable site graphs as they represent actual configurations of agents and connected components. However, we can use arbitrary site graphs as types: a homomorphism from a (realizable) site graph G to an arbitrary site graph C guarantees that all edges and stubs in G also occur in C, so C could be taken as a specification of admissible stubs and edges that is satisfied by G. We formalize this intuition with the standard notion of a slice category over C.

Categories over C

The slice category SGrph/C over a site graph C has, for objects, all arrows h : G → C of SGrph into C; we think of these as witnesses that 'G has type C'. We refer to C as the contact graph and h : G → C as a contact map. We require no particular properties of C; its status as a contact graph is bestowed by fiat.

An arrow

f : h 1 → h 2 of SGrph/C between the objects h 1 : G 1 → C and h 2 : G 2 → C is an arrow f : G 1 → G 2 of SGrph making h 1 = h 2 • f .
In other words, f is a homomorphism from G 1 to G 2 that preserves typing. The basic categorical structure of SGrph carries over largely unchanged to SGrph/C, the exception being the terminal object: in SGrph/C, any automorphism of C is now a terminal object.

Given contact maps h

i : G i → C, the pull-back of h 1 f 13 / / h 3 h 2 f 23 o o is constructed by taking the pull-back in SGrph G 0 f 02 / / f 01 G 2 f 23 G 1 f 13 / / G 3 and defining h 0 := h 1 • f 01 = h 2 • f 02 . This is well-defined since, for any agent, site or state x of G 0 , f 13 (f 01 (x)) = f 23 (f 02 (x)) and so h 1 (f 01 (x)) = h 3 (f 13 (f 01 (x))) = h 3 (f 23 (f 02 (x))) = h 2 (f 02 (x)
). The push-outs of SGrph carry over to SGrph/C in analogous fashion.

The category SGrph C is obtained as a subcategory of SGrph/C by restricting the objects to be those contact maps h : G → C that are locally injective on sites: no two sites of the same agent of G can map to the same site of C. This means that each agent a of G has at most one copy of each site of its corresponding agent h(a) of C, i.e. agents have sets, not multi-sets, of sites. As an immediate consequence, all arrows f : h 1 → h 2 are locally injective on sites. If, moreover, f is injective on agents then it is injective on sites too; however, the converse is not true in general, e.g. there is a natural arrow from G 1 := A(s), A(t) to G 2 := A(s, t).

The subcategory rSGrph C

We can analogously define the slice category rSGrph/C. However, the situation is rather more interesting in rSGrph C , the full subcategory of rSGrph/C containing only locally injective contact maps (from realizable site graphs), which is also our main category of interest.

An arrow of rSGrph C is still a mono if, and only if, its three constituent maps are all injective. However, the characterization of epis requires some care. Specifically, an arrow f : h 1 → h 2 is an epi if, and only if, every connected component of G 2 contains at least one agent in the image of f . This follows from the following rigidity lemma that depends on G 2 being realizable and the contact maps h 1 and h 2 being locally injective:

Lemma [rigidity] Let h 1 : G 1 → C and h 2 : G 2 → C be objects of rSGrph C . If G 1 is connected then the least partial function f A : A G 1 A G 2 sending a 1 to a 2 extends to at most one matching f : h 1 → h 2 .
Proof. The proof is iterative. For the base case, if a 2 ∈ h -1 2 (h 1 (a 1 )) then, by local injectivity of h 1 and h 2 , there is at most one way to define f S on a 1 's sites; and, by injectivity of ε G 2 , at most one way to define f E on a 1 's states. If this succeeds and all stubs of a 1 are also preserved, we have a 'partial matching' f defined on a 1 . We now iterate, assuming such a partial f that preserves all links between the agents of dom(f A ). Consider any a 1 ∈ A G 1 -dom(f A ) having links to a non-empty set S of sites in dom(f S ). Since G 2 is realizable, there can be at most one a 2 ∈ h -1 2 (h 1 (a 1 )) (possibly already in the image of f ) that has links to all the s ∈ f S (S). If this a 2 exists then, by local injectivity of h 1 and h 2 and by injectivity of ε G 2 , there is at most one way to extend f S and f E . If all stubs of a 1 are preserved in a 2 , we continue; otherwise f does not extend to any matching.

The point of this lemma is that, given a 'seed', the matching process is deterministic. This is a synergistic consequence of the realizability of G 2 and local injectivity of the contact maps; dropping any of these constraints immediately invalidates rigidity. An important consequence of rigidity is that, for any arrow f 2 : h 2 → h 3 of rSGrph C , if we know how just one agent of each connected component of G 2 maps into G 3 , we know the whole matching f 2 . Therefore, f 1 : h 1 → h 2 is an epi if, and only if, at least one agent of each connected component of G 2 is in its image.

Another consequence of rigidity is that any arrow f : h 1 → h 2 of rSGrph C decomposes uniquely (up to automorphisms) into an epi f : h 1 h 2 , where h 2 : G 2 → C, and the unique arrow ! G 2 : 0 → G 2 from the initial object:

G 1 ∼ = / / f G 1 + 0 f +! G 2 G 2 ∼ = / / G 2 + G 2
There is a special class of objects h : G → C in rSGrph C , which we call mixtures, characterized as those h that are

• locally surjective: every agent a of G displays the same sites as its counterpart h A (a) in C;

• definite: if s ∈ λ G then h S (s) ∈ λ C ; and if ε -1 G (s) = ∅ then ε -1 C (h S (s)) = ∅.
In words, a mixture is a site graph where every agent displays every site it possibly can, if a site has a state in C then it must also in G and if a site has a stub and/or incident edge in C then it must have one or the other in G too. In effect, a mixture is a fully-specified site graph with respect to C.

Change of contact graph

Given a homomorphism h : C → C , we can define functors between the slice categories SGrph/C and SGrph/C . The mapping from SGrph/C to SGrph/C is immediate:

• an object h 1 : G 1 → C becomes h * (h 1 ) := h • h 1 : G 1 → C ; • an arrow f : h 1 → h 2 becomes h * (f ) := f : h • h 1 → h • h 2 .
The reverse mapping relies on the existence of pull-backs in SGrph:

• an object h 1 : G 1 → C becomes h * (h 1 ) := h 1 : G 1 → C as defined by the pull-back G 1 h / / h 1 G 1 h 1 C h / / C • an arrow f : h 1 → h 2 becomes h * (f ) := f : h 1 → h 2 G 1 f h 1 f •h $ $ G 2 h 2 h / / G 2 h 2 C h / / C
by applying universality of the pull-back to the outer commuting square.

It is then straightforward to show that h * : SGrph/C → SGrph/C is left adjoint to h * : SGrph/C → SGrph/C. The right adjoint h * can be used to re-visualize a site graph according to the contact graph C rather than C . As we will see later, this can be exploited to verify dynamically whether or not an instance of a rule respects its declared type.

In general, the pull-back of h and h 1 -even from realizable G 1 -need not yield realizable G 1 . However, if h is a matching then, since pull-backs preserve monos, h and h are both matchings, so G 1 and G 2 are realizable. If, additionally, f is a matching then f • h is a matching, so f is also a matching and thus an arrow of rSGrph. The h * functor thus restricts to a functor from rSGrph/C to rSGrph/C. Finally, if we also have that h 1 and h 2 are locally injective on sites, then clearly h 1 and h 2 are also locally injective on sites, i.e. they are objects of rSGrph C .

In summary, h * is a functor from SGrph/C to SGrph/C that restricts to a functor from rSGrph/C to rSGrph/C and, if additionally h 1 and h 2 are locally injective on sites, further restricts to a functor from rSGrph C to rSGrph C .

Rewriting site graphs

In this section, we introduce actions, the semantic analogue of action scripts, and use them to define rewriting of site graphs in the double-push-out (DPO) style. This is largely a straightforward exercise but does require a little care to identify an appropriate class of actions for which DPO rewriting works correctly. We begin with a very general notion of action and gradually home in on the desired class of valid actions.

Actions as spans

The most general possible definition of action is as a span in SGrph

G 0 x x x x & & G G r
with intuitive reading that G is to be rewritten into G r while the common part of G and G r matched by G 0 remains unchanged. Indeed, this is an instance of the well-known general approach of building (bi-)categories of partial maps out of categories of total maps [START_REF] Robinson | Categories of partial maps[END_REF].

It would be perfectly possible to develop a theory of untyped site graph rewriting along these lines. For the purposes of this paper, however, we prefer to work in the typed setting of rSGrph C from the outset as this has the advantage of coming with an intrinsic notion of mixture. Moreover, a span h h 0 α o o αr / / h r in rSGrph C comes with the guarantee that h • α = h 0 = h r • α r meaning that the contact information of everything in G 0 is the same on both sides of the span.

• E M 0 := E M -(E G -E G 0 ); • λ M 0 := λ M -(λ G -λ G 0 ).
We cannot define A M 0 or S M 0 in this more subtle way as this could lead to 'orphaned' sites, states and links, e.g. a site might not be attached to any agent. It is easy to see that this always gives rise to a commuting square with the inclusions from G 0 to M 0 and M 0 to M . However, unless α is surjective on agents and sites, this square cannot be a push-out since any agent or site of G not also in G 0 would have to be duplicated by the push-out.

Intuitively, this condition enforces the idea that G 0 contains everything that is preserved by the action; in particular, the existence of the agents and sites of G is not in question. This condition plays an analogous role to the dangling condition in DPO rewriting of normal graphs although, rather than using it as a means to reject certain matchings, we instead use it to constrain our notion of action.

Technically speaking, now that this push-out has been constructed, it is always possible to complete the DPO rewrite:

G 0 } } α } } G 0 } } α } } " " " " G m M 0 } } / / G m M 0 } } ! ! G r M M M r
However, in order for M r to be a mixture, we need some additional properties of α r . Firstly, that it is a mono and also surjective on agents and sites so that there is a bijection between the agents and sites of G and G r . Secondly, for all sites s of G , s ∈ λ G if, and only if, s ∈ λ Gr (where we have slightly abusively reused s to denote the counterpart of s in G r ). In other words, unspecified binding statuses must be preserved by actions. These conditions rule out non-deterministic rules, e.g. sending s ∈ λ G to s λ Gr , and guarantee that actions are always reversible, i.e. the span

G 0 } } α r } } ! ! α ! ! G r G
is also an action-which is in fact just another way of saying that actions cannot have side-effects.

Indeed, in full Kappa, there are only two kinds of rule that violate reversibility-the deletion of only part of a connected component; and the undoing of a wild-card-binding-both of which also induce side-effects due to the implicit deletion of links not mentioned by the action. Our restriction on actions rules out the former and the latter cannot even be expressed with the present formulation of site graphs; so our formalism allows us to express only side-effect-free Kappa.

In summary, a valid action, or rule, is an action where α and α r are bijections on agents and sites, the eliminated G and introduced G r are mixtures and where sites with unspecified binding status must be preserved by the rule and its reverse. We should stress that these are sufficient, but not necessary, conditions on actions for them to be compatible with DPOstyle rewriting; however, this is sufficient for side-effect-free Kappa since all actions expressible therein are valid. Note that, in what follows, we generally write rules in the more familiar form G → G r , leaving the preserved region G 0 implicit.

Static constraints on actions

The explicit typing of site graphs with a contact graph allows us to express certain invariants as static constraints on rules.

For example, the unbinding rule A(s 1 ), B(s 1 ) -→ A(s ), B(s ) cannot be expressed as a span over the contact graph

T := A(s 1, ), B(s 1,2 ), C(s 2, )
since its RHS does not respect the typing constraints of T . Specifically, the lack of a stub on B's site s means that s must always be bound, preventing any rule that destroys this invariant.

A careful choice of contact graph can therefore enforce some fairly subtle constraints, e.g. the 'bond displacement' rule

A(s 1 ), B(s 1 ), C(s ) -→ A(s ), B(s 1 ), C(s 1 )
can be expressed as a span over T since it does preserve the invariant.

Note that this use of contact graphs only determines the validity, or otherwise, of a rule with respect to a type: the rule is either accepted or rejected. In the next section, we show how to use types to constrain which instances of a rule are valid in order to constrain the dynamics engendered by rules.

Rule-based dynamics

In this section, we assume a collection of rules R valid with respect to a contact graph C. Each rule r ∈ R has a real-valued rate constant k r and may also have its own family of types (C r ) accompanied by homomorphisms h r,i : C r,i → C which we will use, in conjunction with the change of contact graph adjunction, to reject certain instances of r dynamically. However, let us first briefly recall the standard notion of continuous-time Markov chain (CTMC) which underlies the stochastic semantics of R.

A CTMC has a set S of states and a set T of transitions between distinct states, i.e. no self-loops. Each transition τ from s is assigned a real number A τ (s) known as its activity; each state s acquires a total activity, defined as the sum A(s) := τ A τ (s) of the activities of all its outgoing transitions.

The dynamics of a CTMC depends on the waiting time in, and transition probabilities from, each state s. The former is described by the exponential random variable p(δt) := A(s)•e -A(s)δt , the minimum of the family p τ (δt) := A τ (s)•e -Aτ (s)δt of independent random variables, i.e. the time until the first transition; and, for the latter, each transition τ from s naturally acquires the probability A τ (s)/A(s) of being chosen.

The stochastic semantics of R

In order to instantiate this general scheme to the specific case of our system R of rules, we must define the states, transitions and activities thereof that R induces. It turns out that the states are straightforward to define-they are just mixtures with respect to the contact graph C-but the definition of transitions is more subtle.

To see why, consider first the case of traditional chemical kinetics, i.e. rewriting of a multi-set of named, structureless molecular species. In this setting, the notion of event, or transition, is straightforward: the choice of a multi-set of reactants that are to be replaced by the multi-set of products. The only subtle point comes about when dealing with reactions that have symmetries between reactants, e.g. A + A -→ B; is an event an ordered or an unordered pair of As? The answer depends on whether the reaction is intended to represent the formation of an asymmetric or a symmetric dimer, the former necessarily proceeding twice as fast as the latter. However, the relative paucity of the formal language of reactions makes it impossible to express this distinction syntactically; it must therefore be encoded in the rate constant-given a semantic convention fixing whether one considers an event as an ordered or an unordered pair by default.

In the case of rules, this question acquires new potency since we are now working in a far richer syntactic medium: not only do molecular species, i.e. complexes, have internal structure-agents, sites, links, et c.-but the rules need only partially specify those complexes. This means that we can now express the distinction between symmetric and asymmetric homodimerization:

r s := A(s ), A(s ) -→ A(s 1 ), A(s 1 ) r a := A( , r ), A( , r ) -→ A( , r 1 ), A( 1 , r )
Each rule has a non-trivial automorphism of its LHS, suggesting perhaps that our notion of event should be that of an unordered pair. However, what happens if either rule is matched to a pair of non-isomorphic complexes? Or, indeed, if an asymmetric rule is applied in a symmetric context?

Ultimately, the question being posed is: when should two matchings of the LHS of a rule into a mixture be considered indistinguishable from the rule's point of view ? Any non-trivial automorphism of that LHS may give rise to such indistinguishability-but only if it survives the action of the rule. If an automorphism is destroyed by the action, the two matchings can be distinguished post hoc and correspond to two distinct reaction centres.

In the case of r s above, the non-trivial automorphism is preserved and, as such, r s defines a symmetric binding mechanism which cannot distinguish between two complexes that match it, even if they are actually different. On the other hand, r a breaks the symmetry and, as such, defines an asymmetric binding mechanism that induces two distinct reaction centres and can even distinguish identical complexes that match it.

In general, for a rule r, we therefore define an r-event to be a matching of the LHS of r up to automorphisms of the LHS preserved by the action of r, cf. [START_REF] Blinov | Graph theory for rule-based modeling of biochemical networks[END_REF]. We write E r (M ) for the set of all r-events in the mixture M ; this is always a finite set. Note that any matchings identified by this quotient necessarily provoke exactly the same rewrite of the mixture; moreover, any other matching would perform a different microscopic rewrite, so our notion of event is the coarsest possible quotienting of matchings that ensures that an event induces a unique microscopic transition.

We can finally complete our description of the CTMC defined by R. The set of transitions from a mixture M is the union T := r E r (M ) of all events in M . The activity of each r ∈ R in M is defined as A r (M ) := k r • |E r (M )| so that the activity of any given r-event is simply k r . This convention for activity is known as the mass-action rate law.

Dynamic rejection of events

We now turn to the question of rejecting events dynamically. We write r L (resp. r R , r P ) for the LHS (resp. RHS, preserved zone) of r ∈ R; h L : r L → C, h P : r P → C and h R : r R → C for the static typing of r by the contact graph C; and α L : h P h L and α R : h P h R for the action of r. We also assume that each r ∈ R is accompanied by a finite collection of refined types C r,i , each with a mono h r,i : C r,i C to the overall contact graph C. We require that, for each h r,i , there exist arrows h L,i : r L → C r,i , h P,i : r P → C r,i and h R,i : r R → C r,i making the obvious triangles commute:

r L h L,i } } h L r P h P,i } } h P r R h R,i } } h R C r,i h r,i / / C C r,i h r,i / / C C r,i h r,i / / C
This ensures that C r,i is still a valid static type for r. Each h r,i thus specifies a (potentially) more stringent requirement for r to be applied. The idea is that an r-event will be accepted if, and only if, it respects at least one of the C r,i s. Note that this is a property of an instance of r, not of r itself; it is verified with the change of contact graph adjunction. In order to define precisely what we mean by an instance of the rule r, recall that a matching f : r L → M of r into a mixture M decomposes into an epi f M : r L M r L and an arrow from the initial object 0 to the rest of M (which we ignore); for the sake of readability, we are writing r L rather than the more correct h L . We call the graph M r L a ground refinement of r L . We obtain the ground refinements, M r P and M r R , of r P and r R by the DPO-rewriting of M r L according to the action of r. We obtain a new action defined by α L,f : M r P M r L and α R,f : M r P M r R . In effect, we slide the rule r along the matching f to obtain a specific, fully-instantiated instance of r in the mixture M .

For each refined type C r,i , we now use h * r,i to change contact graph from C to C r,i :

M P,i α L,i | | α R,i # # M r L M L,i o o M R,i / / M r R C C r,i h r,i o o C r,i h r,i / / C
Since h r,i is a mono, M L,i , M R,i and M P,i are realizable. The resulting span M L,i M P,i o o / / M R,i defines an action that refines the original rule r,

i.e. it describes the same rewrite as r but with a (potentially) more stringent test which matches fewer mixtures with respect to C. However, in general, one or other (or both) of M L,i and M R,i need not be a mixture with respect to C r,i ; such a refinement does not respect the typing constraint C r,i .

If, for some i, M L,i and M R,i are both mixtures with respect to C r,i then we say that the (original) matching satisfies the refined type C r,i ; otherwise it is a null event. In the former case, we are now free to perform the rewrite specified by the rule and its matching; otherwise, the rewrite is definitively rejected.

For example, consider the rule

A(d ), D(a ) -→ A(d 1 ), D(a 1 )
with contact graph C, further constrained by contact graphs C 1 and C 2 :

C := A(d 1, , b 2,3, ), B 1 (a 2, ), D(a 1, ), B 2 (a 3, ) C 1 := A(d , b 2 ), B 1 (a 2, ), D(a ) C 2 := A(d 1, , b 3, ), D(a 1, ), B 2 (a 3, ).
The ground refinement

A(d , b 2 ), B 1 (a 2 ), D(a ) -→ A(d 1 , b 2 ), B 1 (a 2 ), D(a 1 )
does not respect C 1 because, in its RHS, A's site d and D's site a have the opposing binding status to what they have in C 1 , so they acquire unspecified binding status in the pull-back:

A(d, b 2 ), B 1 (a 2 ), D(a) / / A(d 1 , b 2 ), B 1 (a 2 ), D(a 1 ) C 1 / / C
Moreover, this ground refinement cannot respect C 2 either simply because C 2 does not contain B 1 . It is therefore a null event.

Intuitively, C 1 and C 2 express the logical constraint that 'B 1 , but not B 2 , blocks D's access to A', a phenomenon known to biophysicists as steric occlusion which arises when (i) one protein physically blocks the access of a second to its desired binding site; and (ii) the second protein could have bound if the first were not there.

Instead of using them for dynamic rejection of events, we could instead employ the C r,i s as a growth policy [START_REF] Murphy | Rule-based modelling and model refinement[END_REF] to generate statically the collection of rules that refine r and respect the C r,i s. We prefer not to do this since, in general, it leads to an explosion in the number of rules and, as we will see in the next section, we can easily obtain the same effect through dynamic rejection of events. However, such an approach may still be preferable, for reasons of simulation efficiency, in the case of a system generating a large number of null events.

However, the principal advantage of enforcing constraints dynamically, rather than refining rules explicitly, is that it allows us to make a clean separation of the essential mechanism from more incidental problems such as steric occlusion: it is surely not the fault of the binding mechanism if it fails only because some other agent is 'in the way' and it should not be the rule's responsibility to keep track of all the incidental ways by which it can be frustrated. Of course, rules can always be appropriately massaged to enforce such constraints but such rules are fragile and difficult to modify and/or incorporate into larger rule sets that need not be aware of their builtin assumptions. It seems more prudent, and scalable, to keep the rule simple and document its steric demands, et c., separately with types.

Overestimating activity

In the previous section, we have seen how certain transitions of our CTMC built out of R may be rejected during simulation. When this happens, the state s of the CTMC does not change-it is as if there were a self-loop-so, in particular, the activity A r (s) of each rule r and the total activity A(s) remain unchanged.

This requires a modification of the dynamics of the CTMC since the existence of a self-loop tends to increase the waiting time in that state. Specifically, the waiting time in state s becomes the time until a real event occurs.

It is well-known that the time for n ≥ 1 events to occur in a Poisson process is described by the Gamma random variable Γ n,A(s) (δt) = (A(s) n • δt n-1 /(n -1)!) • e -A(s)δt so, if the probability of a null event occurring in state s is q(s), the total waiting time in state s is distributed as p(δt) = ∞ n=0 q(s) n (1 -q(s)) • Γ n+1,A(s) (δt).

In the case of our CTMC derived from R, the probability q M for each state M is not known statically; however, whenever a transition t from M is chosen, we can then detect whether or not it is a null event. Given that the chosen event is some r-event, the fact that r-events are chosen uniformly at random means that the probability q r (M ) that 'the chosen r-event is a null event' is just the number of null r-events divided by the total number |E r (M )| of r-events. The overall probabilility that 'the chosen event is a real r-event' is therefore A r (M )/A(M ). In effect, M has a true activity A (M ) = r (1 -q r (M )) • A r (M ) underestimating its usual activity.

It follows that the probability that 'the chosen event is null' is q(M ) = r q r (M ) • A r (M )/A(M ) = (A(M ) -A (M ))/A(M ) and the probability that 'the next real event is an r-event' is (A r (M )/A(M ))/(A (M )/A(M ) = A r (M )/A (M ). Finally, we instantiate the above equation to obtain

p(δt) = A (M ) • e -A(M )δt • ∞ n=0 (A(M ) -A (M )) n • δt n /n! = A (M ) • e -A (M )δt .
In summary, the waiting time in, and transition probabilities from, state M depend only on the (unknown!) true activities A r (M ) and so the modified CTMC behaves exactly as if it were actually the true CTMC with no selfloops obtained by statically generating all rules satisfying the growth policy C r . This argument is a more general use of the technique for dealing with null events arising for reasons of implementation efficiency [START_REF] Danos | Scalable Simulation of Cellular Signaling Networks[END_REF][START_REF] Yang | Kinetic Monte Carlo method for rule-based modeling of biochemical networks[END_REF].

Conclusions

In this paper, we have given the first fully semantic definition of a rule-based language which encompasses a large fragment of Kappa, the only restriction being the forbidding of side-effects. This has clarified the connection between the notion of site graph rewriting, as expressed by rules in Kappa, and more traditional graph rewriting that has long used the double-push-out technique to formalize rewriting.

We have also investigated for the first time the possibility of typing rules to express invariants hidden in a rule or enforce constraints on the dynamics engendered by a rule set. This approach should usefully complement the analyses made with abstract interpretation [START_REF] Danos | Abstract Interpretation of Cellular Signalling Networks[END_REF], some of which address similar issues. However, this initial investigation remains purely mathematical; the important question remains as to how a powerful and pragmatically useful type system for rules should be defined and implemented.

g

  / / B , we fix A + C B to be the quotient of A + B by (the reflexive, symmetric and transitive closure of) the relation inl(a) inr(b) iff, for some c ∈ C, a = f (c) and b = g(c). This set, together with the injections ι A : A → A + C B and ι B : B → A + C B defined by a → [inl(a)] and b → [inr(b)], is our canonical choice of push-out in Set.

Acknowledgements. We would like to thank Eric Deeds, Jérôme Feret, Walter Fontana and Jean Krivine for many discussions on topics related to the subject of this paper.

Double push-out rewriting

Let us now investigate the class of actions that we can use in order to express the rewriting of site graphs in rSGrph C as an instance of the general doublepush-out (DPO) approach.

The essential difficulty of DPO rewriting comes in the first step where, given the left leg of the span and a matching into some mixture M , we must 'complete the push-out' via an intermediate M 0 :

(To lighten notation, we write just G 0 , et c., rather than the more accurate

Let us first consider the special case where G 0 is the empty site graph 0 which corresponds to a situation where G is to be completely excised from M and replaced by G r -since G 0 is everything of G to be preserved by the action. In this case, since a push-out from an initial object is always a co-product, we know that, if M 0 exists, then M ∼ = G + M 0 . In effect, this means that G does not merely match M but that it is literally contained in M ; so an action that removes and/or adds agents can only remove and/or add entire connected components of/to M , i.e. mixtures with respect to the ambient contact graph C:

This restriction enforces a 'no side-effects' condition that guarantees that all things in M that are modified by the action are explicitly mentioned by the action, just as is the case for multi-set rewriting.

In the general case, where G 0 may be non-empty, we first decompose α uniquely (up to isomorphism) into an epi α : G 0 G and ! G : 0 → G , so that G ∼ = G + G . Provided that G is a mixture, it is then sufficient to be able to complete the push-out for α and the restriction m := m • ι G of m to G ; the missing mixture G can be dealt with afterwards as per the above special case.

We construct an M 0 by setting A M 0 := A M , S M 0 := S M and defining the interesting part of its structure according to the standard DPO-style prescription of 'add to G 0 everything that is in M but not in G ':