Abstract
Probabilistic model checking is a formal verification technique that has been successfully applied to the analysis of systems from a broad range of domains, including security and communication protocols, distributed algorithms and power management. In this paper we illustrate its applicability to a complex biological system: the FGF (Fibroblast Growth Factor) signalling pathway. We give a detailed description of how this case study can be modelled in the probabilistic model checker PRISM, discussing some of the issues that arise in doing so, and show how we can thus examine a rich selection of quantitative properties of this model. We present experimental results for the case study under several different scenarios and provide a detailed analysis, illustrating how this approach can be used to yield a better understanding of the dynamics of the pathway.
Supported in part by EPSRC grants GR/S72023/01, GR/S11107 and GR/S46727 and Microsoft Research Cambridge contract MRL 2005-44.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Verifying continuous time Markov chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 269–276. Springer, Heidelberg (1996)
Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model checking continuous-time Markov chains by transient analysis. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 358–372. Springer, Heidelberg (2000)
Calder, M., Gilmore, S., Hillston, J.: Modelling the influence of RKIP on the ERK signalling pathway using the stochastic process algebra PEPA. Transactions on Computational Systems Biology (to appear, 2006)
Calder, M., Vyshemirsky, V., Gilbert, D., Orton, R.: Analysis of signalling pathways using continuous time Markov chains. Transactions on Computational Systems Biology (to appear, 2006)
Dikic, I., Giordano, S.: Negative receptor signalling. Curr. Opin. Cell Biol. 15, 128–135 (2003)
Eswarakumar, V., Lax, I., Schlessinger, J.: Cellular signaling by fibroblast growth factor receptors. Cytokine Growth Factor Rev. 16(2), 139–149 (2005)
Gillespie, D.: Exact stochastic simulation of coupled chemical reactions. Journal of Physical Chemistry 81(25), 2340–2361 (1977)
Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, Cambridge (1996)
Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006)
Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: A hybrid approach. International Journal on Software Tools for Technology Transfer (STTT) 6(2), 128–142 (2004)
Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic model checking in practice: Case studies with PRISM. ACM SIGMETRICS Performance Evaluation Review 32(4), 16–21 (2005)
Phillips, A., Cardelli, L.: A correct abstract machine for the stochastic pi-calculus. In: Proc. BioCONCUR 2004. ENTCS. Elsevier, Amsterdam (2004)
PRISM, web site, www.cs.bham.ac.uk/~dxp/prism
Priami, C.: Stochastic π-calculus. The Computer Journal 38(7), 578–589 (1995)
Priami, C., Regev, A., Silverman, W., Shapiro, E.: Application of a stochastic name passing calculus to representation and simulation of molecular processes. Information Processing Letters 80, 25–31 (2001)
Regev, A., Shapiro, E.: Cellular abstractions: Cells as computation. Nature 419(6905), 343 (2002)
Regev, A., Silverman, W., Shapiro, E.: Representation and simulation of biochemical processes using the pi- calculus process algebra. In: Altman, R., Dunker, A., Hunter, L., Klein, T. (eds.) Pacific Symposium on Biocomputing, 2001, vol. 6, pp. 459–470. World Scientific Press, Singapore (2001)
Rutten, J., Kwiatkowska, M., Norman, G., Parker, D.: Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. CRM Monograph Series, vol. 23. AMS (2004)
Schlessinger, J.: Epidermal growth factor receptor pathway. Sci. STKE (Connections Map), http://stke.sciencemag.org/cgi/cm/stkecm;CMP_14987
Tsang, M., Dawid, I.: Promotion and attenuation of FGF signaling through the Ras-MAPK pathway. Science STKE, 17 (2004)
Tymchyshyn, O., Norman, G., Heath, J., Kwiatkowska, M.: Computer assisted biological reasoning: The simulation and analysis of FGF signalling pathway dynamics (submitted for publication)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Heath, J., Kwiatkowska, M., Norman, G., Parker, D., Tymchyshyn, O. (2006). Probabilistic Model Checking of Complex Biological Pathways. In: Priami, C. (eds) Computational Methods in Systems Biology. CMSB 2006. Lecture Notes in Computer Science(), vol 4210. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11885191_3
Download citation
DOI: https://doi.org/10.1007/11885191_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-46166-1
Online ISBN: 978-3-540-46167-8
eBook Packages: Computer ScienceComputer Science (R0)