Integrated Simulation and Model-Checking for the Analysis of Biochemical Systems

Federica Ciocchetta, Stephen Gilmore, Maria Luisa Guerriero, Jane Hillston

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

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 languageEnglish
Pages (from-to)17-38
Number of pages22
JournalElectronic Notes in Theoretical Computer Science
Publication statusPublished - 2009

Keywords / Materials (for Non-textual outputs)

  • stochastic simulation


Dive into the research topics of 'Integrated Simulation and Model-Checking for the Analysis of Biochemical Systems'. Together they form a unique fingerprint.

Cite this