A Couple of Systems Biological Stories told by Formal Methods David Šafránek IUI Masaryk University ^w?^ Czech Republic Outline Q Introduction and Motivation 0 Methodology • Biological Networks • Modelling Problems Q Story I: Signalling Pathways of Fibroblast Growth Factors Q Story II: Synthetic Biology: Trichlorpropane Degradation Outline Introduction and Motivation KA pi- n n r^cr\/ i v i c u 11 w w i w ci. y • Biological Networks • Modelling Problems C j- I C" II" D , I Biology • since ancient times • empirically studies life and living organisms • studied aspects: structure, function, growth, development and evolution • used concepts: • the cell - the unit of life • the gene - the unit of inherited information • the evolution - the mechanism of species creation Biophysics and Theoretical Biology Domain Roots Biophysics • since the mid of 19th century • living organism = open (thermodynamic) system • the goal: why and how the living matter works? • uses mathematical apparatus 9 a fascinating phenomenon: homeostasis • maintain a stable condition in a changing environment • robust (up-to certain limits) Motivation: Rigorously Answer Biological Questions • biology is goal-oriented 9 biological problems typically address complex processes Examples of biological problems How the bacteria cell utilises particular nutritions? Which nutritions imply fastest growth under given conditions? Motivation: Rigorously Answer Biological Questions • biology is goal-oriented 9 biological problems typically address complex processes Examples of biological problems How the bacteria cell utilises particular nutritions? Which nutritions imply fastest growth under given conditions? The answer should fullfil specific requirements • to formulate and analyse a biological problem holistically • to give mechanistic explanation based on known facts -mechanistic means in the context of laws of physics/chemistry • to project the mechanistic details onto the genetic information From Biologist's Table From Biologist's Table Systems Approach: The Grand Challenge Complex Organism as a System |^|| 1 INTEGRATED REACTIVE 1 SYSTEM INPUT SIGNALS H M RESPONSE SIGNALS E(exposures) metabolK: response N(nutrrtion) proteomic response L(lifestyle) evolutionary response FG(E, N, L) Systems Approach: The Grand Challenge Complex Organism as a System ^ An |^ * ^ INTEGRATED REACTIVE SYSTEM INPUT SIGNALS II RESPONSE SIGNALS E(exposures) FAST metabolic response N(nutrition) II proteomic response L(lifestyte) evolutionary response SLOW LONG-TERM FG(E, N, L) Systems Approach: A Moderate Challenge Population of Bacteria as a System for a particular set of genes G Fq : (environment exposure, nutrition) —>> growth profile slide credits: Ralf Steuer (HU Berlin) Systems View of Processes Driving the Cell The Cell as a Complex Interaction Network Literature System boundary KEGG iiMAZE DIP BIND Metabolic networks Signalling Pathways Protein-protein Interaction protein 1 A c metabolite Metabolome space metabolite3 ..PathDB. TRANSPATH Gene RNA1 Regulatory Pathways r^\MT2r^Klotlio^ Brenda ENZYME -J teome space ranscriptome space gene3 gene Genome space GenBaiik ,'DDBJ/ ^EMBL^. slide credits: David Gilbert (Brunei Univ Outline Q Methodology • Biological Networks o Modelling Problems ^ y I. ^"5' 'a' 'o aLiivvayj The Paradigm of Computational Systems Biology Assumptions • The biological reality (a biophysical process) is understood as a biological system. 9 A biological system is given as a network M of biochemical components connected by chemical/physical interactions. 9 The components include relevant genes and gene products. Biological Networks CRNs • basic form: chemical reaction networks (CRNs) • elementary chemical reactions • represent the flow of the mass • example: Biological Networks Reaction-Influence Networks • simplified form: reaction-influence networks (RINs) • chemical reactions influenced by other molecules • represent the modulated flow of the mass • example: SBGN standard notation, see https://www.sbgn.org Biological Networks Influence Networks o abstract form: influence networks (INs) • represent positive/negative influences among molecules • well fit incomplete knowledge • typically gene regulatory networks, signalling pathways • example: [ mt:prote.n } SBGN standard notation, see https://www.sbgn.org The Goal of Computational Systems Biology The General Goa For a biological system given by a network M reconstruct the system's dynamics: Define a function that encodes the information (signal) processing occuring in all components of the system in time. Fj\[ : (input stimuli, environment signals) —>> response signals Model-Based Workflow network reconstruction biological knowledge databases "kIgg" Brendel ENZYME XeyulotiDB n t model validation gene reporters, DNA microarray, mass spectrometry, ... Bacterial DNA biological network hypothesis emergent properties model questions model specification Petri Net, ODEs, rule-based, process calculus, Boolean network, ... Qnadph 4.1.2.15 4.6.1.3 4.2.1.10 1.1.1.2s\ erythrose-4- -»| [--»| |-M^)-*\ |-►T^)-»j |->C^) NADP phosphate _______— f\ phospho- /—^ phosphate f J (J *—o<—-i u—o<—n«—(~) ATP < 2.5./.Í9 2.7.7.7;T Q ADP d^ = -k1[E][5] + k2[ES\ d^ = -k1[E][S\ + k2lES] + k3[ES} at d^ = k1[E\[S\-k2[ES\-k3[ES] -1 computer lab model analysis static analysis, numerical simulation, analytical methods, model checking | [Y]|"[Z]| [X]| Kyz hypothesis testing, property detection, new hypothesis inference Modelling Frameworks state-transition systems states: discrete molecule numbers or qualities (on/off) ualitative mode stochastic model Continuous-Time Markov Chains states: discrete molecule numbers abstracted time modeled V continuous model Ordinary Differential Equations states: continuous concentrations states discrete continuous I Outline Introuuction anu iviotivation • Biological Networks • Modelling Problems Q Story I: Signalling Pathways of Fibroblast Growth Factors • Boolean Networks Model Construction Discrete Models of Influence (Regulatory) Networks protein A gene a KA,0 = 1 protein B gene b kb& = 2 Model Construction Discrete Models of Influence (Regulatory) Networks protein A protein B gene a Asynchronous Update State Transition Graph (STG) gene b KA,0 = 1 kb& = 2 Model Construction Negative Influence (Inhibition) o( protein A gene a Model Construction Negative Influence (Inhibition) o( protein A gene a AAA} - Model Construction — A Remark Regulatory Networks as Petri Nets tfi(0) = O,tfi({s2}) = l 9i <-92 K1(®) = l,K1({g2}) = 0 9i I-92 Model Construction Discrete Models of Influence (Regulatory) Networks protein B gene a gene b K A,{A,B} K A,{A) K A,{B} -KA,0 = ? 1 lBA — 1 Model Construction Discrete Models of Influence (Regulatory) Networks Model Construction Discrete Models of Influence (Regulatory) Networks protein A gene a KA,{A,B] = 0 KA,{A) = 0 KA,{B) = 0 KA,0 = 1 protein B gene b 0 1 lBA — 1 Revealing the Story Behind Boolean Network Approach FGF FRS2 i- ERK KFGF,® = 0 KFGF,{FGF} = 1 KFRs2,® = 0 KFRS2,{FGF} = 1 KFRS2,{ERK} = 0 KFRS2,{FGF,ERK} KErk,9 = 0 KERK,{FRS2} = 1 = 0 KFGF,Q = 0 KFGF,{FGF} = 1 KFRS2i® = 0 Kfrs2, {FGF} = 1 KFRS2, {ERK} = 0 Kfrs2, {FGF, ERK} KErk,9 = 0 KErk, {FRS2} = 1 = 1 100 101 I 110 111 101 100 I (ITT) 110 Revealing the Story Behind Boolean Network Approach SHC KFRS2,{FGF,ERK} = 0 KErk,® = 0 KERK,{FRS2} = 1 KERK,{SHC} = 1 KERKi{FRS2,SHC} = l Kshc,Q = 0 Kshc, {FGF} = 1 1100 1000 1001 1101 1110 r 1010 1011 mi KFRS2,{FGF,ERK} = 1 KErk,Q = 0 Kerk, {FRS2} = 1 KERK, {SHC} = 1 Kerk, {FRS2, SHC} = 1 Kshc,Q = 0 Kshc, {FGF} = 1 1100 1101 1000 1010 1001 1011 1110 1111 Revealing the Story Behind Boolean Network Approach FGF hGhR Ras Raf MEK T ERK Revealing the Story Behind Boolean Network Approach FGF hGhR Ras HOW MANY STATES HAS THE TRANSITION SYSTEM? Raf MLK ERK Revealing the Story Behind Boolean Network Approach FGF SHC GS HOW MANY STATES HAS THE TRANSITION SYSTEM? HOW MANY MODELS WE CAN MAKE BASED ON THIS NETWORK? K? Revealing the Story Behind Boolean Network Approach USE MODEL CHECKING WITH TEMPORAL LOGICS Ras HOW MANY STATES HAS THE TRANSITION SYSTEM? Raf MLK ERK HOW MANY MODELS WE CAN MAKE BASED ON THIS NETWORK? K? Kripke Structure Definition Let AP be the set of atomic propositions (logical expressions over model variables, typical inequalities). Kripke structure is the quadruple K = (S, So, T, L) where: • S is the finite set of states • So Q S is the set of inititial states • T C S x S such that Vs e S, 3s; e S : (s, s;) e 7" • L is the labeling L : S —>► 2^p Kripke structure - properties • for a state s e S, L(s) represents the set of all atomic propositions satisfied in s • unfolding of the Kripke structure from any initial state is always an infinite-depth tree 9 maximal paths in the unfolding represent individual (infinite) executions of the Kripke structure Linear-time Temporal Logic - syntax Let AP be the set of atomic propositions. Formula tp is linear temporal logic (LTL) formula iff the following holds: • cp = p for any p 6 /4P • If (£>i and y?2 LTL formulae then: • ^Pi, ^1 A ^2 and (^i V ip2 are LTL formulae • X(pi, Fcpi a Gy?i are LTL formulae • (fili(f2 a are LTL formulae Linear Temporal Logic - semantics Let 7r = so, si,s/,... be an infinite sequence of states (a path) in a Kripke structure K. For j > 0 we denote 7T7 the suffix Sj, sy+i,s/,.... Satisfiability relation |= is defined by induction: • 7T |= p iff p e i-(so) • 7T |= iff 7T ^= • |= if I A (^2 iff 7T |= ^1 and 7T |= (f2 • 7T |= (fil V y?2 iff |= (fl Or 7T |= (f2 • 7T |= iff 7T1 |= © 7T |= F(/9 iff 3/ > 0. 7T1 |= If a 7T |= G(£> iff V/ > 0. 7T1 |= • 7r |= v^iU(^2 iff 3y > 0.7T7' |= and V/ < j. tv1 |= tpi a 7r |= (^iR(^2 iff Vy > 0, V0 < / < j. 7r' ^= =4> 7r7' |= y>2- Linear Temporal Logic - semantics Model checking Kripke structure as a model for a formula Let K be a Kripke structure. A formula cp is satisfied by K, K |= cp iff for each execution tv = sq, ... such that sq G Sq it holds 7r |= y?. Model Checking Problem Model checking problem is to deside for a given Kripke structure K and a temporal property 0 the problem K |= 0. If the result is negative, a path tt such that 7r ^= 0 is returned (a so-called counterexample). Model-Checking Overview Requirements System Formalization I Property Specification Formalization System Model Error 1 Simulation Model Checking Invalid Counterexample Valid Temporal Properties Transient vs. Sustained Dynamics Sustained Dynamics FG(ERK > 0) FG(FRS2 > 0) FG(ERK > 0) A FG(FRS2 > 0) Transient Dynamics F(ERK > 0) A GF(ERK < 1) F(ERK > 0) A GF(ERK < 1) Revealing the Story Behind Growth Factor Signalling Boolean Network Approach FGF Kshp2-as, {FRS2} = 1 KshP2-as, {Gobi} = 1 KshP2-as, {FRS2, Gobi} = 1 KShP2-GS, {ERK, FRS2} = 1 KShP2-GS, {ERK, Gabl} = 1 Kshp2-as, {ERK, FRS2, Gabl} KShp2-GS, {ERK} = 0 = 1 Ar9i)0 = o KFGFR, {FGF} = 1 Kshc, {FGFR} = 1 KGabl,{FGFR} = l KFRS2,{FGFR} = 1 KFRS2, {FGFR, ERK} = 1 KFRS2,{ERK} = Q KRas, {GS} = 1 KRas, {Shp2 -GS} = 1 KRas,{GS,Shp2-GS} = \ KRaf,{Ras} = 1 Kmek, {Raf} = 1 KERK,{MEK} = 1 KGS, {SHC} = 1 KGS, {Gabl} = 1 KGS, {SHC, Gabl} = 1 KGS,{ERK,Gabl} = 0 KGS, {ERK, SHC} = 0 KGS, {ERK, SHC, Gabl} = 0 KGS, {ERK} = 0 Revealing the Story Behind Growth Factor Signalling Boolean Network Approach FGF Kg%,Q = 0 FGFR Kfgfr, {FGF} = 1 Kshc, {FGFR} = 1 SMC Gab1 FRS 2 KGabi, {FGFR} = 1 KFRS2,{FGFR} = \ Satisfied Properties • (FG(ERK > 0)) V (F(ERK > 0) A GF(ERK < 1)) = TRUE FG(FRS2 > 0) = TRUE ERK Kshp2-Kshp2-Kshp2-Kshp2-Kshp2-Kshp2-Kshp2- .GS,{FRS2} = 1 GS,{Gabl} = l -gs, {FRS2, Gabl} = 1 GS,{ERK,FRS2} = 1 GS,{ERK,Gabl} = l gs, {ERK, FRS2, Gabl} GS,{ERK} = 0 = 1 KGS,{SHC} = 1 Kgs, {Gabl} = 1 KGs,{SHC, Gabl} = 1 KGS,{ERK, Gabl} = 0 KGs,{ERK,SHC} = 0 Kgs, {ERK, SHC, Gabl} KGS,{ERK} = 0 = 0 From Model Checking to Parameter Synthesis temporal constraints Model M(p) : parameterised dynamics fr y parameter constraints 0/ Parameter Synthesis Problem Assume V is the admissible parameter space. Given a behaviour constraint cp, parameter constraint 0/, and a parameterised model A4, find the maximal set P C V of parameterisations such that p |= 0/ and M(p) |=

FGFR(L!1,R).FGF(R!1) begin molecule types FGF (R) FGFR(L,R,Y1~u~p,Y2 ~u~p) FRS2(pR,Yl~u~p,Thl~u~p,S) GS(SH2,REM) SHIP(Y~u~p) SFK(Y~u~p) RAS(sos,g~GDP~GTP) RasGAP(ras) RAF(S~A~I~P) MEK(T2 92~U~P,S~U~P~PP) ERK(S~U~P~PP) end molecule types kpl, kml # Receptor-dimerisation FGFR(L!+,R) + FGFR(L!+,R) <-> FGFR(L!+,R!3).FGFR(L!+,R!3) kp2, km2 # FRS2 phosphorylation by FGFR FGFR(R!+,Yl~p!1).FRS2(pR!1,Yl~u,Thl~u) -> FGFR(R!+,Yl~p!1).FRS2(pR!1,Yl~p,Thl~u) kpl4 FRS2(pR!+,Yl~p) -> FRS2(pR!+,Yl~u) kml4 #SFK-mediated FRS2 phosphorylation (hypothetised) FRS2(Yl~u) + SFK(Y~p) -> FRS2(Yl~p) + SFK(Y~p) 1000*kpl4 Revealing the Story Behind Growth Factor Signalling Rule-Based Approach c 2.00E0S 3 + [ECH] d[CPD] k3-EchA-[ECH] kA- HheC -[CPD] dt ~ Km>3 + [ECH] KmA + [CPD] d[GDL] kA- HheC -[CPD] k5-HheC-[GDL] dt ~ KmA+[CPD] Km}5 + [GDL] d[GLY] k5- HheC -[GDL] dt ~ Km^ + [GDL] o biodegradation of toxic substrate and intermediates • synthetic pathway utilising enzymes from two other bacteria Rhodococcus rhodochrous NCI MB 13064; Agrobacterium radiobacter AD1 • find optimal enzymes concentration balancing metabolic burden and toxicity Modelling Frameworks state-transition systems states: discrete molecule numbers or qualities (on/off) ualitative model stochastic model J Continuous-Time Markov Chains states: discrete molecule numbers ^ approximation abstracted time modeled t continuous model Ordinary Differential Equations states: continuous concentrations states discrete continuous The Approach: Rectangular Abstraction of ODE From a Continuous System to a Discrete Finite Quotient P. Collins, L. Habets, J.H. van Schuppen, I. Černá, J. Fabriková, and D. Šafránek. Abstraction of Biochemical Reaction Systems on Polytopes. In Proceedings of 18th IFAC World Congress, 2011. Parameter Synthesis over Rectangular Abstraction Phase Space Discretisation Leads to Parameter Space Discretisation b 5 dA Hi = -ki ■ A + k2- B dB ~~di = ki ■ A - k2- B k2 = 0.8 /ci = 0.6 5 a Parameter Synthesis over Rectangular Abstraction Phase Space Discretisation Leads to Parameter Space Discretisation b 5 dA Hi dB ~~di = -ki ■ A + k2- B = ki ■ A - k2- B k2 = 0.8 /ci = 0.6 2.5 \\\\\ \ \ \ \ ^ \ \ \ \ ^ \ \ \ ^ ^ \ \ \ * \ \ \ * * ■ a -J J j« ji J > r ' 1 1 i~ IT N S. * * ' Sj * 31 A i( X 1 j a -J r i"" r i j r r rc k k k K r r * * N - r k K \ N K ^ \ \ \ \ \ \ \ \ \ \ \ \ \ 0 2.5 5 a Parameter Synthesis over Rectangular Abstraction Phase Space Discretisation Leads to Parameter Space Discretisation b 5 dA Hi = -ki ■ A + k2- B dB ~~di = ki ■ A - k2- B k2 = 0.8 /ci = 0.6 ! * j j A 0 4 r rz K \ N k \ \ \ \ \ \ \ \ \ 5 a Parameter Synthesis over Rectangular Abstraction Phase Space Discretisation Leads to Parameter Space Discretisation b 5 dA Hi = -ki ■ A + k2- B dB ~~di = ki ■ A - k2- B k2 = 0.8 /ci = 0.6 5 a Parameter Synthesis over Rectangular Abstraction Phase Space Discretisation Leads to Parameter Space Discretisation (0,0.4) (0.4,0.8) (0.8,1.6) (1.6,max) o \ \ \ \ \ \ \ \ \ \ o \ \ \ \ 0 \ \ \ Parameter Synthesis over Rectangular Abstraction Phase Space Discretisation Leads to Parameter Space Discretisation B 5 dA ~di dB ~~di = -ki ■ A + k2- B = ki ■ A - k2 ■ B k2 = 0.8 ki = ? : O:. 0 r rc K N \ \ \ \ \ \ \ ^ \ W% 5 A (0,0.4) (0.4,0.8) (0.8,1.6) (1.6,max) o \ \ \ \ \ \ \ \ o \ \ \ \ 0 \ \ -2.5 -ki>0 2.5-/ci+2.5-/c2 > 0 Parameter Synthesis over Rectangular Abstraction Phase Space Discretisation Leads to Parameter Space Discretisation dA ~di = -ki ■ A + k2- B dB ~~di = ki ■ A - k2- B k2 = 0.8 ki = ? b 5 2.5^ W \ \ \ \ \ ^ ^ S s » V ii x J : O:. 4 o \ \ \ \ \ \ \ 5 a 0 stateOO—estate 10 = -2.5 • /ci > 0 V -2.5 • /ci + 2.5 • k2 > 0 The transition exists if and only if the formula is satisfiable. Local parameter constraints are predicates over reals. Parameter Synthesis over Rectangular Abstraction parameterized Kripke structure of the model [B] 2.5 £2 1 ^1 e y i f—^i ► ► 2.5 [A] o o CD Q. O < identify states and colors for which the property does/doesn't hold YES NO parameter intervals where the specification is guaranteed (some might be missing) parameter intervals where the specification might be violated Parameterised Kripke Structures State Transition Systems with Parameters Transitions with Parameters (coloured transitions) <* each parameter valuation represents one Kripke structure • shared state space, different transition space Parameterised Kripke Structures State Transition Systems with Parameters Transitions with Parameters (coloured transitions) <* each parameter valuation represents one Kripke structure • shared state space, different transition space Pithya Tool % C:/Users/User/skola/pracovny/R/vector_field_multi_dim - Shiny http://127.fi.0,1:5294 Open in Browser number of arrows parameter y_pRB 100 0 EHH I 1 1 I 1 1 I 1 1 I 1 1 I 1 1 I 1 1 I 1 'T' 1 I 1 1 I 11 I I 1 1 I mi I 1 1 I 1 1 I 1 1 I 1 1 I 1 1 I 1 1 I 1 1 I 1 1 I ~' I 1 1 I 1 1 I 1 1 I 1 1 I 1 1 I 1 1 I 1 1 I 1 1 I 1 1 I I 1 1 I 1 1 I 1 1 I 1 1 I 1 1 I 1 1 I 1 1 I ■ 10 19 23 37 46 55 64 73 £2 91 100 0 0.01 O.02 003 0.04 0.05 0.06 007 O.OS 0.09 0.1 0 0.06 0.1 0.16 02 025 03 036 04 045 0.5 200 260 320 3SO 440 500 660 620 parameter y_pRB imiEi height of plots 0.5 200 coloring threshold 0 zoom in pRE D 1 0 (S 111 1 i1 111 1 i1 111 1 i1 111 1 i1 111 1 i 0 001 002 003 0.04 0.05 0.06 007 0.08 0.09 0.1 coloring direction C horizontal C vertical choose .bio file Choose File I ij3/model 1P sorjR-Mo (• both choose .json file Choose File 4.5 6 7.5 10.5 12 13.5 15 horizontal ax in plot 1 vertical ax in plot 1 pRB E2F1 w horizontal ax in plot 2 vertical ax in plot 2 ■w «Download image ■m Download image . Start - 1 * 1 1 1 1 - -i- 1 -s- •------"I 1 .......i - t 1 • «c- - t 1 1 1 ►------T 1 1 <- - ►------1 i - •------f 1 } - •------f 4 - •------"V i i • <- 1 I i I I 1 I 'l I I I I 1 1 1 1 1 I I I I I pRB aliolo ^1^1 http://pithya.ics.muni.cz U: S7.S4kbit's yj EN I « » S8 O O D: 2651.52 I .bit s I » « * V [CAV 2017] 0' Biodegradation of Trichloropropane in E. coli Desired behaviour: "TCP is finally completely degraded and the concentration of intermediates does not exceed given bounds" Formally: x)U(FG [TCP] < y)), y>2 = (([GLY] < y)U(FG [GLY] > x)), cps = (G [DCP] < v) A (G [GDL] < w), where x, y, v and w are estimated values making an instance of this property: • x = 1.9 (according to authors1 using the value 2 mM), • y = 0.01 (obviously, cannot be zero), • v G {0.5,0.3,0.1} (variations based on experimental data observation) • w G {0.5,0.25,0.1} (variations based on experimental data observation) "^urumbang et al., ACS Synthetic Biology, 2013 Biodegradation of Trichloropropane in E. coli 0.005 0.01 0.015 0.015 0.01 — 0.005 0.000 0.005 0.010 0.015 0.020 8 o d o o o US a) ° o d 0.000 0.005 0.010 DhaA 0.015 0.020 o d u LLI o d 0.000 0.005 0.010 0.015 0.020 DhaA HheC A sample of the resulting parameter space for a particular initial state: TCP G [1.9,1.9586], DCP G [0.448898, 0.5], GDL G [0.0, 0.0669138], GLY G [0.0, 0.01] Dotted area corresponds to if (v = 0.5, w = 0.25). Biodegradation of Trichloropropane in E. coli Preliminary Biological Validation DhaA 0 0.005 0.01 0.015 0.02 1—0.02 g 2.0 c 1.5 O 03 1.0 0.005 0 0.02 0.015 0.01 °-005 HheC c o ^ U O 0.0 U \ TCF GLY C )CP < ó c o O 50 100 150 200 250 300 Time (min) Biodegradation of Trichloropropane in E. coli Extending the Model with Population Growth Bact GLY "1-1-1-1-1-1— —i-1-1-1-1-r~ 02468 10 02468 10 time (h) time (h) Demko et al. Microorganisms (2019) Biodegradation of Trichloropropane in E. coli Extending the Model with Population Growth 0.0 H-1-1-1-1-r- 0 2 4 6 8 10 time (h) Demko et al. Microorganisms (2019) Biodegradation of Trichloropropane in E. coli Extending the Model with Population Growth 100 IPTG - - + + TCP + - + Demko et al. Microorganisms (2019) Biodegradation of Trichloropropane in E. coli Extending the Model with Population Growth d[Bact] dt d[GLY] dt rf[TCP] dt d[(R)-~DCP] = + + dt d[(S)-DCP] dt