Probabilistic model checking of complex biological pathways

  • Heath J
  • Kwiatkowska M
  • Norman G
 et al. 
  • 2

    Readers

    Mendeley users who have this article in their library.
  • N/A

    Citations

    Citations of this article.

Abstract

Probabilistic model checking is a formal verification technique that has been successfully applied to the analysis of systems from a broad range of domains, including security and communication protocols, distributed algorithms and power management. In this paper we illustrate its applicability to a complex biological system: the FGF (Fibroblast Growth Factor) signalling pathway. We give a detailed description of how this case study can be modelled in the probabilistic model checker PRISM, discussing some of the issues that arise in doing so, and show how we can thus examine a rich selection of quantitative properties of this model. We present experimental results for the case study under several different scenarios and provide a detailed analysis, illustrating how this approach can be used to yield a better understanding of the dynamics of the pathway.

Author-supplied keywords

  • QA75 Electronic computers. Computer science
  • QH301 Biology

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document

Authors

  • J. Heath

  • M. Kwiatkowska

  • G. Norman

  • D. Parker

  • O. Tymchyshyn

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free