Date Published: July 3, 2017
Publisher: Public Library of Science
Author(s): Adnan Rashid, Osman Hasan, Umair Siddique, Sofiène Tahar, Andrew Adamatzky.
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.
The discovery and design of effective drugs for infectious and chronic biological diseases, like cancer and cerebral malaria, require a deep understanding of behaviorial and structural characteristics of underlying biological entities (e.g., cells, molecules and enzymes). Traditional approaches, which rely on verbal and personal intuitions without concrete logical explanations of biological phenomena, often fail to provide a complete understanding of the behavior of such diseases, mainly due to the complex interactions of molecules connected through a chain of reactions. Systems biology  overcomes these limitations by integrating mathematical modeling and high-speed computing machines in the understanding of biological processes and thus provides the ability to predict the effect of potential drugs for the treatment of chronic diseases. System biology is widely used to model the biological processes as pathways or networks. Some of the examples are signaling pathways and protein-protein interaction networks . These biological networks such as gene regulatory networks (GRNs) or biological regulatory networks (BRNs) , are analysed using the principles of molecular biology. This analysis, in turn, plays an important role for the investigation of the treatment of various human infectious diseases as well as future drug design targets. For example, the BRNs analysis has been recently used for the prediction of treatment decisions for sepsis patients .
In the last few decades, various modeling formalisms of computer science have been widely used in system biology. We briefly outline here the applications of computational modeling and analysis approaches in system biology, where the main idea is to transform a biological model into a computer program.
In this section, we provide a brief introduction to the higher-order-logic theorem proving and HOL Light theorem prover.
The proposed theorem proving based formal reasoning framework for system biology, depicted in Fig 1, allows the formal deduction of the complete pathway from any given time instance and model and analyze the ordinary differential equations (ODEs) corresponding to a kinetic model for any molecular reaction. For this purpose, the framework builds upon existing higher-order-logic formalizations of Lists, Pairs, Vectors, and Calculus.
Most of the existing research related to the formal analysis of the biological systems has been focussed on using model checking. However, this technique suffers from the inherent state-space explosion problem, which limits the scope of this success to systems where the biological entities can acquire only a small set of possible levels. Moreover, the underlying differential equations describing the reaction kinetics are solved using numerical approaches , which compromises the precision of the analysis. To the best of our knowledge, our work is the first one to leverage the distinguishing features of interactive theorem proving to reason about the solutions to system biology problems. We consider the concentration of the species of the biological systems in reaction kinetic based formal analysis as a continuous variable. Besides formalizing Zsyntax and the reaction kinetics of commonly used biological pathways, we also formally verified their classical properties. This verification guarantees the soundness and the correctness of our formal definitions. It also enables us to conduct formal analysis of real-world case studies. In order to illustrate the practical effectiveness of our formalization, we presented the automatic Zsyntax based formal analysis of pathway leading to TP53 Phosphorylation and a pathway leading to the death of CSCs in the tumor growth model, and reaction kinetics based analysis of the tumor growth model. Our source code is available online  and can be used by other biologists and computer scientists for further applications and experimentation.