Using probabilistic model checking in systems biology

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Using probabilistic model checking in systems biology

Full text

Pdf (18.59 MB)

Source

ACM SIGMETRICS Performance Evaluation Review archive
Volume 35 , Issue 4 (March 2008) table of contents

SPECIAL ISSUE: Special issue on the quantitative evaluation of biological systems table of contents

Pages 14-21

Year of Publication: 2008

ISSN:0163-5999

Authors

Marta Kwiatkowska	Oxford University, Oxford
Gethin Norman	Oxford University, Oxford
David Parker	Oxford University, Oxford

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 4, Downloads (12 Months): 68, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1364644.1364651 What is a DOI?

ABSTRACT

Probabilistic model checking is a formal verification framework for systems which exhibit stochastic behaviour. It has been successfully applied to a wide range of domains, including security and communication protocols, distributed algorithms and power management. In this paper we demonstrate its applicability to the analysis of biological pathways and show how it can yield a better understanding of the dynamics of these systems. Through a case study of the MAP (Mitogen-Activated Protein) Kinase cascade, we explain how biological pathways can be modelled in the probabilistic model checker PRISM and how this enables the analysis of a rich selection of quantitative properties.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Adnan Aziz , Kumud Sanwal , Vigyan Singhal , Robert Brayton, Model-checking continuous-time Markov chains, ACM Transactions on Computational Logic (TOCL), v.1 n.1, p.162-170, July 2000 [doi>10.1145/343369.343402]
	2	C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen. Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Software Engineering, 29(6):524--541, 2003.
	3	M. Calder, S. Gilmore, and J. Hillston. Modelling the influence of RKIP on the ERK signalling pathway using the stochastic process algebra PEPA. Trans. Computational Systems Biology, 7:1--23, 2006.
	4	M. Calder, V. Vyshemirsky, D. Gilbert, and R. Orton. Analysis of signalling pathways using continuous time Markov chains. Trans. Computational Systems Biology, 4:44--67, 2006.
	5	E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
	6	Joost-Pieter Katoen , Maneesh Khattri , Reza Pulungan, Model Checking Markov Reward Models with Impulse Rewards, Proceedings of the 2005 International Conference on Dependable Systems and Networks, p.722-731, June 28-July 01, 2005 [doi>10.1109/DSN.2005.64]
	7	Alastair F. Donaldson , Alice Miller , David Parker, GRIP: Generic Representatives in PRISM, Proceedings of the Fourth International Conference on Quantitative Evaluation of Systems, p.115-116, September 17-19, 2007 [doi>10.1109/QEST.2007.23]
	8	E. Emerson and T. Wahl. On combining symmetry reduction and symbolic representation for efficientc model checking. In D. Geist and E. Tronci, editors, Proc. 12th Conf. Correct Hardware Design and Verification Methods (CHARME 2003), volume 2860 of Lecture Notes in Computer Science, pages 216--230. Springer, 2003.
	9	D. Gillespie. Exact stochastic simulation of coupled chemical reactions. Journal of Physical Chemistry, 81(25):2340--2361, 1977.
	10	Stephen Gilmore , Jane Hillston, The PEPA workbench: a tool to support a process algebra-based approach to performance modelling, Proceedings of the 7th international conference on Computer performance evaluation : modelling techniques and tools: modelling techniques and tools, p.353-368, June 1994, Vienna, Austria
	11	H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6(5):512--535, 1994.
	12	John Heath , Marta Kwiatkowska , Gethin Norman , David Parker , Oksana Tymchyshyn, Probabilistic model checking of complex biological pathways, Theoretical Computer Science, v.391 n.3, p.239-257, February, 2008 [doi>10.1016/j.tcs.2007.11.013]
	13	H. Hermanns, J.-P. Katoen, J. Meyer-Kayser, and M. Siegle. A tool for model checking Markov chains. Software Tools for Technology Transfer, 4(2):153--172, 2003.
	14	Jane Hillston, A compositional approach to performance modelling, Cambridge University Press, New York, NY, 1996
	15	A. Hinton, M. Kwiatkowska, G. Norman, and D. Parker. PRISM: A tool for automatic verification of probabilistic systems. In H. Hermanns and J. Palsberg, editors, Proc. 12th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06), volume 3920 of Lecture Notes in Computer Science, pages 441--444. Springer, 2006.
	16	C. Huang and J. Ferrell. Ultrasensitivity in the mitogen-activated protein kinase cascade. Proc. Natl. Acad. Sci., 93:10078--10083, 1996.
	17	Joost-Pieter Katoen , Maneesh Khattri , Ivan S. Zapreev, A Markov Reward Model Checker, Proceedings of the Second International Conference on the Quantitative Evaluation of Systems (QEST'05) on The Quantitative Evaluation of Systems, p.243, September 19-22, 2005 [doi>10.1109/QEST.2005.2]
	18	Marta Kwiatkowska , Gethin Norman , David Parker, Probabilistic symbolic model checking with PRISM: a hybrid approach, International Journal on Software Tools for Technology Transfer (STTT), v.6 n.2, p.128-142, August 2004 [doi>10.1007/s10009-004-0140-2]
	19	Marta Kwiatkowska , Gethin Norman , David Parker, Probabilistic model checking in practice: case studies with PRISM, ACM SIGMETRICS Performance Evaluation Review, v.32 n.4, p.16-21, March 2005 [doi>10.1145/1059816.1059820]
	20	M. Kwiatkowska, G. Norman, and D. Parker. Symmetry reduction for probabilistic model checking. In T. Ball and R. Jones, editors, Proc. 18th Int. Conf. Computer Aided Verification (CAV'06), volume 4114 of Lecture Notes in Computer Science, pages 234--248. Springer, 2006.
	21	M. Kwiatkowska, G. Norman, and D. Parker. Stochastic model checking. In M. Bernardo and J. Hillston, editors, Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM'07), volume 4486 of Lecture Notes in Computer Science, pages 220--270. Springer, 2007.
	22	P. Lecca and C. Priami. Cell cycle control in eukaryotes: A BioSpi model. In Proc. Workshop Concurrent Models in Molecular Biology (BioConcur'03), Electronic Notes in Theoretical Computer Science, 2003.
	23	Gethin Norman , Catuscia Palamidessi , David Parker , Peng Wu, Model checking the probabilistic pi-calculus, Proceedings of the Fourth International Conference on Quantitative Evaluation of Systems, p.169-178, September 17-19, 2007 [doi>10.1109/QEST.2007.27]
	24	D. Parker. Implementation of Symbolic Model Checking for Probabilistic Systems. PhD thesis, University of Birmingham, 2002.
	25	A. Phillips and L. Cardelli. Efficient, correct simulation of biological processes in the stochastic π-calculus. In M. Calder and S. Gilmore, editors, Proc. 5th Int. Conf. Computational Methods in Systems Biology (CMSB'07), volume 4695 of Lecture Notes in Bioinformatics, pages 184--199. Springer Verlag, 2007.
	26	PRISM web site. http://www.prismmodelchecker.org/.
	27	C. Priami. Stochastic π-calculus. The Computer Journal, 38(7):578--589, 1995.
	28	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]
	29	T. Pronk, E. de Vink, D. Bosnacki, and T. Breit. Stochastic modeling of Codon bias with PRISM. In I. Linden and C. Talcott, editors, Proc. 3rd Int. Workshop Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems (MTCoord 2007). Computer Science Department, University of Cyprus, Nicosia, 2007.
	30	F. Romero-Campero, M. Gheorghe, L. Bianco, D. Pescini, M. Prez-Jimnez, and R. Ceterchi. Towards probabilistic model checking on P Systems using PRISM. In H. Hoogeboom, G. Paun, G. Rozenberg, and A. Salomaa, editors, Proc. 7th Int. Workshop Membrane Computing (WMC06), volume 4361 of Lecture Notes in Computer Science, pages 477--495. Springer, 2006.
	31	J. Rutten, M. Kwiatkowska, G. Norman, and D. Parker. Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems, volume 23 of CRM Monograph Series. AMS, 2004.
	32	SBML-to-PRISM translator. http://www.prismmodelchecker.org/sbml/.
	33	SBML web site. http://sbml.org/.
	34	O. Wolkenhauer, M. Ullah, W. Kolch, and K.-H. Cho. Modeling and simulation of intracellular dynamics: choosing an appropriate framework. IEEE Trans. Nanobioscience, 3:200--207, 2004.
	35	H. Younes. Ymer: A statistical model checker. In K. Etessami and S. Rajamani, editors, Proc. 17th Int. Conf. Computer Aided Verification (CAV'05), volume 3576 of Lecture Notes in Computer Science, pages 429--433. Springer, 2005.
	36	Håkan L. S. Younes , Marta Kwiatkowska , Gethin Norman , David Parker, Numerical vs. statistical probabilistic model checking, International Journal on Software Tools for Technology Transfer (STTT), v.8 n.3, p.216-228, June 2006 [doi>10.1007/s10009-005-0187-8]