Automated Formal Reasoning to Uncover Molecular Programs of Self-Renewal

OneSC: A computational platform for recapitulating cell state transitions

Computational modelling of cell state transitions has been a great interest of many in the field of developmental biology, cancer biology and cell fate engineering because it enables performing perturbation experiments in silico more rapidly and cheaply than could be achieved in a wet lab. Recent advancements in single-cell RNA sequencing (scRNA-seq) allow the capture of high-resolution snapshots of cell states as they transition along temporal trajectories. Using these high-throughput datasets, we can train computational models to generate in silico 'synthetic' cells that faithfully mimic the temporal trajectories. Here we present OneSC, a platform that can simulate synthetic cells across developmental trajectories using systems of stochastic differential equations govern by a core transcription factors (TFs) regulatory network. Different from the current network inference methods, OneSC prioritizes on generating Boolean network that produces faithful cell state transitions and steady cell states that mimic real biological systems. Applying OneSC to real data, we inferred a core TF network using a mouse myeloid progenitor scRNA-seq dataset and showed that the dynamical simulations of that network generate synthetic single-cell expression profiles that faithfully recapitulate the four myeloid differentiation trajectories going into differentiated cell states (erythrocytes, megakaryocytes, granulocytes and monocytes). Finally, through the in-silico perturbations of the mouse myeloid progenitor core network, we showed that OneSC can accurately predict cell fate decision biases of TF perturbations that closely match with previous experimental observations.

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.