Using probabilistic model checking in systems biology

Probabilistic model checking is a formal verification frame-work for systems which exhibit stochastic behaviour. It has been successfully applied to a wide range of domains, includ-ing security and communication protocols, distributed algo-rithms and power management. In this paper we demon-strate 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 ex-plain how biological pathways can be modelled in the prob-abilistic model checker PRISM and how this enables the analysis of a rich selection of quantitative properties. 1