Analysis of signalling pathways using the prism model checker

Muffy Calder, Vladislav Vyshemirsky, David Gilbert, Richard Orton

Research output: Contribution to conferencePaper

Abstract

We describe a new modelling and analysis approach for signal transduction networks in the presence of incomplete data. We illustrate the approach with an example, the RKIP inhibited ERK pathway [1]. Our models are based on high level descriptions of continuous time Markov chains: reactions are modelled as synchronous processes and concentrations are modelled by discrete, abstract quantities. The main advantage of our approach is that using a (continuous time) stochastic logic and the PRISM model checker, we can perform quantitative analysis of queries such as if a concentration reaches a certain level, will it remain at that level thereafter? We also perform standard simulations and compare our results with a traditional ordinary differential equation model. An
interesting result is that for the example pathway, only a small number of discrete data values is required to render the simulations practically indistinguishable.
LanguageEnglish
Number of pages12
Publication statusPublished - 2005
EventCMSB'2005 - Edinburgh, United Kingdom
Duration: 3 Apr 20055 Apr 2005

Conference

ConferenceCMSB'2005
CountryUnited Kingdom
CityEdinburgh
Period3/04/055/04/05

Fingerprint

Prisms
Signal transduction
Ordinary differential equations
Markov processes
Chemical analysis

Keywords

  • analysis
  • signalling pathways
  • prism
  • model checker

Cite this

Calder, M., Vyshemirsky, V., Gilbert, D., & Orton, R. (2005). Analysis of signalling pathways using the prism model checker. Paper presented at CMSB'2005, Edinburgh, United Kingdom.
Calder, Muffy ; Vyshemirsky, Vladislav ; Gilbert, David ; Orton, Richard. / Analysis of signalling pathways using the prism model checker. Paper presented at CMSB'2005, Edinburgh, United Kingdom.12 p.
@conference{aedfeffc0f5d4e98afb26b368451859c,
title = "Analysis of signalling pathways using the prism model checker",
abstract = "We describe a new modelling and analysis approach for signal transduction networks in the presence of incomplete data. We illustrate the approach with an example, the RKIP inhibited ERK pathway [1]. Our models are based on high level descriptions of continuous time Markov chains: reactions are modelled as synchronous processes and concentrations are modelled by discrete, abstract quantities. The main advantage of our approach is that using a (continuous time) stochastic logic and the PRISM model checker, we can perform quantitative analysis of queries such as if a concentration reaches a certain level, will it remain at that level thereafter? We also perform standard simulations and compare our results with a traditional ordinary differential equation model. Aninteresting result is that for the example pathway, only a small number of discrete data values is required to render the simulations practically indistinguishable.",
keywords = "analysis, signalling pathways, prism, model checker",
author = "Muffy Calder and Vladislav Vyshemirsky and David Gilbert and Richard Orton",
year = "2005",
language = "English",
note = "CMSB'2005 ; Conference date: 03-04-2005 Through 05-04-2005",

}

Calder, M, Vyshemirsky, V, Gilbert, D & Orton, R 2005, 'Analysis of signalling pathways using the prism model checker' Paper presented at CMSB'2005, Edinburgh, United Kingdom, 3/04/05 - 5/04/05, .

Analysis of signalling pathways using the prism model checker. / Calder, Muffy; Vyshemirsky, Vladislav; Gilbert, David; Orton, Richard.

2005. Paper presented at CMSB'2005, Edinburgh, United Kingdom.

Research output: Contribution to conferencePaper

TY - CONF

T1 - Analysis of signalling pathways using the prism model checker

AU - Calder, Muffy

AU - Vyshemirsky, Vladislav

AU - Gilbert, David

AU - Orton, Richard

PY - 2005

Y1 - 2005

N2 - We describe a new modelling and analysis approach for signal transduction networks in the presence of incomplete data. We illustrate the approach with an example, the RKIP inhibited ERK pathway [1]. Our models are based on high level descriptions of continuous time Markov chains: reactions are modelled as synchronous processes and concentrations are modelled by discrete, abstract quantities. The main advantage of our approach is that using a (continuous time) stochastic logic and the PRISM model checker, we can perform quantitative analysis of queries such as if a concentration reaches a certain level, will it remain at that level thereafter? We also perform standard simulations and compare our results with a traditional ordinary differential equation model. Aninteresting result is that for the example pathway, only a small number of discrete data values is required to render the simulations practically indistinguishable.

AB - We describe a new modelling and analysis approach for signal transduction networks in the presence of incomplete data. We illustrate the approach with an example, the RKIP inhibited ERK pathway [1]. Our models are based on high level descriptions of continuous time Markov chains: reactions are modelled as synchronous processes and concentrations are modelled by discrete, abstract quantities. The main advantage of our approach is that using a (continuous time) stochastic logic and the PRISM model checker, we can perform quantitative analysis of queries such as if a concentration reaches a certain level, will it remain at that level thereafter? We also perform standard simulations and compare our results with a traditional ordinary differential equation model. Aninteresting result is that for the example pathway, only a small number of discrete data values is required to render the simulations practically indistinguishable.

KW - analysis

KW - signalling pathways

KW - prism

KW - model checker

M3 - Paper

ER -

Calder M, Vyshemirsky V, Gilbert D, Orton R. Analysis of signalling pathways using the prism model checker. 2005. Paper presented at CMSB'2005, Edinburgh, United Kingdom.