Quantitative Verification Techniques for Biological Processes

  • Marta KwiatkowskaEmail author
  • Gethin Norman
  • David Parker
Part of the Natural Computing Series book series (NCS)


Probabilistic model checking is a formal verification framework for systems which exhibit stochastic behavior. It has been successfully applied to a wide range of domains, including security and communication protocols, distributed algorithms and power management. In this chapter, 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 Mitogen-Activated Protein (MAP), Kinase cascade, we explain how biological pathways can be modeled in the probabilistic model checker PRISM and how this enables the analysis of a rich selection of quantitative properties.


Model Check Temporal Logic MAPK Cascade Atomic Proposition Symmetry Reduction 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Aziz A, Sanwal K, Singhal V, Brayton R (2000) Model checking continuous time Markov chains. ACM Trans Comput Log 1(1):162–170 CrossRefMathSciNetGoogle Scholar
  2. 2.
    Baier C, Haverkort B, Hermanns H, Katoen J-P (2003) Model-checking algorithms for continuous-time Markov chains. IEEE Trans Softw Eng 29(6):524–541 CrossRefGoogle Scholar
  3. 3.
    Calder M, Gilmore S, Hillston J (2006) Modelling the influence of RKIP on the ERK signaling pathway using the stochastic process algebra PEPA. Trans Comput Syst Biol 7:1–23 MathSciNetGoogle Scholar
  4. 4.
    Calder M, Vyshemirsky V, Gilbert D, Orton R (2006) Analysis of signaling pathways using continuous time Markov chains. Trans Comput Syst Biol 4:44–67 CrossRefMathSciNetGoogle Scholar
  5. 5.
    Clarke E, Emerson E, Sistla A (1986) Automatic verification of finite-state concurrent systems using temporal logics. ACM Trans Program Lang Syst 8(2):244–263 zbMATHCrossRefGoogle Scholar
  6. 6.
    Cloth L, Katoen J-P, Khattri M, Pulungan R (2005) Model checking Markov reward models with impulse rewards. In: Proceedings of the international conference on dependable systems and networks (DSN’05). IEEE Computer Society, Los Alamitos, pp 722–731 Google Scholar
  7. 7.
    Donaldson A, Miller A, Parker D (2007) GRIP: Generic representatives in PRISM. In: Proceedings of the 4th international conference on quantitative evaluation of systems (QEST’07). IEEE Computer Society, Los Alamitos, pp 115–116 CrossRefGoogle Scholar
  8. 8.
    Emerson E, Wahl T (2003) On combining symmetry reduction and symbolic representation for efficient model checking. In: Geist D, Tronci E (eds) Proceedings of the 12th conference on correct hardware design and verification methods (CHARME 2003). Lecture notes in computer science, vol 2860. Springer, Berlin, pp 216–230 Google Scholar
  9. 9.
    Gillespie D (1977) Exact stochastic simulation of coupled chemical reactions. J Phys Chem 81(25):2340–2361 CrossRefGoogle Scholar
  10. 10.
    Hansson H, Jonsson B (1994) A logic for reasoning about time and reliability. Form Asp Comput 6(5):512–535 zbMATHCrossRefGoogle Scholar
  11. 11.
    Heath J, Kwiatkowska M, Norman G, Parker D, Tymchyshyn O (2008) Probabilistic model checking of complex biological pathways. Theor Comput Sci 319:239–257 CrossRefMathSciNetGoogle Scholar
  12. 12.
    Hermanns H, Katoen J-P, Meyer-Kayser J, Siegle M (2003) A tool for model checking Markov chains. Softw Tools Technol Transf 4(2):153–172 CrossRefGoogle Scholar
  13. 13.
    Hillston J (1996) A compositional approach to performance modeling. Cambridge University Press, Cambridge Google Scholar
  14. 14.
    Hinton A, Kwiatkowska M, Norman G, Parker D (2006) PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns H, Palsberg J (eds) Proceedings of the 12th international conference on tools and algorithms for the construction and analysis of systems (TACAS’06). Lecture notes in computer science, vol 3920. Springer, Berlin, pp 441–444 CrossRefGoogle Scholar
  15. 15.
    Huang C, Ferrell J (1996) Ultrasensitivity in the mitogen-activated protein kinase cascade. Proc Natl Acad Sci 93:10078–10083 CrossRefGoogle Scholar
  16. 16.
    Katoen J-P, Khattri M, Zapreev I (2005) A Markov reward model checker. In: Proceedings of the 2nd international conference on quantitative evaluation of systems (QEST’05). IEEE Computer Society, Los Alamitos, pp 243–244 CrossRefGoogle Scholar
  17. 17.
    Kwiatkowska M, Norman G, Parker D (2004) Probabilistic symbolic model checking with PRISM: a hybrid approach. Softw Tools Technol Transf 6(2):128–142 Google Scholar
  18. 18.
    Kwiatkowska M, Norman G, Parker D (2005) Probabilistic model checking in practice: case studies with PRISM. ACM SIGMETRICS Perform Eval Rev 32(4):16–21 CrossRefGoogle Scholar
  19. 19.
    Kwiatkowska M, Norman G, Parker D (2006) Symmetry reduction for probabilistic model checking. In: Ball T, Jones R (eds) Proceedings of the 18th international conference on computer aided verification (CAV’06). Lecture notes in computer science, vol 4114. Springer, Berlin, pp 234–248 Google Scholar
  20. 20.
    Kwiatkowska M, Norman G, Parker D (2007) Stochastic model checking. In: Bernardo M, Hillston J (eds) Formal methods for the design of computer, communication and software systems: performance evaluation (SFM’07). Lecture notes in computer science, vol 4486. Springer, Berlin, pp 220–270 CrossRefGoogle Scholar
  21. 21.
    Lecca P, Priami C (2003) Cell cycle control in eukaryotes: a BioSpi model. In: Proceedings of the workshop concurrent models in molecular biology (BioConcur’03). Electronic notes in theoretical computer science Google Scholar
  22. 22.
  23. 23.
  24. 24.
    Norman G, Palamidessi C, Parker D, Wu P (2007) Model checking the probabilistic π-calculus. In: Proceedings of the 4th international conference on quantitative evaluation of systems (QEST’07). IEEE Computer Society, Los Alamitos, pp 169–178 CrossRefGoogle Scholar
  25. 25.
    Parker D (2002) Implementation of symbolic model checking for probabilistic systems. PhD thesis, University of Birmingham Google Scholar
  26. 26.
    Phillips A, Cardelli L (2007) Efficient, correct simulation of biological processes in the stochastic π-calculus. In: Calder M, Gilmore S (eds) Proceedings of the 5th international conference on computational methods in systems biology (CMSB’07). Lecture notes in bioinformatics, vol 4695. Springer, Berlin, pp 184–199 Google Scholar
  27. 27.
  28. 28.
    Priami C (1995) Stochastic π-calculus. Comput J 38(7):578–589 CrossRefGoogle Scholar
  29. 29.
    Priami C, Regev A, Silverman W, Shapiro E (2001) Application of a stochastic name passing calculus to representation and simulation of molecular processes. Inf Process Lett 80:25–31 zbMATHCrossRefMathSciNetGoogle Scholar
  30. 30.
    Pronk T, de Vink E, Bosnacki D, Breit T (2007) Stochastic modeling of codon bias with PRISM. In: Linden I, Talcott C (eds) Proceedings of the 3rd international workshop on methods and tools for coordinating concurrent, distributed and mobile systems (MTCoord 2007). Computer Science Department, University of Cyprus, Nicosia Google Scholar
  31. 31.
    Romero-Campero F, Gheorghe M, Bianco L, Pescini D, Pérez-Jiménez M, Ceterchi R (2006) Towards probabilistic model checking on P systems using PRISM. In: Hoogeboom H, Păun G, Rozenberg G, Salomaa A (eds) Proceedings of the 7th international workshop on membrane computing (WMC06). Lecture notes in computer science, vol 4361. Springer, Berlin, pp 477–495 Google Scholar
  32. 32.
    Rutten J, Kwiatkowska M, Norman G, Parker D (2004) Mathematical techniques for analyzing concurrent and probabilistic systems. CRM monograph series, vol 23. AMS, Providence zbMATHGoogle Scholar
  33. 33.
    SBML-to-PRISM translator.
  34. 34.
    SBML web site.
  35. 35.
  36. 36.
    Wolkenhauer O, Ullah M, Kolch W, Cho K-H (2004) Modeling and simulation of intracellular dynamics: choosing an appropriate framework. IEEE Trans Nanobiosci 3:200–207 CrossRefGoogle Scholar
  37. 37.
    Younes H (2005) Ymer: A statistical model checker. In: Etessami K, Rajamani S (eds) Proceedings of the 17th international conference on computer aided verification (CAV’05). Lecture notes in computer science, vol 3576. Springer, Berlin, pp 429–433 Google Scholar
  38. 38.
    Younes H, Kwiatkowska M, Norman G, Parker D (2006) Numerical vs. statistical probabilistic model checking. Softw Tools Technol Transf 8(3):216–228 CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Marta Kwiatkowska
    • 1
    Email author
  • Gethin Norman
    • 1
  • David Parker
    • 1
  1. 1.Oxford University Computing LaboratoryOxfordUK

Personalised recommendations