Analysis of signalling pathways using the prism model checker

Calder, Muffy and Vyshemirsky, Vladislav and Gilbert, David and Orton, Richard (2005) Analysis of signalling pathways using the prism model checker. In: CMSB'2005, 2005-04-03 - 2005-04-05, Edinburgh.

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.

Actions (login required)