Modelling and verification of reconfigurable multi-agent systems.

We propose a formalism to model and reason about reconfigurable multi-agent systems. In our formalism, agents interact and communicate in different modes so that they can pursue joint tasks; agents may dynamically synchronize, exchange data, adapt their behaviour, and reconfigure their communication interfaces. Inspired by existing multi-robot systems, we represent a system as a set of agents (each with local state), executing independently and only influence each other by means of message exchange. Agents are able to sense their local states and partially their surroundings. We extend ltl to be able to reason explicitly about the intentions of agents in the interaction and their communication protocols. We also study the complexity of satisfiability and model-checking of this extension.

Heterogeneity of Myc expression in breast cancer exposes pharmacological vulnerabilities revealed through executable mechanistic modeling.

Cells with higher levels of Myc proliferate more rapidly and supercompetitively eliminate neighboring cells. Nonetheless, tumor cells in aggressive breast cancers typically exhibit significant and stable heterogeneity in their Myc levels, which correlates with refractoriness to therapy and poor prognosis. This suggests that Myc heterogeneity confers some selective advantage on breast tumor growth and progression. To investigate this, we created a traceable MMTV-Wnt1-driven in vivo chimeric mammary tumor model comprising an admixture of low-Myc- and reversibly switchable high-Myc-expressing clones. We show that such tumors exhibit interclonal mutualism wherein cells with high-Myc expression facilitate tumor growth by promoting protumorigenic stroma yet concomitantly suppress Wnt expression, which renders them dependent for survival on paracrine Wnt provided by low-Myc-expressing clones. To identify any therapeutic vulnerabilities arising from such interdependency, we modeled Myc/Ras/p53/Wnt signaling cross talk as an executable network for low-Myc, for high-Myc clones, and for the 2 together. This executable mechanistic model replicated the observed interdependence of high-Myc and low-Myc clones and predicted a pharmacological vulnerability to coinhibition of COX2 and MEK. This was confirmed experimentally. Our study illustrates the power of executable models in elucidating mechanisms driving tumor heterogeneity and offers an innovative strategy for identifying combination therapies tailored to the oligoclonal landscape of heterogenous tumors.

A toolbox for discrete modelling of cell signalling dynamics.

In an age where the volume of data regarding biological systems exceeds our ability to analyse it, many researchers are looking towards systems biology and computational modelling to help unravel the complexities of gene and protein regulatory networks. In particular, the use of discrete modelling allows generation of signalling networks in the absence of full quantitative descriptions of systems, which are necessary for ordinary differential equation (ODE) models. In order to make such techniques more accessible to mainstream researchers, tools such as the BioModelAnalyzer (BMA) have been developed to provide a user-friendly graphical interface for discrete modelling of biological systems. Here we use the BMA to build a library of discrete target functions of known canonical molecular interactions, translated from ordinary differential equations (ODEs). We then show that these BMA target functions can be used to reconstruct complex networks, which can correctly predict many known genetic perturbations. This new library supports the accessibility ethos behind the creation of BMA, providing a toolbox for the construction of complex cell signalling models without the need for extensive experience in computer programming or mathematical modelling, and allows for construction and simulation of complex biological systems with only small amounts of quantitative data.

SCNS: a graphical tool for reconstructing executable regulatory networks from single-cell genomic data.

BACKGROUND: Reconstruction of executable mechanistic models from single-cell gene expression data represents a powerful approach to understanding developmental and disease processes. New ambitious efforts like the Human Cell Atlas will soon lead to an explosion of data with potential for uncovering and understanding the regulatory networks which underlie the behaviour of all human cells. In order to take advantage of this data, however, there is a need for general-purpose, user-friendly and efficient computational tools that can be readily used by biologists who do not have specialist computer science knowledge. RESULTS: The Single Cell Network Synthesis toolkit (SCNS) is a general-purpose computational tool for the reconstruction and analysis of executable models from single-cell gene expression data. Through a graphical user interface, SCNS takes single-cell qPCR or RNA-sequencing data taken across a time course, and searches for logical rules that drive transitions from early cell states towards late cell states. Because the resulting reconstructed models are executable, they can be used to make predictions about the effect of specific gene perturbations on the generation of specific lineages. CONCLUSIONS: SCNS should be of broad interest to the growing number of researchers working in single-cell genomics and will help further facilitate the generation of valuable mechanistic insights into developmental, homeostatic and disease processes.

