Abstract:
Symbolic systems biology aims to explore biological processes as whole systems instead of small and independent elements. The goal is to define formal models that capture biologists intuitions and reasoning. Pathway Logic is a system for developing executable formal models of biomolecular processes. Using the Maude system, these models of dynamic processes can be represented and analyzed. The Pathway Logic Assistant uses forwards and backwards collection to assemble a connected set of rules from a rule knowledge base to model a system specified by an initial state (experimental setup). For this to succeed the rules must represent component states at the same level of detail, while we would like the knowledge base to capture as much detail as possible. In this paper, we propose a different way to perform matching in the process of rewriting in the high-performance rewriting language Maude. The basic concept is that of ‘‘fuzzy match’’ or ‘‘fuzzy instantiates to’’. It will be used to check requirements imposed by controls in forward collection, and with some elaboration to check whether the change part of a rule applies forwards or backwards.
Abstract:
The analysis of equilibria of ordinary differential equations (ODEs) that represent biochemical reaction networks is crucial in order to understand various functional properties of regulation in systems biology. In this paper, we develop a numerical algorithm to compute equilibria under the assumption that the regulatory network satisfies certain graph-theoretic conditions which lead to fixed-point iterations over an anti-monotonic function. Unlike generic approaches based on Newton’s method, our algorithm does not require the availability of the Jacobian of the ODE vector field, which may be expensive when the dimensionality of the system is large. More important, it produces an estimation (through over-approximation) of the entire set of equilibria, with the guarantee of yielding the unique equilibrium of the ODE in the case that the returned set is a singleton. We demonstrate the applicability of our algorithm to two signaling pathways of MAPK and EGFR.
Abstract:
Stochastic processes can model many emerging phenomena on networks, like the spread of computer viruses, rumors, or infectious diseases. Understanding the dynamics of such stochastic spreading processes is therefore of fundamental interest. In this work we consider the wide-spread compartment model where each node is in one of several states (or compartments). Nodes change their state randomly after an exponentially distributed waiting time and according to a given set of rules. For networks of realistic size, even the generation of only a single stochastic trajectory of a spreading process is computationally very expensive.
Here, we propose a novel simulation approach, which combines the advantages of event-based simulation and rejection sampling. Our method outperforms state-of-the-art methods in terms of absolute runtime and scales significantly better while being statistically equivalent.
Abstract:
Protein levels can be controlled by regulating protein synthesis or half life. The aim of this paper is to investigate how introducing feedback in burst frequency or protein decay rate affects the stochastic distribution of protein level. Using a tractable hybrid mathematical framework, we show that the two feedback pathways lead to the same mean and noise predictions in the small-noise regime. Away from the small-noise regime, feedback in decay rate outperforms feedback in burst frequency in terms of noise control. The difference is particularly conspicuous in the strong-feedback regime. We also formulate a fine-grained discrete model which reduces to the hybrid model in the large system-size limit. We show how to approximate the discrete protein copy-number distribution and its Fano factor using hybrid theory. We also demonstrate that the hybrid model reduces to an ordinary differential equation in the limit of small noise. Our study thus contains a comparative evaluation of feedback in burst frequency and decay rate, and provides additional results on model reduction and approximation.
Abstract:
Cell signaling plays an important role in the normal functioning of cells and in health conditions such as cancers and immune diseases. Cell signaling models, capturing the transformations of many different molecular species, are one of the most successful applications of dynamical systems biology. Since they involve highly nonlinear dynamics, the predicting power of these models is often limited due to the difficulty in estimating the relevant kinetic parameters. Fluorescent labeling in conjunction with super-resolution microscopy provides in vivo trajectories of receptors and other bio-molecules of interest. This modality is possibly the most direct source of quantitative information on molecular processes in cells. Unfortunately, it is separated by a few orders of magnitude from the resolution of current quantitative models of cell signaling. Signaling models typically require properties (concentrations, reaction rates) averaged over the entire cell; single particle tracking looks at individual molecules in small fraction of the cell. In principle, the gap in resolution can be bridged using simulations: validate a fully spatial model at SPT resolution, then use a consistent abstraction / averaging procedure to infer effective kinetics on larger spatial scales. Extrapolating diffusion coefficients and dimerization rates observed at SPT resolution is complicated by the presence of spatial structure that interferes with the free movement of molecules of interest. Here we present a method used to identify such structures, based on deviations from ideal Brownian motion and outline a framework aimed at refinement using simulated motion in a known landscape.
Abstract:
The understanding of mechanisms that control epigenetic changes is an important research area in modern functional biology. Epigenetic modifications such as DNA methylation are in general very stable over many cell divisions. DNA methylation can however be subject to specific and fast changes over a short time scale even in non dividing (i.e. not-replicating) cells. Such dynamic DNA methylation changes are caused by a combination of active demethylation and de novo methylation processes which have not been investigated in integrated models. Here we present a hybrid (hidden) Markov model to describe the cycle of methylation and demethylation over (short) time scales. Our hybrid model describes several molecular events either happening at deterministic points (i.e. describing mechanisms that occur only during cell division) and other events occurring at random time points. We test our model on mouse embryonic stem cells using time-resolved data. We predict methylation changes and estimate the efficiencies of the different modification steps related to DNA methylation and demethylation.
Abstract:
Metabolism and cell cycle are two central processes in the life of a eukaryote cell. If they have been extensively studied in their own right, their interconnection remains relatively poorly understood. In this paper, we propose to use a differential model of the central carbon metabolism. After verifying it reproduces major known variations across the cell cycle’s phases, we extend it into a hybrid system reproducing an imposed succession of the phases. This first hybrid approach recovers interesting dynamical results, providing a good first step towards a more complex hybrid system.
Abstract:
Stochastic population models are widely used to model phenomena in different areas such as chemical kinetics or collective animal behaviour. Quantitative analysis of stochastic population protocols easily becomes challenging, due to the combinatorial propagation of dependencies across the population. The complexity becomes especially prominent when model’s parameters are not known and available measurements are limited. In this paper, we illustrate this challenge on a concrete scenario: we assume a simple communication scheme among identical individuals, inspired by how social honeybees emit the alarm pheromone to protect the colony in case of danger. Together, n individuals induce a population Markov chain model with n parameters. In addition, we assume to be able to experimentally observe the states only after the steady-state is reached. In order to obtain the parameters of the individual’s behaviour, by utilising the available data, and without making any further modelling assumption, we combine two existing techniques. First, we use the tools for parameter synthesis for Markov chains with respect to temporal logic properties, and then we employ CEGAR-like reasoning to find the viable parameter space up to desired coverage. We report the performance on a number of synthetic data sets.
Abstract:
In this work we introduce the software rPrism, as an branch of the software PRISM model checker, in order to be able to study weighted reactive state transition models. This kind of model gathers together the concepts of reactivity - which consists on the capacity of a state transition model to alter its accessibility relation - and weights, which can be seen as costs, rates, etc.. Given a specific model, the tool performs a simulation based on a Continuous Time Markov Chain. In particular, we show an example of its application for biological systems.
Abstract:
We introduce a metabolic-regulatory network model (MRN) extending the self-replicator system proposed by Molenaar et al. (2011). Our model allows integrating metabolism with catalytic macromolecules, structural building blocks and regulatory proteins. Using MRN, we show that the dynamic interplay between cellular metabolism, macromolecule production and regulation can be formalized by a hybrid automaton, combining continuous dynamics and discrete control.
Abstract:
Comprehensive Modelling Platform is a general framework for public sharing, annotation, and visualisation of domain-specific biological models. For a selected system (e.g. an organism, particular process), the framework is instantiated as a web-based application which allows capturing several aspects of biological models represented as biochemical reaction networks or ordinary differential equations.
Abstract:
Fluid approximations have been greatly successful in approximating the macro-scale behaviour of Markov systems with a large number of discrete states. However, these methods rely on the continuous-time Markov chain (CTMC) having a particular population structure which suggests a natural continuous state-space endowed with a dynamics for the approximating process.
We construct here a general method based on spectral analysis of the transition matrix of the CTMC, without the need for a population structure. Specifically, we use the popular manifold learning method of diffusion maps to analyse the transition matrix as the operator of a hidden continuous process. An embedding of states in a continuous space is recovered, and the space is endowed with a drift vector field inferred via Gaussian process regression. In this manner, we construct an ODE whose solution approximates the evolution of the CTMC mean, mapped onto the continuous space (known as the fluid limit).
Abstract:
Synthesis methods based on formal reasoning are a powerful way to automate the process of constructing computational models of gene regulatory networks (GRNs) and increase predictive power by considering a set of consistent models that are guaranteed to satisfy known experimental data. Previously, a formal reasoning based approach enabling the synthesis and analysis of biological networks formalized using Abstract Boolean Networks (ABNs) was developed, where the precise interactions and update rules are only partially known. System dynamics can be constrained with specifications of some required behaviors, thereby providing a characterization of the set of all networks capable of reproducing given experimental observations. The synthesis method is supported by a tool, the Reasoning Engine for Interaction Networks (RE:IN). Starting with the synthesis framework supported by RE:IN, we provide translations of experimental observations to temporal logic and semantics of Abstract Boolean Networks, enabling us to use off-the-shelf model checking tools and algorithms. An initial prototype implementation we have developed demonstrates this is a gainful approach, providing speed-up gains for some benchmarks, while also opening the way to study extensions of the experimental observations specification language currently supported in RE:IN by using the rich expressive power of temporal logic.