Model Checking a Synchronous Diabetes-Cancer Logical Network

Author(s): Haijun Gong, Paolo Zuliani, Edmund M. Clarke

Journal Name: Current Bioinformatics

Volume 8 , Issue 1 , 2013

Become EABM
Become Reviewer
Call for Editor


Cancer and diabetes are two highly malignant diseases. Accumulating evidence suggests that cancer incidence might be associated with diabetes mellitus, especially Type-2 diabetes which is characterized by hyperinsulinemia, hyperglycemia, obesity, and overexpression of multiple components of the WNT pathway. These diabetes risk factors can activate a number of signaling pathways that are important in the development of different cancers. To systematically understand the signaling components that link diabetes and cancer risk, we have constructed a single-cell, synchronous Boolean network model by integrating the signaling pathways that are influenced by these risk factors. Then, we have applied Model Checking, a formal verification approach, to qualitatively study several temporal logic properties of our diabetes-cancer model. Our aim was to study insulin resistance, cancer cell proliferation and apoptosis. The verification results show that the diabetes risk factors might not increase cancer risk in normal cells, but they will promote cell proliferation if the cell is in a precancerous or cancerous stage characterized by losses of the tumor-suppressor proteins ARF and INK4a.

Keywords: Apoptosis, boolean network, cancer, diabetes, model checking, signaling pathway, temporal logic, Glucose-AMPK-mTOR, Insulin-PI3K, Obesity-ROS-JNK

Rights & PermissionsPrintExport Cite as

Article Details

Year: 2013
Published on: 08 January, 2013
Page: [9 - 15]
Pages: 7
DOI: 10.2174/1574893611308010004
Price: $65

Article Metrics

PDF: 9