Forward and Backward Bisimulations for Chemical Reaction Networks
We present two quantitative behavioral equivalences over species of a chemical reaction network (CRN) with semantics based on ordinary differential equations. Forward CRN bisimulation identifies a partition where each equivalence class represents the exact sum of the concentrations of the species belonging to that class. Backward CRN bisimulation relates species that have identical solutions at all time points when starting from the same initial conditions. Both notions can be checked using only CRN syntactical information, i.e., by inspection of the set of reactions. We provide a unified algorithm that computes the coarsest refinement up to our bisimulations in polynomial time. Further, we give algorithms to compute quotient CRNs induced by a bisimulation. As an application, we find significant reductions in a number of models of biological processes from the literature. In two cases we allow the analysis of benchmark models which would be otherwise intractable due to their memory requirements.
Chemical reaction networks
ordinary differential equations
bisimulation
partition refinement
226-239
Regular Paper
Luca
Cardelli
Luca Cardelli
Mirco
Tribastone
Mirco Tribastone
Max
Tschaikowski
Max Tschaikowski
Andrea
Vandin
Andrea Vandin
10.4230/LIPIcs.CONCUR.2015.226
C. Baier, B. Engelen, and M. E. Majster-Cederbaum. Deciding bisimilarity and similarity for probabilistic processes. J. Comput. Syst. Sci., 60(1):187-231, 2000.
D. Barua, J. R. Faeder, and J. M. Haugh. A bipolar clamp mechanism for activation of jak-family protein tyrosine kinases. PLoS Computational Biology, 5(4), 2009.
D. Barua and W. S. Hlavacek. Modeling the effect of apc truncation on destruction complex function in colorectal cancer cells. PLoS Comput Biol, 9(9):e1003217, 09 2013.
M. Bernardo. A survey of Markovian behavioral equivalences. In Formal Methods for Perf. Eval., volume 4486 of LNCS, pages 180-219. Springer Berlin Heidelberg, 2007.
M. L. Blinov, J. R. Faeder, B. Goldstein, and W. S. Hlavacek. BioNetGen: software for rule-based modeling of signal transduction based on the interactions of molecular domains. Bioinformatics, 20(17):3289-3291, 2004.
M. L. Blinov, J. R. Faeder, B. Goldstein, and W. S. Hlavacek. A network model of early events in epidermal growth factor receptor signaling that accounts for combinatorial complexity. Biosystems, 83:136-151, 2006.
P. Buchholz. Exact and Ordinary Lumpability in Finite Markov Chains. Journal of Applied Probability, 31(1):59-75, 1994.
P. Buchholz. Markovian Process Algebra: Composition and Equivalence. In Proc. 2nd Workshop on Process Algebra and Performance Modelling, Erlangen, Germany, 1994.
F. Camporesi and J. Feret. Formal reduction for rule-based models. Electronic Notes in Theoretical Computer Science, 276:29-59, 2011. MFPS XXVII.
Ferdinanda Camporesi, Jérôme Feret, Heinz Koeppl, and Tatjana Petrov. Combining model reductions. Electr. Notes Theor. Comput. Sci., 265:73-96, 2010.
L. Cardelli. Morphisms of reaction networks that couple structure to function. BMC Systems Biology, 8(1):84, 2014.
L. Cardelli and A. Csikász-Nagy. The cell cycle switch computes approximate majority. Sci. Rep., 2, 2012.
L. Cardelli, M. Tribastone, M. Tschaikowski, and A. Vandin. Forward and Backward Bisimulations for Chemical Reaction Networks. Extended Version. http://arxiv.org/abs/1507.00163. http://arxiv.org/abs/1507.00163, 2015.
http://arxiv.org/abs/1507.00163
J. Colvin, M. I. Monine, J. R. Faeder, W. S. Hlavacek, D. D. Von Hoff, and R. G. Posner. Simulation of large-scale rule-based models. Bioinformatics, 25(7):910-917, 2009.
J. Colvin, M. I. Monine, R. N. Gutenkunst, W. S. Hlavacek, D. D. Von Hoff, and R. G. Posner. Rulemonkey: software for stochastic simulation of rule-based models. BMC Bioinformatics, 11:404, 2010.
H. Conzelmann, J. Saez-Rodriguez, T. Sauter, B. Kholodenko, and E. Gilles. A domain-oriented approach to the reduction of combinatorial complexity in signal transduction networks. BMC Bioinformatics, 7(1):34, 2006.
V. Danos, J. Feret, W. Fontana, R. Harmer, and J. Krivine. Abstracting the differential semantics of rule-based models: Exact and automated model reduction. In LICS, pages 362-381, 2010.
V. Danos and C. Laneve. Formal molecular biology. TCS, 325(1):69-110, 2004.
R. De Nicola, U. Montanari, and F. Vaandrager. Back and forth bisimulations. In CONCUR, volume 458 of LNCS, pages 152-165. Springer, 1990.
J. R. Faeder, W. S. Hlavacek, I. Reischl, M. L. Blinov, H. Metzger, A. Redondo, C. Wofsy, and B. Goldstein. Investigation of early events in FcεRI-mediated signaling using a detailed mathematical model. The Journal of Immunology, 170(7):3769-3781, 2003.
J. Feret, T. Henzinger, H. Koeppl, and T. Petrov. Lumpability abstractions of rule-based systems. TCS, 431:137-164, 2012.
Jerome Feret, Heinz Koeppl, and Tatjana Petrov. Stochastic fragments: A framework for the exact reduction of the stochastic semantics of rule-based models. International Journal of Software and Informatics, 7(4):527-604, 2013.
J. Fisher and T.A. Henzinger. Executable cell biology. Nature Biotechnology, 25(11):1239-1249, 2007. See also correspondence in Nature Biotechnology 26(7):737-8;738-9, 2008.
D. Gillespie. The chemical Langevin equation. The Journal of Chemical Physics, 113(1):297-306, 2000.
J. Heath, M. Kwiatkowska, G. Norman, D. Parker, and O. Tymchyshyn. Probabilistic model checking of complex biological pathways. TCS, 391(3):239-257, 2008.
H. Hermanns and M. Rettelbach. Syntax, semantics, equivalences, and axioms for MTIPP. In Proceedings of Process Algebra and Probabilistic Methods, pages 71-87, Erlangen, 1994.
J. Hillston. A Compositional Approach to Performance Modelling. CUP, 1996.
P. Kocieniewski, J. R. Faeder, and T. Lipniacki. The interplay of double phosphorylation and scaffolding in MAPK pathways. Journal of Theoretical Biology, 295:116-124, 2012.
K. G. Larsen and A. Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1):1-28, 1991.
M. S. Okino and M. L. Mavrovouniotis. Simplification of mathematical models of chemical reaction systems. Chemical Reviews, 2(98):391-408, 1998.
R. Paige and R. Tarjan. Three partition refinement algorithms. SIAM Journal on Computing, 16(6):973-989, 1987.
S. W. Shin, C. Thachuk, and E. Winfree. Verifying chemical reaction network implementations: A pathway decomposition approach. In VEMPD, Vienna Summer of Logic, 2014.
M. W. Sneddon, J. R. Faeder, and T. Emonet. Efficient modeling, simulation and coarse-graining of biological complexity with NFsim. Nature Methods, 8(2):177-183, 2011.
J. Sproston and S. Donatelli. Backward Bisimulation in Markov Chain Model Checking. IEEE Trans. Software Eng., 32(8):531-546, 2006.
R. Suderman and E. J. Deeds. Machines vs. ensembles: Effective MAPK signaling through heterogeneous sets of protein complexes. PLoS Comput Biol, 9(10):e1003278, 10 2013.
J. Toth, G. Li, H. Rabitz, and A. S. Tomlin. The effect of lumping and expanding on kinetic differential equations. SIAM Journal on Applied Mathematics, 57(6):1531-1556, 1997.
M. Tschaikowski and M. Tribastone. Exact fluid lumpability for Markovian process algebra. In CONCUR, LNCS, pages 380-394, 2012.
M. Tschaikowski and M. Tribastone. A unified framework for differential aggregations in Markovian process algebra. JLAMP, 84(2):238-258, 2015.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode