Towards a Causal Semantics for Brane Calculi

Towards a Causal Semantics for Brane Calculi Nadia Busi Dipartimento di Scienze dell’Informazione, Universit`a di Bologna, Mura A. Zamboni 7, I-40127 Bologna, Italy. [email protected] Summary. Brane Calculi are a family of biologically inspired process calculi, proposed in [6] to model the interactions of dynamically nested membranes. We propose a semantics that describes the causal dependencies occurring between the reactions of a system described in Brane Calculi. We investigate the basic properties that are satisfied by such a semantics. The notion of causality turns out to be quite relevant for biological systems, as it permits to point out which events occurring in a biological pathway are necessary for another event to happen. 1 Introduction Brane calculi [6] are a family of process calculi proposed for modeling the behavior of biological membranes. The formal investigation of biological membranes has been initiated by G. P˘aun [20], in the field of automata and formal language theory, with the definition of P systems. In a process algebraic setting, the notions of membranes and compartments are explicitly represented in BioAmbients [23], a variant of Mobile Ambients [8] based on a set of biologically inspired primitives of interaction. Brane calculi represent an evolution of BioAmbients: the main difference w.r.t. previous approaches consists in the fact that the active entities reside on membranes, and not inside membranes. In [6] two basic instances of brane calculi have been proposed: the Phago/Exo/Pino (PEP) and the Mate/Bud/Drip (MBD) calculi. In this paper we concentrate on the MBD calculus. The primitives of MBD are inspired by membrane fusion (mate) and fission (mito). Because membrane fission is an uncontrollable process that can split a membrane at an arbitrary place, it is replaced by two simpler operations: budding, that is splitting off one internal membrane, and dripping, that consists in splitting off zero internal membranes. The aim of this work is to start an investigation of the causal dependencies arising in Brane Calculi, and more precisely in the MBD calculus. The main motivation for this work comes from system biology, as the understanding of the causal 98 N. Busi relations occurring between the events of a complex biological pathway could be of precious help, e.g., for limiting the search space in the case some unpredicted event occurs. The study of a causal semantics for process algebras dates back to the early nineties for CCS [17] (see, e.g., [10, 9, 15]), and to the mid nineties for the πcalculus [18] (see, e.g., [1, 3, 11, 12]). To the best of our knowledge, the only other work that deals with causality in bio-inspired calculi is [14], where a causal semantics for Beta Binders [21, 22] – based on the π-calculus semantics and on the enhanced operational semantics approach of [12] – is defined. One of the main differences between Beta Binders and Brane Calculi is that the membrane structure in Beta Binders is flat, whereas in Brane Calculi the membranes are nested to form a hierarchical structure. As we will see, this difference has a deep impact on the complexity of the causal relation. The other differences between the two approaches will be discussed throughout the paper. The paper is organized as follows. Section 2 introduces the syntax and the interleaving semantics for the MBD fragment of the Brane Calculus. Sections 3 and 4 are devoted to the definition of the causal semantics. Section 3 provides an informal description of the features of the causal semantics we are defining, and illustrates the problems that have arised through a list of examples. The formal definition of the causal semantics is in Section 4, followed by a discussion concerning the properties that are (not) satisfied by such a semantics. Finally, Section 5 reports some conclusive remarks. 2 MBD Calculus: Syntax and Semantics In this section we recall the syntax and the standard, interleaving semantics of Brane Calculi, and specialize it to MBD [6]. 2.1 Syntax and structural congruence of Brane Calculi A system consists of nested membranes, and a process is associated to each membrane. Definition 1. The set of systems is defined by the following grammar: P, Q ::=  | P◦Q|!P|σ(|P|) The set of membrane processes is defined by the following grammar: σ, τ ::= 0 |σ|τ|!σ|a.σ Variables a, b range over actions, that will be detailed later. Towards a Causal Semantics for Brane Calculi 99 The term represents the empty system; the parallel composition operator on systems is ◦. The replication operator ! denotes the parallel composition of an unbounded number of instances of a system. The term σ(|P|) denotes the membrane that performs process σand contains system P. The term 0 denotes the empty process, whereas |is the parallel composition of processes; with !σwe denote the parallel composition of an unbounded number of instances of process σ. Term a.σ is a guarded process: after performing the action a, the process behaves as σ. We adopt the following abbreviations: with awe denote a.0, with (|P|) we denote 0(|P|), and with σ(| |) we denote σ(||). The structural congruence relations on systems and processes is defined as follows:1 Definition 2. The structural congruence ≡is the least congruence relation satisfying the following axioms: P◦Q≡Q◦P σ |τ≡τ|σ P◦(Q◦R)≡(P◦Q)◦R σ |(τ|ρ)≡(σ|τ)|ρ P◦  ≡ P σ |0≡σ ! ≡  !0 ≡0 !(P◦Q)≡!P◦!Q!(σ|τ)≡!σ|!τ !!P≡!P!!σ≡!σ P◦!P≡!P σ |!σ≡!σ 0(||)≡  2.2 Interleaving semantics of Brane Calculi We recall the standard, interleaving semantics. At each computational step, a single reaction is chosen and executed. The next definition provides the set of generic reaction rules that are valid for all brane calculi, while the reaction axioms are specific for each brane calculus; the reaction axioms for MBD will be provided in Definition 5. Definition 3. The basic reaction rules are the following: (par)P→Q P◦R→Q◦R (brane)P→Q σ(|P|)→σ(|Q|) (strucong)P0≡P P →Q Q ≡Q0 P0→Q0 1With abuse of notation we use ≡to denote both structural congruence on systems and structural congruence on processes. 100 N. Busi Rules (par) and (brane) are the contextual rules that respectively permit to a system to execute also if it is in parallel with another process or if it is inside a membrane, respectively. Rule (strucong) ensures that two structurally congruent systems have the same reactions. With →∗we denote the reflexive and transitive closure of a relation →. Given a reduction relation →, we say that the system P0is a derivative of the system P if P→∗P0; the set of derivatives of a system Pis denoted by Deriv(P). We say that a system Phas a divergent computation (or infinite computation) if there exist an infinite sequence of systems P0, P1, . . . , Pi, . . . such that P=P0 and ∀i≥0 : Pi→Pi+1. We say that a system Phas a terminating computation if there exists Q∈Deriv(P) such that Q6→. We say that all computations of a system Pterminate if Phas no divergent computations. We use Q(resp. ) to denote the parallel composition of a set of processes (resp. systems), i.e., Qi∈{1,...,n}σi=σ1|. . . |σnand i∈{1,...,n}Pi=P1◦. . . ◦ Pn. Moreover, Qi∈∅ σi= 0 and i∈∅Pi=. Finally, Qnσ(resp. nP) denotes the parallel composition of ncopies of process σ(resp. system P). 2.3 Syntax and interleaving semantics of MBD The actions of the MBD calculus, proposed in [6], are inspired by membrane fusion and splitting. To make membrane splitting more controllable, in [6] two more basic operations are used: budding, consisting in splitting off one internal membrane, and dripping, consisting in splitting off zero internal membranes. Membrane fusion, or merging, is called mating. Definition 4. Let Name be a denumerable set of names, ranged over by n, m, . . .. The set of actions of MBD is defined by the following grammar: a::= maten|mate⊥ n|budn|bud⊥ n(σ)|drip(σ) Actions matenand mate⊥ nwill synchronize to obtain membrane fusion. Action budnpermits to split one internal membrane, and synchronizes with the co-action bud⊥ n. Action drip permits to split off zero internal membranes. Actions bud⊥and drip are equipped with a process σ, that will be associated to the new membrane created by the membrane performing the action. Definition 5. The reaction relation for MBD is the least relation containing the following axioms, and satisfying the rules in Definition 3: (mate)maten.σ|σ0(|P|)◦mate⊥ n.τ|τ0(|Q|)→σ|σ0|τ|τ0(|P◦Q|) (bud)bud⊥ n(ρ).τ|τ0(|budn.σ|σ0(|P|)◦Q|)→ρ(|σ|σ0(|P|)|)◦τ|τ0(|Q|) (drip)drip(ρ).σ|σ0(|P|)→ρ(| |)◦σ|σ0(|P|) Towards a Causal Semantics for Brane Calculi 101 3 A Causal Semantics for MBD: an informal explanation In this section we provide a causal semantics for MBD. To define a causal semantics for process calculi, we follow the approach used in [15] for CCS, and in [1] for the π-calculus. The idea consists in decorating the reaction relation with two pieces of information: •a fresh name k, that is associated to the reaction and it is taken from the set of causes K; •a set H⊆ K, containing all the names associated to the already occurred reactions, that represent a cause for the current reaction. To keep track of the names of the already occurred reactions that may represent a cause for the reactions that may happen in the future, the syntax of the terms of the calculus is enriched with such an information on causal dependencies. As in [1], for the sake of clarity we only keep track of the so called immediate causes, as the set of general causes can be reconstructed by transitive closure of the immediate causal relation. We will provide more explanation on this point with an example in the following part of the paper. Now we start with an informal introduction of causality in MBD. First we discuss how the standard kinds of causality arising in most process calculi – i.e., those due to the prefix structure of processes and to the synchronization of two complementary actions – scale to Brane Calculi. Then we perform a design choice concerned with the semantics of calculi for membranes, and finally we discuss other features peculiar of the MBD operations. 3.1 Classical causal dependencies: structural and synchronization causality We start the kind of causal dependencies that arises in all process calculi, namely, structural causality and synchronization causality. Structural causality arises from the prefix structure of terms. Consider for example the following system: drip(σ).drip(ρ)(| |) Such a system can first create a new membrane with process σ, followed by the creation of a second new membrane with process ρ; i.e., it can perform the sequence of reactions drip(σ).drip(ρ)(| |)→drip(ρ)(| |)◦σ(| |)→0(| |)◦σ(| |)◦ρ(| |) The creation of the first membrane is a necessary condition for the creation of the second membrane, hence we say that the execution of the drip(ρ) operation is caused by the execution of the drip(σ) operation. To remember the fact that the action drip(σ) will be a cause for the actions performed by the continuation of the prefix, we replace the drip(σ) prefix with a 102 N. Busi causal operator containing the cause name associated to the drip(σ) action. Thus, we obtain the following causal reactions: drip(σ).drip(ρ)(| |)h;∅ −−→ {h}:: drip(ρ)(| |)◦σ(| |)k;{h} −−−→ {k}:: 0(| |)◦σ(| |)◦ρ(| |) The decoration h;∅of the first reaction means that the first reaction is labeled with the causal name hand that its set of causes is empty. The decoration k;{h} of the second reaction means that the second reaction has associated the causal name k, and it is caused by the reaction named h(i.e., the first reaction). The process {h}:: drip(ρ) means that the first action performed by process drip(ρ) is caused by the reaction named h. Note that – for the sake of brevity – process {k}:: 0 is decorated only with the immediate cause {k}, as the whole set of causes, i.e., {h, k}can be easily constructed. To lighten the notation, in the following we will drop the parentheses surrounding the set of causes, if this creates no confusion. The other kind of causality, i.e., synchronization causality, arises when two processes synchronize on complementary actions. Consider the system drip(σ1).maten.drip(τ1)(| |)◦drip(σ2).mate⊥ n.drip(τ2)(| |) The mate reaction can be performed when both the actions drip(σ1) and drip(σ2) have been performed; hence, it is caused by both actions. We obtain the following: drip(σ1).maten.drip(τ1)(| |)◦drip(σ2).mate⊥ n.drip(τ2)(| |)h1;∅ −−−→ h1:: maten.drip(τ1)(| |)◦drip(σ2).mate⊥ n.drip(τ2)(| |)◦σ1(| |)h2;∅ −−−→ h1:: maten.drip(τ1)(| |)◦h2:: mate⊥ n.drip(τ2)(| |)◦σ1(| |)◦σ2(| |)k;h1,h2 −−−−−→ k:: (drip(τ1)|drip(τ2)(| |)◦σ1(| |)◦σ2(| |) Hence, the (label kof the) mate reaction will be an immediate cause for both drip(τ1) and drip(τ2), and the global set of causes of these two drip actions will be {h1, h2, k}. 3.2 How does the causes distribute over the parallel components of a membrane process? When moving to consider the features of the causal relation peculiar of membrane calculi, a first question arises: if a process on a membrane performs an action, this action will be a cause only for its continuation (and eventually for the continuation of its synchronizing action), or for the whole process on the membrane? In other words, consider the system maten|drip(σ)(| |)◦mate⊥ n(| |) If the system performs the mate synchronization, then the drip action will be caused or not by the mate action? The assumption that the drip will be caused Towards a Causal Semantics for Brane Calculi 103 by the mate may have the following biological interpretation: when a membrane interaction operation is performed, all the membrane is involved, and at the end of the operation the structure of all the membrane has been affected. This assumption is considered in [14] in the definition of a causal semantics for Beta-binders [21, 22] , a bio-inspired process calculus roughly consisting of unnested compartments enclosing π-calculus processes. It is also used in [2] for the definition of a maximal parallelism semantics (i.e., step semantics with maximal progress: if an action can be performed in the current step, then it must be performed) for MBD. It is also the common approach used in the definition of the maximal parallelism semantics for Membrane Systems with evolving membranes (see, e.g., [19, 20]). In the present paper, we consider the opposite approach: in the above system, we consider the drip operation independent from the mate operation, as the drip operation can be executed regardless of the fact that the mate synchronization has been performed or not. The biological interpretation may be the following: the membrane proteins and the part of the lipid bilayer involved in the mate synchronization are different from the membrane proteins and the part of the bilayer that is performing the drip operation, and they lie in different parts of the membrane surface. Thus, we consider the following causal reactions: maten|drip(σ)(| |)◦mate⊥ n(| |)h;∅ −−→ h:: 0 |drip(σ)|h:: 0(| |)k;∅ −−→ h:: 0 |k:: 0 |h:: 0(| |) Note that the information on the causes of the empty process 0 is completely irrelevant, hence in the following we will replace H:: 0 with 0. 3.3 Causal dependencies generated by the mate operation Now we analyze the features peculiar of the MBD operations. According to the informal explanation above, a mate action turns out to be a cause for the continuations of the mate and the co-mate prefixes that synchronize to perform the operation. However, when considering the mate operation, a more subtle kind of causality, we call environment causality, is originated, e.g., between the mate action and the processes on the child membranes of the two membranes performing the mate and co-mate actions. This causality is due to the fact that the environment of such child membranes, i.e., the set of membranes with which they can interact, is increased by the execution of the mate action. Mate followed by mate Consider the following process: maten(|(matem|mateo)(| |)◦mate⊥ o(| |)|)◦ mate⊥ n(|mate⊥ m(| |)|) 104 N. Busi Now the mate synchronization on mcannot be performed, as the two membranes whose processes can synchronize on such an operation belong to different membranes. On the other hand, the mate synchronization on ocan take place, as both membranes whose processes can synchronize on such an operation belong to the same membrane. However, if the mate synchronization on ntakes place, the two external membranes are fused; this results in a change of the environment of the child membrane; now the mate on mcan take place, as the two child membranes now belong to the same father membrane and can get in contact. Hence, the mate on mcausally depends on the mate on n. To this aim, we decorate the processes of the child membranes of the external membrane performing a mate with label kin the following way: the child membranes on the left are decorated with the enriched label k+ i, whereas the child membrane on the right with the enriched complementary label k− i.2Note that we cannot simply decorate both groups of child membranes with label k, otherwise we are no longer able to distinguish between the synchronization on m, that is caused by k, and the synchronization on owhich has no causes. The enriched labels are used in the following way: when two processes preceded by enriched labels synchronize on a mate operation, the label kwill be a cause for such a synchronization if one process in decorated with an enriched label and the synchronizing process is decorated with the complementary label. We obtain the following causal reductions: maten(|(matem|mateo)(| |)◦mate⊥ o(| |)|)◦ mate⊥ n(|mate⊥ m(| |)|) h;∅ −−→ (0 |0)(|(h+ i:: matem|h+ i:: mateo)(| |)◦h+ i:: mate⊥ o(| |)◦ h− i:: mate⊥ m(| |)|) Now, if the mate on m is executed, then it will be caused by h, as the mate and comate processes are labeled with h+ iand h− i, respectively: (0 |0)(|(h+ i:: matem|h+ i:: mateo)(| |)◦h+ i:: mate⊥ o(| |)◦ h− i:: mate⊥ m(| |)|) k;h −−→ (0 |0)(|(0 |h+ i:: mateo)(| |)◦h+ i:: mate⊥ o(| |)◦ 0(| |)|) On the other hand, if the mate on ois executed, then it is not caused by hn, because the mate and comate processes are labeled with the same label h+ i. 2The iin the labels k+ iand k− istands for “internal”, and means that the action with label khas been performed by the father membrane. The need for such a label will be made clear in the following. Towards a Causal Semantics for Brane Calculi 105 Mate followed by bud A similar problem arises between the father and the child membrane when a bud operation is performed. Consider the following process: (maten|bud⊥ m(ρ1))(|budm(| |)◦budo(| |)|)◦ (mate⊥ n|bud⊥ o(ρ2))(| |) Now only the bud on mcan be performed, as the membrane performing the bud on ois not a child of the membrane performing the corresponding cobud. However, the bud on ocan be performed after the mate on nis performed, hence the bud causally depends on the mate. Thus, besides decorating the children of a membrane performing a mate (resp comate) with complementary labels k+ i(resp. k− i), we also decorate the subprocesses in parallel with the subprocess performing the mate (resp. the comate) with k+ e(resp. k− e)3. When a bud is performed, it is caused by kif the process performing the cobud on the father membrane is decorated, e.g., with k+ eand the process performing the bud on the child membrane is decorated with k− e. Note that, in case of a mate followed by a drip, the decorated causes will give rise to no causal dependency: the drip is caused by the mate only if the mate (or the comate) is a prefix of the drip. 3.4 Causal dependencies generated by the bud and the drip operations The bud (resp. drip) operation create a new membrane – whose membrane process is specified in the cobud (resp. drip) action – surrounding the child membrane that performs the synchronizing bud action (resp. with no children). As the new membrane does not exist before the bud (resp. drip) operation is performed, all the actions that such a membrane will perform are caused by the bud (resp. drip) operation. Consider the following system: bud⊥ n(drip(σ))(|budn(| |)|) This system can perform the following causal reactions: bud⊥ n(drip(σ))(|budn(| |)|)h;∅ −−→ 0(| |)◦h:: drip(σ)(|0(| |)|)k;h −−→ 0(| |)◦0(|0(| |)|)◦k:: σ(| |) We note that the bud operation generates no environmental cause. Regarding the child membranes, they are essentially divided into two sets, thus possibly preventing some mate (or bud) operation that was possible before to happen. On the other hand, the other processes in the father membrane are left unchanged. 3Here the emeans “external”