University of Cambridge > > CoSBi Computational and Systems Biology Series > On Automatic Quantitative Verification of Biological Systems

On Automatic Quantitative Verification of Biological Systems

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Dr Fabien Petitcolas.

Time changed

Abstract: Automatic verification of living systems is an appealing subject of research which is attracting the attention of a fairly large part of the scientific community. The basic idea is one of providing life scientists with a modelling technique in which they can specify the biological system of interest as well as the relevant properties for which it has to be tested. An automatic procedure will then verify the property against the model and provide a measure of “how true” is the considered property with respect to the considered model. A variety of approaches for the automatic verification of bio-systems have been studied in recent years. They can be distinguished according to several factors, such as, for example, the nature of the model they refer to (probabilistic vs. non-probabilistic), hence the nature of the verification they support (i.e. qualitative vs quantitative). Independently of their type, automatic verification techniques, invariably, are affected by the so-called state-space explosion problem, which is: the dimension of the underlying state-space is so large that the model is intractable (something which is even more true with biological systems). In this work, we first briefly survey existing works in the field and then focus on techniques for the automatic quantitative verification of stochastic models of biological systems. By means of two fairly simple examples (i.e. a stochastic model of a simple oscillator and a stochastic model of a cell-cycle regulatory network) we illustrate the space complexity of quantitative model-checking for stochastic biological models. Although simple those two systems are enough to demonstrate the space-complexity of system biology modelling: the dimension of the underlying continuous time Markov chain can be huge. We then illustrate a novel method which allows us to reduce the memory requirements for computing the probability of paths in large, structured Markov chain models. We believe that such an approach may constitute the basis for rendering model-checking verification applicable to large Markovian models.

Biography: Master’s degree in Computer Science from the University of Torino (1999). PhD in Computer Science from the University of Torino (co-supervised by Prof. Jane Hillston at the Laboratory for Foundations of Computer Science at the University of Edinburgh). Postdoctoral researcher at the University of Liverpool (2004-2006) and the University of Glasgow (2006-2007). Temporary lecturer at the University of Liverpool (2005). Paolo joined the CoSBi Centre in January 2008.

This talk is part of the CoSBi Computational and Systems Biology Series series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2019, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity