Model Checking a Synchronous Diabetes-Cancer Logical Network
Model Checking a Synchronous Diabetes-Cancer Logical Network
复制标题
同步糖尿病-癌症逻辑网络的模型检查
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
E. Clarke
中科院分区：
文献类型：
--
作者：
Haijun Gong;P. Zuliani;E. Clarke
癌症和糖尿病是两种高度恶性的疾病。越来越多的证据表明，癌症的发病率可能与糖尿病有关，尤其是2型糖尿病，其特征在于高胰岛素血症、高血糖症、肥胖和WNT途径的多种组分的过表达。这些糖尿病风险因素可以激活许多在不同癌症发展中重要的信号通路。为了系统地了解将糖尿病和癌症风险联系起来的信号成分，我们通过整合受这些风险因素影响的信号通路，构建了一个单细胞同步布尔网络模型。然后，我们应用模型检测，一种形式化的验证方法，定性地研究我们的糖尿病-癌症模型的几个时间逻辑特性。我们的目的是研究胰岛素抵抗，癌细胞增殖和凋亡。验证结果表明，糖尿病风险因素可能不会增加正常细胞的癌症风险，但如果细胞处于癌前或癌阶段，其特征在于肿瘤抑制蛋白ARF和INK 4a的丢失，则它们会促进细胞增殖。
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.