Full Papers

  • Sophie Le Bars, Jérémie Bourdon and Carito Guziolowski.  Comparing probabilistic and logic programming approaches to predict the effects of enzymes in a Neurogenerative disease model
    Abstract: The impact of a given treatment over a disease can be modeled by measuring the action of genes on enzymes, and the effect of perturbing these last over the optimal biomass production of an associated metabolic network. Following this idea, the relationship between genes and enzymes can be established using signaling and regulatory networks. These networks can be modeled using several mathematical paradigms, such as Boolean or Bayesian networks, among others. In this study we focus on two approaches related to the cited paradigms: a logical (discrete) Iggy, and a probabilistic (quantitative) one Probregnet. Our objective was to compare the computational predictions of the enzymes in these models upon a model pes.frerturbation. We used data from two previously published works that focused on the HIF-signaling pathway, known to regulate cellular processes in hypoxia and angiogenesis and to play a role in neurodegenerative diseases, in particular on the Alzheimer Disease (AD). The first study used Microarray gene expression data-sets from the Hippocampus of 10 AD patients and 13 healthy ones, the perturbation and thus the prediction was done in silico. The second one, used RNA-seq data from Human umbilical vein endothelial cells over-expressing adenovirally HIF1A proteins, here the enzyme was experimentally perturbed and the prediction was done in silico. Our results on the Microarray data-set were that Iggy and Probregnet showed very similar (73.3% of agreement) computational enzymes predictions upon the same perturbation. On the second data-set, we obtained different enzyme predictions (only 66.6% of agreement) using both modeling approaches; however Iggy’s predictions followed experimentally measured results on enzyme expression.
  • Eva Šmijáková, Samuel Pastva, David Šafránek and Lubos Brim Parameter Synthesis for Hybrid Systems from Hybrid CTL Specifications
    Abstract: We consider the parameter synthesis problem for multi-affine hybrid systems and properties specified using a hybrid extension of CTL (HCTL). The goal is to determine the sets of parameter valuations for which the given hybrid system satisfies the desired HCTL property. As our main contribution, we propose a shared-memory parallel algorithm which efficiently computes such parameter valuation sets. We combine a rectangular discretisation of the continuous dynamics with the discrete transitions of the hybrid system to obtain a single over-approximating semi-symbolic transition system. Such system can be then analysed using a fixed-point parameter synthesis algorithm to obtain all satisfying parametrisations. We evaluate the scalability of the method and demonstrate its applicability in a biological case study.
  • Alexandru Oarga, Bridget Bannerman and Jorge Julvez.  Growth Dependent Computation of Chokepoints in Metabolic Networks
    Abstract: Bacterial infections are among the major causes of mortality in the world. Despite the social and economical burden produced by bacteria, the number of new drugs to combat them increases very slowly due to the cost and time to develop them. Thus, innovative appoaches to identify efficiently drug targets are required. In the absence of genetic information, chokepoint reactions represent appealing drug targets since their inhibition might involve an important metabolic damage. In contrast to the standard definition of chokepoints, which is purely structural, this paper makes use of the dynamical information of the model to compute chokepoints. This novel approach can provide a more realistic set of chokepoints. The dependence of the number of chokepoints on the growth rate is assessed on a number of metabolic networks. A software tool has been implemented to facilitate the computation of growth dependent chokepoints by the practitioners.
  • Candan Çelik, Pavol Bokes and Abhyudai Singh.  Stationary distributions and metastable behaviour for self-regulating proteins with general lifetime distributions
    Abstract: Regulatory molecules such as transcription factors are often present at relatively small copy numbers in living cells. The copy number of a particular molecule fluctuates in time due to the random occurrence of production and degradation reactions. Here we consider a stochastic model for a self-regulating transcription factor whose lifespan (or time till degradation) follows a general distribution modelled as per a multi-dimensional phase-type process. We show that at steady state the protein copy-number distribution is the same as in a one-dimensional model with exponentially distributed lifetimes. This invariance result holds only if molecules are produced one at a time: we provide explicit counterexamples in the bursty production regime. Additionally, we consider the case of a bistable genetic switch constituted by a positively autoregulating transcription factor. The switch alternately resides in states of up- and downregulation and generates bimodal protein distributions. In the context of our invariance result, we investigate how the choice of lifetime distribution affects the rates of metastable transitions between the two modes of the distribution. The phase-type model, being non-linear and multi-dimensional whilst possessing an explicit stationary distribution, provides a valuable test example for exploring dynamics in complex biological systems.
  • Marielle Péré, Madalena Chaves and Jérémie Roux Core models of receptor reactions evaluate basic pathway designs enabling heterogeneous commitments to apoptosis
    Abstract: Isogenic cells can respond differently to cytotoxic treatments, such as the tumor necrosis factor-related apoptosis inducing ligand (TRAIL), with only a fraction committing to apoptosis. Since non-genetic transient resistance to TRAIL has been shown to dependent on caspase-8 dynamics at the receptor level \textit{in vitro}, here we investigate the core reactions leading to caspase-8 activation, based on mass-action kinetics models, to evaluate the basic mechanisms giving rise to the observed heterogeneous response. In this work, we fit our models to single-cell trajectories of time-resolved caspase-8 activation measured in clonal cells after treatment with TRAIL. Then, we analyse our results to assess the relevance of each model and evaluate how well it captures the extent of biological heterogeneity observed \textit{in vitro}. Particularly, we focus on a positive feedback loop on caspase-8, the impacts of initial condition variations and the relevance of the caspase-8 degradation.
  • Déborah Boyenval, Gilles Bernot, Hélène Collavizza and Jean-Paul Comet.  What is a cell cycle checkpoint ? The TotemBioNet answer
    Abstract: TotemBioNet is a new software platform to assist the design of qualitative regulatory network models by combining “genetically modified Hoare logic”, temporal logic model-checking and optimized enumeration techniques. TotemBioNet is particularly efficient to manage parameter identification, the most critical step of formal modelling. It is also
    remarkably flexible and efficient to check properties in order to explore biological assumptions. To illustrate this efficacy, we address the classical example of the cell cycle, where the passage from one phase to the next one, called checkpoint, is crucial but is usually a rather fuzzy informal concept. The cyclic behaviour of the cell cycle is specified by temporal logic and the order of individual events inside each phase is explored thanks to quantifiers introduced in Hoare logic. This way, TotemBioNet rapidly suggests a sensible formalization of checkpoints.
  • Stéphanie ChevalierVincent Noel, Laurence Calzone, Andrei Zinovyev and Loïc Paulevé Synthesis and Simulation of Ensembles of Boolean Networks for Cell Fate Decision
    Abstract: The construction of models of biological networks from prior knowledge and experimental data often leads a multitude of candidate models. Devising a single model from them can require arbitrary choices, which may lead to strong biases in subsequent predictions.We introduce here a methodology for a) synthesizing Boolean model ensembles satisfying a set of biologically relevant constraints and b) reasoning on the dynamics of the ensembles of models. The synthesis is performed using Answer-Set Programming, based on the approach introduced by us earlier. Here we extend the synthesis to account for solution diversity and for universal constraints on reachable fixed points, enabling accurate specification of desired dynamics.The sampled models are then simulated and the simulation results are aggregated through averaging or can be analyzed as a multi-dimensional distribution. The obtained results allow an interpretation at the level of cell population and take into account its heterogeneity.We illustrate our approach on a previously published Boolean model of a molecular network regulating the cell fate decisions in cancer progression. It appears that the ensemble-based approach to Boolean modelling brings new insights on the variability of the synergistically interacting mutation effect with respect to the propensity of a cancer cell to metastasize.

  • Ousmane Diop, Madalena Chaves and Laurent Tournier.  Qualitative analysis of mammalian circadian oscillations: cycle dynamics and robustness
    Abstract: In asynchronous Boolean models, periodic solutions are represented by terminal strongly connected graphs, which are typically composed of hundreds of states and transitions. For biological systems, it becomes a challenging task to compare such mathematical objects with biological knowledge, or interpret the transitions inside an attractor in terms of the sequence of events in a biological cycle. A recent methodology generates summary graphs to help visualizing complex asynchronous attractors and order the dynamic progression based on known biological data. In this article we apply this method to a Boolean model of the mammalian circadian clock, for which the summary graph recovers the main phases of the cycle, in the expected order. It also provides a detailed view of the attractor, suggesting improvements in the design of the model’s logical rules and highlighting groups of transitions that are essential for the attractor’s robustness.
  • Robert Schwieger, Matías Bender, Heike Siebert and Christian Haase.  Classifier construction in Boolean networks using algebraic methods
    Abstract: We investigate how classifiers for Boolean networks (BNs) can be constructed and modified under constraints. A typical constraint is that we assume to observe only states in attractors or even more specifically steady states of BNs. Steady states of BNs are one of the most interesting features for application. Large models can possess many steady states. In the typical scenario motivating this paper we start from a Boolean model with a given classification of the state space into phenotypes defined by high-level readout components. In order to link molecular biomarkers with experimental design, we search for alternative components suitable for the given classification task. This is useful for modelers of regulatory networks for suggesting experiments and measurements based on their models. It can also help to explain causal relations between components and phenotypes. To tackle this problem we need to use the structure of the Boolean network and the constraints. This calls for an algebraic approach. Indeed we demonstrate that this problem can be reformulated into the language of algebraic geometry. While already interesting in itself, this allows us to use Gröbner bases to construct an algorithm for finding such classifiers. We demonstrate the usefulness of this algorithm as a proof of concept on a model with 25 components.
  • Cui Su and Jun Pang Sequential Temporary and Permanent Control of Boolean Networks
    Abstract: Direct cell reprogramming makes it feasible to reprogram abundant somatic cells into desired cells. It has great potential for regenerative medicine and tissue engineering. In this work, we study the control of biological networks, modelled as Boolean networks, to identify control paths driving the dynamics of the network from a source attractor (undesired cells) to the target attractor (desired cells). Instead of achieving control in one step, we develop attractor-based sequential temporary and permanent control methods (AST and ASP) to identify a sequence of interventions that can alter the dynamics in a stepwise manner. To improve their feasibility, both AST and ASP only use biologically observable attractors as intermediates. They can find the shortest sequential paths and guarantee 100% reachability of the target attractor. We apply the two methods to several real-life biological networks and compare their performance with the attractor-based sequential instantaneous control (ASI). The results demonstrate that AST and ASP have the ability to identify a richer set of control paths with fewer perturbations than ASI, which will greatly facilitate practical applications.
  • Stefan HaarLoic Paulevé and Stefan Schwoon Drawing the Line: Basin Boundaries in Safe Petri Nets
    Abstract: Attractors of network dynamics represent the long-term behaviours of the modelled system. Understanding the basin of an attractor, comprising all those states from which the evolution will eventually lead into that attractor, is therefore crucial for understanding the response and differentiation
    capabilities of a dynamical system.
    Building on our previous results from CMSB 2014 allowing to find
    attractors via Petri net Unfoldings, we exploit further the unfolding technique for a backward exploration of the state space, starting from a known attractor, and show how all strong or weak basins of attractions can be explicitly computed.
  • Aurelien Desoeuvres, Gilles Trombettoni and Ovidiu Radulescu.  Interval Constraint Satisfaction and Optimization for Biological Homeostasis and Multistationarity
    Abstract: Homeostasis occurs in a biological or chemical system when some output variable remains approximately constant as one or several input variables or parameters change over some intervals.
    We propose in this paper a new computational method based on interval techniques to find species in biochemical systems that verify homeostasis. A somehow dual and equally important property is multistationarity, which means that the system has multiple steady states and possible outputs, at constant parameters. We also propose an interval method for testing multistationarity. We have tested homeostasis, absolute concentration robustness and multistationarity on a large collection of biochemical models from the Biomodels and DOCSS databases.
    The codes used in this paper are publicly available at: https://github.com/Glawal/IbexHomeo.
  • Gareth Molyneux and Alessandro Abate ABC(SMC)^2: Simultaneous inference and model checking of chemical reaction networks
    Abstract: We present an approach that simultaneously infers model parameters while statistically verifying properties of interest to chemical reaction networks,
    which we observe through data and model as parametrised continuous-time Markov Chains.
    The new approach simultaneously integrates formal verification over models,
    done by statistically model checking logical specifications expressed in CSL,
    with learning models from data,
    done by likelihood-free Bayesian inference, specifically Approximate Bayesian Computation.
    The approach generates a probability (or credibility calculation) on whether the underlying chemical reaction network satisfies the CSL property of interest.
  • Mathieu Hemery, François Fages and Sylvain Soliman On the Complexity of Binomialization for Polynomial Differential Equations
    Abstract: Chemical reaction networks (CRNs) are a standard formalism used in chemistry and biology to reason about the dynamics of molecular interaction networks. In their interpretation by ordinary differential equations, CRNs provide a Turing-complete model of analog computation, in the sense that any computable function over the reals can be computed by a finite number of molecular species with a continuous CRN which approximates the result of that function in one of its components in arbitrary precision. The proof of that result is based on a previous result of Bournez et al. on the Turing-completeness of polynomial ordi- nary differential equations with polynomial initial conditions (PIVP). It uses an encoding of real variables by two non-negative variables for con- centrations, and a transformation to an equivalent binomial PIVP with degree at most 2 for restricting to at most bimolecular reactions. In this paper, we study the theoretical and practical complexities of the binomial transformation. We show that both problems of minimizing either the number of variables (i.e., molecular species) or the number of monomials (i.e. elementary reactions) in a binomial transformation of a PIVP are NP-hard. We present an encoding of those problems in MAX-SAT and show the practical complexity of this algorithm on a benchmark of binomialization problems inspired from CRN design problems.
  • Elisabeth Degrand, François Fages and Sylvain Soliman Graphical Conditions for Rate Independence in Chemical Reaction Networks
    Abstract: Chemical Reaction Networks (CRNs) provide a useful abstraction of molecular interaction networks in which molecular structures as well as mass conservation principles are abstracted away to focus on the main dynamical properties of the network structure. In their interpretation by ordinary differential equations, we say that a CRN with distinguished input and output species computes a positive real function f : R+ → R+, if for any initial concentration x of the input species, the concentration of the output molecular species stabilizes at concentration f(x). The Turing-completeness of that notion of chemical analog computation has been established by proving that any computable real function can be computed by a CRN over a finite set of molecular species. Rate independent CRNs form a restricted class of CRNs of high practical value since they enjoy a form of absolute robustness in the sense that the result is completely independent of the reaction rates and depends solely on the input concentrations. The functions computed by rate-independent CRNs have already been characterized mathematically by Soloveichik et al. as the set of piecewise linear functions from input species. In this paper, we provide graphical conditions on the Petri Net structure of a CRN which entail the rate-independence property. We show that in the curated part of the Biomodels repository, among the 590 reaction models tested, 94 are found rate-independent for some output species, and 2 for all species. Our graphical conditions are based on a non-standard use of the Petri net notions of place-invariants and siphons which are computed here by constraint programming for efficiency reasons.
  • Julia Klein, Pavol Bokes and Tatjana Petrov.  Accelerating reactions at the DNA can slow down transient gene expression
    Abstract: The expression of a gene is characterised by the upstream transcription factors and the biochemical reactions at the DNA processing them. Transient profile of gene expression then depends on the amount of involved transcription factors, and the scale of kinetic rates of regulatory reactions at the DNA. Due to the combinatorial explosion of the number of possible DNA configurations and uncertainty about the rates, a detailed mechanistic model is often difficult to analyse and even to write down. For this reason, modelling practice often abstracts away details such as the relative speed of rates of different reactions at the DNA, and how these reactions connect to one another.
    In this paper, we investigate how the transient gene expression depends on the topology and scale of the rates of reactions involving the DNA. We consider a generic example where a single protein is regulated through a number of arbitrarily connected DNA configurations, without feedback. In our first result, we analytically show that, if all switching rates are uniformly speeded up, then, as expected, the protein transient is faster and the noise is smaller. Our second result finds that, counterintuitively, if all rates are fast but some more than others (two orders of magnitude vs. one order of magnitude), the opposite effect may emerge: time to equilibration is slower and protein noise increases. In particular, focusing on the case of a mechanism with four DNA states, we first illustrate the phenomenon numerically over concrete parameter instances. Then, we use singular perturbation analysis to systematically show that, in general, the fast chain with some rates even faster, exactly reduces to a slow-switching chain. Our analysis has wide implications for quantitative modelling of gene regulation: it emphasises the importance of accounting for the network topology of regulation among DNA states, and the importance of accounting for different magnitudes of respective reaction rates. We conclude the paper by discussing the results in context of general collective behaviour.
  • Laura Cifuentes Fontanals, Elisa Tonello and Heike Siebert Control Strategy Identification via Trap Spaces in Boolean Networks
    Abstract: The control of biological systems presents interesting applications such as cell reprogramming or drug target identification. A common type of control strategy consists in a set of interventions that, by fixing the values of some variables, force the system to evolve to a desired state. This work presents a new approach for finding control strategies in biological systems modeled by Boolean networks. In this context, we explore the properties of trap spaces, subspaces of the state space which the dynamics cannot leave. Trap spaces for biological networks can often be efficiently computed, and provide useful approximations of attraction basins. Our approach provides control strategies for a target phenotype that are based on interventions that allow the control to be eventually released. Moreover, our method can incorporate information about the attractors to find new control strategies that would escape usual percolation-based methods. We show the applicability of our approach to two cell fate decision models.
  • Vincent Danos, Tobias Heindel, Ricardo Honorato-Zimmer and Sandro Stucki Rate Equations for Graphs
    Abstract: In this paper, we combine ideas from two different scientific traditions: 1) graph transformation systems (GTSs) stemming from the theory of formal languages and concurrency, and 2) mean field approximations (MFAs), a collection of approximation techniques ubiquitous in the study of complex dynamics. Using existing tools from algebraic graph rewriting, as well as new ones, we build a framework which generates rate equations for stochastic GTSs and from which one can derive MFAs of any order (no longer limited to the humanly computable). The procedure for deriving rate equations and their approximations can be automated. An implementation and example models are available online at http://rhz.github.io/fragger. We apply our techniques and tools to derive an expression for the mean velocity of a two-legged walker protein on DNA.

Tool Papers

  • Luca Cardelli Kaemika app: Integrating protocols and chemical simulation
    Abstract: Kaemika is an app available on the four major app stores. It provides deterministic and stochastic simulation, supporting natural chemical notation enhanced with recursive and conditional generation of chemical reaction networks. It has a liquid-handling protocol sublanguage compiled to a virtual digital microfluidic device. Chemical and microfluidic simulations can be interleaved for full experimental-cycle modeling. A novel and unambiguous representation of directed multigraphs is used to lay out chemical reaction networks in graphical form.
  • Jorge Julvez and Stephen G Oliver.  fnyzer: a Python package for the analysis of Flexible Nets
    Abstract: This paper introduces fnyzer, a Python package for the analysis of Flexible Nets (FNs). FNs is a modelling formalism for dynamical systems that can accommodate a number of uncertain parameters, and that is particularly well suited to model the different types of networks arising in systems biology. fnyzer offers different types of analysis, can handle nonlinear dynamics, and can transform SBML models into FN format.
  • Matej Troják, David Šafránek, Lukrécia Mertová and Lubos Brim eBCSgen: A Software Tool for Biochemical Space Language
    Abstract: eBCSgen is a tool for development and analysis of models written in Biochemical Space Language (BCSL). BCSL is a rule-based language for biological systems designed to combine compact description with a specific level of abstraction which makes it accessible to users from life sciences. Currently, eBCSgen represents the only tool completely supporting BCSL. It has the form of a command line interface which is integrated into Galaxy — a web-based bioinformatics platform automating data-driven and model-based analysis pipelines.
  • Filipe Gouveia, Ines Lynce and Pedro T. Monteiro ModRev - Model Revision tool for Boolean logical models of biological regulatory networks
    Abstract: Biological regulatory networks can be represented by computational models, which allow the study and the analysis of biological behaviours, therefore providing a better understanding of a given biological process.
    However, as new information is acquired, biological models may need to be revised, in order to also account for this new information.

    Here, we present a model revision tool, capable of repairing inconsistent Boolean biological models. Moreover, the tool is able to confront the models, both with steady state observations, as well as time-series data, considering both synchronous and asynchronous update schemes.
    The tool was tested with a well-known biological model that was corrupted with different random changes. The presented tool was able to successfully repair the majority of the corrupted models.