Marta Kwiatkowska
David Parker
Skip Abstract Section
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.
- A. Aziz, K. Sanwal, V. Singhal, and R. Brayton. Model checking continuous time Markov chains. ACM Trans. Computational Logic, 1(1):162--170, 2000. Google Scholar
Digital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- E. Clarke, E. Emerson, and A. Sistla. Automatic verification of finite-state concurrent systems using temporal logics. ACM Trans. Programming Languages and Systems, 8(2):244--263, 1986. Google ScholarDigital Library
- L. Cloth, J.-P. Katoen, M. Khattri, and R. Pulungan. Model checking Markov reward models with impulse rewards. In Proc. Int. Conf. Dependable Systems and Networks (DSN'05), pages 722--731. IEEE Computer Society Press, 2005. Google ScholarDigital Library
- A. Donaldson, A. Miller, and D. Parker. GRIP: Generic representatives in PRISM. In Proc. 4th Int. Conf. Quantitative Evaluation of Systems (QEST'07), pages 115--116. IEEE Computer Society, 2007. Google ScholarDigital Library
- 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.Google Scholar
- D. Gillespie. Exact stochastic simulation of coupled chemical reactions. Journal of Physical Chemistry, 81(25):2340--2361, 1977.Google ScholarCross Ref
- S. Gilmore and J. Hillston. The PEPA workbench: A tool to support a process algebra-based approach to performance modelling. In G. Haring and G. Kotsis, editors, Proc. 7th Int. Conf. Modelling Techniques and Tools for Computer Performance Evaluation, volume 794 of LNCS, pages 353--368. Springer, 1994. Google Scholar
- H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6(5):512--535, 1994.Google ScholarDigital Library
- J. Heath, M. Kwiatkowska, G. Norman, D. Parker, and O. Tymchyshyn. Probabilistic model checking of complex biological pathways. Theoretical Computer Science, 319:239--257, 2008. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- J. Hillston. A Compositional Approach to Performance Modelling. Cambridge University Press, 1996. Google ScholarDigital Library
- 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. Google Scholar
- C. Huang and J. Ferrell. Ultrasensitivity in the mitogen-activated protein kinase cascade. Proc. Natl. Acad. Sci., 93:10078--10083, 1996.Google ScholarCross Ref
- J.-P. Katoen, M. Khattri, and I. Zapreev. A Markov reward model checker. In Proc. 2nd Int. Conf. Quantitative Evaluation of Systems (QEST'05), pages 243--244. IEEE Computer Society Press, 2005. Google ScholarDigital Library
- M. Kwiatkowska, G. Norman, and D. Parker. Probabilistic symbolic model checking with PRISM: A hybrid approach. Software Tools for Technology Transfer, 6(2):128--142, 2004. Google ScholarDigital Library
- M. Kwiatkowska, G. Norman, and D. Parker. Probabilistic model checking in practice: Case studies with PRISM. ACM SIGMETRICS Performance Evaluation Review, 32(4):16--21, 2005. Google ScholarDigital Library
- 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. Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- G. Norman, C. Palamidessi, D. Parker, and P. Wu. Model checking the probabilistic π-calculus. In Proc. 4th Int. Conf. Quantitative Evaluation of Systems (QEST'07), pages 169--178. IEEE Computer Society, 2007. Google ScholarDigital Library
- D. Parker. Implementation of Symbolic Model Checking for Probabilistic Systems. PhD thesis, University of Birmingham, 2002.Google Scholar
- 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. Google Scholar
- PRISM web site. http://www.prismmodelchecker.org/.Google Scholar
- C. Priami. Stochastic π-calculus. The Computer Journal, 38(7):578--589, 1995.Google ScholarCross Ref
- C. Priami, A. Regev, W. Silverman, and E. Shapiro. Application of a stochastic name passing calculus to representation and simulation of molecular processes. Information Processing Letters, 80:25--31, 2001. Google ScholarDigital Library
- 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.Google Scholar
- 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. Google Scholar
- 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.Google Scholar
- SBML-to-PRISM translator. http://www.prismmodelchecker.org/sbml/.Google Scholar
- SBML web site. http://sbml.org/.Google Scholar
- 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.Google ScholarCross Ref
- 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. Google Scholar
- H. Younes, M. Kwiatkowska, G. Norman, and D. Parker. Numerical vs. statistical probabilistic model checking. Software Tools for Technology Transfer, 8(3):216--228, 2006. Google ScholarDigital Library
Index Terms
- Using probabilistic model checking in systems biology
Recommendations
Probabilistic model checking in practice: case studies with PRISM
In this paper, we describe some practical applications of probabilistic model checking, a technique for the formal analysis of systems which exhibit stochastic behaviour. We give an overview of a selection of case studies carried out using the ...
Model checking epistemic-probabilistic logic using probabilistic interpreted systems
Model checking is a formal technique widely used to verify security and communication protocols in epistemic multi-agent systems against given properties. Qualitative properties such as safety and liveliness have been widely analyzed in the literature. ...
Model checking hierarchical probabilistic systems
ICFEM'10: Proceedings of the 12th international conference on Formal engineering methods and software engineeringProbabilistic modeling is important for random distributed algorithms, bio-systems or decision processes. Probabilistic model checking is a systematic way of analyzing finite-state probabilistic models. Existing probabilistic model checkers have been ...
Comments