The Reasoning Engine: A Satisfiability Modulo Theories-Based Framework for Reasoning About Discrete Biological Models.

We present a framework called the Reasoning Engine, which implements Satisfiability Modulo Theories (SMT)-based methods within a unified computational environment to address diverse biological analysis problems. The Reasoning Engine was used to reproduce results from key scientific studies, as well as supporting new research in stem cell biology. The framework utilizes an intermediate language for encoding partially specified discrete dynamical systems, which bridges the gap between high-level domain-specific languages and low-level SMT solvers. We provide this framework as open source together with various biological case studies, illustrating the synthesis, enumeration, optimization, and reasoning over models consistent with experimental observations to reveal novel biological insights.

Esrrb guides naive pluripotent cells through the formative transcriptional programme.

During embryonic development, naive pluripotent epiblast cells transit to a formative state. The formative epiblast cells form a polarized epithelium, exhibit distinct transcriptional and epigenetic profiles and acquire competence to differentiate into all somatic and germline lineages. However, we have limited understanding of how the transition to a formative state is molecularly controlled. Here we used murine embryonic stem cell models to show that ESRRB is both required and sufficient to activate formative genes. Genetic inactivation of Esrrb leads to illegitimate expression of mesendoderm and extra-embryonic markers, impaired formative expression and failure to self-organize in 3D. Functionally, this results in impaired ability to generate formative stem cells and primordial germ cells in the absence of Esrrb. Computational modelling and genomic analyses revealed that ESRRB occupies key formative genes in naive cells and throughout the formative state. In so doing, ESRRB kickstarts the formative transition, leading to timely and unbiased capacity for multi-lineage differentiation.

Solving Exact Cover Instances with Molecular-Motor-Powered Network-Based Biocomputation.

Information processing by traditional, serial electronic processors consumes an ever-increasing part of the global electricity supply. An alternative, highly energy efficient, parallel computing paradigm is network-based biocomputation (NBC). In NBC a given combinatorial problem is encoded into a nanofabricated, modular network. Parallel exploration of the network by a very large number of independent molecular-motor-propelled protein filaments solves the encoded problem. Here we demonstrate a significant scale-up of this technology by solving four instances of Exact Cover, a nondeterministic polynomial time (NP) complete problem with applications in resource scheduling. The difficulty of the largest instances solved here is 128 times greater in comparison to the current state of the art for NBC.

Modeling the C. elegans germline stem cell genetic network using automated reasoning.

Computational methods and tools are a powerful complementary approach to experimental work for studying regulatory interactions in living cells and systems. We demonstrate the use of formal reasoning methods as applied to the Caenorhabditis elegans germ line, which is an accessible system for stem cell research. The dynamics of the underlying genetic networks and their potential regulatory interactions are key for understanding mechanisms that control cellular decision-making between stem cells and differentiation. We model the "stem cell fate" versus entry into the "meiotic development" pathway decision circuit in the young adult germ line based on an extensive study of published experimental data and known/hypothesized genetic interactions. We apply a formal reasoning framework to derive predictive networks for control of differentiation. Using this approach we simultaneously specify many possible scenarios and experiments together with potential genetic interactions, and synthesize genetic networks consistent with all encoded experimental observations. In silico analysis of knock-down and overexpression experiments within our model recapitulate published phenotypes of mutant animals and can be applied to make predictions on cellular decision-making. A methodological contribution of this work is demonstrating how to effectively model within a formal reasoning framework a complex genetic network with a wealth of known experimental data and constraints. We provide a summary of the steps we have found useful for the development and analysis of this model and can potentially be applicable to other genetic networks. This work also lays a foundation for developing realistic whole tissue models of the C. elegans germ line where each cell in the model will execute a synthesized genetic network.

Formal Analysis of Network Motifs Links Structure to Function in Biological Programs.

A recurring set of small sub-networks have been identified as the building blocks of biological networks across diverse organisms. These network motifs are associated with certain dynamic behaviors and define key modules that are important for understanding complex biological programs. Besides studying the properties of motifs in isolation, current algorithms typically evaluate the occurrence frequency of a specific motif in a given biological network compared to that in random networks of similar structure. However, it remains challenging to relate the structure of motifs to the observed and expected behavior of the larger, more complex network they are contained within. This problem is compounded as even the precise structure of most biological networks remains largely unknown. Previously, we developed a formal reasoning approach enabling the synthesis of biological networks capable of reproducing some experimentally observed behavior. Here, we extend this approach to allow reasoning over the requirement for specific network motifs as a way of explaining how these behaviors arise. We illustrate the approach by analyzing the motifs involved in sign-sensitive delay and pulse generation. We demonstrate the scalability and biological relevance of the approach by studying the previously defined networks governing myeloid differentiation, the yeast cell cycle, and naïve pluripotency in mouse embryonic stem cells, revealing the requirement for certain motifs in these systems.

Discovering Essential Multiple Gene Effects Through Large Scale Optimization: An Application to Human Cancer Metabolism.

Computational modelling of metabolic processes has proven to be a useful approach to formulate our knowledge and improve our understanding of core biochemical systems that are crucial to maintaining cellular functions. Towards understanding the broader role of metabolism on cellular decision-making in health and disease conditions, it is important to integrate the study of metabolism with other core regulatory systems and omics within the cell, including gene expression patterns. After quantitatively integrating gene expression profiles with a genome-scale reconstruction of human metabolism, we propose a set of combinatorial methods to reverse engineer gene expression profiles and to find pairs and higher-order combinations of genetic modifications that simultaneously optimize multi-objective cellular goals. This enables us to suggest classes of transcriptomic profiles that are most suitable to achieve given metabolic phenotypes. We demonstrate how our techniques are able to compute beneficial, neutral or "toxic" combinations of gene expression levels. We test our methods on nine tissue-specific cancer models, comparing our outcomes with the corresponding normal cells, identifying genes as targets for potential therapies. Our methods open the way to a broad class of applications that require an understanding of the interplay among genotype, metabolism, and cellular behaviour, at scale.

A Method to Identify and Analyze Biological Programs through Automated Reasoning.

Predictive biology is elusive because rigorous, data-constrained, mechanistic models of complex biological systems are difficult to derive and validate. Current approaches tend to construct and examine static interaction network models, which are descriptively rich but often lack explanatory and predictive power, or dynamic models that can be simulated to reproduce known behavior. However, in such approaches implicit assumptions are introduced as typically only one mechanism is considered, and exhaustively investigating all scenarios is impractical using simulation. To address these limitations, we present a methodology based on automated formal reasoning, which permits the synthesis and analysis of the complete set of logical models consistent with experimental observations. We test hypotheses against all candidate models, and remove the need for simulation by characterizing and simultaneously analyzing all mechanistic explanations of observed behavior. Our methodology transforms knowledge of complex biological processes from sets of possible interactions and experimental observations to precise, predictive biological programs governing cell function.

How computational models contribute to our understanding of the germ line.

Computational models are an invaluable tool in modern biology. They provide a framework within which to summarize existing knowledge, enable competing hypotheses to be compared qualitatively and quantitatively, and to facilitate the interpretation of complex data. Moreover, models allow questions to be investigated that are difficult to approach experimentally. Theories can be tested in context, identifying the gaps in our understanding and potentially leading to new hypotheses. Models can be developed on a variety of scales and with different levels of mechanistic detail, depending on the available data, the biological questions of interest, and the available mathematical and computational tools. The goal of this review is to provide a broad picture of how modeling has been applied to reproductive biology. Specifically, we look at four uses of modeling: (i) comparing hypotheses; (ii) interpreting data; (iii) exploring experimentally challenging questions; and (iv) hypothesis evaluation and generation. We present examples of each of these applications in reproductive biology, drawing from a range of organisms-including Drosophila, Caenorhabditis elegans, mouse, and humans. We aim to describe the data and techniques used to construct each model, and to highlight the benefits of modeling to the field, as complementary to experimental work. Mol. Reprod. Dev. 83: 944-957, 2016 © 2016 Wiley Periodicals, Inc.

Automated Synthesis and Analysis of Switching Gene Regulatory Networks.

Studying the gene regulatory networks (GRNs) that govern how cells change into specific cell types with unique roles throughout development is an active area of experimental research. The fate specification process can be viewed as a biological program prescribing the system dynamics, governed by a network of genetic interactions. To investigate the possibility that GRNs are not fixed but rather change their topology, for example as cells progress through commitment, we introduce the concept of Switching Gene Regulatory Networks (SGRNs) to enable the modelling and analysis of network reconfiguration. We define the synthesis problem of constructing SGRNs that are guaranteed to satisfy a set of constraints representing experimental observations of cell behaviour. We propose a solution to this problem that employs methods based upon Satisfiability Modulo Theories (SMT) solvers, and evaluate the feasibility and scalability of our approach by considering a set of synthetic benchmarks exhibiting possible biological behaviour of cell development. We outline how our approach is applied to a more realistic biological system, by considering a simplified network involved in the processes of neuron maturation and fate specification in the mammalian cortex.

Mechano-logical model of C. elegans germ line suggests feedback on the cell cycle.

The Caenorhabditis elegans germ line is an outstanding model system in which to study the control of cell division and differentiation. Although many of the molecules that regulate germ cell proliferation and fate decisions have been identified, how these signals interact with cellular dynamics and physical forces within the gonad remains poorly understood. We therefore developed a dynamic, 3D in silico model of the C. elegans germ line, incorporating both the mechanical interactions between cells and the decision-making processes within cells. Our model successfully reproduces key features of the germ line during development and adulthood, including a reasonable ovulation rate, correct sperm count, and appropriate organization of the germ line into stably maintained zones. The model highlights a previously overlooked way in which germ cell pressure may influence gonadogenesis, and also predicts that adult germ cells might be subject to mechanical feedback on the cell cycle akin to contact inhibition. We provide experimental data consistent with the latter hypothesis. Finally, we present cell trajectories and ancestry recorded over the course of a simulation. The novel approaches and software described here link mechanics and cellular decision-making, and are applicable to modeling other developmental and stem cell systems.

A model of stem cell population dynamics: in silico analysis and in vivo validation.

The proper renewal and maintenance of tissues by stem cell populations is simultaneously influenced by anatomical constraints, cell proliferation dynamics and cell fate specification. However, their relative influence is difficult to examine in vivo. To address this difficulty we built, as a test case, a cell-centered state-based computational model of key behaviors that govern germline development in C. elegans, and used it to drive simulations of cell population dynamics under a variety of perturbations. Our analysis provided unexpected possible explanations for laboratory observations, including certain 'all-or-none' phenotypes and complex differentiation patterns. The simulations also offered insights into niche-association dynamics and the interplay between cell cycle and cell fate. Subsequent experiments validated several predictions generated by the simulations. Notably, we found that early cell cycle defects influence later maintenance of the progenitor cell population. This general modeling approach is potentially applicable to other stem cell systems.

Biocharts: a visual formalism for complex biological systems.

We address one of the central issues in devising languages, methods and tools for the modelling and analysis of complex biological systems, that of linking high-level (e.g. intercellular) information with lower-level (e.g. intracellular) information. Adequate ways of dealing with this issue are crucial for understanding biological networks and pathways, which typically contain huge amounts of data that continue to grow as our knowledge and understanding of a system increases. Trying to comprehend such data using the standard methods currently in use is often virtually impossible. We propose a two-tier compound visual language, which we call Biocharts, that is geared towards building fully executable models of biological systems. One of the main goals of our approach is to enable biologists to actively participate in the computational modelling effort, in a natural way. The high-level part of our language is a version of statecharts, which have been shown to be extremely successful in software and systems engineering. The statecharts can be combined with any appropriately well-defined language (preferably a diagrammatic one) for specifying the low-level dynamics of the pathways and networks. We illustrate the language and our general modelling approach using the well-studied process of bacterial chemotaxis.

A scenario-based approach to modeling development: a prototype model of C. elegans vulval fate specification.

Studies of developmental biology are often facilitated by diagram "models" that summarize the current understanding of underlying mechanisms. The increasing complexity of our understanding of development necessitates computational models that can extend these representations to include their dynamic behavior. Here we present a prototype model of Caenorhabditis elegans vulval precursor cell fate specification that represents many processes crucial for this developmental event but that are hard to integrate using other modeling methodologies. We demonstrate the integrative capabilities of our methodology by comprehensively incorporating the contents of three seminal papers, showing that this methodology can lead to comprehensive models of developmental biology. The prototype computational model was built and is run using a language (Live Sequence Charts) and tool (the Play-Engine) that facilitate the same conceptual processes biologists use to construct and probe diagram-type models. We demonstrate that this modeling approach permits rigorous tests of mutual consistency between experimental data and mechanistic hypotheses and can identify specific conflicting results, providing a useful approach to probe developmental systems.