21 April 2005
Marta Kwiatkowska
School of Computer Science
University of Birmingham
Stochastic pi-calculus has been used to model biological processes and analyse them via simulation tools such as BioSPI. More recently, an automated formal verification technique called probabilistic model checking has been developed and used to model signalling pathways. Probabilistic model checking aims to establish if a desired property holds in a probabilistic model, and with what probability. Models are described in stochastic pi-calculus or similar. Properties are typically expressed in a probabilistic variant of temporal logic, and allow specifications such as "what is the probability that a reaction will occur?" and "what is the concentration of the compound at a given time?". Unlike simulation, probabilistic model checking involves an exhaustive analysis of the transitions of the model, and thus can identify behaviours of interest with certainty. A brief introduction to probabilistic model checking with the tool PRISM developed at the University of Birmingham will be given. Examples will include eukaryotic cell cycle control, RKIP inhibited ERK pathway analysed by Calder at al, and the FGF pathway.
P Lecca and C Priami, "Cell cycle control in eukaryotes: a BioSpi model", Proceedings Workshop on Concurrent Models in Molecular Biology (BioConcur'03), Electronic Notes in Theoretical Computer Science, to appear. Model in PRISM
M Calder, V Vyshermirsky, D Gilbert and R Orton, "Analysis of signalling pathways using the PRISM model checker", CMSB'05, Abstract, PDF