Simulation and verification for computational modelling of signalling pathways

ABSTRACT

Modelling of the dynamics of biochemical reaction networks typically proceeds by solving ordinary differential equations or stochastic simulation via the Gillespie algorithm. More recently, computational methods such as process algebra techniques have been successfully applied to the analysis of signalling pathways. One advantage of these is that they enable automatic verification of the models, via model checking, against qualitative and quantitative temporal logic specifications, for example, "what is the probability that the protein eventually degrades?". Such verification is exhaustive, that is, the analysis is carried out over all paths, producing exact quantitative measures. In this paper, we give an overview of the simulation, verification and differential equation approaches to modelling biochemical reaction networks. We discuss the advantages and disadvantages of the respective methods, using as an illustration a fragment of the FGF signalling pathway.

REFERENCES

• 1: Antoniotti, M., A. Policriti, N. Ugel, and B. Mishra. 2003. Model building and model checking for biochemical processes. Cell Biochemistry and Biophysics 38.
• 2: Calder, M., S. Gilmore, and J. Hillston. 2006a. Modelling the influence of RKIP on the ERK signalling pathway using the stochastic process algebra PEPA. Transactions on Computational Systems Biology 4230.
• 3: Calder, M., V. Vyshemirsky, D. Gilbert, and R. Orton. 2006b. Analysis of signalling pathways using continuous time Markov chains. Transactions on Computational Systems Biology 4220.
• 4: Cardelli, L., and A. Phillips. 2004. A correct abstract machine for the stochastic pi-calculus. In Proceedings of BioConcur'04.
• 5: Eccher, C. 2006. Translation of Systems Biology Markup Language into process algebra. Ph.D. thesis.
• 6: Frame, M. 2004. Newest findings on the oldest oncogene; how activated Src does it. Journal of Cell Science 117.
• 7: Gillespie, D. 1977. Exact stochastic simulation of coupled chemical reactions. Journal of Physical Chemistry 81(25).
• 8: Heath, J., M. Kwiatkowska, G. Norman, D. Parker, and O. Tymchyshyn. 2006. Probabilistic model checking of complex biological pathways. In Proceedings of the International Conference on Computational Methods in Systems Biology, Volume 4210 of LNBI: Springer.
• 9: Jane Hillston, A compositional approach to performance modelling, Cambridge University Press, New York, NY, 1996
• 10: Hinton, A., M. Kwiatkowska, G. Norman, and D. Parker. 2006. PRISM: A tool for automatic verification of probabilistic systems. In Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Volume 3920 of LNCS: Springer.
• 11: Kwiatkowska, M., G. Norman, and D. Parker. 2006. Symmetry reduction for probabilistic model checking. In Proceedings of the 18th International Conference on Computer Aided Verification, Volume 4144 of LNCS: Springer-Verlag.
• 12: Murray, J. 1989. Mathematical biology. Springer Verlag.
• 13: Novère, N. L., and T. Shimizu. 2001. Stochsim: modelling of stochastic biomolecular processes. Bioinformatics 17.
• 14: Phillips, A., and L. Cardelli. 2005. A graphical representation for the stochastic pi-calculus. In Proceedings of Bioconcur'05.
• 15: Piazza, C., M. Antoniotti, V. Mysore, A. Policriti, F. Winkler, and B. Mishra. 2005. Algorithmic algebraic model checking I: Challenges from systems biology. In Proceedings of the 17th International Conference on Computer Aided Verification, Volume 3576 of LNCS.
• 16: Corrado Priami , Aviv Regev , Ehud Shapiro , William Silverman, Application of a stochastic name-passing calculus to representation and simulation of molecular processes, Information Processing Letters, v.80 n.1, p.25-31, October 15, 2001 [doi>10.1016/S0020-0190(01)00214-9]
• 17: PRISM 2006. <www.cs.bham.ac.uk/dxp/prism>.
• 18: Regev, A., and E. Shapiro. 2002. Cells as computation. Nature 419.
• 19: Regev, A., and E. Shapiro. 2004. The pi-calculus as an abstraction for biomolecular systems. In Modelling in Molecular Biology: Springer.
• 20: Rutten, J., M. Kwiatkowska, G. Norman, and D. Parker. 2004. Mathematical techniques for analyzing concurrent and probabilistic systems, Volume 23 of CRM Monograph Series. American Mathematical Society.
• 21: SBML 2006. <http://sbml.org/index.psp>.
• 22: Shapiro, B., A. Levchenko, E. Meyerowitz, B. Wold, and E. Mjolsness. 2003. Cellerator: extending a computer algebra system to include biochemical arrows for signal transduction simulations. Bioinformatics 19 (5).
• 23: M. Tokman, Efficient integration of large stiff systems of ODEs with exponential propagation iterative (EPI) methods, Journal of Computational Physics, v.213 n.2, p.748-776, 10 April 2006 [doi>10.1016/j.jcp.2005.08.032]
• 24: Ware, M., D. Tice, S. Parsons, and D. Lauffenburger. 1997. Overexpression of cellular Src in fibroblasts enhances endocytic internalization of Epidermal Growth Factor receptor. Journal of Biological Chemistry 272.
• 25: Wolkenhauer, O., M. Ullah, W. Kolch, and K. Cho. 2004. Modeling and simulation of intracellular dynamics: choosing an appropriate framework. IEEE Transactions on Nanobioscience 3.
• 26: Yamada, S., T. Taketomi, and A. Yoshimura. 2004. Model analysis of difference between EGF pathway and FGF pathway. Biochemical and Biophysical Research Communications 314.