Interactions between Causal Structures in Graph Rewriting Systems

TL;DR

This paper develops a formal framework to analyze how different causal mechanisms in graph rewriting systems interact, enabling verification of mutual influences and compliance with empirical data in complex molecular models.

Contribution

It introduces a rigorous method to define and verify interference between mechanisms in graph rewriting systems, advancing understanding of molecular interactions.

Findings

Framework for interference analysis between mechanisms

Ability to verify if influences are realizable

Potential to guide rule adjustments for empirical compliance

Abstract

Graph rewrite formalisms are a powerful approach to modeling complex molecular systems. They capture the intrinsic concurrency of molecular interactions, thereby enabling a formal notion of mechanism (a partially ordered set of events) that explains how a system achieves a particular outcome given a set of rewrite rules. It is then useful to verify whether the mechanisms that emerge from a given model comply with empirical observations about their mutual interference. In this work, our objective is to determine whether a specific event in the mechanism for achieving X prevents or promotes the occurrence of a specific event in the mechanism for achieving Y. Such checks might also be used to hypothesize rules that would bring model mechanisms in compliance with observations. We define a rigorous framework for defining the concept of interference (positive or negative) between mechanisms induced by a system of graph-rewrite rules and for establishing whether an asserted influence can be realized given two mechanisms as an input.

Equations

$$e_i<e_j⟺e_i\stackrel{+\overrightarrow{f}}{\to }{e}_j\text{ and }{e}_i⊩e_j⟺e_j\stackrel{-\overrightarrow{f}}{\to }{e}_i.$$

$$x::=$$

$$t^s::=$$

$$t^e::=$$

$$t::=$$

$$\phi ::=$$

$$\neg \phi |{\phi }_1\wedge {\phi }_2|$$

$$t^e\in t^s|\ell (t^e)=\overrightarrow{r}|t_1^e{\le }_{t^s}{t}_2^e|t_1^e{⊢}_{t^s}{t}_2^e$$

$$|t_1^e\in t_1^s\stackrel{-}{⇝}{t}_2^e\in t_2^s|t_1^e\in t_1^s\stackrel{+}{⇝}{t}_2^e\in t_2^s$$

$$[[\forall x^s.\phi ]{]}_v$$

$$[[\exists x^s.\phi ]{]}_v$$

$$[[\neg \phi ]{]}_v$$

$$[[{\phi }_1\wedge {\phi }_2]{]}_v$$

$$[[t^e\in t^s]{]}_v$$

$$[[\ell (t^e)=\overrightarrow{r}]{]}_v$$

$$[[t_1^e{\le }_{t^s}{t}_2^e]{]}_v$$

$$[[t_1^e{⊢}_{t^s}{t}_2^e]{]}_v$$

$$[[t_1^e\in t_1^s\stackrel{+/-}{⇝}{t}_2^e\in t_2^s]{]}_v$$

$$s_1=\{t_1^s{\}}_v,s_2=\{t_2^s{\}}_v$$

$$\{x{\}}_v$$

$$\{e{\}}_v$$

$$\{s{\}}_v$$

Full text

1 Introduction

A persistent challenge across molecular biology is to understand how a multitude of diverse and asynchronous interactions between molecular entities give rise to coherent system behavior. One difficulty arises from the combinatorial complexity inherent in chemistry: A reaction (or interaction) between structured entities, such as molecules, consists in the transformation of specific parts in a manner that depends on a few rather than all aspects specifying the reactants. Combinatorial complexity then arises because a given reactant combination can exhibit several distinct reactive patterns and the same pattern can occur across many distinct reactant combinations. This idea generalizes beyond chemistry.

A molecular system can thus be described in terms of rewrite rules. In this way, rule-based modeling tackles combinatorial complexity without succumbing to it because it only specifies rules of pattern transformation and not the multitude of possible carriers of these patterns. Many physical systems can be conveniently described as graphs. A rule-based approach then becomes a graph rewriting formalism with a domain-specific execution model that determines the probability with which a rule fires at a given time. The currently most developed approaches are the Kappa language [9, 6] and BNGL [12] for molecular biology and Mød [2] for organic chemistry.

A rule formalizes the interaction between physical entities at some chosen level of abstraction. Processes occurring below that level are abstracted away, yet not ignored: They inform what a rule should say, but they are not explicitly represented by it. For instance, in organic chemistry, a rule of reaction between molecules expresses a local reconfiguration of bonds among atoms without explicitly representing the underlying mechanism of electron pushing that engenders such reconfiguration. In molecular biology, an interaction between proteins is typically expressed by asserting the conditions for a change of protein state without representing the structural mechanisms enabling that change. In essence, a mechanism below the chosen abstraction level becomes an axiomatic rule at the abstraction level [15].

Many observations of system behavior are assertions rather than rules. For example, an assertion might claim that the activation of protein $\mathtt{X}$ inhibits the assembly of molecular machine $\mathtt{Z}$. It is desirable to determine whether and why an assertion holds in terms of the joint action among rules that represent a particular system. This is tantamount to providing a mechanism that explains a given assertion at the level of abstraction at which rules are defined.

The stochastic application of rules (a simulation) typically generates a long trace of state transitions. A mechanism is a set of transitions that were jointly necessary in producing a specified outcome. Mechanisms so-defined can be extracted from traces [5, 4] and abstracted into partial orders (posets) of events111In Ref.[5], a partially ordered set of events that account for an outcome was dubbed a “story”, which is akin to the biological notion of a “pathway”..

Here we propose a formal logic to express and verify a particular kind of assertion about a model written in the Kappa language. We focus on assertions in which the occurrence of one event is claimed to interfere with another event. Our approach takes as input two posets of events (i.e. mechanisms), which might be hypothesized or abstracted from a simulation, and provides evidence whether the two posets interfere with one another at the specified events. The key is that each poset builds up a context that is required for its terminal event. These contexts can be reconstructed and checked for mutual consistency. To lay the foundation for this approach requires setting up some formal machinery which occupies the bulk of this paper.

Interaction between graph rewriting posets. The graphs in Kappa consist of nodes, called agents, meant to represent proteins. Agents are equipped with sites through which they connect to one another. A site represents a resource and hence can bear at most one edge. Such graphs are called site-graphs.

An event is the application of a rewrite rule to a usually large graph representing the state of the system. Events are partially ordered by a relation of precedence. Intuitively, an event $e_{1}$ precedes an event $e_{2}$ if $e_{1}$ contributes to establishing the context necessary for $e_{2}$. Consider, for example, the simple model in Figure 1 with the initial state consisting of nodes $\{\mathtt{A},\mathtt{B},\mathtt{C}\}$, all unbound. Suppose furthermore that the binding of agent $\mathtt{X}$ to $\mathtt{A}$ (rule $r_{\text{AX}}$) and of agent $\mathtt{Y}$ to $\mathtt{A}$ (rule $r_{\text{AY}}$) are two significant events $e_{\text{AX}}$ and $e_{\text{AY}}$, respectively. We wish to verify the assertion that either event inhibits the other. The assertion is cast in terms of two mechanisms (posets) that could have been extracted from a simulation trace of this model, one mechanism resulting in $e_{\text{AX}}$, the other in $e_{\text{AY}}$ (Figure 2A).

A static inspection of rules $r_{\text{AX}}$ and $r_{\text{AY}}$, underlying the events that are the subject of our query, shows that both use the same site of $\mathtt{A}$. This might suggest that the two events are in conflict and therefore inhibit each other. This, however, is not a valid conclusion. Given the poset AX of Figure 2A, we can reconstruct the context—specifically the site-graph $G_{\text{AX}}$ of Figure 2B—in which rule $r_{\text{AX}}$ fires. Note that $G_{\text{AX}}$ specifies that site $2$ of $\mathtt{A}$ must be unbound. Likewise, the firing of rule $r_{\text{AY}}$ is contingent upon context $G_{\text{AY}}$, which is built up by poset AY. $G_{\text{AY}}$ requires that site $2$ of $\mathtt{A}$ be bound. These two contexts are in conflict and thus cannot be realized at the same time. This means, in turn, that there is no inhibition at this point between the two mechanisms: Whether a particular $\mathtt{A}$ gets bound to $\mathtt{X}$ or to $\mathtt{Y}$ is already decided before the mechanisms reach the events whose relationship of inhibition we queried. As a whole, the mechanisms AX and AY must interfere with one another negatively, as $\mathtt{A}$ cannot be bound to both $\mathtt{X}$ and $\mathtt{Y}$ at the same time; but the point of conflict is somewhere else. (It is between event $r_{\text{AB}}$ and $r_{\text{AY}}$.) To determine the earliest event combination at which two mechanisms conflict with one another can be done by scanning all events of one against all events of the other.

If we change the model by replacing rule $r_{\text{AB}}$ with rule $r^{\prime}_{\text{AB}}$ (Figure 3), the context for the application of rule $r_{\text{AX}}$ becomes consistent with the context of application of rule $r_{\text{AY}}$. This means both rules can fire. Since the firing of $r_{\text{AX}}$ destroys part of the context needed by $r_{\text{AY}}$ (and vice versa), the mechanisms inhibit each other at the events queried. In sum, the key in determining whether two events in the scope of distinct mechanisms are mutually exclusive consists in reconstructing from the given mechanisms the context required for both events and determining whether it can be realized. We call this critical context a “scenario”.

Related work.

The notion of rule influence, introduced in Refs. [8, 7], is used to detect inhibition and promotion between posets (Definition 18). Our approach to abstracting traces of state transitions into partial orders is similar to Refs. [17, 3], but we use more fine-grained relations on graphs (the enablement and prevention relations of Section 2.4). As a consequence, we do not need Petri nets as an intermediate encoding between state transitions and posets. In any case, our main focus is on reconstructing a trace from a poset, which is obtained from a causal structure extracted from a Kappa simulation. This extraction is the subject of Ref. [4] and outside the scope of this paper.

Outline.

In Section 2 we introduce site-graphs, the graph rewriting framework of Kappa, and the notion of rule influence. To define partial orders between events in a manner informed by rule influence, we need to take a detour via the transition system induced by the rules (Section 2.4). In order to determine the scenario that establishes enablement or prevention between posets, we need to reconstruct a trace from a poset. To this end, in Section 3, we formalize trace reconstruction as the reverse of poset abstraction from traces. In Section 4 we define a logic for expressing assertions on the posets provided as inputs. We conclude in Section 5.

Length limitations preclude a description of our implementation, which can be found at https://github.com/Kappa-Dev/PosetLogic. All constructions on site-graphs presented here can be adapted to simple graphs.

2 Graph rewriting and transition systems

2.1 Site-graphs

Let $\mathsf{A}$ be a set of agents, ranged over by $\mathrm{a},\mathrm{b}$ and $\mathsf{K}=\{A,B,..\}$ be a set of agent types, equipped with a map $\mathsf{site}:\mathsf{K}\to{\rm Nature}_{>0}$. The function $\mathsf{type}:\mathsf{A}\to\mathsf{K}$ assigns a type to each agent.

Definition 1** (Site-graph).**

A site-graph is a structure $(\mathcal{A},\mathcal{N},\mathcal{E})$ where

• •

$\mathcal{A}\subseteq\mathsf{A}$ is a set of agents;

• •

$\mathcal{N}\subseteq\mathcal{A}\times{\rm Nature}_{>0}\uplus\{\mathrm{free}\}$ is a set of nodes, with a special node $\mathrm{free}$, and where each non-$\mathrm{free}$ node is a pair $(\mathrm{a},i)$ of an agent $\mathrm{a}\in\mathcal{A}$ and site $i<\mathsf{site}(\mathsf{type}(\mathrm{a}))$;

• •

$\mathcal{E}\subseteq\mathcal{N}\times\mathcal{N}$ is a symmetric set of edges with the constraint that it is conflict-free: $\forall(n_{1},n_{2}),(n_{1}^{\prime},n_{2}^{\prime})\in\mathcal{E}$, $(n_{1}=n_{1}^{\prime}\wedge n_{2}=n_{2}^{\prime})$ $\vee$ $(n_{1}=n_{2}^{\prime}\wedge n_{2}=n_{1}^{\prime})$ $\vee$ $(\{n_{1},n_{2}\}\cap\{n_{1}^{\prime},n_{2}^{\prime}\}\subseteq\{\mathrm{free}\})$.

Definition 2** (Morphism on site-graphs).**

A morphism $f:G\to H$, for $G$ and $H$ two site-graphs, is a pair of functions $f=(v,e)$ with

• •

$v:\mathcal{A}_{G}\to\mathcal{A}_{H}$ a function on agents that preserves types: $\mathsf{type}(v(\mathrm{a}))=\mathsf{type}(\mathrm{a})$ and that can be extended to a function on nodes: $v(\mathrm{a},i)=(v(\mathrm{a}),i)$ and $v(\mathrm{free})=\mathrm{free}$, for all $\mathrm{a}\in\mathcal{A}_{G}$ and for all $i<\mathsf{site}(\mathsf{type}(\mathrm{a}))$;

• •

and $e:\mathcal{E}_{G}\to\mathcal{E}_{H}$ a function on edges such that for any two nodes $n_{1},n_{2}\in\mathcal{N}_{G}$, if $(n_{1},n_{2})\in\mathcal{E}_{G}$ then $e(n_{1},n_{2})=(v(n_{1}),v(n_{2}))$.

Site-graphs and their morphisms form a category, denoted $\mathcal{G}$. Morphisms in $\mathcal{G}$ preserve the node type and the edge structure of nodes in site-graphs. Isomorphisms are denoted with $\cong$. A mono is a morphism with injective functions on nodes and edges. We denote the empty graph with $\varepsilon$ and write $\overset{\rightarrow}{f}=\langle f_{1},f_{2}\rangle$ for the span $G_{1}\overset{f_{1}}{\leftarrow}G_{2}\overset{f_{2}}{\rightarrow}G_{3}$. The same notation is used to denote the cospan $G_{1}\overset{f_{1}}{\rightarrow}G_{2}\overset{f_{2}}{\leftarrow}G_{3}$. For simplicity, we write $f$ for $v$ (or $e$) in $f=(v,e)$. Finally, we write $\text{hom}(\mathcal{G})$ and $\text{span}(\mathcal{G})$ for the class of morphisms and spans of $\mathcal{G}$, respectively.

2.2 Graph rewriting

A rule-based model consists of graph-rewriting rules that are applied in a stochastic fashion to a typically large graph representing the state of a system. In Kappa the stochastic application of rewrite rules follows basic principles of stochastic chemical kinetics [13, 8]. Each graph-rewrite action constitutes a state transition and a temporal sequence of such transitions is a trace. We also refer to the state of the system as a “mixture”.

Definition 3** (Pushout).**

The pushout of a span $\overset{\rightarrow}{g}$ is a cospan $\overset{\rightarrow}{f}$ such that $f_{1}g_{1}=f_{2}g_{2}$222We write $fg(x)=f(g(x))$, with $x$ in the domain of $g$, for morphisms composition. and such that for any other cospan $\overset{\rightarrow}{f^{\prime}}$ for which $f_{1}^{\prime}g_{1}=f_{2}^{\prime}g_{2}$, there is a unique morphism $M\to M^{\prime}$ that makes diagram PO below commute.

In the category of site-graphs, the pushout does not always exist. For a span $\overset{\rightarrow}{g}$ of monos, if the pushout exists, then it asserts a gluing of $G_{1}$ and $G_{2}$, resulting in $M$, based on the identifications (gluing instructions) expressed by $\overset{\rightarrow}{g}$.

Definition 4** (Rule).**

A rule is a span of monos $\overset{\rightarrow}{r}=L\overset{p}{\leftarrow}K\overset{q}{\rightarrow}R$ such that for some $\mathrm{a}\in\mathcal{A}_{K}$ and $i<\mathsf{site}(\mathsf{type}(\mathrm{a}))$, if $(\mathrm{a},i)\in\mathcal{N}_{K}$ then \big{(}(q(\mathrm{a}),i),n\big{)}\in\mathcal{E}_{R}\iff\big{(}(p(\mathrm{a}),i),n^{\prime}\big{)}\in\mathcal{E}_{L}, with $n\in\mathcal{N}_{R}$ and $n^{\prime}\in\mathcal{N}_{L}$.

In site-graphs the site of an agent can be specified without specifying if the site is free or bound to another site. Formally, in a site-graph $G$ with an agent $\mathrm{a}\in\mathcal{A}_{G}$, we can have $(\mathrm{a},i)\in\mathcal{N}_{G}$ for which there is no edge $(n_{1},n_{2})\in\mathcal{E}_{G}$ such that $n_{1}=(\mathrm{a},i)$ or $n_{2}=(\mathrm{a},i)$. Rules however, need to satisfy a constraint related to sites: if an edge exists for a site in either sides of a rule, then it exists in both sides.

Definition 5** (Double-pushout rewriting [10]).**

Let $\overset{\rightarrow}{r}=L\overset{p}{\leftarrow}K\overset{q}{\rightarrow}R$ be a rule. Let $M$ be a site-graph (typically a system state) and let $m:L\rightarrow M$ be a mono, called a matching. The double pushout rewriting consists in defining the site-graph $D$, called the context graph, and the site-graph $N$ such that the two squares in diagram DPO are pushouts. We refer to the dpo rewrite of $M$ to $N$ as $M\overset{m,\overset{\rightarrow}{r}}{\Rightarrow}N$ and denote the state transition associated with the application of rule $\overset{\rightarrow}{r}=\langle p,q\rangle$ at ”location” $m$ of the system state $M$ (i.e. the mixture) as $\mathsf{mix}(M\overset{m,\overset{\rightarrow}{r}}{\Rightarrow}N)=M{\leftarrow}D{\rightarrow}N$.

PO:M^{\prime}$$O$$G_{1}$$G_{2}$$M$$g_{1}$$g_{2}$$f_{1}~{}$$~{}f_{2}$$f_{1}^{\prime}$$f_{2}^{\prime}

DPO:L$$K$$R$$M$$D$$N$$p$$q$$m

Given the definition above, a context graph $D$ need not always exist. We use dpo rewriting for the sake of simplicity, but our work extends to other graph rewriting techniques.

2.3 Influence

The postcondition resulting from the application of a rule $\overset{\rightarrow}{r_{1}}$ can satisfy or, more generally, contribute (in conjunction with other rules) to satisfying the precondition for the application of another rule $\overset{\rightarrow}{r_{2}}$. Alternatively, $\overset{\rightarrow}{r_{1}}$ might destroy the precondition of $\overset{\rightarrow}{r_{2}}$. In the former case we speak of a positive influence of $\overset{\rightarrow}{r_{1}}$ on $\overset{\rightarrow}{r_{2}}$ and, in the latter case, of a negative influence. Of course, a rule may also have no influence on a particular other rule.

Influence333Positive and negative influence were referred to as activation, inhibition or overlaps in Refs.[8, Section 3.4],[7, Section 4.2.3][14]. belongs to the realm of possibility: it is a latent relation between rules that becomes manifest as a relation between events (i.e. actual rule applications) in the specific context of a trace, as we discuss formally in Section 3.

We next define two categorical concepts needed for capturing influence. Multisums are meant to characterize all possible ways of gluing together two graphs $G_{1}$ and $G_{2}$.

Definition 6** (Multisum in the subcategory of monos).**

Let $G_{1}$ and $G_{2}$ be two graphs. The multisum of $G_{1}$ and $G_{2}$, denoted with $\mathsf{multisum}(G_{1},G_{2})$, is a family of cospans of monos $\overset{\rightarrow}{f_{i}}=\langle f_{1,i},f_{2,i}\rangle$, with $f_{j,i}:G_{j}\rightarrow M_{i}$, $i\leq n$, $j\in\{1,2\}$, such that for any other cospan of monos $\overset{\rightarrow}{f^{\prime}}$, with $f_{j}^{\prime}:G_{j}\rightarrow M^{\prime}$, there exists an $M_{k}$, $k\leq n$ and a unique mono $M_{k}\rightarrow M^{\prime}$ that makes diagram MS below commute. Moreover, for any monos $M_{k}\rightarrow M^{\prime}$ and $M_{i}\rightarrow M^{\prime}$, $i,k\leq n$, for which diagram MS commutes, we have $M_{k}\cong M_{i}$.

Unlike other constructions, which are defined in $\mathcal{G}$, multisums are defined in the subcategory of $\mathcal{G}$ whose morphisms are restricted to monos. Multisums always exists in this subcategory.

Definition 7** (Pullback).**

The pullback of the cospan $\overset{\rightarrow}{f}$ consists of a span $\overset{\rightarrow}{g}$ such that $f_{1}g_{1}=f_{2}g_{2}$. In addition, for any other span $\overset{\rightarrow}{g^{\prime}}$ such that $f_{1}g_{1}^{\prime}=f_{2}g_{2}^{\prime}$, there is a unique morphism $O^{\prime}\to O$ that makes diagram PB commute.

MS:G_{1}$$G_{2}$$M_{1}$$\cdots$$M_{k}$$\cdots$$M_{n}$$M^{\prime}$$f_{1}^{\prime}$$f_{2}^{\prime}

PB:O$$G_{1}$$G_{2}$$M$$O^{\prime}$$g_{1}$$g_{2}$$f_{1}~{}$$~{}f_{2}$$g_{1}^{\prime}$$g_{2}^{\prime}

The pullback always exists in $\mathcal{G}$. Using these notions we can define influence.

Definition 8** (Positive influence [14]).**

Given two rules $\overset{\rightarrow}{r_{1}}=L_{1}{\leftarrow}K_{1}\overset{i}{\rightarrow}R_{1}$ and $\overset{\rightarrow}{r_{2}}=L_{2}{\leftarrow}K_{2}{\rightarrow}R_{2}$, consider an overlap between $R_{1}$ and $L_{2}$, i.e. a cospan $\overset{\rightarrow}{f}\in\mathsf{multisum}(R_{1},L_{2})$, and let $\overset{\rightarrow}{g}$ be the pullback of $\overset{\rightarrow}{f}$. Moreover, let $\overset{\rightarrow}{h}$ be the pullback of $\langle i,g_{1}\rangle$. The rule $\overset{\rightarrow}{r_{1}}$ has a positive influence on rule $\overset{\rightarrow}{r_{2}}$, if $h_{2}$ is not an iso. In other words, if $O$ is not contained in $P$ and, thus, in $K_{1}$. The influence is induced by the overlap $\overset{\rightarrow}{g}$ corresponding to $\overset{\rightarrow}{f}$ and is denoted by $\overset{\rightarrow}{r_{1}}\mathrel{\xrightarrow{+\overset{\rightarrow}{g}}}\overset{\rightarrow}{r_{2}}$.

The diagram on the right depicts the relationships used in Definition 8. The rule $\overset{\rightarrow}{r_{1}}$ has a positive influence on $\overset{\rightarrow}{r_{2}}$ if it creates a subgraph of $L_{2}$. By requiring $h_{2}$ not to be an iso, we assert that $O$ is not already present in $L_{1}$ and must, therefore, be produced by $\overset{\rightarrow}{r_{1}}$. Negative influence $\overset{\rightarrow}{r_{1}}\mathrel{\xrightarrow{-\overset{\rightarrow}{g}}}\overset{\rightarrow}{r_{2}}$ is defined analogously, but with $\overset{\rightarrow}{g}$ now the pullback of a cospan $\overset{\rightarrow}{f}\in\mathsf{multisum}(L_{1},L_{2})$ between the left hand sides: $\overset{\rightarrow}{r_{1}}$ has a negative influence on $\overset{\rightarrow}{r_{2}}$, if it destroys a subgraph of $L_{2}$.

Example 1**.**

The rule $\overset{\rightarrow}{r_{1}}$ has a positive influence on $\overset{\rightarrow}{r_{2}}$, because $\overset{\rightarrow}{r_{1}}$ produces an agent $\mathtt{B}$ needed for a subsequent application of $\overset{\rightarrow}{r_{2}}$ shown in Figure 4. Similarly $\overset{\rightarrow}{r_{2}}$ has a negative influence on $\overset{\rightarrow}{r_{1}}$ since it erases an agent $\mathtt{A}$ needed by $\overset{\rightarrow}{r_{1}}$.

2.4 Transition systems

Following Refs. [10, 3] we introduce the notion of transition system (TS) on state graphs and an independence relation between transitions. We then propose new relations of enablement and prevention between transitions, based on the notions of rule influence just defined, and connect them to independence.

Definition 9** (TS on graphs [10]).**

A transition system $TS=(Q,\mathcal{R},T)$ on graphs consists of:

• •

a set of states $Q\subseteq\mathcal{G}$, where each state is a graph;

• •

a set of rules $\mathcal{R}$;

• •

a set of labeled transitions $T\subseteq Q\times\text{hom}(\mathcal{G})\times\mathcal{R}\times Q$, where each transition $t$ is a dpo rewriting step $M\overset{m,\overset{\rightarrow}{r}}{\Rightarrow}N$ with $M,\,N\in Q$, an underlying rule $\overset{\rightarrow}{r}:L\leftarrow K\rightarrow R\in\mathcal{R}$, and a matching $m:L\rightarrow M\in\text{hom}(\mathcal{G})$.

Transitions can be composed $t_{1};t_{2}$ if the source state of $t_{2}$ matches the destination state of $t_{1}$. A trace $\theta$ is a (possibly empty) sequence of composable transitions: $\theta=t_{1};t_{2};\cdots;t_{n}$.

Definition 10** (Independence relation on transitions [10]).**

Let $t_{1}:M\overset{m_{1},\overset{\rightarrow}{r_{1}}}{\Rightarrow}M_{1}$, $t_{2}:M_{1}\overset{m_{2},\overset{\rightarrow}{r_{2}}}{\Rightarrow}M_{2}$ and $t_{3}:M\overset{m_{3},\overset{\rightarrow}{r_{3}}}{\Rightarrow}M_{3}$ be transitions with underlying rules $\overset{\rightarrow}{r_{i}}=L_{i}{\leftarrow}K_{i}{\rightarrow}R_{i}\in\mathcal{R}$, $i\in\{1,2,3\}$ and corresponding matchings $m_{i}$ as indicated in the diagrams below.

sequential independence

$t_{1}$ and $t_{2}$ are sequentially independent, written $t_{1}\Diamond_{\text{seq}}t_{2}$, iff there exist morphisms $i:R_{1}\rightarrow D_{2}$ and $j:L_{2}\rightarrow D_{1}$ such that $f_{2}i=n_{1}$ and $g_{1}j=m_{2}$.

parallel independence

$t_{1}$ and $t_{3}$ are parallel independent, written $t_{1}\Diamond_{\text{par}}t_{3}$, iff there exist morphisms $i:L_{1}\rightarrow D_{3}$ and $j:L_{3}\rightarrow D_{1}$ such that $f_{3}i=m_{1}$ and $f_{1}j=m_{3}$.

R_{1}$$M_{1}$$L_{2}$$D_{1}$$K_{1}$$D_{2}$$K_{2}$$L_{1}$$M$$R_{2}$$M_{2}sequential independenceg_{1}$$f_{2}$$m_{2}$$n_{1}$$m_{1}

L_{1}$$M$$L_{3}$$D_{1}$$K_{1}$$D_{3}$$K_{3}$$R_{1}$$M_{1}$$R_{3}$$M_{3}parallel independencef_{1}$$f_{3}$$m_{3}$$m_{1}

In the following, we use the function $\mathsf{mix}$ (of Definition 5) to chain transitions by span composition (see diagrams below). Given two spans $\overset{\rightarrow}{f}=\langle f_{1},f_{2}\rangle$ and $\overset{\rightarrow}{g}=\langle g_{1},g_{2}\rangle$, we define their composition as $\overset{\rightarrow}{g}\overset{\rightarrow}{f}=\langle f_{1}h_{1},g_{2}h_{2}\rangle$ where $\overset{\rightarrow}{h}$ is the pullback of $\langle f_{2},g_{1}\rangle$. A partial morphism $f:M_{1}\rightharpoonup M_{3}$ is a total morphism from the subgraph $\text{dom}(f)$ of $M_{1}$ to $M_{3}$, that is $f:M_{1}\supseteq\text{dom}(f)\to M_{3}$. Given a span $M_{1}\overset{l}{\leftarrow}D\overset{r}{\rightarrow}M_{3}$, its corresponding partial morphism, denoted $M_{1}\rightharpoonup M_{3}$, is defined on $l(D)$ as $l^{-1}r$ and undefined otherwise [11].

M_{1}$$D_{1}$$M_{2}$$D_{2}$$M_{3}$$D$$f_{1}$$f_{2}$$g_{1}$$g_{2}$$h_{1}$$h_{2}

M_{1}$$M_{3}$$D$$l$$r

Definition 11** (Causality).**

Let $t_{1}:M_{1}\overset{m_{1},\overset{\rightarrow}{r_{1}}}{\Rightarrow}N_{1}$ and $t_{2}:M_{2}\overset{m_{2},\overset{\rightarrow}{r_{2}}}{\Rightarrow}N_{2}$ be two transitions bracketing a trace $\theta:t_{1};t_{1}^{\prime};t_{2}^{\prime};\cdots;t_{n}^{\prime};t_{2}$. The rules inducing $t_{i},i\in\{1,2\}$, are $\overset{\rightarrow}{r_{i}}=L_{i}{\leftarrow}K_{i}{\rightarrow}R_{i}$ with matchings $m_{i}\in\text{hom}(\mathcal{G})$ into $M_{1}$ and $M_{2}$, respectively.

enablement

Let $\overset{\rightarrow}{g}$ be a span such that $\overset{\rightarrow}{r_{1}}\mathrel{\xrightarrow{+\overset{\rightarrow}{g}}}\overset{\rightarrow}{r_{2}}$. If the diagram below on the left commutes then $t_{1}$ enables $t_{2}$, denoted $t_{1}<_{\theta}t_{2}$. In the diagram below on the left, the partial morphism $N_{1}\rightharpoonup M_{2}$ is obtained from the composition of $\mathsf{mix}(t_{1}^{\prime})\circ\dots\circ\mathsf{mix}(t_{n}^{\prime})$.

prevention

Let $\overset{\rightarrow}{g}$ be a span such that $\overset{\rightarrow}{r_{2}}\mathrel{\xrightarrow{-\overset{\rightarrow}{g}}}\overset{\rightarrow}{r_{1}}$. If the diagram below on the right commutes then $t_{2}$ prevents $t_{1}$, denoted $t_{2}\dashv_{\theta}t_{1}$. In the diagram below on the right the partial morphism $M_{1}\rightharpoonup M_{2}$ is the composition of $\mathsf{mix}(t_{1})\circ\mathsf{mix}(t_{1}^{\prime})\circ\dots\circ\mathsf{mix}(t_{n}^{\prime})$.

O$$M_{1}$$D_{1}$$N_{1}$$N_{2}$$D_{2}$$M_{2}$$R_{1}$$K_{1}$$L_{1}$$L_{2}$$K_{2}$$R_{2}enablementg_{1}$$g_{2}

O$$M_{1}$$M_{2}$$L_{1}$$L_{2}preventiong_{1}$$g_{2}

To make the underlying span explicit, we sometimes write $(t_{1},t_{2},\overset{\rightarrow}{g})\in<_{\theta}$ and $(t_{1},t_{2},\overset{\rightarrow}{g})\in\dashv_{\theta}$.

Example 2**.**

Consider the trace of Figure 5. The first transition enables the second and third transitions. The second transition enables the last transition. However, it is a “delayed” enabler: it partially fulfills the precondition of the last transition, but the third transition has to happen before. Note that such type of causality is not captured by the graph rewriting framework of [10, 3, 16]444For immediate transitions, enablement and prevention coincide with the sequential dependence and critical pairs, respectively, of Refs. [10, 3, 16]. See the appendix for more details.. Lastly note that the third transition is a preventer for the second one.

3 Posets of graph rewriting events

In this section we abstract a trace into a poset of events, and concretize a poset back into a set of traces. Each transition becomes an event in a poset with the underlying rule as its label. Similarly, in the concretization, each event in a poset corresponds to a transition such that transitions compose into a trace. The abstraction is used to reduce the number of simulation traces to a small set of posets, and the concretization recomputes a “representative” trace from each poset. Concretized traces are used in the next section.

3.1 From traces to posets

A transition $t$ (Definition 5) is a pair of spans—$\mathsf{mix}(t)=M\leftarrow D\rightarrow N$ and the underlying rule $\overset{\rightarrow}{r}:L\leftarrow K\rightarrow R$—and a matching $m:L\to M$. When abstracting a trace into a partial order, we drop the span $\mathsf{mix}(t)$ and $m$. The enabling and prevention relations between transitions in a trace (Section 2.4) translate into a partial order on events, labeled by the underlying rules.

We proceed in two steps. Enabling and prevention between transitions hinge on positive and negative influence between the underlying rules (see Definition 11). Recall that when transition $t$ enables transition $t^{\prime}$ within a trace $\theta$ there exists a span $\overset{\rightarrow}{f}$ for which $(t,t^{\prime},\overset{\rightarrow}{f})\in<_{\theta}$. The first abstraction, $\mathcal{A}_{1}$, forgets the matching and the span $\mathsf{mix}(t)$ of a transition $t$, but preserves enablement and prevention relations between transitions and the positive and negative influence between the underlying rules.

Definition 12** (Abstraction step 1).**

Let $\theta=t_{1};t_{2};\cdots;t_{n}$ be a trace and $E=\{e_{1},e_{2},\cdots,e_{n}\}$555We can define a function $\text{id}:T\to{\rm Nature}$ from transitions to natural numbers such that $\text{id}(t_{i})=i$. The set of events is then $E=\{1,2,\cdots n\}$. be a set of events. Events are labeled using a function $\ell:E\to\mathcal{R}$ such that $\ell(e_{i})=r_{i}$ if $t_{i}:M_{i}\overset{m_{i},\overset{\rightarrow}{r_{i}}}{\Rightarrow}N_{i}$, for $i\leq n$. We then define two relations $\mathrel{\cdot\xrightarrow{+\cdot}\cdot},\mathrel{\cdot\xrightarrow{-\cdot}\cdot}\subseteq E\times E\times\text{span}(\mathcal{G})$:

$e_{i}\mathrel{\xrightarrow{+\overset{\rightarrow}{f}}}e_{j}\iff(t_{i},t_{j},\overset{\rightarrow}{f})\in<_{\theta}$ and $e_{i}\mathrel{\xrightarrow{-\overset{\rightarrow}{f}}}e_{j}\iff(t_{i},t_{j},\overset{\rightarrow}{f})\in\dashv_{\theta}$,

for $e_{i},e_{j}\in E$, $i,j\leq n$ and $\overset{\rightarrow}{f}\in\text{span}(\mathcal{G})$. We denote this first abstraction of $\theta$ with $\mathcal{A}_{1}(\theta)=(E,\ell,\mathrel{\xrightarrow{+}},\mathrel{\xrightarrow{-}})$.

The notation $e\mathrel{\xrightarrow{+\overset{\rightarrow}{f}}}e^{\prime}$, for some span $\overset{\rightarrow}{f}$, overloads the notation $\ell(e)\mathrel{\xrightarrow{+\overset{\rightarrow}{f}}}\ell(e^{\prime})$. Keep in mind, however, that the first is defined on events whereas the second can be inferred from the rules on which it holds (see Definition 8).

In the second abstraction step, $\mathcal{A}_{2}$, we map the relations $\mathrel{\xrightarrow{+}}$ and $\mathrel{\xrightarrow{-}}$ to corresponding partial orders on events. This step simply forgets the spans responsible for the enablement and prevention relations on transitions.

Definition 13** (Abstraction step 2).**

Let $E$ be a set of events equipped with a labeling function $\ell:E\to\mathcal{R}$ and two relations $\mathrel{\cdot\xrightarrow{+\cdot}\cdot},\mathrel{\cdot\xrightarrow{-\cdot}\cdot}\subseteq E\times E\times\text{span}(\mathcal{G})$. We translate the relations on events from Definition 12 into two new relations $<,\Vdash\subseteq E\times E$:

[TABLE]

The associated poset is defined as $\mathcal{A}_{2}(E,\ell,\mathrel{\xrightarrow{+}},\mathrel{\xrightarrow{-}})=(E,\ell,\leq,\vdash)$, where $\leq$ and $\vdash$ are the transitive and reflexive closure of $<$ and $\Vdash$, respectively. We call the two relations $\leq$ and $\vdash$, (enabling) precedence and non-enabling precedence, respectively666In order to not introduce unnecessary terminology, we abuse the term poset to mean the structure $(E,\ell,\leq,\vdash)$ where the set of events $E$ is equipped with two partial orders. We could instead define $(E,\ell,(<\cup\Vdash)^{\star})$ but in this case we forget the distinction between $<$ and $\Vdash$..

Lemma 1**.**

Let $\theta$ be a trace and let $e,e^{\prime}\in E$ be two events with $\mathcal{A}_{2}\mathcal{A}_{1}(\theta)=(E,\ell,\leq,\vdash)$. If $e<e^{\prime}$ then there exists a span $\overset{\rightarrow}{f}$ such that $\ell(e)\mathrel{\xrightarrow{+\overset{\rightarrow}{f}}}\ell(e^{\prime})$. Similarly, if $e\Vdash e^{\prime}$, then there exists a span $\overset{\rightarrow}{f}\in\text{span}(\mathcal{G})$ such that $\ell(e^{\prime})\mathrel{\xrightarrow{-\overset{\rightarrow}{f}}}\ell(e)$.

A morphism on posets is a function on events that preserves labels and the two precedence relations. An isomorphism between two posets $s_{1}$ and $s_{2}$ is denoted by $s_{1}\cong s_{2}$. For a set of traces $\Theta=\{\theta_{1},\cdots,\theta_{n}\}$, we write $\mathcal{S}=(s_{1},\cdots,s_{k})/_{\cong}\text{ with }k\leq n$ for the set of posets obtained via $\mathcal{A}_{2}\mathcal{A}_{1}$ and quotiented by iso.

Example 3**.**

Consider the trace $\theta=t_{1};t_{2};t_{3};t_{4}$ of Example 2. The corresponding poset consists of the events $\{e_{1},e_{2},e_{3},e_{4}\}$ with the relations $<=\{(e_{1},e_{2});(e_{1},e_{3});$ $(e_{2},e_{4});(e_{3},e_{4})\}$ and $\Vdash=\{(e_{2},e_{3})\}$. Note that $e_{2}$ is a non-enabling precedent of $e_{3}$, as in the original trace transition $t_{3}$ prevents transition $t_{2}$.

3.2 From posets to traces

We next specify the concretization from posets to traces. Again, we proceed in two steps. The first concretization retrieves the intermediate structure $(E,\ell,\mathrel{\xrightarrow{+}},\mathrel{\xrightarrow{-}})$ from a poset $(E,\ell,\leq,\vdash)$. This step recovers the influence (positive or negative) between the rules underlying two events that are in a particular precedence or non-enabling precedence relation.

Definition 14** (Concretization step 1).**

Let $(E,\ell,\leq,\vdash)$ be a poset. We define the relations $\mathrel{\xrightarrow{+}},\mathrel{\xrightarrow{-}}\subseteq E\times E\times\text{span}(\mathcal{G})$ as follows:

• •

$e_{i}\mathrel{\xrightarrow{+\overset{\rightarrow}{f}}}e_{j}\iff\ell(e_{i})\mathrel{\xrightarrow{+\overset{\rightarrow}{f}}}\ell(e_{j})$ and $e_{i}<e_{j}$, for some $\overset{\rightarrow}{f}\in\text{span}(\mathcal{G})$;

• •

$e_{i}\mathrel{\xrightarrow{-\overset{\rightarrow}{f}}}e_{j}\iff\ell(e_{i})\mathrel{\xrightarrow{-\overset{\rightarrow}{f}}}\ell(e_{j})$ and $e_{j}\Vdash e_{i}$, for some $\overset{\rightarrow}{f}\in\text{span}(\mathcal{G})$

where $<$ and $\Vdash$ are the reduced relation of $\leq$ and $\vdash$, respectively. The concretization of a poset is then $\mathcal{C}_{1}(E,\ell,\leq,\vdash)=(E,\ell,\mathrel{\xrightarrow{+}},\mathrel{\xrightarrow{-}})$.

Example 4**.**

Consider a poset of events $e_{1},e_{2}$ and $e_{3}$ with labels $\overset{\rightarrow}{r_{1}}$, $\overset{\rightarrow}{r_{2}}$ and $\overset{\rightarrow}{r_{3}}$, respectively, as shown in Figure 6. Furthermore, suppose that events $e_{1}$ and $e_{2}$ both precede $e_{3}$. For the pair $e_{1}<e_{3}$, one can infer the positive influence $\overset{\rightarrow}{r_{1}}\mathrel{\xrightarrow{+\overset{\rightarrow}{f}}}\overset{\rightarrow}{r_{3}}$. For the pair $e_{2}<e_{3}$, we need to consider two possibilities: either

$\overset{\rightarrow}{r_{2}}\mathrel{\xrightarrow{+\overset{\rightarrow}{g}}}\overset{\rightarrow}{r_{3}}$ or $\overset{\rightarrow}{r_{2}}\mathrel{\xrightarrow{+\overset{\rightarrow}{h}}}\overset{\rightarrow}{r_{3}}$. The relation induced by the span $\overset{\rightarrow}{g}$ is problematic. Intuitively, the events $e_{1}$ and $e_{2}$ should produce a distinct set of agents for event $e_{3}$. Specifically, both cannot produce the same agent $\mathtt{A}$ that binds to $\mathtt{B}$ in $e_{3}$. The consistent span attributes the creation of agent $\mathtt{A}$ to $e_{1}$ and the creation of $\mathtt{B}$ to $e_{2}$ (in addition to a further $\mathtt{A}$ not used in $e_{3}$). In this manner, both $e_{1}$ and $e_{2}$ are necessary for the occurence of $e_{3}$.

As the example indicates, it is not trivial to retrieve the influence between events from the influence between rules. The problem is that influence between events is a global property of the poset, whereas influence between rules is local to the two rules. Lack of space prevents us from characterizing the correct concretizations of a poset. Informally, a concretization of a poset $s$ is correct if (i) every relation on events in $s$ is due to a shared resource (i.e. an agent or an edge) and if (ii) every resource in $s$ is consistent throughout $s$.

The second concretization maps events into transitions such that: (i) the transitions compose into a valid trace and (ii) the relations defined on the events hold on the transitions of the trace. We call a candidate for concretization any function from events to transitions that satisfies condition (i).

Definition 15**.**

Let $E$ be a set of events with a labeling function $\ell:E\to\mathcal{R}$ and a total order on events $\sqsubset\subseteq E\times E$. A function $\mathsf{concrete}:E\to T$ is called a candidate for concretization if $\mathsf{concrete}(e)=M\overset{m,\overset{\rightarrow}{r}}{\Rightarrow}N$ such that $\ell(e)=\overset{\rightarrow}{r}$, for some graphs $M,N$, and a morphism $m$. Moreover $\mathsf{concrete}(e_{1});\cdots;\mathsf{concrete}(e_{n})$, with $e_{i}\sqsubset e_{i+1}$, $i\leq n$, compose into a trace.

Any such function must also satisfy condition (ii), as in the following definition.

Definition 16** (Concretization step 2).**

Let $E$ be a set of events equipped with a function $\ell:E\to\mathcal{R}$ and two relations $\mathrel{\cdot\xrightarrow{+\cdot}\cdot},\mathrel{\cdot\xrightarrow{-\cdot}\cdot}\subseteq E\times E\times\text{span}(\mathcal{G})$. Let $\sqsubset$ be a total order on events and let $\mathsf{concrete}:E\to T$ be a function from events to transitions such that the following hold:

• •

$(t_{i},t_{j},\overset{\rightarrow}{f})\in<_{\theta}\iff e_{i}\mathrel{\xrightarrow{+\overset{\rightarrow}{f}}}e_{j}$ and

• •

$(t_{i},t_{j},\overset{\rightarrow}{f})\in\dashv_{\theta}\iff e_{i}\mathrel{\xrightarrow{-\overset{\rightarrow}{f}}}e_{j}$

for $e_{i},e_{j}\in E$, $i,j\leq n$. Then the concretized trace is $\mathcal{C}_{2}(E,\ell,\mathrel{\xrightarrow{+}},\mathrel{\xrightarrow{-}},\mathsf{concrete},\sqsubset)$ $=$ $\mathsf{concrete}(e_{1});\cdots;$ $\mathsf{concrete}(e_{n})$, for $e_{i}\sqsubset e_{i+1}$, $i\leq n$.

For $(E,\ell,\leq,\dashv)$ a poset, we write $\mathcal{C}(E,\ell,\leq,\dashv)$ for the set of all possible concretisations, i.e. the set of all traces $\theta$ as specified by $\mathcal{C}_{1}(E,\ell,\leq,\dashv)$ and $\mathcal{C}_{2}(E,\ell,\mathrel{\xrightarrow{+}},\mathrel{\xrightarrow{-}},\mathsf{concrete},\sqsubset)$. We write $(\theta,\mathsf{concrete})\in\mathcal{C}(E,\ell,\leq,\dashv)$ for the concretization function used in reconstructing a particular $\theta$.

Theorem 1**.**

Let $\theta$ be a trace. Then $\theta\in\mathcal{C}\mathcal{A}_{2}\mathcal{A}_{1}(\theta)$. Moreover, for any trace $\theta^{\prime}\in\mathcal{C}\mathcal{A}_{2}\mathcal{A}_{1}(\theta)$, $\mathcal{A}_{2}\mathcal{A}_{1}(\theta)\cong\mathcal{A}_{2}\mathcal{A}_{1}(\theta^{\prime})$.

4 A logic on posets

In Figure 7 we define a fragment of a first order logic that can be used to express assertions about positive and negative influence between mechanisms, that is, posets. We interpret the logic on the set of posets $\mathcal{S}$, ranged over by $s$, and on the set of events $\mathcal{E}=\cup_{s_{i}\in S}E_{s_{i}}$, where $E_{s_{i}}$ is the set of events in $s_{i}$. To distinguish between the partial orders of different posets in $\mathcal{S}$, we write $s=(E_{s},\leq_{s},\vdash_{s},\ell_{s})$. In the following, $x$ stands for variables, $t$ for terms and the superscripts $e$ and $s$ indicate whether the variables and terms range over events or posets, respectively. Formulas are denoted by $\varphi$ and are built from predicates on variables and terms.

A valuation for $\varphi$ is a function $v:\text{fv}(\varphi)\to\mathcal{E}\uplus\mathcal{S}$ from the set of free variables of $\varphi$ to the set of events and posets. The evaluation of $\varphi$ is defined below and requires a valuation function $v$ for the set of free variables of $\varphi$; the evaluation is therefore parametric on $v$. We use two functions, one to evaluate terms $\{\}_{v}:t\to\mathcal{E}\uplus\mathcal{S}$ and one to evaluate formulas $[\![]\!]_{v}:\varphi\to\{T,F\}$. A formula $\varphi$ is satisfiable if there exists $v$ such that $[\![\varphi]\!]_{v}$ evaluates to true. The interpretation of formulas and terms is shown in Figure 8.

Example 5**.**

We return to the introductory example. The mechanisms of binding an agent $\mathtt{A}$ to an agent $\mathtt{X}$ or to an agent $\mathtt{Y}$ consist in the application of rule $\overset{\rightarrow}{r_{\text{AX}}}$ and $\overset{\rightarrow}{r_{\text{AY}}}$, respectively. The assertion that the first mechanism prevents (or conflicts with) the second is written as $\exists e_{1}.(e_{1}\in s_{1}\wedge\ell(e_{1})=\overset{\rightarrow}{r_{\text{AX}}})\wedge\exists e_{2}.(e_{2}\in s_{2}\wedge\ell(e_{2})=\overset{\rightarrow}{r_{\text{AY}}})\wedge e_{1}\in s_{1}\overset{-}{\leadsto}e_{2}\in s_{2}$. The logic allows us to formulate more complex mechanisms. For our example, we can write $\exists e.e\in s\wedge\ell(e)=\overset{\rightarrow}{r_{\text{AX}}}\vee\ell(e)=\overset{\rightarrow}{r_{\text{AY}}}$ for a mechanism that produces $\mathtt{A}$ bound to either $\mathtt{X}$ or $\mathtt{Y}$.

The predicates $e_{1}\in s_{1}\overset{+}{\leadsto}e_{2}\in s_{2}$ and $e_{1}\in s_{1}\overset{-}{\leadsto}e_{2}\in s_{2}$ check for enablement and prevention between two posets. Informally, $e_{1}$ and $e_{2}$ represent the ”meeting point” of the two posets $s_{1}$ and $s_{2}$. We use these events to reconstruct a graph that represents a context in which $s_{1}$ enables or prevents $s_{2}$.

The causal past of an event is the set of events that preceded it. We denote with $[e]_{s}$ the causal past of an event $e\in E_{s}$ and define $[e]_{s}=(E^{\prime},\leq^{\prime},\vdash^{\prime},\ell^{\prime})$ with $E^{\prime}=\{e^{\prime}:e^{\prime}\in E,e^{\prime}\leq e\}$ and $\leq^{\prime},\vdash^{\prime},\ell^{\prime}$ defined like $\leq,\vdash,\ell$ but restricted to $E^{\prime}$.

Definition 17** (Occurrence context of an event in a poset).**

Let $s$ be a poset and let $e\in E_{s}$ be an event. Furthermore, let $(\theta,\mathsf{concrete})\in\mathcal{C}([e]_{s})$ be a concretization of $[e]_{s}$. We say that a morphism $m$ is an occurrence context of $e$ in $s$ if $\mathsf{concrete}(e)=M\overset{m,\ell(e)}{\Rightarrow}N$, for some graphs $M,N$.

The occurrence context of $e_{1}$ in $s_{1}$ and of $e_{2}$ in $s_{2}$ is specified by matchings $m_{1}:L_{1}\to M_{1}$ and $m_{2}:L_{2}\to M_{2}$, respectively. The diagram on the right illustrates the prevention of $s_{2}$ by $s_{1}$. Since the graph $M$ contains both $M_{1}$ and $M_{2}$, both events $e_{1}$ and $e_{2}$ can occur in that context. We then say that $M$ is a scenario for the prevention of $s_{2}$ by $s_{1}$, which is induced by a negative influence between the underlying rules, $\ell(e_{1})\mathrel{\xrightarrow{-\overset{\rightarrow}{f}}}\ell(e_{2})$. The scenario graph $M$ is formally defined as follows.

Definition 18** (Scenario for prevention).**

Let $m_{i}$ be an occurrence context of event $e_{i}$ in the poset $s_{i}$, $i\in\{1,2\}$. Let $\overset{\rightarrow}{f}$ be a span such that $\ell(e_{1})\mathrel{\xrightarrow{-\overset{\rightarrow}{f}}}\ell(e_{2})$. Define the span $\overset{\rightarrow}{g}=\langle g_{1},g_{2}\rangle$ as $g_{i}=m_{i}f_{i}$, $i\in\{1,2\}$. We say that the graph $M$ obtained by the pushout $\overset{\rightarrow}{g}$ is a scenario (graph) for the prevention of $e_{2}\in s_{2}$ by $e_{1}\in s_{1}$.

Example 6**.**

Let $L_{1}$, $L_{2}$ be the left hand sides of rules $r_{\text{AX}}$ and $r_{\text{AY}}$ from Figure 2. We have a negative influence between the rules $r_{\text{AX}}$ and $r_{\text{AY}}$ induced by the agent $\mathtt{A}$. The occurence context of $e_{\text{AX}}$ in the poset AX is obtained from the concretization of the poset AX and consists of the morphism $L_{1}\to G_{\text{AX}}$. Similarly the occurence context of $e_{\text{AY}}$ in the poset AY is $L_{2}\to G_{\text{AY}}$. There is no scenario for prevention as the graph $G$ (in Figure 2) is not a site-graph.

In a similar manner we interpret the enabling relation between two mechanisms. The predicate $(e_{1}\in s_{1}\overset{+/-}{\leadsto}e_{2}\in s_{2})$ returns true if there exists a scenario $M$ as defined above. The pushout does not always exists and, in consequence, mechanisms do not always interact with one another.

The logic is implemented as a systematic inspection of each poset. The set of posets does not have in itself a structure, and therefore there is no smart strategy for deciding whether a formula holds. The point of the logic is to give a formal language and an interpretation for influence between posets.

Example 7**.**

Let us look at a Kappa model slightly more complicated than the one in the Introduction. We give the rules in the figure below. The two posets build up the graphs $G_{\text{AX}}$ and $G_{\text{AY}}$. Then there are two “resources” which can produce an inhibition between the two posets. They produce two scenario graphs for inhibition $G_{1}$ and $G_{2}$, shown in Figure 9.

Let us change rule $r^{\prime}_{\text{AB}}$ into $r^{\prime\prime}_{\text{AB}}$ and keep everything else the same. With the new rule the graph build up by Poset AX requires the site $2$ of agent $C$ to be free. In this case only one scenario for inhibition can still occur, shown in Figure 10.

5 Conclusions

Given a categorical notion of graph rewrite system, we defined positive and negative influence between rules. This allowed us to define sequential and parallel independence between state transitions and the relations of enablement and prevention. These were then lifted to the poset abstraction of a trace of state transitions, where they became enabling and non-enabling precedence relations within a poset. The formulation of a logic on posets then allows us to formulate questions about enablement and prevention relations between posets. We ended by specifying how the concretization of posets back into a trace provides a scenario graph that establishes the truth (or falsity) of a statement about poset interaction. These notions, together with their implementation, are meant to assist a modeler in checking the consistency between observations and the mechanisms that are implied by a rule-based model.

Acknowledgements. We gratefully acknowledge illuminating discussions with Russ Harmer, Jerome Feret, and Jonathan Laurent. Special thanks to Pierre Boutillier for his help in developing and integrating the model checker resulting from this contribution into the Kappa software framework.