Probabilistic verification of ER stress-induced signaling pathways

Endoplasmic reticulum (ER) is a communication hub for several signaling and secretory pathways that regulate the cell cycle progression. Recent studies revealed that deregulation of ER stress-induced signaling pathways are involved in the patho-genesis of cancer and Alzheimers disease. Computational analysis and verification of these pathways will provide insights into the mechanism linking ER stress with different diseases. Based on the experimental observation and our recent bioinformatics studies, we construct a quantitative model to systematically study the ER stress-induced apoptosis and survival signaling pathways. To overcome the limitations of traditional simulation techniques, a formal verification method, called Probabilistic Model Checking, was introduced and applied to formally analyze the temporal logic properties of the stochastic model, which is written in the PRISM language. Compared with the symbolic model verification method, this PRISM verification technique can not only qualitatively verify the signaling pathway model using sequential probability ratio test (SPRT), but also provide a quantitative estimation of the temporal properties using confidence interval estimation method. The probabilistic verification studies show that, overexpressed ER transmembrane proteins will promote the expression of Cyclin D, Amyloid-β and MDM2, leading to the pathogenesis of cancer and other diseases in the long term, and inhibit the apoptosis. Our work also verified that, varying IKK´s expression level will influence the number of NFκB molecules in the nucleus, which explained why IKK inhibitor could inhibit tumorigenesis. The proposed signaling pathway model and PRISM method can help our understanding of the mechanisms that link ER stress with cancer and other diseases.