Hybrid Systems Biology

The problem of model parametrization is a core issue for all varieties of mathematical modelling in biology. This problem becomes more tractable when qualitative modelling is used, since the range of parameter values is finite and consequently it is possible to enumerate and evaluate all possible parametrizations of a model. If such an approach is undertaken, one usually obtains a vast set of parametrizations that are scored for various properties, e.g. fitness. The usual next step is to take the best scoring parametrization. However, as noted in recent works [1, 4], there is knowledge to be gained from examining sets of parametrizations based on their scoring. In this article we extend this line of thought and introduce a comprehensive workflow for comparing such sets and obtaining knowledge from the comparison.

We develop a GPU based technique to analyze bio-pathway models consisting of systems of ordinary differential equations (ODEs). A key component in our technique is an online procedure for verifying whether a numerically generated trajectory of a model satisfies a property expressed in bounded linear temporal logic. Using this procedure, we construct a statistical model checking algorithm which exploits the massive parallelism offered by GPUs while respecting the severe constraints imposed by their memory hierarchy and the hardware execution model. To demonstrate the computational power of our method, we use it to solve the parameter estimation problem for bio-pathway models. With three realistic benchmarks, we show that the proposed technique is computationally efficient and scales well with the number of GPU units deployed. Since both the verification framework and the computational platform are generic, our scheme can be used to solve a variety of analysis problems for models consisting of large systems of ODEs.

Analysis of equilibria, their stability and instability, is an unavoidable ingredient of model analysis in systems biology. In particular, bifurcation analysis which focuses on behaviour of phase portraits under variations of parameters is of great importance. We propose a novel method for bifurcation analysis that employs coloured model checking to analyse phase portraits bifurcation in rectangular abstractions of piecewise-affine systems. The algorithm works on clusters of workstations and multi-core computers to allow scalability. We demonstrate the method on a repressilator genetic regulatory network.

In this work we propose an automatic way of generating and verifying formal hybrid models of signaling and transcriptional events, gathered in large-scale regulatory networks.This is done by integrating temporal and stochastic aspects of the expression of some biological components. The hybrid approach lies in the fact that measurements take into account both times of lengthening phases and discrete switches between them. The model proposed is based on a real case study of keratinocytes differentiation, in which gene time-series data was generated upon Calcium stimulation.

To achieve this we rely on the Process Hitting (PH) formalism that was designed to consider large-scale system analysis. We first propose an automatic way of detecting and translating biological motifs from the Pathway Interaction Database to the PH formalism. Then, we propose a way of estimating temporal and stochastic parameters from time-series expression data of action on the PH. Simulations emphasize the interest of synchronizing concurrent events.

Hybrid systems whose mode dynamics are governed by non-linear ordinary differential equations (ODEs) are often a natural model for biological processes. However such models are difficult to analyze. To address this, we develop a probabilistic analysis method by approximating the mode transitions as stochastic events. We assume that the probability of making a mode transition is proportional to the measure of the set of pairs of time points and value states at which the mode transition is enabled. To ensure a sound mathematical basis, we impose a natural continuity property on the non-linear ODEs. We also assume that the states of the system are observed at discrete time points but that the mode transitions may take place at any time between two successive discrete time points. This leads to a discrete time Markov chain as a probabilistic approximation of the hybrid system. We then show that for BLTL (bounded linear time temporal logic) specifications the hybrid system meets a specification iff its Markov chain approximation meets the same specification with probability 1. Based on this, we formulate a sequential hypothesis testing procedure for verifying–approximately–that the Markov chain meets a BLTL specification with high probability. Our case studies on cardiac cell dynamics and the circadian rhythm indicate that our scheme can be applied in a number of realistic settings.

We consider the problem of automatically finding safe and robust values of timing parameters of cardiac pacemaker models so that a quantitative objective, such as the pacemaker energy consumption or its cardiac output (a heamodynamic indicator of the human heart), is optimised in a finite path. The models are given as parametric networks of timed I/O automata with data, which extend timed I/O automata with priorities, real variables and real-valued functions, and specifications as Counting Metric Temporal Logic (CMTL) formulas. We formulate the parameter synthesis as a bilevel optimisation problem, where the quantitative objective (the outer problem) is optimised in the solution space obtained from optimising an inner problem that yields the maximal robustness for any parameter of the model. We develop an SMT-based method for solving the inner problem through a discrete encoding, and combine it with evolutionary algorithms and simulations to solve the outer optimisation task. We apply our approach to the composition of a (non-linear) multi-component heart model with the parametric dual chamber pacemaker model in order to find the values of multiple timing parameters of the pacemaker for different heart diseases.

We consider the problem of understanding how DNA methylation fidelity, i.e. the preservation of methylated sites in the genome, varies across the genome and across different cell types. Our approach uses a stochastic model of DNA methylation across generations and trains it using data obtained through next generation sequencing. By training the model locally, i.e. learning its parameters based on observations in a specific genomic region, we can compare how DNA methylation fidelity varies genome-wide. In the paper, we focus on the computational challenges to scale parameter estimation to the whole-genome level, and present two methods to achieve this goal, one based on moment-based approximation and one based on simulation. We extensively tested our methods on synthetic data and on a first batch of experimental data.

