Document Open Access Logo

Forward and Backward Bisimulations for Chemical Reaction Networks

Authors Luca Cardelli, Mirco Tribastone, Max Tschaikowski, Andrea Vandin

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2015.226.pdf
  • Filesize: 0.5 MB
  • 14 pages

Document Identifiers

Author Details

Luca Cardelli
Mirco Tribastone
Max Tschaikowski
Andrea Vandin

Cite AsGet BibTex

Luca Cardelli, Mirco Tribastone, Max Tschaikowski, and Andrea Vandin. Forward and Backward Bisimulations for Chemical Reaction Networks. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 226-239, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.CONCUR.2015.226

Abstract

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.
Keywords
  • Chemical reaction networks
  • ordinary differential equations
  • bisimulation
  • partition refinement

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. 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. Google Scholar
  2. 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. Google Scholar
  3. 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. Google Scholar
  4. 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. Google Scholar
  5. 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. Google Scholar
  6. 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. Google Scholar
  7. P. Buchholz. Exact and Ordinary Lumpability in Finite Markov Chains. Journal of Applied Probability, 31(1):59-75, 1994. Google Scholar
  8. P. Buchholz. Markovian Process Algebra: Composition and Equivalence. In Proc. 2nd Workshop on Process Algebra and Performance Modelling, Erlangen, Germany, 1994. Google Scholar
  9. F. Camporesi and J. Feret. Formal reduction for rule-based models. Electronic Notes in Theoretical Computer Science, 276:29-59, 2011. MFPS XXVII. Google Scholar
  10. Ferdinanda Camporesi, Jérôme Feret, Heinz Koeppl, and Tatjana Petrov. Combining model reductions. Electr. Notes Theor. Comput. Sci., 265:73-96, 2010. Google Scholar
  11. L. Cardelli. Morphisms of reaction networks that couple structure to function. BMC Systems Biology, 8(1):84, 2014. Google Scholar
  12. L. Cardelli and A. Csikász-Nagy. The cell cycle switch computes approximate majority. Sci. Rep., 2, 2012. Google Scholar
  13. 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.
  14. 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. Google Scholar
  15. 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. Google Scholar
  16. 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. Google Scholar
  17. 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. Google Scholar
  18. V. Danos and C. Laneve. Formal molecular biology. TCS, 325(1):69-110, 2004. Google Scholar
  19. R. De Nicola, U. Montanari, and F. Vaandrager. Back and forth bisimulations. In CONCUR, volume 458 of LNCS, pages 152-165. Springer, 1990. Google Scholar
  20. 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. Google Scholar
  21. J. Feret, T. Henzinger, H. Koeppl, and T. Petrov. Lumpability abstractions of rule-based systems. TCS, 431:137-164, 2012. Google Scholar
  22. 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. Google Scholar
  23. 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. Google Scholar
  24. D. Gillespie. The chemical Langevin equation. The Journal of Chemical Physics, 113(1):297-306, 2000. Google Scholar
  25. J. Heath, M. Kwiatkowska, G. Norman, D. Parker, and O. Tymchyshyn. Probabilistic model checking of complex biological pathways. TCS, 391(3):239-257, 2008. Google Scholar
  26. 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. Google Scholar
  27. J. Hillston. A Compositional Approach to Performance Modelling. CUP, 1996. Google Scholar
  28. 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. Google Scholar
  29. K. G. Larsen and A. Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1):1-28, 1991. Google Scholar
  30. M. S. Okino and M. L. Mavrovouniotis. Simplification of mathematical models of chemical reaction systems. Chemical Reviews, 2(98):391-408, 1998. Google Scholar
  31. R. Paige and R. Tarjan. Three partition refinement algorithms. SIAM Journal on Computing, 16(6):973-989, 1987. Google Scholar
  32. S. W. Shin, C. Thachuk, and E. Winfree. Verifying chemical reaction network implementations: A pathway decomposition approach. In VEMPD, Vienna Summer of Logic, 2014. Google Scholar
  33. 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. Google Scholar
  34. J. Sproston and S. Donatelli. Backward Bisimulation in Markov Chain Model Checking. IEEE Trans. Software Eng., 32(8):531-546, 2006. Google Scholar
  35. 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. Google Scholar
  36. 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. Google Scholar
  37. M. Tschaikowski and M. Tribastone. Exact fluid lumpability for Markovian process algebra. In CONCUR, LNCS, pages 380-394, 2012. Google Scholar
  38. M. Tschaikowski and M. Tribastone. A unified framework for differential aggregations in Markovian process algebra. JLAMP, 84(2):238-258, 2015. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact