A Graph-Based Tool to Embed the π-Calculus into a Computational DPO Framework Jakob L. Andersen1 , Marc Hellmuth2 , Daniel Merkle1,3 , Nikolai Nøjgaard1,2 , and Marco Peressotti1 1 Department of Mathematics and Computer Science, University of Southern Denmark, Odense, DK {jlandersen,daniel,nojgaard,peressotti}@imada.sdu.dk 2 Institute of Mathematics and Computer Science, University of Greifswald, DE mhellmuth@mailbox.org 3 Harvard Medical School, Department of Systems Biology, Boston, MA, US Abstract Graph transformation approaches have been successfully used to analyse and design chemical and biological systems. Here we build on top of a DPO framework, in which molecules are modelled as typed attributed graphs and chemical reactions are modelled as graph trans- formations. Edges and vertexes can be labelled with first-order terms, which can be used to encode, e.g., steric information of molecules. While targeted to chemical settings, the computational framework is intended to be very generic and applicable to the exploration of arbitrary spaces derived via iterative application of rewrite rules, such as process calculi like Milner’s π-calculus. To illustrate the generality of the framework, we introduce EpiM: a tool for computing execution spaces of π-calculus processes. EpiM encodes π-calculus processes as typed attributed graphs and then exploits the existing DPO framework to compute their dynam- ics in the form of graphs where nodes are π-calculus processes and edges are reduction steps. EpiM takes advantage of the graph-based represent- ation and facilities offered by the framework, like efficient isomorphism checking to prune the space without resorting to explicit structural equi- valences. EpiM is available as an online Python-based tool. Keywords: Double Pushout, Process Calculi, Typed Attributed Graphs, Graph Isomorphism 1 Introduction Graph transformation approaches have been shown to provide formalisms that elegantly facilitate the construction of reaction rules in organic chemistry and biology [2, 10, 14]. Many of these frameworks, while aimed at modelling organic chemistry and biology, are constructed as generic foundations which can be used to model in a wider variety of domains. The framework focused on in this paper is MØD and is traditionally used to model organic chemistry [2, 3]. Here, graphs represent molecules, transforma- tion rules specify how molecules can interact, and direct derivations represent Copyright c 2020 for this paper by its authors. Use permitted under Creative Com- mons License Attribution 4.0 International (CC BY 4.0). 121 122 Andersen et al. concrete chemical reactions. Specifically, graph transformations are in MØD per- formed with the double-pushout (DPO) approach, with injective graph morph- isms [11, 13]. A higher-level “strategy framework” then allows for programming the sequence of rules to apply on sets of graphs, while performing the necessary graph isomorphism checks [1]. Additionally, graphs in MØD are labelled with first- order terms which allows for the specification of even more abstract rules with named variables as attributes. In this paper we will use the foundational framework of MØD to implement a tool for computing execution spaces of π-calculus processes. π-calculus is a process algebra that, like all process algebras, is concerned with the problem of formally modelling concurrent systems [18,19]. A process in π-calculus represents a “unit” of computation. In a concurrent system several of such processes can run concurrently and communication between processes occurs via channels on which channel names are sent. Given a set of processes, all running concurrently, the execution space is then all possible state transitions up to structural congruence. The modelling of π-calculus as a graph transformation system is not a new concept [12, 17]. Similarly, tools already exist that simulates π-calculus [7, 20]. Few tools, however, simulates the execution space of a process up to structural congruence, and no tools, to our knowledge, does this by using established graph transformation concepts such as the DPO approach. Here, we present the tool EpiM, which is a Python-based library that embeds the language of π-calculus into the framework of MØD. It allows the modelling of processes as simple Python expressions which are then encoded into graphs. The execution space of processes is modelled as a set of transformation rules applied on their corresponding graph encodings. Structural congruence is checked using efficient graph isomorphism checking of graphs labelled with first-order terms provided by MØD. The encoding and the simulation of process communication via graph transformations are based on the results established in [12], with the notable modification that our encoding obtains simple labelled graphs, while their model is concerned with directed typed hypergraphs. A web front-end of EpiM is provided at http://cheminf.imada.sdu.dk/epim. 2 Preliminaries 2.1 The π-calculus The π-calculus is a mathematical model of concurrent interacting processes (P , Q, R, . . . ) that communicate using names (x, y, z, . . . ). A name represents a communication channel or session, and can be sent and received as a mes- sage [18, 19]. Process terms are given by the following grammar: P, Q ::= x[y].P output name y on channel x and continue as P | x(y).P input a name on x, bind it to y and continue as P | P |Q run processes P and Q in parallel (parallel composition) | P +Q run either P or Q (choice) | (νx)P bind x in P (restriction) | 0 terminated process A Graph-Based Tool to Embed the π-Calculus. 123 The sets f n(P ) and bn(P ) of free and bound names in a process P are defined as expected as well as α-conversion. Intuitively, process terms that differ solely on the order of parallel composi- tion |, sums +, and restrictions ν represent the same process. This intuition is formalised by structural equivalence, i.e., the least relation ≡ on process terms that is a congruence w.r.t. the grammar above and closed under the Abelian laws for  ∈ {|, +} under 0: P Q≡QP (P  Q)  R ≡ P  (Q  R) P 0≡0 and under the distributivity laws for restriction: (νx)(νy)P ≡ (νy)(νx)P (νx)0 ≡ 0 (νx)(P | Q) ≡ (νy)P | Q for x ∈ / f n(Q). For the sake of simplicity, we adopt the common assumption that choices are always guarded (i.e. every branch in a sum + is either a choice or a communic- ation): in the sequel we assume, similarly to [12], the following grammar: P, Q := M | P | Q M, N := 0 | x(y).P | x[y].P | M + N The semantics of process terms is given by the reduction relation →, i.e., the least relation closed under the rules below: Com (x(y).P + M ) |(x[z].Q + N ) → P {y/z} | Q P ≡ P0 P → Q0 Q0 ≡ Q 0 P →Q P → P0 Str Res Par P →Q (νx)P → (νx)Q P |Q → P0 |Q Rule Com models synchronous communication between two processes, possibly under a non-deterministic context (subterm M may simply be 0). Rule Str en- sures structurally equivalent processes have the same behaviour. Rule Par mod- els the (interleaved) execution of parallel components. Rule Res allows execution under a restriction. 2.2 Graphs, Transformation Rules, and the MØD framework In this section we will be giving a very brief overview of the MØD framework and refer to [2] for a full overview. Encodings of processes will be represented as simple labelled graphs, where vertices and edges of graphs are labelled with first-order terms. We use the common definitions of graph and monomorphisms for labelled graphs, where we require a most general unifier to exist for the set of term mappings induced by the underlying graph morphisms. For full details see Companion Technical Report [6]. Graph transformation rules are modelled in the traditional DPO framework with injective morphisms. See [13] of an overview of the DPO approach. The span of a rule, L ← K → R is illustrated in Fig. 4. Using first-order terms as labels is useful, since it allows us to specify abstract graph transformation rules 124 Andersen et al. such as in Fig. 4, where any term leading with an underscore, e.g., _X, specifies a variable term. The application of graph transformation rules on some input graph, is done by using a strategy framework, where a specific order in which the graph transform- ation rules should be applied can be specified. The direct derivations obtained from applying a given strategy on an input graph is illustrated by a derivation graph. A derivation graph is a directed graph, where vertices are graphs obtained from rule applications and where an edge (G, H), represents a direct derivation G ⇒ H. Any pair of graphs in the derivation graph are non-isomorphic, and as a result the closure up to isomorphism of a given strategy can be automatically computed by MØD. See Fig. 2 for an example. 3 Encoding π-calculus Suppose we wanted to model the process P = x(z).z[w] | x[y] as a graph. To encode P in EpiM we can write the following: 1 x , y , z , w = names ( " x y z w " ) 2 p1 = Process () . input (x , z ) . output (z , w ) 3 p2 = Process () . output (x , y ) 4 P = p1 | p2 5 G = P . encode () 6 G . print () Line 1 defines the names to be used in P . Line 2–3 defines the behaviour of each subprocess in P , while line 4 defines P as the parallel composition between them. Finally, line 5 encodes P as a graph that is printed in line 6. The resulting graph is illustrated in Fig. 1a. The encoding is based on [12] modified to work on simple labelled graphs instead of typed directed hypergraphs. We denote the graph encoded by a process P as [P ]. The overall topology of [P ] can be thought of as tree-like, describing the behaviour of P , just like a syntax tree for a context-free grammar, but where names are shared between operators. Since MØD works on undirected graphs, [P ] is equipped with a special vertex with the label go, representing the “root” of the tree. This will be useful later, to be able to specify the “top” of the graph in transformation rules. All other vertices in [P ] is wrapped in one of two functions v(_X) or t(_X). Any vertex equipped with the function v represents a name with the value of _X. On the other hand, vertices equipped with t describes the behaviour of the corresponding process or represents an implementation detail that will prove use- ful later. More precisely, the argument of t can represent input/output operators t(in)/t(out), or parallel/sum composition operators t(p)/t(s). We allow vertices with the terms t(p) or t(s) to have a degree less than 3 as seen in Fig. 1a. In this case, the vertices do not actually represent a cor- responding parallel or sum composition, but are useful implementation details when implementing the reduction mechanism with graph transformation. Any input or output operator is followed by a vertex with the term t(p), regardless of t(p) representing a parallel composition or not. Moreover, every vertex with the term t(p), is either a leaf or immediately followed by a vertex with the label t(s). A Graph-Based Tool to Embed the π-Calculus. 125 go t(p) t(s) t(s) t(p) t(in) t(out) sync sync arg t(in) t(out) t(p) v(x) v(y) t(p) sync sync arg t(s) arg t(out) arg v(x) v(y) t(out) arg sync arg sync t(p) v(w) v(z) v(w) v(z) (a) (b) Figure 1: (a) The encoded process [P ] for P = x(z).z[w] | x[y]. (b) The simplified version of [P ]. Any prefix operator points to a name corresponding to the received or sent channel. Since the graphs considered here are not embedded, and hence do not have an order on the neighbourhood of a vertex, we label an edge emanating from a prefix operator with “sync” or “arg” whether the corresponding name is used for synchronization or as the argument for the operator. If a name is both the channel and argument of an operator, then the corresponding edge is equipped with “arg-sync” since MØD does not support parallel edges. The vertices corresponding to names of the process are shared among vertices corresponding to input and output operators. In this way, if an input and output operator synchronize on the same name, it is illustrated in the resulting graph by both of them pointing to the vertex corresponding to that name. For example, the outermost input and output operator of the process encoded in Fig. 1a both synchronize on the free name x, and hence they both contain an edge to the vertex with the term v(x). Many of the vertices found in [P ] are implementation details, that are useful for simulating process reductions, but makes it difficult to interpret the behaviour of P simply by looking at [P ]. In this regard, by default, EpiM filters away such implementation details, and instead depicts a simplified version of the encoding illustrated in Fig. 1b. 4 Computing Execution Spaces Suppose we were given the process P = x(z).z[w] |(x[y] + x[y]) and we are able to encode it into its graph equivalent [P ]. Supplied with [P ], we want to compute the execution space of P . In EpiM we can write the following: 1 x , y , z , w = names ( " x y z w " ) 2 p1 = Process () . input (x , z ) . output (z , w ) 3 p2 = Process () . output (x , y ) + Process () . output (x , y ) 4 P = ( p1 | p2 ) 5 exec_space = ReductionDG ( P ) 126 Andersen et al. t(p) t(in) t(s) t(out) arg sync t(out) arg sync t(out) t(out) r123 , r127 v(w) v(y) arg sync sync arg sync arg v(w) v(z) v(x) v(y) out(y, w).0 in(x, z).out(z, w).0 | out(x, y).0 + out(x, y).0 Figure 2: The execution space for P = x(z).z[w] |(x[y] + x[y]). 6 exec_space . calc () 7 exec_space . print () Line 1–4 specifies the process P as explained in the previous section. Line 5–6 computes all possible reductions, while the result is printed in line 7. The result is illustrated in Fig. 2. The execution space of P is illustrated as a directed graph G where each vertex in G corresponds to a process encoding, [Q], derived from reductions on P , while each edge, ([Q], [R]), represents the reduction Q → R, for some processes Q and R. For instance, Fig. 3 contains the transformation that encodes the reduction x(z).z[w] |(x[y] + x[y]) → y[w]. In practice, the reduction step is simulated as three distinct strategies. The first strategy, Rπ , takes care of the actual reduction (→), while the two other strategies, Rgc , Rm , functions as “house-cleaning”, ensuring that the trans- formed graphs represent process encodings. The strategy Rπ consists of two rules, one of which is depicted in Fig. 4. The rule in Fig. 4 simulates the reduction (x(y).P + M ) |(x[w].Q + R) → P {y/w} | Q. The match of the rule searches for the parallel composition on the outermost prefix operators, i.e., a vertex labelled t(p) attached to the root. Recall that every vertex corresponding to a parallel composition is followed by the sum compos- ition vertex with the label t(s). One of these branches of the sum composition vertex is matched such that we find an input and output operator vertex both synchronizing on the same name. When a match is found, the reduction is then simulated by deleting the prefix operators and marking their continuations (which are always followed by a parallel composition vertex) to be coalesced into the “top” parallel composition operator. Additionally, the name y is now bound to w, which is simulated by merging the corresponding vertices. An example of applying Rπ to an encoded process is shown in Fig. 3 as the direct derivation [P ] ⇒ G0 , where [P ] describes the process defined in the start of this section. Note, that the rules are constructed such that when applying a rule any resulting connected component not containing the root vertex will never be part of the corresponding process encoding and hence such components are not depicted here. The input operator in P can synchronize on the output operator in both branches of P , and similarly there exists two matches of the rule depicted in Fig. 4 when applied to [P ]. Either match of the rule, however, A Graph-Based Tool to Embed the π-Calculus. 127 go go t(p) t(p) d d t(s) t(s) merge(t(p)) merge(t(p)) t(in) t(out) t(out) t(s) sync sync sync arg arg t(out) t(p) v(x) t(p) v(y) t(p) Rπ sync arg arg t(s) t(p) merge(v(z)) v(w) d t(out) sync arg v(x) gc t(p) v(y) sync arg v(z) t(p) v(w) t(out) [P ] 0 G Rm go go t(p) t(p) t(s) t(s) Rgc t(out) t(out) sync arg sync arg v(x) gc t(p) t(p) v(y) v(w) t(p) v(y) v(w) sync arg [Q] t(out) G00 Figure 3: The application of each strategy, Rπ , Rm , Rgc , to simulate the reduc- tion P → Q. leads to a graph isomorphic to G0 . The graph G0 does not represent an actual encoding of a process. The reason for this is two-fold: First, we have simply marked vertices that must be coalesced, but not actually coalesced them yet, due to the DPO approach in MØD only supporting injective morphisms. Second, the encoding of any branch not chosen, in this case one of the output operators of P , must be deleted. The coalescing of vertices is done by Rm , obtaining the graph G00 from G0 in Fig. 3, while the deletion of non-chosen summation branches is done by Rgc , finally resulting in the graph [Q] obtained from G00 in Fig. 3. For more details on Rm and Rgc see Companion Technical Report [6]. It was shown in [12] that for the resulting graph [Q] there exists some process π R Q with the encoding [Q]. Let [P ] ==⇒ ∗ [Q] be the sequence of derivations obtained by applying Rπ , Rm , and Rgc on [P ] as illustrated in Fig. 3 transforming the encoded process [P ] into some encoded process [Q]. Then, it was additionally π R shown that given two processes P and Q, the reduction P → Q exists iff [P ] ==⇒ ∗ [Q] exists. The actual derivation graph obtained from computing every possible trans- Rπ ition [P ] ==⇒ ∗ [Q], involves many direct derivations, as is evident from Fig. 3, that does not correspond to any specific state of a process, but are necessary implementation details to transition from one process state to another. Equipped with the derivations illustrated in Fig. 3, however, we can identify all direct derivations between actual graphs corresponding to processes. We can 128 Andersen et al. L K R go go go t(p) t(p) t(p) t(s) t(s) gc gc ht(s), gci ht(s), gci d d t(in) t(out) sync sync ht(p), merge(t(p))i v( X) ht(p), merge(t(p))i merge(t(p)) v( X) merge(t(p)) t(p) arg v( X) arg t(p) hv( Z), merge(v( Z))i v( Y) d merge(v( Z)) v( Y) v( Z) v( Y) Figure 4: The rule for synchronization in Rπ when channel and argument differ, represented as the span L ← K → R. Terms starting with an underscore rep- resents variables, e.g., the match in L is searching for a name “v(_X)”, where the actual name is unspecified and contained in “_X”. The variable can then be used in R. Matched vertices and edges coloured blue in L will be modified by the rule while vertices and edges coloured black will be in the context K of the rule. We see, e.g., that the vertex with the term “go” remains unchanged, while the vertex with the term “t(in)” in L is deleted in R. Vertices whose terms will be relabelled will be coloured purple in the context. We see that vertices with the term “t(s)” in L will be renamed to “gc” in R, represented in the context with “ht(s), gci”. Finally, vertices marked for coalescing will be wrapped in a term called “merge” and connected to the vertex they should be coalesced into. This is seen by the renaming of the name “v(_Z)” to “merge(v(_Z))” and con- necting it to “v(_Y)”, representing the name “_Y” being bound to “_Z” in the simulated reduction. then use such direct derivations to create a new abbreviated derivation graph, Rπ representing our execution space, where any sequence of derivations [P ] ==⇒ ∗ [Q] is modelled as an edge. The result is an execution space as illustrated in Fig. 2, as first introduced in the start of this section. 5 A Final Example Suppose we want to model the following behaviour: – a patient stumbles into a hospital with two doctors; Dr. Jekyll and Mr. Hyde; – the patient will be treated by the first doctor the patient comes across; – Dr. Jekyll will cure the patient while Mr. Hyde will kill the patient. The behaviour can be simulated with the expression Hospital = P | J | H, for the process φ defined by: P =φ stumble[name].name(d).P 0 P 0 =φ kill(x) + cure(x).P J =φ stumble(n).n[jekyll].cure[j] H =φ stumble(n).n[hyde].kill[h] A Graph-Based Tool to Embed the π-Calculus. 129 We refer to the Companion Technical Report [6] for details about the encod- ing of recursive processes and how to compute the execution spaces including recursive processes. The arguments are not given for the recursive processes, as they are just the set of free names of the respective process. A patient walks into the hospital and gives their name to either Jekyll or Hyde via the stumble channel. The doctor then sends his own name back to the patient as a greeting via the patients name as a channel (note, this serves no practical purpose for the model). Finally, the patient is either cured or killed, depending on the doctor received. If cured, P is called recursively simulating that the patient can get sick and stumble into the hospital again. If the patient died, we reached a deadlock as there is no cure for death. Note, many of the arguments sent over the channels are not used, but are simply there for illustrative purposes. We can model the above example in EpiM as follows: 1 s , n , pn , j , h , cu , ki , d , x = names ( " s n pn j h cu ki d x " ) 2 free_names = [s , n , ki , cu ] 3 4 rp = RecursiveProcess () 5 6 P = Process () . output (s , n ) . input (n , d ) . call ( " Pp " , free_names ) 7 rp . add ( " P " , free_names , P ) 8 9 Pp = Process () . input ( ki , x ) + Process () . input ( cu , x ) . call ( " P " , free_names ) 10 rp . add ( " Pp " , free_names , Pp ) 11 12 J = Process () . input (s , pn ) . output ( pn , j ) . output ( cu , j ) . call ( " J " , free_names ) 13 rp . add ( " J " , free_names , J ) 14 15 H = Process () . input (s , pn ) . output ( pn , h ) . output ( ki , h ) . call ( " H " , free_names ) 16 rp . add ( " H " , free_names , H ) 17 18 Hospital = P | J | H 19 20 exec_space = ReductionDG ( Hospital , rp ) 21 exec_space . calc () 22 exec_space . print () Note, we have shortened the names to simple single letter names for illus- trative purposes. The resulting execution space, representing the simulation of Hospital, is illustrated in Fig. 5. Although, it might be difficult to parse the graph, the expected behaviour should be clear from the graph: if the patient is treated by Dr. Jekyll, P is called recursively and as a result the behaviour is modelled as the only cycle in the derivation graph. If on the other hand the patient was killed off then P is terminated. Hence the behaviour is modelled in the graph as a path that end in a vertex with no outgoing edges (reached a deadlock). 6 Conclusion We have introduced EpiM, available as a web front-end at http://cheminf. imada.sdu.dk/epim; a tool using graph transformation for computing execu- tion spaces of π-calculus processes. In this regard we presented a brief overview 130 Andersen et al. t(p) t(p) t(call(Pp)) t(in) t(in) t(out) arg t(out) arg t(s) sync sync 3 1 0 t(out) sync 2 t(out) arg v(pn2) t(out) sync arg t(out) v(pn2) t(in) t(in) arg arg r500 arg arg arg arg sync t(call(J)) v(j) t(call(H)) sync v(h) v(j) sync v(h) sync t(call(J)) t(call(H)) t(call(P)) sync v(x) sync 3 1 0 3 2 1 0 2 3 0 3 3 1 0 0 2 1 1 2 2 v(cu) v(n) v(s) v(ki) v(cu) v(s) v(n) v(ki) in(s, pn2).out(pn2, h).out(ki, h).H() | Pp() | out(cu, j).J() in(s, pn2).out(pn2, h).out(ki, h).H() | out(cu, j).J() | in(ki, x).0 + in(cu, x).P() r494 r506 t(p) t(p) t(p) t(in) t(in) t(in) t(in) t(out) t(out) arg t(out) t(out) arg arg t(out) t(out) arg sync r489 sync sync r512 sync t(in) t(out) arg sync t(out) arg v(pn2) t(in) t(out) arg v(pn1) sync sync v(pn2) t(out) arg t(out) arg v(pn2) sync arg sync arg arg arg arg sync arg arg arg sync v(d) t(call(Pp)) sync t(call(J)) v(j) t(call(H)) sync v(h) sync v(d) t(call(Pp)) sync t(call(J)) v(j) t(call(H)) sync v(h) t(call(P)) t(call(J)) t(call(H)) sync v(h) 1 3 1 1 0 3 3 2 0 0 2 2 1 1 3 1 0 3 0 3 2 2 0 2 3 1 3 3 2 1 1 2 0 02 0 v(n) v(cu) v(s) v(ki) v(n) v(cu) v(s) v(ki) v(cu) v(n) v(ki) v(s) in(s, pn2).out(pn2, h).out(ki, h).H() | in(n, d).Pp() | out(n, j).out(cu, j).J() out(s, n).in(n, d).Pp() | in(s, pn1).out(pn1, j).out(cu, j).J() | in(s, pn2).out(pn2, h).out(ki, h).H() in(s, pn2).out(pn2, h).out(ki, h).H() | J() | P() r492 t(p) t(p) t(p) t(in) t(in) t(call(Pp)) t(in) arg t(out) t(out) t(out) arg t(out) arg t(s) sync sync sync sync v(pn1) t(out) arg t(in) t(out) arg arg t(out) v(pn1) sync 3 t(out) 0 1 2 arg t(out) v(pn1) sync t(in) t(in) t(out) arg arg sync arg r497 arg arg r503 arg arg arg arg sync t(call(J)) v(j) t(call(Pp)) v(d) sync t(call(H)) sync v(h) v(j) sync t(call(J)) v(h) t(call(H)) sync v(j) sync sync t(call(J)) t(call(P)) v(x) t(call(H)) sync v(h) sync 0 0 0 3 3 1 3 1 2 2 1 2 3 0 1 3 0 2 1 2 3 0 3 3 1 0 2 1 0 2 1 2 v(s) v(cu) v(n) v(ki) v(cu) v(s) v(n) v(ki) v(cu) v(s) v(n) v(ki) in(s, pn1).out(pn1, j).out(cu, j).J() | in(n, d).Pp() | out(n, h).out(ki, h).H() in(s, pn1).out(pn1, j).out(cu, j).J() | Pp() | out(ki, h).H() in(s, pn1).out(pn1, j).out(cu, j).J() | out(ki, h).H() | in(ki, x).0 + in(cu, x).P() r509 t(p) t(p) t(in) t(in) t(in) arg t(out) t(out) arg arg t(out) sync sync r515 sync v(pn1) arg t(out) sync sync t(out) arg v(pn2) sync v(pn1) arg t(out) arg arg arg v(j) sync t(call(J)) t(call(H)) sync v(h) t(call(H)) v(j) t(call(J)) sync 3 1 0 3 2 1 0 2 0 0 1 1 2 2 3 3 v(cu) v(n) v(s) v(ki) v(s) v(n) v(ki) v(cu) in(s, pn1).out(pn1, j).out(cu, j).J() | in(s, pn2).out(pn2, h).out(ki, h).H() in(s, pn1).out(pn1, j).out(cu, j).J() | H() Figure 5: The execution space for Hospital. The start of the simulation, i.e., [Hospital], is the single vertex with a degree of 3. The vertex for [Hospital] contains two out-edges corresponding to the patient P either synchronizing on Dr. Jekyll J or Mr. Hyde H. If P synchronizes with J, we see that we end up in a cycle, representing P being cured and called recursively. On the other hand synchronizing on H, leads to a vertex with no out-edges, and hence no reductions are possible from the corresponding encoding, representing the patient being killed off and we are left with the encoded process [H | J]. of the encodings and transformations involved. Practically, execution spaces can be used for basic analysis of processes such as determining liveness. Since EpiM is directly embedded into MØD, it would be possible to use the range of features provided by the MØD framework, notably [5]. Since structural congruence can be determined directly from graph isomorphism of the encoded processes, canonic- alization of processes is given for free. MØD provides a framework for stochastic simulations [4], suggesting the possibilities of using a version of the encoding of π-calculus presented here to simulate stochastic π-calculus processes [9]. The type of DPO supported by MØD does not allow rewriting rules that per- form bulk duplication or deletion of subgraphs. This means that duplicating or deleting processes cannot be implemented with a single rewrite operation. On one hand, this elicits the cost of process duplication or recursion often ignored in process calculi, on the other, it suggests to explore the use of MØD with “resource aware calculi” like linear variations of the π-calculus [8, 15, 16]. Acknowledgements. This work was partially supported by the Independent Research Fund Denmark, grant no. DFF-7014-00041. A Graph-Based Tool to Embed the π-Calculus. 131 References 1. Jakob L. Andersen, Christoph Flamm, Daniel Merkle, and Peter F. Stadler. Gen- eric strategies for chemical space exploration. Int. J. Comp. Bio. and Drug Design, 2014. 2. Jakob L. Andersen, Christoph Flamm, Daniel Merkle, and Peter F. Stadler. A software package for chemically inspired graph transformation. In Graph Trans- formation - 9th International Conference, ICGT 2016, Proceedings, volume 9761 of Lecture Notes in Computer Science, pages 73–88. Springer, 2016. 3. Jakob L. Andersen, Christoph Flamm, Daniel Merkle, and Peter F. Stadler. Chemical transformation motifs — modelling pathways as integer hyperflows. IEEE/ACM Transactions on Computational Biology and Bioinformatics, 2018. in press, early access online. 4. Jakob L. Andersen, Christoph Flamm, Daniel Merkle, and Peter F. Stadler. Rule- based gillespie simulation of chemical systems. In 3rd Workshop on Verification of Engineered Molecular Devices and Programs, VEMDP 2016, Proceedings. Springer, 2018. 5. Jakob L. Andersen and Daniel Merkle. A generic framework for engineering graph canonization algorithms. In 2018 Proceedings of the 20th Workshop on Algorithm Engineering and Experiments (ALENEX), pages 139–153, 2018. 6. Jakob Lykke Andersen, Marc Hellmuth, Daniel Merkle, Nikolai Nøjgaard, and Marco Peressotti. A Graph-Based Tool to Embed the π-Calculus into a Compu- tational DPO Framework, 2019. 7. Anja Bog and Frank Puhlmann. A tool for the simulation of π-calculus systems. Open. BPM, 2006. 8. Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In CONCUR, volume 6269 of Lecture Notes in Computer Science, pages 222–236. Springer, 2010. 9. Luca Cardelli and Radu Mardare. Stochastic pi-calculus revisited. In International Colloquium on Theoretical Aspects of Computing, pages 1–21. Springer, 2013. 10. Vincent Danos, Jérôme Feret, Walter Fontana, Russell Harmer, and Jean Krivine. Rule-based modelling of cellular signalling. In CONCUR 2007 - Concurrency The- ory, 18th International Conference, Proceedings, volume 4703 of Lecture Notes in Computer Science, pages 17–41. Springer, 2007. 11. Hartmut Ehrig, Michael Pfender, and Hans Jürgen Schneider. Graph-grammars: An algebraic approach. In 14th Annual Symposium on Switching and Automata Theory (SWAT 1973), pages 167–180. IEEE, 1973. 12. Fabio Gadducci. Graph rewriting for the π-calculus. Mathematical Structures in Computer Science, 17(3):407–437, 2007. 13. Annegret Habel, Jürgen Müller, and Detlef Plump. Double-pushout graph trans- formation revisited. Mathematical Structures in Computer Science, 11(5):637–688, 2001. 14. Leonard A. Harris, Justin S. Hogg, José Juan Tapia, John A. P. Sekar, San- jana Gupta, Ilya Korsunsky, Arshi Arora, Dipak Barua, Robert P. Sheehan, and James R. Faeder. Bionetgen 2.2: advances in rule-based modeling. Bioinformatics, 32(21):3366–3368, 2016. 15. Naoki Kobayashi, Benjamin C. Pierce, and David N. Turner. Linearity and the pi-calculus. ACM Trans. Program. Lang. Syst., 21(5):914–947, 1999. 16. Wen Kokke, Fabrizio Montesi, and Marco Peressotti. Better late than never: a fully-abstract semantics for classical processes. PACMPL, 3(POPL):24:1–24:29, 2019. 132 Andersen et al. 17. Barbara König. A graph rewriting semantics for the polyadic pi-calculus. In Proc. of GT-VMT’00 (Workshop on Graph Transformation and Visual Modeling Techniques), pages 451–458, 2000. 18. Robin Milner. Communicating and mobile systems - the Pi-calculus. Cambridge University Press, 1999. 19. Davide Sangiorgi and David Walker. The Pi-Calculus - a theory of mobile processes. Cambridge University Press, 2001. 20. Björn Victor and Faron Moller. The mobility workbench : A tool for the pi-calculus. In Proceedings of CAV’94 :, pages 428–440, 1994.