When designing genetic circuits, the typical primitives used in major existing modelling formalisms are gene interaction graphs, where edges between genes denote either an activation or inhibition relation. However, when designing experiments, it is important to be precise about the low-level mechanistic details as to how each such relation is implemented. The rule-based modelling language Kappa allows to unambiguously specify mechanistic details such as DNA binding sites, dimerisation of transcription factors, or co-operative interactions. Such a detailed description comes with complexity and computationally costly executions. We propose a general method for automatically transforming a rule-based program, by eliminating intermediate species and adjusting the rate constants accordingly. To the best of our knowledge, we show the first automated reduction of rule-based models based on equilibrium approximations.

Our algorithm is an adaptation of an existing algorithm, which was designed for reducing reaction-based programs; our version of the algorithm scans the rule-based Kappa model in search for those interaction patterns known to be amenable to equilibrium approximations (e.g. Michaelis-Menten scheme). Additional checks are then performed in order to verify if the reduction is meaningful in the context of the full model. The reduced model is efficiently obtained by static inspection over the rule-set. The tool is tested on a detailed rule-based model of a \(\lambda \)-phage switch, which lists 92 rules and 13 agents. The reduced model has 11 rules and 5 agents, and provides a dramatic reduction in simulation time of several orders of magnitude.

We present what we believe to be the first formal verification of a biologically realistic (nonlinear ODE) model of a neural circuit in a multicellular organism: Tap Withdrawal (TW) in C. Elegans, the common roundworm. TW is a reflexive behavior exhibited by C. Elegans in response to vibrating the surface on which it is moving; the neural circuit underlying this response is the subject of this investigation. Specially, we perform reach-tube-based reachability analysis on the TW circuit model of Wicks et al. (1996) to estimate key model parameters. Underlying our approach is the use of Fan and Mitra’s recently developed technique for automatically computing local discrepancy (convergence and divergence rates) of general nonlinear systems.

The results we obtain are a significant extension of those of Wicks et al. (1996), who equip their model with fixed parameter values that reproduce the predominant TW response they observed experimentally in a population of 590 worms. In contrast, our techniques allow us to much more fully explore the model’s parameter space, identifying in the process the parameter ranges responsible for the predominant behavior as well as the non-dominant ones. The verification framework we developed to conduct this analysis is model-agnostic, and can thus be re-used on other complex nonlinear systems.

Many biological processes are described with coupled non-linear systems of ordinary differential equations that contain a plethora of parameters. The goal is to understand these systems and to predict the effect of different influences. This asks for a dynamical systems approach where numerical continuation methods and bifurcation analysis are used to detect the solutions and their stability as a function of the parameters. We developed PyNCT – Python Numerical Continuation Toolbox – an open source Python package that implements numerical continuation methods and can perform bifurcation analysis based on sparse linear algebra. The software gives the user the choice of different solvers (direct and iterative) and allows the use of preconditioners to reduce the number of iterations and guarantee the convergence when working with complex non-linear models.

In this paper we demonstrate the usefulness of the toolbox with a class of models pertaining to auxin transport between cells in plant organs.We show how easy it is to compute the steady state solutions for different parameter values, to calculate how they depend on each other and to map parts of the solution landscape.

An interactive model development and discovery cycle is key in bio-systems research. It allows one to investigate and compare different model parameter settings and even different models and gauge the model’s usefulness. Our toolbox allows for such quick experimentation and has a low entry barrier for non-technical users.

Although PyNCT was developed particularly for the study of transport models in biology, its implementation is generic and extensible, and can be used in many other dynamical system applications.

Systems biology attempts to understand biological systems by their structure, dynamics, and control methods. Hepatocyte growth factor (HGF) and interleukin 6 (IL6) are two proteins involved in cellular signaling that bind specific cell surface receptors (HGFR and IL6R, respectively) in order to induce cellular proliferation in different cell types or cell contexts. In both cases, the signaling is initiated by binding the ligand (HGF or IL6) to the membrane-bound receptors (HGFR or IL6R) so as to trigger two cellular signaling paths that have several common elements. In this paper we discuss the processes by which an initial cell leads to cellular proliferation and/or survival signaling by using one of these two ligand/receptor systems analyzed by “rewriting logic” methodology. Rewriting logic procedures are suitable computational tools that handle these dynamic systems, and they can be applied to the study of specific biological pathways behavior. Pathway Logic (PL) constitutes a rewriting logic formalism that provides a knowledge base and development environment to carry out model checking, searches, and executions of signaling systems. Moreover, Pathway Logic Assistant (PLA) is a tool that helps us visualize, analyze and understand graphically cellular elements and their relations. We compare the models of HGF/HGFR and IL6/IL6R signaling pathways in order to investigate the relation between these processes and the way in which they induce cellular proliferation. In conclusion, our results illustrate the use of a logical system that explores complex and dynamic cellular signaling processes.