The ambition of EC-MOAN (FP7) is to model and analyse a living cell in order to predict its behavior from first principles. An integrated model should explain how various modules mutually interact across different levels, e.g. gene regulation, metabolism and signaling. Our target is the model-organism Escherichia Coli.
In EC-MOAN, 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 utilization, the key enzymes, as well 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, approximation, and abstraction, eventually leading to a (very large) discrete automaton model.
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 implemented, 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.
Microorganisms predominantly rely on two component signaling to sense their environment. Typically, a given species contains tens of such systems. The design of two component signaling systems is remarkably simple despite their versatile role in governing adaptive responses. In this presentation, I will discuss how two-component signaling can achieve fast and robust responses at low molecule numbers. I will show that molecular noise does not impede signaling to a great extent and that most of the noise in the response time derives from diffusion. I will show that noise can be reduced by particular operon organization of two component signaling systems. I will discuss the results of a large bioinformatics screen of the abundance of those operon designs accross prokaryotic species.
Modelling is an important technology in systems biology research. In this paper, we present a kinetic model for the complex ammonium assimilation regulation system of E. coli. Based on a previous published model, the new model includes the AmtB mediated ammonium transport and its regulation by GlnK, thus can simulate the cellular behaviour at very low ammonium concentration. Steady state analysis of the model suggests that AmtB and GS are coupled to maximal assimilation flux at very low N availability. Furthermore, energy consuming hydrogen ion generation process may need to be coupled with the AmtB transport process to maintain a higher intracellular NH4 concentration, thus reducing the need for further increasing GS. Simulation of the dynamic response to increased ammonium concentration implies that the maximal rate for GlnK uridylylation/deuridylylation and GS adenylylation/deadenylylation may be much higher for a quick response to environmental changes.
Joint work with Fred C. Boogerd, F. Bruggeman, I. Goryanin
Bio-PPEA is a stochastic process algebra which enables description of biochemical pathways in order to support analysis using a variety of mathematical models. Bio-PEPA models can be interpreted as sets of ODEs or as Continuous Time Markov Chains (CTMCs) suitable for simulation using Gillespie's stochastic simulation algorithm. Additionally Bio-PEPA models can give rise to a more abstract CTMC, the so-called CTMC with levels, which can be subjected to explicit state space analyses such as numerial solution of probability distributions and stochastic model checking in PRISM. In this talk I will present Bio-PEPA and its semantics, focusing in particular on the CTMC with levels.
Joint work with Federica Ciocchetta
On the methodological side, I will speak about two of the main challenges for sound integration of modelling in conventional experimental biology. The first challenge concerns unique identification of model properties, also in the all too common situation where the parameters themselves cannot be uniquely identified; a challenge I refer to as core prediction identification. The second challenge concerns sound merging of models and insights for sub-systems into larger contexts, modelling the whole; here carried out through so called hierarchical modelling.
On the biological side, I will illustrate these concepts at work in some of our recent studies, concerning type 2 diabetes. We have used numerous iterations between core predictions and experimental tests, to characterise the role of various mechanisms concerning insulin signalling in primary human adipocytes. We have also integrated these models and insights into a well-characterised model for the whole-body interactions, a model which has been formally accepted as an official part of drug certifications.
Replication of DNA, translation of mRNA and translesion synthesis or TLS (invocation of polymerases that bypass DNA damage) can be modeled using stochastic automata. At points, construction of the particular automata is difficult. To keep automata compact in size, abstractions seek to capture various detailed biological mechanisms involving a number of molecules by a few transitions. However, in this view, different explanations of the same mechanism may not be consistent and parameters may not be available. Stochastic modeling helps identifying missing information and, when successful, stochastic analysis helps to explain the underlying dynamics. The cell processes of replication, translation and TLS are discussed to illustrate the approach.
Joint work with Dragan Bosnacki and Huub ten Eikelder
Signalling pathways are abstractions that help life scientists structure the coordination of cellular activity. Cross-talk between pathways accounts for many of the complex behaviours exhibited and is often critical in producing the correct signal-response relationship. Formal models of signalling pathways and cross-talk in particular can aid understanding and drive experimentation. In this talk we present an approach to modelling cross-talk based on the concept of a pathway as a process. We show how cross-talk can be modelled naturally using synchronous composition and action renaming, and we define a set of Continuous Stochastic Logic (CSL) properties that distinguish the five types. We have used PRISM for both modelling and property verification. We illustrate the approach with small examples and conclude with an analysis of the cross-talk between the TGF-β/BMP, WNT and MAPK pathways.Joint work with Muffy Calder
We study the biochemical processes involved in scaffold-mediated crosstalk between the cAMP and the Raf-1/MEK/ERK pathways. We model the interactions by a continuous time Markov chain with levels and analyse properties using Continuous Stochastic Logic and the symbolic probabilistic model checker PRISM. We consider a number of biologically relevant properties of the model, including sequentially dependent events and pulsating behaviour. In order to handle these kinds of properties, we extend the model with signs of first order derivatives.Joint work with Muffy Calder
The adaptation of bacteria to changes in their environment involves adjustments in the expression level of genes coding for enzymes, transcription factors, membrane transporters, and other cellular proteins. In response to a lack of glucose, the bacterium Escherichia coli enters a stationary phase, during which the cell stops dividing, capitalising upon the few remaining resources to maintain its essential functions. This shift is accompanied by changes in the bacterial phenotype and by marked rearrangements of metabolic fluxes and gene expression.
We have analysed the network of global regulators controlling the adaptation of the bacterium to environmental stress conditions [1]. Even though E. coli is one of the best studied model organisms, it is currently little understood how a stress signal is sensed and propagated throughout the network of global regulators, and leads the cell to respond in an adequate way.
Using standard methods for kinetic modeling and system reduction [2], we have built a simplified model of the carbon starvation response network. This model has been analysed by means of a qualitative simulation method that is able to overcome the current lack of quantitative data on kinetic parameters and molecular concentrations [3,4]. We have used the reduced model to simulate the response of E. coli cells to carbon deprivation [5]. This has allowed us to identify essential features of the transition between exponential and stationary phase and to get new insights into the role of the global regulators in the growth-phase transition. The model predictions can be tested experimentally by means of luciferase and fluorescence reporter systems.
Joint work with D. Ropers, J. Geiselmann, H. de Jong
References
- R. Hengge-Aronis, 2000, Bacterial Stress Responses, G. Storz and R. Hengge-Aronis (eds.), ASM Press, Washington DC, 161-178.
- R. Heinrich and S. Schuster (1996), The Regulation of Cellular Systems, Chapman & Hall, New York.
- H. de Jong et al., 2004, Bull. Math. Biol., 66(2):301-340.
- H. de Jong et al., 2003, Bioinformatics, 19(3):336-344.
- D. Ropers et al., 2006, Biosystems, 84(2):124-152.
In this talk we deal with continuous deterministic approach to modeling and analysis of biochemical reactions. In particular, we present our recent results regarding computational analysis of special classes of ODE models. Especially, we focus on discrete abstractions of multi-affine systems and piece-wise affine systems. For each of the classes we show which kinds of particular qualitative linear-time temporal properties can be interpreted on such abstractions and we briefly present qualitative analysis algorithms based on model-checking. Special emphasis will be given to parallel algorithms suitable for large-scale models. In the part of the talk, the tool BioDiVinE for parallel analysis of multi-affine ODE models will be presented as well.
When researching kinase signaling pathways in cells, molecular biologists are confronted with large experimental data sets. Evaluation of these data sets, together with the fitting of these data on possible pathway models, is a highly non-trivial task. The aim of this research is to support biologists in exploring the space of networks inferred from experimental data by means of software that is both interactive and visual, thereby considerably alleviating this task.
At the basis of the software lies a quantitative modeling technique that makes use of a computer science model called timed automata. Timed automata models can be created, simulated, and analyzed with UPPAAL, which is a state-of-the-art tool for analysis and design of real-time systems. Modeling a pathway with timed automata makes it possible to decide, using UPPAAL, whether experimental data fits a specific model, or whether such a model should somehow be updated.
In order to hide the technical intricacies of timed automata and UPPAAL from the molecular biologist, a prototype interface tool has been built. This interface tool lets users draw a network and add experimental data to it, and then exports this information to a timed automata model to be verified by UPPAAL. Finally, the results from this verification process are translated back to the interface and presented in a graphical manner.
Joint work with Wim Bos, Jetse Scholma, Paul van der Vet
The robustness of biological systems behaviors has been demonstrated many times both experimentally and theoretically. In most cases however, the definition of robustness is highly problem-dependent, if not purely informal. An interesting general formal definition of robustness has recently been given by H. Kitano [Mol.Syst.Biol, 2007]. The robustness of a property with respect to a set of perturbations is the average value of the functionality of the system under all perturbations, weighted by the perturbation probabilities. Unfortunately, no indications are given on how to define and quantify the "functionality" of a system.
Here, we propose an instantiation of this abstract definition, and an effective procedure to estimate it computationally. In this setting, the expected behavior is given as a temporal logic specification, and the behavior of the system under perturbations is simply given by a set of numerical traces. Our technique is rather general since most modeling formalisms provide numerical traces as simulation results and since temporal logics are versatile specification languages adapted to capture the quantitative yet imprecise aspects of cellular behavior. The computation of the robustness estimate is based on the notion of violation degree that measures the distance between the expected behavior and the behavior of the perturbed system [Rizk et al, CMSB'08]. This method has been implemented in the modeling environment Biocham and applied to cell cycle and transcriptional cascade models.
Joint work with Aurélien Rizk, Sylvain Soliman and François Fages
Understanding the processes involved in multi-cellular pattern formation is a central problem of developmental biology, hopefully leading to many new insights, e.g., in the treatment of various diseases. Defining suitable computational techniques for development modelling, able to perform in silico simulation experiments, is an open and challenging problem. Here we apply the coarse-grained, quantitative approach based on the basic Petri net formalism we introduced previously to mimic the behaviour of the biological processes during multicellular differentiation. We show that for the well-studied process of C. elegans vulval development, our model correctly reproduces a large set of in vivo experiments with statistical accuracy. It also generates gene expression time series in accordance with recent biological evidence. Finally, we modelled the role of microRNA mir-61 during vulval development and predict its contribution in stabilising cell pattern formation.
In this talk we introduce the concept of Model Engineering, which is a systematic approach for designing, constructing and analyzing computational models of biological systems, and takes some inspiration from efficient software engineering strategies. We will focus on how model checking can be used to aid the contruction and validation of models of biological systems. The approaches that we describe contribute to efforts both in Systems Biology as well as Synthetic Biology.
Model checking in this context is to "Formally check whether a model of a biological system does what we want", and involves the use of a computer programme to check whether a formal model of a biological system exhibits a desired behavioural property. We will discuss the application of model checking to model validation, model analysis, model development, model searching and biosystem verification.
We illustrate these by reference to the simulative MC2 Model Checker which operates over properties written in Probabilistic Linear-time Temporal Logic with numerical constraints (PLTLc), and which can handle descriptions ranging from highly qualitative to fully quantitative.