Projects per year
Abstract
Model-checking can provide valuable insight into the behaviour of biochemical systems, answering quantitative queries which are more difficult to answer using stochastic simulation alone. However, model-checking is a computationally intensive technique which can become infeasible if the system under consideration is too large. Moreover, the finite nature of the state representation used means that a priori bounds must be set for the numbers of molecules of each species to be observed in the system. In this paper we present an approach which addresses these problems by using stochastic simulation and the PRISM model checker in tandem. The stochastic simulation identifies reasonable bounds for molecular populations in the context of the considered experiment. These bounds are used to parameterise the PRISM model and limit its state space. A simulation pre-run identifies interesting time intervals on which model-checking should focus, if this information is not available from experimental data.
Original language | English |
---|---|
Pages (from-to) | 17-38 |
Number of pages | 22 |
Journal | Electronic Notes in Theoretical Computer Science |
Volume | 232 |
DOIs | |
Publication status | Published - 2009 |
Keywords
- stochastic simulation
Fingerprint
Dive into the research topics of 'Integrated Simulation and Model-Checking for the Analysis of Biochemical Systems'. Together they form a unique fingerprint.Projects
- 4 Finished
-
SIGNAL: SIGNAL -Stochastic process algebra for biochemical signaling pathway analysis
1/09/07 → 31/01/11
Project: Research
-
SynthSys; formerly CSBE: Centre for Systems Biology at Edinburgh
Millar, A., Beggs, J., Ghazal, P., Goryanin, I., Hillston, J., Plotkin, G., Tollervey, D., Walton, A. & Robertson, K.
8/01/07 → 31/12/12
Project: Research
-