Skip to main content
SpringerLink
Log in

Quantitative Verification Techniques for Biological Processes

  • Chapter
  • First Online:
Algorithmic Bioprocesses

Part of the book series: Natural Computing Series ((NCS))

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 169.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 219.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 219.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aziz A, Sanwal K, Singhal V, Brayton R (2000) Model checking continuous time Markov chains. ACM Trans Comput Log 1(1):162–170

    Article  MathSciNet  Google Scholar 

  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

    Article  Google Scholar 

  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

    MathSciNet  Google Scholar 

  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

    Article  MathSciNet  Google Scholar 

  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

    Article  MATH  Google Scholar 

  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. 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

    Chapter  Google Scholar 

  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. Gillespie D (1977) Exact stochastic simulation of coupled chemical reactions. J Phys Chem 81(25):2340–2361

    Article  Google Scholar 

  10. Hansson H, Jonsson B (1994) A logic for reasoning about time and reliability. Form Asp Comput 6(5):512–535

    Article  MATH  Google Scholar 

  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

    Article  MathSciNet  Google Scholar 

  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

    Article  Google Scholar 

  13. Hillston J (1996) A compositional approach to performance modeling. Cambridge University Press, Cambridge

    Google Scholar 

  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

    Chapter  Google Scholar 

  15. Huang C, Ferrell J (1996) Ultrasensitivity in the mitogen-activated protein kinase cascade. Proc Natl Acad Sci 93:10078–10083

    Article  Google Scholar 

  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

    Chapter  Google Scholar 

  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. 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

    Article  Google Scholar 

  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. 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

    Chapter  Google Scholar 

  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. MAPLE. www.maplesoft.com/products/maple/

  23. MATLAB. http://www.mathworks.com/products/matlab/

  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

    Chapter  Google Scholar 

  25. Parker D (2002) Implementation of symbolic model checking for probabilistic systems. PhD thesis, University of Birmingham

    Google Scholar 

  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. PRISM web site. http://www.prismmodelchecker.org/

  28. Priami C (1995) Stochastic π-calculus. Comput J 38(7):578–589

    Article  Google Scholar 

  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

    Article  MATH  MathSciNet  Google Scholar 

  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. 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. Rutten J, Kwiatkowska M, Norman G, Parker D (2004) Mathematical techniques for analyzing concurrent and probabilistic systems. CRM monograph series, vol 23. AMS, Providence

    MATH  Google Scholar 

  33. SBML-to-PRISM translator. http://www.prismmodelchecker.org/sbml/

  34. SBML web site. http://sbml.org/

  35. SBML-shorthand. http://www.staff.ncl.ac.uk/d.j.wilkinson/software/sbml-sh/

  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

    Article  Google Scholar 

  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. Younes H, Kwiatkowska M, Norman G, Parker D (2006) Numerical vs. statistical probabilistic model checking. Softw Tools Technol Transf 8(3):216–228

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK

    Marta Kwiatkowska, Gethin Norman & David Parker

Authors
  1. Marta Kwiatkowska
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gethin Norman
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. David Parker
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Marta Kwiatkowska .

Editor information

Editors and Affiliations

  1. Dept. Computer Science, University of British Columbia, Main Mall 201-2366, Vancouver, V6T 1Z4, Canada

    Anne Condon

  2. Dept. Applied Mathematics, Weizmann Institute of Science, Rehovot, 76100, Israel

    David Harel

  3. Leiden Inst. Advanced Computer Science, Leiden University, Niels Bohrweg 1, Leiden, 2333 CA, Netherlands

    Joost N. Kok

  4. Turku Centre for Computer Science, Lemminkaisenkatu 14 A, Turku, 20520, Finland

    Arto Salomaa

  5. Computer Science, Computation,, California Inst. of Technology, Pasadena, 91125, U.S.A.

    Erik Winfree

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Kwiatkowska, M., Norman, G., Parker, D. (2009). Quantitative Verification Techniques for Biological Processes. In: Condon, A., Harel, D., Kok, J., Salomaa, A., Winfree, E. (eds) Algorithmic Bioprocesses. Natural Computing Series. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-88869-7_20

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-88869-7_20

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-88868-0

  • Online ISBN: 978-3-540-88869-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation