Computational Modeling and Verification of Signaling Pathways in Cancer

We propose and analyze a rule-based model of the HMGB1 signaling pathway. The protein HMGB1 can activate a number of regulatory networks – the p53, NF

κ

B, Ras and Rb pathways – that control many physiological processes of the cell. HMGB1 has been recently shown to be implicated in cancer, inflammation and other diseases. In this paper, we focus on the NF

κ

B pathway and construct a crosstalk model of the HMGB1-p53-NF

κ

B-Ras-Rb network to investigate how these couplings influence proliferation and apoptosis (programmed cell death) of cancer cells. We first built a single-cell model of the HMGB1 network using the rule-based BioNetGen language. Then, we analyzed and verified qualitative properties of the model by means of simulation and statistical model checking. For model simulation, we used both ordinary differential equations and Gillespie’s stochastic simulation algorithm. Statistical model checking enabled us to verify our model with respect to behavioral properties expressed in temporal logic. Our analysis showed that HMGB1-activated receptors can generate sustained oscillations of irregular amplitude for the NF

κ

B, I

κ

B, A20 and p53 proteins. Also, knockout of A20 can destroy the I

κ

B-NF

κ

B negative feedback loop, leading to the development of severe inflammation or cancer. Our model also predicted that the knockout or overexpression of the I

κ

B kinase can influence the cancer cell’s fate – apoptosis or survival – through the crosstalk of different pathways. Finally, our work shows that computational modeling and statistical model checking can be effectively combined in the study of biological signaling pathways.