BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:On Automatic Quantitative Verification of Biological Systems - Pao
 lo Ballarini\, CoSBi
DTSTART:20090121T140000Z
DTEND:20090121T150000Z
UID:TALK14744@talks.cam.ac.uk
CONTACT:Dr Fabien Petitcolas
DESCRIPTION:*Abstract*: Automatic verification of living systems is an app
 ealing subject of research which is attracting the attention of a fairly l
 arge part of the scientific community. The basic idea is one of providing 
 life scientists with a modelling technique in which they can specify the b
 iological 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 pr
 operty with respect to the considered model.\nA variety of approaches for 
 the automatic verification of bio-systems have been studied in recent year
 s. They can be distinguished according to several factors\, such as\, for 
 example\, the nature of the model they refer to (probabilistic vs. non-pro
 babilistic)\, hence the nature of the verification they support (i.e. qual
 itative vs quantitative). \nIndependently of their type\, automatic verifi
 cation 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 t
 rue with biological systems).\nIn this work\, we first briefly survey exis
 ting works in the field and then focus on techniques for the automatic qua
 ntitative verification of stochastic models of biological systems. By mean
 s of two fairly simple examples (i.e. a stochastic model of a simple oscil
 lator and a stochastic model of a cell-cycle regulatory network) we illust
 rate the space complexity of quantitative model-checking for stochastic bi
 ological models. Although simple those two systems are enough to demonstra
 te 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 computi
 ng 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.\n\n*Biography
 *: Master’s degree in Computer Science from the University of Torino (19
 99). PhD in Computer Science from the University of Torino (co-supervised 
 by Prof. Jane Hillston at the Laboratory for Foundations of Computer Scien
 ce at the University of Edinburgh). Postdoctoral researcher at the Univers
 ity of Liverpool (2004-2006) and the University of Glasgow (2006-2007). Te
 mporary lecturer at the University of Liverpool (2005). Paolo joined the C
 oSBi Centre in January 2008.
LOCATION:Small public lecture room\, Microsoft Research Ltd\, 7 J J Thomso
 n Avenue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR