Skip to main page content
U.S. flag

An official website of the United States government

Dot gov

The .gov means it’s official.
Federal government websites often end in .gov or .mil. Before sharing sensitive information, make sure you’re on a federal government site.

Https

The site is secure.
The https:// ensures that you are connecting to the official website and that any information you provide is encrypted and transmitted securely.

Access keys NCBI Homepage MyNCBI Homepage Main Content Main Navigation
. 2017 Jul 3;12(7):e0180179.
doi: 10.1371/journal.pone.0180179. eCollection 2017.

Formal reasoning about systems biology using theorem proving

Adnan Rashid  1 , Osman Hasan  1 , Umair Siddique  2 , Sofiène Tahar  2
Affiliations

Formal reasoning about systems biology using theorem proving

Adnan Rashid et al. PLoS One. .

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.

PubMed Disclaimer

Conflict of interest statement

Competing Interests: The authors have declared that no competing interests exist.

Figures

Fig 1
Fig 1. Proposed framework.
Fig 2
Fig 2. Graphical depiction of formalization of Zsyntax.
(a) Elimination of the Z-Conjunction Rule (zsyn_conjun_elimin) (b) Introduction of Z-Conjunction (zsyn_conjun_intro) (c) Reactants Deletion (zsyn_delet) (d) EVF Matching (zsyn_EVF).
Fig 3
Fig 3. Reaction schemes.
(a) Irreversible Consecutive Reactions (b) Consecutive Reactions with the Second Step being Reversible (c) Consecutive Reactions with the First Step as a Reversible Reaction (d) Consecutive Reactions with a Reversible Step.
Fig 4
Fig 4. Case studies.
(a) Reaction Representing the TP53 Phosphorylation (b) Model for the Tumor Growth [20].
Fig 5
Fig 5. Case studies.
(a) Reaction Representing the death of CSC (b) Another Model for the Growth of Tumor Cell.
See this image and copyright information in PMC

References

    1. Alon U. An Introduction to Systems Biology: Design Principles of Biological Circuits Chapman & Hall/CRC Mathematical and Computational Biology. Taylor & Francis; 2006. Available from: http://books.google.ca/books?id=pAUdPQlCZ54C
    1. Wang E. Cancer Systems Biology. CRC Press; 2010.
    1. Bernot G, Cassez F, Comet JP, Delaplace F, Müller C, Roux O. Semantics of Biological Regulatory Networks. Electronic Notes in Theoretical Computer Science. 2007;180(3):3–14. 10.1016/j.entcs.2004.01.038 - DOI
    1. Langmead CJ. Generalized Queries and Bayesian Statistical Model Checking in Dynamic Bayesian Networks: Application to Personalized Medicine. In: International Conference on Computational Systems Bioinformatics; 2009. p. 201–212.
    1. Hunt NH, Golenser J, Chan-Ling T, Parekh S, Rae C, Potter S, et al. Immunopathogenesis of Cerebral Malaria. International Journal for Parasitology. 2006;36(5):569–582. 10.1016/j.ijpara.2006.02.016 - DOI - PubMed

Substances