Kevin Burrage was a Federation Fellow of the Australian Research Council (2003-2008). Until the end of 2007 he was also Professor of Computational Mathematics at the University of Queensland and Director of the Advanced Computational Modelling Centre. He was also founding CEO of the Queensland Parallel Supercomputing foundation (now QCIF).

Kevin joined Oxford University in early 2008 and is Professor of Computational Systems Biology at the Computing Laboratory and the Oxford Centre for integrative Systems Biology. He is also professorial research fellow at the Institute for Molecular Bioscience at the University of Queensland. He shares his time between both institutions. Kevin is also a supernumerary fellow of New College at Oxford University.

Talk title: Stochastic modelling and simulation for the Life Sciences

Abstract: In this talk I will give some overview on stochastic modelling and simulation for the Life Sciences. The focus will be on intrinsic noise effects both temporally and spatially. Applications will include cellular kinetics and genetic regulatory models based on molecular clocks and juxtacrine signalling.

Jaco van de Pol is head of the Formal Methods and Tools group at the University of Twente. His research interests are scalable methods and tools to design and analyze properties of embedded software systems. In particular, he designs algorithms and tools for model checking on multi-core and distributed Grid hardware. Van de Pol is coordinator of the FP6 project EC-MOAN on modeling and analyzing emergent cell behavior. Here scalable analysis techniques are applied to integrated models of genetic and metabolic networks in the E. coli enterobacterium; in collaboration with biologists, biomathematicians and computer scientists. Jaco van de Pol got his MsC in computer science (Utrecht, Dept. of CS in 1992) and his PhD in applied logic (Utrecht, Dept. of Phil. 1996). He has been working as a junior researcher at the LMU Munich (Dept. of Math.) and the TU Eindhoven (Dept. of CS). In 1999 he joined the Centrum voor Wiskunde & Informatica (Amsterdam), where he became team leader of the specification and analysis group. In 2004 he became part-time associate professor at the Technical University of Eindhoven, and became full professor at the University of Twente in September 2007. He is currently coordinator of the FP6 NEST project EC-MOAN.

Talk title: Distributed Model Checking for Emergent Cell Behavior

Abstract: Modeling a living cell in order to predict its behavior from first principles is complicated. The systems biology approach has been quite successful, when focusing on individual modules, such as e.g. ammonium assimilation. However, an integrated model that explains how various modules mutually interact across different levels, e.g. gene regulation, metabolism and signaling, is a real challenge. Precisely this was the ambition of the EC-MOAN project that started two and a half years ago, focusing on the model-organism Escherichia Coli. Biologists from different groups have step by step integrated their models based on (non-linear) ordinary differential equations. Indeed, we are close to one integrated model, comprising metabolic reactions for ammonium assimilation and carbon usage, the key enzymes, as wel  as the genetic regulation going on. The resulting model is hard to analyze, due to non-linearities, high dimensions, and different time scales, especially between genetic and metabolic processes. Mathematicians in the project develop new methods for:
- system reduction: eliminating slow and fast variables from a system, to obtain a lower dimensional system with less time scale differences;
- system approximation: eliminating non-linearities by discrete step  functions, giving rise to hybrid (discrete/continuous) systems, in   particular piecewise affine systems.
- system abstraction: abstracting from all continuous behavior in favor of a completely discrete system, whose states correspond to regions,
  and whose transitions correspond to passing thresholds.
Finally, computer scientists defined special purpose temporal logics, in order to express interesting hypothetical phenomena of E. Coli bacteria.  Model checking algorithms have been devised to check properties on the models. Due to the enormous size of the resulting automata, parallel and distributed algorithms have been devised, in order to use the memory and CPU power of a cluster of workstations. Eventually, model checking is a way of doing in silicon experiments, thus exploring all consequences of a model. Of course, interesting phenomena are also performed in biological laboratories, if only to validate the models.

Thomas A. Henzinger is Professor of Computer and Communication Sciences at EPFL in Lausanne, Switzerland, and Adjunct Professor of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He holds a Dipl.-Ing. degree in Computer Science from Kepler University in Linz, Austria, an M.S. degree in Computer and Information Sciences from the University of Delaware, and a Ph.D. degree in Computer Science from Stanford University (1991). He was Assistant Professor of Computer Science at Cornell University (1992-95), Assistant Professor (1996-97), Associate Professor (1997-98), and Professor (1998-2005) of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He was also Director at the Max-Planck Institute for Computer Science in Saarbruecken, Germany (1999). His research focuses on modern systems theory, especially models, algorithms, and tools for the design and verification of reliable software, hardware, and embedded systems. His HyTech tool was the first model checker for mixed discrete-continuous systems. He is an ISI highly cited researcher, a member of Academia Europaea, a member of the German Academy of Sciences (Leopoldina), a Fellow of the ACM, and a Fellow of the IEEE. In September 2009, Tom Henzinger will assume his new position as President of IST Austria.

Talk title: An On-the-fly Algorithm for Adaptive Uniformization

Abstract: Within systems biology there is an increasing interest in the stochastic  behavior of biochemical reaction networks. An appropriate stochastic description is provided by the chemical master equation, which represents a continuous-time Markov chain (CTMC).
Standard Uniformization (SU) is an efficient method for the transient analysis of CTMCs. For systems with very different time scales, such as biochemical reaction networks, SU is computationally expensive. In these cases, a variant of SU, called adaptive uniformization (AU), is known to reduce the large number of iterations needed by SU. The additional difficulty of AU is that it requires the solution of a birth process. In this paper we present an on-the-fly variant of AU, where we improve the original algorithm for AU at the cost of a small approximation error. By means of several examples, we show that our approach is particularly well-suited for biochemical reaction networks.