www.prismmodelchecker.org
[KNP09b] Marta Kwiatkowska, Gethin Norman and David Parker. Quantitative Verification Techniques for Biological Processes. In A. Condon, D. Harel, J. Kok, A. Salomaa and E. Winfree (editors), Algorithmic Bioprocesses, pages 391-409, Springer. August 2009. [pdf] [bib] [Tutorial paper on the application of probabilistic model checking and PRISM to biological systems, including an illustrative case study (MAPK cascade).]
Downloads:  pdf pdf (593 KB)  bib bib
Notes: The original publication is available at www.springerlink.com.
Front cover 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 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 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.

Publications