Formal reasoning about systems biology using theorem proving.

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.

Formal modeling and analysis of the MAL-associated biological regulatory network: insight into cerebral malaria.

The discrete modeling formalism of René Thomas is a well known approach for the modeling and analysis of Biological Regulatory Networks (BRNs). This formalism uses a set of parameters which reflect the dynamics of the BRN under study. These parameters are initially unknown but may be deduced from the appropriately chosen observed dynamics of a BRN. The discrete model can be further enriched by using the model checking tool HyTech along with delay parameters. This paves the way to accurately analyse a BRN and to make predictions about critical trajectories which lead to a normal or diseased response. In this paper, we apply the formal discrete and hybrid (discrete and continuous) modeling approaches to characterize behavior of the BRN associated with MyD88-adapter-like (MAL)--a key protein involved with innate immune response to infections. In order to demonstrate the practical effectiveness of our current work, different trajectories and corresponding conditions that may lead to the development of cerebral malaria (CM) are identified. Our results suggest that the system converges towards hyperinflammation if Bruton's tyrosine kinase (BTK) remains constitutively active along with pre-existing high cytokine levels which may play an important role in CM pathogenesis.