Dataset Information

Formal reasoning about systems biology using theorem proving.

ABSTRACT: System biology provides the basis to understand the behavioral properties of complex biological organisms at different levels of abstraction. Traditionally, analysing systems biology based models of various diseases have been carried out by paper-and-pencil based proofs and simulations. However, these methods cannot provide an accurate analysis, which is a serious drawback for the safety-critical domain of human medicine. In order to overcome these limitations, we propose a framework to formally analyze biological networks and pathways. In particular, we formalize the notion of reaction kinetics in higher-order logic and formally verify some of the commonly used reaction based models of biological networks using the HOL Light theorem prover. Furthermore, we have ported our earlier formalization of Zsyntax, i.e., a deductive language for reasoning about biological networks and pathways, from HOL4 to the HOL Light theorem prover to make it compatible with the above-mentioned formalization of reaction kinetics. To illustrate the usefulness of the proposed framework, we present the formal analysis of three case studies, i.e., the pathway leading to TP53 Phosphorylation, the pathway leading to the death of cancer stem cells and the tumor growth based on cancer stem cells, which is used for the prognosis and future drug designs to treat cancer patients.

SUBMITTER: Rashid A

PROVIDER: S-EPMC5495343 | biostudies-literature | 2017

REPOSITORIES: biostudies-literature

ACCESS DATA

Publications

Formal reasoning about systems biology using theorem proving.

Rashid Adnan A Hasan Osman O Siddique Umair U Tahar Sofiène S

PloS one 20170703 7

System biology provides the basis to understand the behavioral properties of complex biological organisms at different levels of abstraction. Traditionally, analysing systems biology based models of various diseases have been carried out by paper-and-pencil based proofs and simulations. However, these methods cannot provide an accurate analysis, which is a serious drawback for the safety-critical domain of human medicine. In order to overcome these limitations, we propose a framework to formally ...[more]

PMID: 28671950

Similar Datasets

Project description:Dendritic cells (DCs) capture pathogens and foreign antigen (Ag) in peripheral tissues and migrate to secondary lymphoid tissues, such as lymph nodes (LNs), where they present processed Ag as MHC-bound peptide (pMHC) to naïve T cells. Interactions between DCs and T cells result, over periods of hours, in activation, clonal expansion and differentiation of antigen-specific T cells, leading to primed cells that can now participate in immune responses. Two-photon microscopy (2PM) has been widely adopted to analyze lymphocyte dynamics and can serve as a powerful in vivo assay for cell trafficking and activation over short length and time scales. Linking biological phenomena between vastly different spatiotemporal scales can be achieved using a systems biology approach. We developed a 3D agent-based cellular model of a LN that allows for the simultaneous in silico simulation of T cell trafficking, activation and production of effector cells under different antigen (Ag) conditions. The model anatomy is based on in situ analysis of LN sections (from primates and mice) and cell dynamics based on quantitative measurements from 2PM imaging of mice. Our simulations make three important predictions. First, T cell encounters by DCs and T cell receptor (TCR) repertoire scanning are more efficient in a 3D model compared with 2D, suggesting that a 3D model is needed to analyze LN function. Second, LNs are able to produce primed CD4+T cells at the same efficiency over broad ranges of cognate frequencies (from 10(-5) to 10(-2)). Third, reducing the time that naïve T cells are required to bind DCs before becoming activated will increase the rate at which effector cells are produced. This 3D model provides a robust platform to study how T cell trafficking and activation dynamics relate to the efficiency of T cell priming and clonal expansion. We envision that this systems biology approach will provide novel insights for guiding vaccine development and understanding immune responses to infection.

Dataset Information

Formal reasoning about systems biology using theorem proving.

Publications

Formal reasoning about systems biology using theorem proving.

Similar Datasets

OmicsDI is part of the ELIXIR infrastructure

Tweets