Statistical Model Checking in BioLab: Applications to the Automated Analysis of T-Cell Receptor Signaling Pathway

Verifiable biology

The formalization of biological systems using computational modelling approaches as an alternative to mathematical-based methods has recently received much interest because computational models provide a deeper mechanistic understanding of biological systems. In particular, formal verification, complementary approach to standard computational techniques such as simulation, is used to validate the system correctness and obtain critical information about system behaviour. In this study, we survey the most frequently used computational modelling approaches and formal verification techniques for computational biology. We compare a number of verification tools and software suites used to analyse biological systems and biochemical networks, and to verify a wide range of biological properties. For users who have no expertise in formal verification, we present a novel methodology that allows them to easily apply formal verification techniques to analyse their biological or biochemical system of interest.

Smart computational exploration of stochastic gene regulatory network models using human-in-the-loop semi-supervised learning

MOTIVATION

Discrete stochastic models of gene regulatory network models are indispensable tools for biological inquiry since they allow the modeler to predict how molecular interactions give rise to nonlinear system output. Model exploration with the objective of generating qualitative hypotheses about the workings of a pathway is usually the first step in the modeling process. It involves simulating the gene network model under a very large range of conditions, due to the large uncertainty in interactions and kinetic parameters. This makes model exploration highly computational demanding. Furthermore, with no prior information about the model behavior, labor-intensive manual inspection of very large amounts of simulation results becomes necessary. This limits systematic computational exploration to simplistic models.

RESULTS

We have developed an interactive, smart workflow for model exploration based on semi-supervised learning and human-in-the-loop labeling of data. The workflow lets a modeler rapidly discover ranges of interesting behaviors predicted by the model. Utilizing that similar simulation output is in proximity of each other in a feature space, the modeler can focus on informing the system about what behaviors are more interesting than others by labeling, rather than analyzing simulation results with custom scripts and workflows. This results in a large reduction in time-consuming manual work by the modeler early in a modeling project, which can substantially reduce the time needed to go from an initial model to testable predictions and downstream analysis.

AVAILABILITY AND IMPLEMENTATION

A python-package is available at https://github.com/Wrede/mio.git.

SUPPLEMENTARY INFORMATION

Supplementary data are available at Bioinformatics online.

Multi-Level Modeling and Simulation of Cellular Systems: An Introduction to ML-Rules

ML-Rules is a rule-based language for multi-level modeling and simulation. ML-Rules supports dynamic nesting of entities and applying arbitrary functions on entity attributes and content, as well as for defining kinetics of reactions. This allows describing and simulating complex cellular dynamics operating at different organizational levels, e.g., to combine intra-, inter-, and cellular dynamics, like the proliferation of cells, or to include compartmental dynamics like merging and splitting of mitochondria or endocytosis. The expressiveness of the language is bought with additional efforts in executing ML-Rules models. Therefore, various simulators have been developed from which the user and automatic procedures can select. The experiment specification language SESSL facilitates design, execution, and reuse of simulation experiments. The chapter illuminates the specific features of ML-Rules as a rule-based modeling language, the implications for an efficient execution, and shows ML-Rules at work.

Computational Modeling, Formal Analysis, and Tools for Systems Biology

As the amount of biological data in the public domain grows, so does the range of modeling and analysis techniques employed in systems biology. In recent years, a number of theoretical computer science developments have enabled modeling methodology to keep pace. The growing interest in systems biology in executable models and their analysis has necessitated the borrowing of terms and methods from computer science, such as formal analysis, model checking, static analysis, and runtime verification. Here, we discuss the most important and exciting computational methods and tools currently available to systems biologists. We believe that a deeper understanding of the concepts and theory highlighted in this review will produce better software practice, improved investigation of complex biological processes, and even new ideas and better feedback into computer science.

Modeling biomolecular site dynamics in immunoreceptor signaling systems

The immune system plays a central role in human health. The activities of immune cells, whether defending an organism from disease or triggering a pathological condition such as autoimmunity, are driven by the molecular machinery of cellular signaling systems. Decades of experimentation have elucidated many of the biomolecules and interactions involved in immune signaling and regulation, and recently developed technologies have led to new types of quantitative, systems-level data. To integrate such information and develop nontrivial insights into the immune system, computational modeling is needed, and it is essential for modeling methods to keep pace with experimental advances. In this chapter, we focus on the dynamic, site-specific, and context-dependent nature of interactions in immunoreceptor signaling (i.e., the biomolecular site dynamics of immunoreceptor signaling), the challenges associated with capturing these details in computational models, and how these challenges have been met through use of rule-based modeling approaches.

A Property-Driven Methodology for Formal Analysis of Synthetic Biology Systems

This paper proposes a formal methodology to analyse bio-systems, in particular synthetic biology systems. An integrative analysis perspective combining different model checking approaches based on different property categories is provided. The methodology is applied to the synthetic pulse generator system and several verification experiments are carried out to demonstrate the use of our approach to formally analyse various aspects of synthetic biology systems.

Qualitative and quantitative analysis of systems and synthetic biology constructs using P systems

Computational models are perceived as an attractive alternative to mathematical models (e.g., ordinary differential equations). These models incorporate a set of methods for specifying, modeling, testing, and simulating biological systems. In addition, they can be analyzed using algorithmic techniques (e.g., formal verification). This paper shows how formal verification is utilized in systems and synthetic biology through qualitative vs quantitative analysis. Here, we choose two well-known case studies: quorum sensing in P. aeruginosas and pulse generator. The paper reports verification analysis of two systems carried out using some model checking tools, integrated to the Infobiotics Workbench platform, where system models are based on stochastic P systems.

Systems biology of cancer: a challenging expedition for clinical and quantitative biologists

A systems-biology approach to complex disease (such as cancer) is now complementing traditional experience-based approaches, which have typically been invasive and expensive. The rapid progress in biomedical knowledge is enabling the targeting of disease with therapies that are precise, proactive, preventive, and personalized. In this paper, we summarize and classify models of systems biology and model checking tools, which have been used to great success in computational biology and related fields. We demonstrate how these models and tools have been used to study some of the twelve biochemical pathways implicated in but not unique to pancreatic cancer, and conclude that the resulting mechanistic models will need to be further enhanced by various abstraction techniques to interpret phenomenological models of cancer progression.

An integrative modeling framework reveals plasticity of TGF-β signaling

Background

The TGF-β transforming growth factor is the most pleiotropic cytokine controlling a broad range of cellular responses that include proliferation, differentiation and apoptosis. The context-dependent multifunctional nature of TGF-β is associated with complex signaling pathways. Differential models describe the dynamics of the TGF-β canonical pathway, but modeling the non-canonical networks constitutes a major challenge. Here, we propose a qualitative approach to explore all TGF-β-dependent signaling pathways.

Results

Using a new formalism, CADBIOM, which is based on guarded transitions and includes temporal parameters, we have built the first discrete model of TGF-β signaling networks by automatically integrating the 137 human signaling maps from the Pathway Interaction Database into a single unified dynamic model. Temporal property-checking analyses of 15934 trajectories that regulate 145 TGF-β target genes reveal the association of specific pathways with distinct biological processes. We identify 31 different combinations of TGF-β with other extracellular stimuli involved in non-canonical TGF-β pathways that regulate specific gene networks. Extensive analysis of gene expression data further demonstrates that genes sharing CADBIOM trajectories tend to be co-regulated.

Conclusions

As applied here to TGF-β signaling, CADBIOM allows, for the first time, a full integration of highly complex signaling pathways into dynamic models that permit to explore cell responses to complex microenvironment stimuli.

Probabilistic model checking analysis of palytoxin effects on cell energy reactions of the Na+/K+-ATPase

Probabilistic model checking (PMC) is a technique used for the specification and analysis of complex systems. It can be applied directly to biological systems which present these characteristics, including cell transport systems. These systems are structures responsible for exchanging ions through the plasma membrane. Their correct behavior is essential for animal cells, since changes on those are responsible for diseases. In this work, PMC is used to model and analyze the effects of the palytoxin toxin (PTX) interactions with one of these systems. Our model suggests that ATP could inhibit PTX action. Therefore, individuals with ATP deficiencies, such as in brain disorders, may be more susceptible to the toxin. We have also used heat maps to enhance the kinetic model, which is used to describe the system reactions. The map reveals unexpected situations, such as a frequent reaction between unlikely pump states, and hot spots such as likely states and reactions. This type of analysis provides a better understanding on how transmembrane ionic transport systems behave and may lead to the discovery and development of new drugs to treat diseases associated to their incorrect behavior.

Efficient stochastic simulation of chemical kinetics networks using a weighted ensemble of trajectories