BTR: training asynchronous Boolean models using single-cell expression data.

BACKGROUND: Rapid technological innovation for the generation of single-cell genomics data presents new challenges and opportunities for bioinformatics analysis. One such area lies in the development of new ways to train gene regulatory networks. The use of single-cell expression profiling technique allows the profiling of the expression states of hundreds of cells, but these expression states are typically noisier due to the presence of technical artefacts such as drop-outs. While many algorithms exist to infer a gene regulatory network, very few of them are able to harness the extra expression states present in single-cell expression data without getting adversely affected by the substantial technical noise present. RESULTS: Here we introduce BTR, an algorithm for training asynchronous Boolean models with single-cell expression data using a novel Boolean state space scoring function. BTR is capable of refining existing Boolean models and reconstructing new Boolean models by improving the match between model prediction and expression data. We demonstrate that the Boolean scoring function performed favourably against the BIC scoring function for Bayesian networks. In addition, we show that BTR outperforms many other network inference algorithms in both bulk and single-cell synthetic expression data. Lastly, we introduce two case studies, in which we use BTR to improve published Boolean models in order to generate potentially new biological insights. CONCLUSIONS: BTR provides a novel way to refine or reconstruct Boolean models using single-cell expression data. Boolean model is particularly useful for network reconstruction using single-cell data because it is more robust to the effect of drop-outs. In addition, BTR does not assume any relationship in the expression states among cells, it is useful for reconstructing a gene regulatory network with as few assumptions as possible. Given the simplicity of Boolean models and the rapid adoption of single-cell genomics by biologists, BTR has the potential to make an impact across many fields of biomedical research.

Emergent stem cell homeostasis in the C. elegans germline is revealed by hybrid modeling.

The establishment of homeostasis among cell growth, differentiation, and apoptosis is of key importance for organogenesis. Stem cells respond to temporally and spatially regulated signals by switching from mitotic proliferation to asymmetric cell division and differentiation. Executable computer models of signaling pathways can accurately reproduce a wide range of biological phenomena by reducing detailed chemical kinetics to a discrete, finite form. Moreover, coordinated cell movements and physical cell-cell interactions are required for the formation of three-dimensional structures that are the building blocks of organs. To capture all these aspects, we have developed a hybrid executable/physical model describing stem cell proliferation, differentiation, and homeostasis in the Caenorhabditis elegans germline. Using this hybrid model, we are able to track cell lineages and dynamic cell movements during germ cell differentiation. We further show how apoptosis regulates germ cell homeostasis in the gonad, and propose a role for intercellular pressure in developmental control. Finally, we use the model to demonstrate how an executable model can be developed from the hybrid system, identifying a mechanism that ensures invariance in fate patterns in the presence of instability.

Drug target optimization in chronic myeloid leukemia using innovative computational platform.

Chronic Myeloid Leukemia (CML) represents a paradigm for the wider cancer field. Despite the fact that tyrosine kinase inhibitors have established targeted molecular therapy in CML, patients often face the risk of developing drug resistance, caused by mutations and/or activation of alternative cellular pathways. To optimize drug development, one needs to systematically test all possible combinations of drug targets within the genetic network that regulates the disease. The BioModelAnalyzer (BMA) is a user-friendly computational tool that allows us to do exactly that. We used BMA to build a CML network-model composed of 54 nodes linked by 104 interactions that encapsulates experimental data collected from 160 publications. While previous studies were limited by their focus on a single pathway or cellular process, our executable model allowed us to probe dynamic interactions between multiple pathways and cellular outcomes, suggest new combinatorial therapeutic targets, and highlight previously unexplored sensitivities to Interleukin-3.

Decoding the regulatory network of early blood development from single-cell gene expression measurements.

Reconstruction of the molecular pathways controlling organ development has been hampered by a lack of methods to resolve embryonic progenitor cells. Here we describe a strategy to address this problem that combines gene expression profiling of large numbers of single cells with data analysis based on diffusion maps for dimensionality reduction and network synthesis from state transition graphs. Applying the approach to hematopoietic development in the mouse embryo, we map the progression of mesoderm toward blood using single-cell gene expression analysis of 3,934 cells with blood-forming potential captured at four time points between E7.0 and E8.5. Transitions between individual cellular states are then used as input to develop a single-cell network synthesis toolkit to generate a computationally executable transcriptional regulatory network model of blood development. Several model predictions concerning the roles of Sox and Hox factors are validated experimentally. Our results demonstrate that single-cell analysis of a developing organ coupled with computational approaches can reveal the transcriptional programs that underpin organogenesis.

Toward synthesizing executable models in biology.

Over the last decade, executable models of biological behaviors have repeatedly provided new scientific discoveries, uncovered novel insights, and directed new experimental avenues. These models are computer programs whose execution mechanistically simulates aspects of the cell's behaviors. If the observed behavior of the program agrees with the observed biological behavior, then the program explains the phenomena. This approach has proven beneficial for gaining new biological insights and directing new experimental avenues. One advantage of this approach is that techniques for analysis of computer programs can be applied to the analysis of executable models. For example, one can confirm that a model agrees with experiments for all possible executions of the model (corresponding to all environmental conditions), even if there are a huge number of executions. Various formal methods have been adapted for this context, for example, model checking or symbolic analysis of state spaces. To avoid manual construction of executable models, one can apply synthesis, a method to produce programs automatically from high-level specifications. In the context of biological modeling, synthesis would correspond to extracting executable models from experimental data. We survey recent results about the usage of the techniques underlying synthesis of computer programs for the inference of biological models from experimental data. We describe synthesis of biological models from curated mutation experiment data, inferring network connectivity models from phosphoproteomic data, and synthesis of Boolean networks from gene expression data. While much work has been done on automated analysis of similar datasets using machine learning and artificial intelligence, using synthesis techniques provides new opportunities such as efficient computation of disambiguating experiments, as well as the ability to produce different kinds of models automatically from biological data.

Cell-cycle regulation of NOTCH signaling during C. elegans vulval development.

C. elegans vulval development is one of the best-characterized systems to study cell fate specification during organogenesis. The detailed knowledge of the signaling pathways determining vulval precursor cell (VPC) fates permitted us to create a computational model based on the antagonistic interactions between the epidermal growth factor receptor (EGFR)/RAS/MAPK and the NOTCH pathways that specify the primary and secondary fates, respectively. A key notion of our model is called bounded asynchrony, which predicts that a limited degree of asynchrony in the progression of the VPCs is necessary to break their equivalence. While searching for a molecular mechanism underlying bounded asynchrony, we discovered that the termination of NOTCH signaling is tightly linked to cell-cycle progression. When single VPCs were arrested in the G1 phase, intracellular NOTCH failed to be degraded, resulting in a mixed primary/secondary cell fate. Moreover, the G1 cyclins CYD-1 and CYE-1 stabilize NOTCH, while the G2 cyclin CYB-3 promotes NOTCH degradation. Our findings reveal a synchronization mechanism that coordinates NOTCH signaling with cell-cycle progression and thus permits the formation of a stable cell fate pattern.

A dynamic physical model of cell migration, differentiation and apoptosis in Caenorhabditis elegans.

The germ line of the nematode C. elegans provides a paradigm to study essential developmental concepts like stem cell differentiation and apoptosis. Here, we have created a computational model encompassing these developmental landmarks and the resulting movement of germ cells along the gonadal tube. We have used a technique based on molecular dynamics (MD) to model the physical movement of cells solely based on the force that arises from dividing cells. This novel way of using MD to drive the model enables calibration of simulation and experimental time. Based on this calibration, the analysis of our model shows that it is in accordance with experimental observations. In addition, the model provides insights into kinetics of molecular pathways within individual cells as well as into physical aspects like the cell density along the germ line and in local neighbourhoods of individual germ cells. In the future, the presented model can be used to test hypotheses about diverse aspects of development like stem cell division or programmed cell death. An iterative process of evolving this model and experimental testing in the model system C. elegans will provide new insights into key developmental aspects.

The executable pathway to biological networks.

As time goes by, it becomes more and more apparent that the puzzles of life involve more and more molecular pieces that fit together in increasingly complex ways. Genomics and Proteomics technologies nowadays, produce reliable and quantitative data that could potentially reveal all the molecular pieces of a particular puzzle. However, this is akin to the opening of Pandora's box; and we are now facing the problem of integrating this vast amount of data with its incredible complexity into some coherent whole. With the aid of engineering methods designed to build and analyze computerized man-made systems, a new emerging field called 'Executable Biology' aims to create computer programmes that put together the pieces in ways that allows capturing their dynamicity and ultimately elucidating how molecular function generates cellular function. This review aspires to highlight the main features characterizing these kinds of executable models and what makes them uniquely qualified to reason about and analyze biological networks.

Computational modeling of the EGFR network elucidates control mechanisms regulating signal dynamics.

BACKGROUND: The epidermal growth factor receptor (EGFR) signaling pathway plays a key role in regulation of cellular growth and development. While highly studied, it is still not fully understood how the signal is orchestrated. One of the reasons for the complexity of this pathway is the extensive network of inter-connected components involved in the signaling. In the aim of identifying critical mechanisms controlling signal transduction we have performed extensive analysis of an executable model of the EGFR pathway using the stochastic pi-calculus as a modeling language. RESULTS: Our analysis, done through simulation of various perturbations, suggests that the EGFR pathway contains regions of functional redundancy in the upstream parts; in the event of low EGF stimulus or partial system failure, this redundancy helps to maintain functional robustness. Downstream parts, like the parts controlling Ras and ERK, have fewer redundancies, and more than 50% inhibition of specific reactions in those parts greatly attenuates signal response. In addition, we suggest an abstract model that captures the main control mechanisms in the pathway. Simulation of this abstract model suggests that without redundancies in the upstream modules, signal transduction through the entire pathway could be attenuated. In terms of specific control mechanisms, we have identified positive feedback loops whose role is to prolong the active state of key components (e.g., MEK-PP, Ras-GTP), and negative feedback loops that help promote signal adaptation and stabilization. CONCLUSIONS: The insights gained from simulating this executable model facilitate the formulation of specific hypotheses regarding the control mechanisms of the EGFR signaling, and further substantiate the benefit to construct abstract executable models of large complex biological networks.

Predictive modeling of signaling crosstalk during C. elegans vulval development.

Caenorhabditis elegans vulval development provides an important paradigm for studying the process of cell fate determination and pattern formation during animal development. Although many genes controlling vulval cell fate specification have been identified, how they orchestrate themselves to generate a robust and invariant pattern of cell fates is not yet completely understood. Here, we have developed a dynamic computational model incorporating the current mechanistic understanding of gene interactions during this patterning process. A key feature of our model is the inclusion of multiple modes of crosstalk between the epidermal growth factor receptor (EGFR) and LIN-12/Notch signaling pathways, which together determine the fates of the six vulval precursor cells (VPCs). Computational analysis, using the model-checking technique, provides new biological insights into the regulatory network governing VPC fate specification and predicts novel negative feedback loops. In addition, our analysis shows that most mutations affecting vulval development lead to stable fate patterns in spite of variations in synchronicity between VPCs. Computational searches for the basis of this robustness show that a sequential activation of the EGFR-mediated inductive signaling and LIN-12 / Notch-mediated lateral signaling pathways is key to achieve a stable cell fate pattern. We demonstrate experimentally a time-delay between the activation of the inductive and lateral signaling pathways in wild-type animals and the loss of sequential signaling in mutants showing unstable fate patterns; thus, validating two key predictions provided by our modeling work. The insights gained by our modeling study further substantiate the usefulness of executing and analyzing mechanistic models to investigate complex biological behaviors.

Computational insights into Caenorhabditis elegans vulval development.

Studies of Caenorhabditis elegans vulval development provide a paradigm for pattern formation during animal development. The fates of the six vulval precursor cells are specified by the combined action of an inductive signal that activates the EGF receptor mitogen-activated PK signaling pathway (specifying a primary fate) and a lateral signal mediated by LIN-12/Notch (specifying a secondary fate). Here we use methods devised for the engineering of complex reactive systems to model a biological system. We have chosen the visual formalism of statecharts and use it to formalize Sternberg and Horvitz's 1989 model [Sternberg, P. W. & Horvitz, H. R. (1989) Cell 58, 679-693], which forms the basis for our current understanding of the interaction between these two signaling pathways. The construction and execution of our model suggest that different levels of the inductive signal induce a temporally graded response of the EGF receptor mitogen-activated PK pathway and make explicit the importance of this temporal response. Our model also suggests the existence of an additional mechanism operating during lateral specification that prohibits neighboring vulval precursor cells from assuming the primary fate.