Title :
Probabilistic verification of ER stress-induced signaling pathways
Author :
Haijun Gong ; Lu Feng
Author_Institution :
Dept. of Math. & Comput. Sci., St. Louis Univ., St. Louis, MO, USA
Abstract :
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.
Keywords :
bioinformatics; biomembranes; cancer; cellular biophysics; inhibitors; molecular biophysics; molecular configurations; probability; proteins; stochastic processes; tumours; Alzheimers disease; Cyclin D expression; ER stress-induced apoptosis; ER stress-induced signaling pathways; IKK expression level; IKK inhibitor; MDM2; NFκB molecules; PRISM language; PRISM verification technique; amyloid-β; apoptosis; bioinformatics; cancer; cell cycle progression; communication hub; computational analysis; confidence interval estimation method; endoplasmic reticulum; overexpressed ER transmembrane proteins; pathogenesis; probabilistic model checking; probabilistic verification; secretory pathways; sequential probability ratio test; stochastic model; temporal logic properties; traditional simulation techniques; tumorigenesis; Cancer; Diseases; Erbium; Estimation; Feedback amplifiers; Proteins; Stress; Alzheimer´s disease; ER stress; PRISM; Probabilistic verification; cancer; confidence Interval; sequential probability ratio test; signaling pathway;
Conference_Titel :
Bioinformatics and Biomedicine (BIBM), 2014 IEEE International Conference on
Conference_Location :
Belfast
DOI :
10.1109/BIBM.2014.6999149