We apply the "weighted ensemble" (WE) simulation strategy, previously employed in the context of molecular dynamics simulations, to a series of systems-biology models that range in complexity from a one-dimensional system to a system with 354 species and 3680 reactions. WE is relatively easy to implement, does not require extensive hand-tuning of parameters, does not depend on the details of the simulation algorithm, and can facilitate the simulation of extremely rare events. For the coupled stochastic reaction systems we study, WE is able to produce accurate and efficient approximations of the joint probability distribution for all chemical species for all time t. WE is also able to efficiently extract mean first passage times for the systems, via the construction of a steady-state condition with feedback. In all cases studied here, WE results agree with independent "brute-force" calculations, but significantly enhance the precision with which rare or slow processes can be characterized. Speedups over "brute-force" in sampling rare events via the Gillespie direct Stochastic Simulation Algorithm range from ~10(12) to ~10(18) for characterizing rare states in a distribution, and ~10(2) to ~10(4) for finding mean first passage times.

Improved statistical model checking methods for pathway analysis

Statistical model checking techniques have been shown to be effective for approximate model checking on large stochastic systems, where explicit representation of the state space is impractical. Importantly, these techniques ensure the validity of results with statistical guarantees on errors. There is an increasing interest in these classes of algorithms in computational systems biology since analysis using traditional model checking techniques does not scale well. In this context, we present two improvements to existing statistical model checking algorithms. Firstly, we construct an algorithm which removes the need of the user to define the indifference region, a critical parameter in previous sequential hypothesis testing algorithms. Secondly, we extend the algorithm to account for the case when there may be a limit on the computational resources that can be spent on verifying a property; i.e, if the original algorithm is not able to make a decision even after consuming the available amount of resources, we resort to a p-value based approach to make a decision. We demonstrate the improvements achieved by our algorithms in comparison to current algorithms first with a straightforward yet representative example, followed by a real biological model on cell fate of gustatory neurons with microRNAs.

A computational model for early events in B cell antigen receptor signaling: analysis of the roles of Lyn and Fyn

BCR signaling regulates the activities and fates of B cells. BCR signaling encompasses two feedback loops emanating from Lyn and Fyn, which are Src family protein tyrosine kinases (SFKs). Positive feedback arises from SFK-mediated trans phosphorylation of BCR and receptor-bound Lyn and Fyn, which increases the kinase activities of Lyn and Fyn. Negative feedback arises from SFK-mediated cis phosphorylation of the transmembrane adapter protein PAG1, which recruits the cytosolic protein tyrosine kinase Csk to the plasma membrane, where it acts to decrease the kinase activities of Lyn and Fyn. To study the effects of the positive and negative feedback loops on the dynamical stability of BCR signaling and the relative contributions of Lyn and Fyn to BCR signaling, we consider in this study a rule-based model for early events in BCR signaling that encompasses membrane-proximal interactions of six proteins, as follows: BCR, Lyn, Fyn, Csk, PAG1, and Syk, a cytosolic protein tyrosine kinase that is activated as a result of SFK-mediated phosphorylation of BCR. The model is consistent with known effects of Lyn and Fyn deletions. We find that BCR signaling can generate a single pulse or oscillations of Syk activation depending on the strength of Ag signal and the relative levels of Lyn and Fyn. We also show that bistability can arise in Lyn- or Csk-deficient cells.

Workflow for generating competing hypothesis from models with parameter uncertainty

Mathematical models are increasingly used in life sciences. However, contrary to other disciplines, biological models are typically over-parametrized and loosely constrained by scarce experimental data and prior knowledge. Recent efforts on analysis of complex models have focused on isolated aspects without considering an integrated approach-ranging from model building to derivation of predictive experiments and refutation or validation of robust model behaviours. Here, we develop such an integrative workflow, a sequence of actions expanding upon current efforts with the purpose of setting the stage for a methodology facilitating an extraction of core behaviours and competing mechanistic hypothesis residing within underdetermined models. To this end, we make use of optimization search algorithms, statistical (machine-learning) classification techniques and cluster-based analysis of the state variables' dynamics and their corresponding parameter sets. We apply the workflow to a mathematical model of fat accumulation in the arterial wall (atherogenesis), a complex phenomena with limited quantitative understanding, thus leading to a model plagued with inherent uncertainty. We find that the mathematical atherogenesis model can still be understood in terms of a few key behaviours despite the large number of parameters. This result enabled us to derive distinct mechanistic predictions from the model despite the lack of confidence in the model parameters. We conclude that building integrative workflows enable investigators to embrace modelling of complex biological processes despite uncertainty in parameters.