Modeling and Analysis of HIF-1 Pathway Using Formal Verification Techniques

Abstract

Mammalian cells must maintain adequate oxygen homeostasis for their aerobic metabolism

and Adenosine triphosphate (ATP) production. In cancer progression, the body devel- ops malignant tumors that lead to an oxygen deficiency known as hypoxia. Hypoxic

condition is usual in multiple types of solid tumors that utilize glucose to produce ATP, in which cancer cells quickly proliferate and form enormous solid tumors that cause blockage and condensing of the blood vessels adjacent to the tumor masses. These types of blood vessels frequently malfunction and cause a poor oxygen supply to the central tumor region. The cancerous cells in these hypoxic regions look to adapt to the low-level oxygen tension states by triggering various ongoing pathways, including

PI3k, AKT, and MAPK. The transcription of the HIF-1 pathway leads to oxygen ten- sion within cells and their hostile microenvironment. As a result, HIF-1 increases the

expression of Glut-1, enhancing glucose consumption and hyperactivating metabolic pathways. Under these conditions, the expression of AKT decreases but the adjacent proteins OGT and VEGF expression increases. However, the collective behavior of Glut-1 along with AKT, OGT, and VEGF is not fully characterized and lacks clarity of how glucose uptake through this pathway (HIF-1) during cancer progression. In order to comprehend the signaling dynamics of HIF-1 and its interlinked proteins, which includes VEGF, ERK, AKT, Glut-1, β-catenin, C-myc, OGT, and p53, this

study uses a qualitative modeling framework to build HIF-1 associated Biological Reg- ulatory Network (BRN) and its dynamic models to look into cancer progression and its

impact on various entities. The dynamic model we have developed reveals continuous

activation of p53, β-catenin, and AKT in cyclic conditions, leading to oscillations rep- vi

resenting homeostasis or a stable, steady state. Any deviation from this cycle results in a cancerous or pathogenic state. We take into account the most critical trajectories; in the first trajectory, the high expression of Glut-1 and OGT leads the pathway toward

a deadlock state. While in the second trajectory, high expression of ERK and Glut- 1 leads toward a pathogenic state, and the system never returns to a normal state.

The model shows that overexpression of VEGF activates ERK and Glut-1, however, it should be retained at a low expression level along with HIF-1. Moreover, it is observed that collective inhibition of VEGF, ERK, and β-catenin is required for therapeutic

intervention because these genes enhance the expression of Glut-1 and play a signifi- cant role in cancer progression, angiogenesis, and cell proliferation. In conclusion, our

observations characterized the homeostasis in the biological system transitions from a dynamic to a cyclic state, and found that critical genes such as p53, β-catenin, and AKT are more viable targets for the stable homeostatic state reactions to take control.