On Automatic Quantitative Verification of Biological Systems

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

• Paolo Ballarini, CoSBi
• Wednesday 21 January 2009, 14:00-15:00
• Small public lecture room, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge.

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.

This talk is included in these lists:

• All CMS Events
• All Talks (aka the CURE list)
• Biology
• CamBridgeSens
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• CoSBi Computational and Systems Biology Series
• Computational and Systems Biology
• Graduate-Seminars
• Guy Emerson's list
• Interested Talks
• Life Science Interface Seminars
• Life Sciences
• Life Sciences
• ME Seminar
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Physical Sciences
• School of Technology
• Small public lecture room, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge
• Trust & Technology Initiative - interesting events
• bld31
• custom
• my_list
• ndk22's list
• ob366-ai4er
• other talks
• personal list
• rp587
• se393's list

Note that ex-directory lists are not shown.