基于CTL模型檢測(cè)的胃腺癌核心路徑形式化驗(yàn)證*

王亞鵬，雷麗暉

(陜西師范大學(xué)計(jì)算機(jī)科學(xué)學(xué)院，陜西西安710119)

1 引言

胃癌是世界范圍內(nèi)最常見的惡性腫瘤之一，而胃腺癌是胃癌中最常見的組織學(xué)類型。胃腺癌可發(fā)生于任何年齡段，其發(fā)病率和死亡率隨著年齡的增長(zhǎng)而呈上升趨勢(shì)。在我國(guó)胃腺癌死亡率占所有胃癌的14%，居各類癌死亡率的第一位。近年來，隨著科技的發(fā)展，癌細(xì)胞基因表達(dá)的異常水平與胃腺癌細(xì)胞發(fā)生發(fā)展和轉(zhuǎn)移的相關(guān)性研究有很大進(jìn)展，已經(jīng)了解到在腫瘤發(fā)生過程中出現(xiàn)了一些基因改變以及由此而產(chǎn)生的信號(hào)轉(zhuǎn)導(dǎo)通路的變化。

細(xì)胞內(nèi)的信號(hào)分子并不是獨(dú)立存在的，多數(shù)信號(hào)分子參與多條信號(hào)通路，因此不同信號(hào)通路之間會(huì)發(fā)生交叉調(diào)控。各條信號(hào)通路通過細(xì)胞內(nèi)或細(xì)胞間信號(hào)分子相互作用在生物體內(nèi)組成一個(gè)高度有序且復(fù)雜的網(wǎng)絡(luò)，共同調(diào)控生物體的生理過程。研究人員通過分析癌細(xì)胞中基因表達(dá)的異常水平，來判斷其與胃腺癌細(xì)胞的發(fā)生、發(fā)展與轉(zhuǎn)移的相關(guān)性。明確胃腺癌發(fā)生發(fā)展和轉(zhuǎn)移過程中關(guān)鍵蛋白和關(guān)鍵信號(hào)通路的過度表達(dá)或者抑制狀態(tài)，有助于胃腺癌的早期診斷和治療。

由于胃腺癌細(xì)胞信號(hào)網(wǎng)絡(luò)的復(fù)雜性，生化反應(yīng)中的許多參數(shù)都是未知的，因此傳統(tǒng)的數(shù)學(xué)模型(如隨機(jī)Petri網(wǎng)、常微分方程等)無法對(duì)其進(jìn)行有效描述和分析。為了自動(dòng)分析和驗(yàn)證復(fù)雜的胃腺癌信號(hào)轉(zhuǎn)導(dǎo)網(wǎng)絡(luò)，我們應(yīng)用強(qiáng)大的模型檢測(cè)［1］技術(shù)驗(yàn)證模型(狀態(tài)轉(zhuǎn)移系統(tǒng))是否滿足時(shí)序邏輯公式中所表達(dá)的期望屬性。通過模型檢測(cè)來實(shí)現(xiàn)形式化驗(yàn)證，這是一種有限狀態(tài)轉(zhuǎn)換系統(tǒng)的自動(dòng)化驗(yàn)證技術(shù)，已經(jīng)成功應(yīng)用于數(shù)字電路和硬件協(xié)議的驗(yàn)證。模型檢測(cè)是確定給定模型是否滿足命題時(shí)序邏輯中的期望屬性/規(guī)范的過程。設(shè)M是一個(gè)狀態(tài)轉(zhuǎn)移圖，S0是一組初始狀態(tài)，φ是時(shí)間邏輯的一個(gè)公式。模型檢測(cè)問題是為了驗(yàn)證對(duì)于所有的初始狀態(tài)s∈S0，模型M滿足屬性φ，記為M，s|=φ。模型檢測(cè)算法詳盡地搜索系統(tǒng)模型的狀態(tài)空間以確定規(guī)范的真實(shí)性。模型檢測(cè)主要分為三個(gè)步驟:首先要給出系統(tǒng)的抽象模型和待驗(yàn)證模型的形式化表達(dá);其次在驗(yàn)證工具上執(zhí)行模型驗(yàn)證算法，以判定系統(tǒng)是否可以滿足性質(zhì);最后給出結(jié)論，若系統(tǒng)不能滿足性質(zhì)，則給出反例?，F(xiàn)有的模型檢測(cè)主要包括計(jì)算樹邏輯CTL(Computation Tree Logic)模型檢測(cè)、線性時(shí)序邏輯LTL(Linear Temporal Logic)模型檢測(cè)和μ演算模型檢測(cè)分支等。

本文將應(yīng)用模型檢測(cè)技術(shù)更好地了解胃腺癌細(xì)胞中的多條信號(hào)轉(zhuǎn)導(dǎo)通路的相互作用，應(yīng)用符號(hào)模型檢測(cè)來研究胃腺癌細(xì)胞模型中的許多重要時(shí)序邏輯性質(zhì)，這些性質(zhì)已通過體內(nèi)或者體外實(shí)驗(yàn)的驗(yàn)證。本文的目的是研究一些信號(hào)通路和蛋白的變化是如何影響細(xì)胞命運(yùn)，從而鑒定出信號(hào)轉(zhuǎn)導(dǎo)網(wǎng)絡(luò)中的關(guān)鍵信號(hào)通路或關(guān)鍵蛋白，為治療胃腺癌提供意見和建議。

2 信號(hào)轉(zhuǎn)導(dǎo)通路

近年來對(duì)胃腺癌關(guān)鍵蛋白和信號(hào)轉(zhuǎn)導(dǎo)通路的研究取得很大的進(jìn)展，Suh等［2］發(fā)現(xiàn)叉頭轉(zhuǎn)錄因子P3(FOX3)影響了Hippo信號(hào)通路，他認(rèn)為FOXP3的低表達(dá)水平促進(jìn)了癌細(xì)胞的發(fā)生發(fā)展，其與Hippo信號(hào)通路的核心激酶Lats2以及下游的轉(zhuǎn)錄輔助因子YAP的表達(dá)水平有一定的關(guān)聯(lián)。Rosania等［3］發(fā)現(xiàn)B細(xì)胞淋巴瘤-2(Bcl-2)的表達(dá)水平降低與萎縮性胃炎(AG)和腸上皮化生(IM)在胃腺癌組織的出現(xiàn)顯著相關(guān)。Tumanskiy等［4］發(fā)現(xiàn)胃腺癌的P53基因表達(dá)水平比正常值高出2倍，認(rèn)為該基因的異常表達(dá)水平與胃腺癌細(xì)胞的侵襲能力有關(guān)。王秋紅等［5］發(fā)現(xiàn)SAOSH1與p-ERK在胃腺癌中的表達(dá)成顯著負(fù)相關(guān)，SASH1蛋白可能通過調(diào)控ERK1/2信號(hào)通路抑制胃腺癌的進(jìn)展。王欣等［6］認(rèn)為Smad1能夠抑制胃腺癌細(xì)胞的增殖和遷移，作用機(jī)制與Akt信號(hào)通路有關(guān)。

研究表明，在胃腺癌中 Ras/Raf/MEK/ERK、PI3k/Akt/mTOR、NFκB、Wnt/β-catenin、P53 等信號(hào)轉(zhuǎn)導(dǎo)通路過度表達(dá)，因此可以通過了解胃腺癌發(fā)生發(fā)展的主要機(jī)制為治療胃腺癌尋求潛在的分子靶點(diǎn)。我們的目標(biāo)是明確胃腺癌信號(hào)轉(zhuǎn)導(dǎo)通路中調(diào)節(jié)癌細(xì)胞周期進(jìn)程的信號(hào)成分，了解胃腺癌的發(fā)生發(fā)展機(jī)理，從中找到潛在靶點(diǎn)為其治療提供建議。圖1所示為胃腺癌信號(hào)轉(zhuǎn)導(dǎo)網(wǎng)絡(luò)［7］，我們用符號(hào)→表示激活，符號(hào)－表示抑制作用。

Ras/Raf/MEK/ERK(MAPK)通路:近年來，MAPK信號(hào)通路已經(jīng)成為治療癌癥的重要靶點(diǎn)，主要功能是通過特異性級(jí)聯(lián)磷酸化，將細(xì)胞外的信號(hào)通過生化反應(yīng)傳入到細(xì)胞內(nèi)。研究表明Ras、Raf、MAPK以及其上游蛋白激酶(ERKs和MEK-1)在胃癌組織中的表達(dá)明顯增加，也說明了此通路在胃癌的發(fā)生發(fā)展中起到重要作用［8］。

PI3k/Akt/mTOR通路:PI3k/Akt/mTOR信號(hào)通路作為細(xì)胞內(nèi)重要信號(hào)轉(zhuǎn)導(dǎo)通路之一，通過影響其下游多種分子的活化狀態(tài)，在生物體內(nèi)發(fā)揮著促進(jìn)細(xì)胞增殖和抑制細(xì)胞凋亡的關(guān)鍵作用，它的過度表達(dá)與多種腫瘤的發(fā)生和發(fā)展密切相關(guān)。由于PI3K通路在調(diào)節(jié)細(xì)胞的各種功能中起著非常重要的作用，已經(jīng)成為抗癌藥物研究的一個(gè)重要靶點(diǎn)。目前代表性藥物是LY294002，它是一種PI3K的抑制劑，研究發(fā)現(xiàn)它能夠抑制抗凋亡分子Bad蛋白的磷酸化，與抗Fas抗體CH-11合用可使胃癌細(xì)胞系MEK-45 凋亡［9］。

核因子 κB NFκB(Nuclear Factor κB) 通路:NFκB作為重要的調(diào)控因子，參與細(xì)胞增殖、細(xì)胞凋亡等過程的調(diào)節(jié)。研究發(fā)現(xiàn)，現(xiàn)在多種人類癌癥細(xì)胞株中NFκB呈過度表達(dá)狀態(tài)，NFκB通過調(diào)控多種靶基因(如 COX-2、MMPS、Bcl-2、Ras、c-myc等，這些基因都含有與NFκB結(jié)合的位點(diǎn))的表達(dá)，從而促進(jìn)腫瘤的發(fā)生發(fā)展及轉(zhuǎn)移。NFκB也是抗癌藥物研究的一個(gè)重要靶點(diǎn)，因?yàn)槠湓诖龠M(jìn)癌細(xì)胞生長(zhǎng)和抑制細(xì)胞凋亡的過程中起著非常重要的作用。研究發(fā)現(xiàn)，NFκB在胃癌組織中的表達(dá)明顯高于周邊正常組織［10］。

腫瘤抑制劑基因P53:腫瘤抑制劑基因在維持基因組的完整性以及調(diào)節(jié)細(xì)胞增殖和凋亡的過程中起著非常重要的作用，因此腫瘤抑制劑基因的功能失活是腫瘤發(fā)生的一個(gè)直接原因。在胃癌發(fā)生發(fā)展的過程中主要涉及的腫瘤抑制劑是P53，因此P53功能的失活能夠促進(jìn)癌細(xì)胞的生成和血管生成并抑制癌細(xì)胞凋亡。

3 胃腺癌離散值模型

胃腺癌信號(hào)通路的作用機(jī)制非常復(fù)雜，涉及大量的基因突變、信號(hào)轉(zhuǎn)導(dǎo)通路和蛋白的表達(dá)異常。我們應(yīng)用胃腺癌信號(hào)轉(zhuǎn)導(dǎo)網(wǎng)絡(luò)的離散值模型定性研究信號(hào)轉(zhuǎn)導(dǎo)通路異?；蛘叩鞍淄蛔儗?dǎo)致過度表達(dá)情況下對(duì)胃腺癌發(fā)生發(fā)展的影響，從而可以根據(jù)胃腺癌發(fā)病機(jī)理找到治療胃腺癌潛在的靶點(diǎn)。

在離散值建模中，每個(gè)節(jié)點(diǎn)表示參與信號(hào)轉(zhuǎn)導(dǎo)網(wǎng)絡(luò)生化反應(yīng)的信號(hào)轉(zhuǎn)導(dǎo)通路或者關(guān)鍵蛋白。在本文構(gòu)建的離散值模型中，每個(gè)節(jié)點(diǎn)有兩個(gè)離散值(每個(gè)節(jié)點(diǎn)也可以同時(shí)有N個(gè)值，分別代表不同的狀態(tài)):0表示信號(hào)轉(zhuǎn)導(dǎo)通路或者蛋白受到抑制作用，1表示信號(hào)轉(zhuǎn)導(dǎo)通路或者蛋白過度表達(dá)作用。而節(jié)點(diǎn)的狀態(tài)更新是依賴于其相鄰節(jié)點(diǎn)狀態(tài)的變化(狀態(tài)更新)，由離散狀態(tài)轉(zhuǎn)移函數(shù)描述。我們的工作類似于文獻(xiàn)［11，12］，胃腺癌信號(hào)轉(zhuǎn)導(dǎo)網(wǎng)絡(luò)模型是相對(duì)封閉的，通路中的各個(gè)蛋白可能受到其他蛋白的促進(jìn)或者抑制作用。我們假設(shè)所有的反應(yīng)都是同步發(fā)生的，即每個(gè)蛋白質(zhì)(節(jié)點(diǎn))的狀態(tài)同時(shí)被更新。

在模型中，從時(shí)間t到t+1每個(gè)蛋白節(jié)點(diǎn)的狀態(tài)是通過傳遞函數(shù)由其父節(jié)點(diǎn)決定，由激活子Ai和抑制子Bj共同作用于節(jié)點(diǎn)，Xt的離散狀態(tài)傳遞函數(shù)為:其中，ai和bi分別是節(jié)點(diǎn)Xn的激活子Ai和抑制子Bj的值，“0”代表抑制狀態(tài)，“1”代表過度表達(dá)狀態(tài)。例如，IKKB被 TAK1激活，但同時(shí)被P53抑制，即在某個(gè)時(shí)刻t，若TAK1=1，P53=0，則下一個(gè)時(shí)刻IKKB(t+1)=1(過度表達(dá)狀態(tài));若TAK1=0，P53=1，則下一個(gè)時(shí)刻IKKB(t+1)=0(抑制狀態(tài))。

在模型中，一些節(jié)點(diǎn)只受到抑制劑的調(diào)控，若在時(shí)刻t，節(jié)點(diǎn)Xn(t)的所有抑制子和為0，則在下一個(gè)時(shí)刻Xn(t+1)=1，但是若至少一種抑制劑是過度表達(dá)狀態(tài)，則Xn(t+1)=0。

只有抑制子的節(jié)點(diǎn)狀態(tài)(更新)傳遞函數(shù)為:

在模型中，一些節(jié)點(diǎn)只受到激活子調(diào)控。若在時(shí)刻t，節(jié)點(diǎn)Xn(t)的所有激活子和為0，則在下一個(gè)時(shí)刻Xn(t+1)=0，但是若至少一種激活子是過度表達(dá)狀態(tài)，則Xn(t+1)=1。

只有激活子的節(jié)點(diǎn)狀態(tài)(更新)傳遞函數(shù)為:

圖1所示的胃腺癌信號(hào)轉(zhuǎn)導(dǎo)網(wǎng)絡(luò)，由77個(gè)節(jié)點(diǎn)組成，其中包含兩個(gè)輸出節(jié)點(diǎn)。可能的狀態(tài)數(shù)為277≈1．5 × 1023。傳統(tǒng)的隨機(jī)模擬［13，14］、布爾網(wǎng)絡(luò)［15］、隨機(jī)微分方程［16］不能有效模擬大型網(wǎng)絡(luò)，我們采用符號(hào)化模型檢測(cè)的方法來分析此模型。在模型中信號(hào)轉(zhuǎn)導(dǎo)通路之間交叉調(diào)控，我們的目的是識(shí)別和發(fā)現(xiàn)一些信號(hào)通路和關(guān)鍵蛋白，分析調(diào)控血管生成和細(xì)胞增殖的旁分泌信號(hào)通路，找到治療胃腺癌潛在的靶點(diǎn)。

4 模型檢測(cè)

4．1 模型檢測(cè)簡(jiǎn)介

模型檢測(cè)是一種有效的自動(dòng)化驗(yàn)證技術(shù)，用于分析軟件和硬件的正確性，主要工作流程如下:

(1)抽象出系統(tǒng)的數(shù)學(xué)模型;

(2)形式化描述期望的性質(zhì)，得到形式化表達(dá);

(3)通過模型檢測(cè)算法來驗(yàn)證系統(tǒng)是否滿足該性質(zhì)，并給出一個(gè)布爾結(jié)果:系統(tǒng)滿足性質(zhì)(正確)或者系統(tǒng)違背性質(zhì)(錯(cuò)誤并給出反例)。

我們用Kripke結(jié)構(gòu)表示模型檢測(cè)系統(tǒng)中有限狀態(tài)轉(zhuǎn)移系統(tǒng)，Kripke結(jié)構(gòu)M用四元組表示:M=(S，S0，R，L)，其中，S 是可數(shù)且非空的狀態(tài)集合，S0表示初始狀態(tài)，R表示狀態(tài)遷移函數(shù)，L表示狀態(tài)的函數(shù)。給定一個(gè)Kripke結(jié)構(gòu)(模型)M和一個(gè)時(shí)態(tài)邏輯公式φ，模型檢測(cè)器會(huì)自動(dòng)、詳盡地搜索狀態(tài)空間來驗(yàn)證模型M是否滿足邏輯公式φ。

4．2 計(jì)算樹時(shí)序邏輯

計(jì)算樹時(shí)序邏輯 CTL［1，17］是一種離散、分支時(shí)間邏輯，是一種在模型檢測(cè)中應(yīng)用較多的時(shí)序邏輯。在模型檢測(cè)中，CTL是一種描述能力非常強(qiáng)的時(shí)序邏輯，它用來描述計(jì)算樹的屬性，計(jì)算樹的根對(duì)應(yīng)于初始狀態(tài)，樹上的其他節(jié)點(diǎn)對(duì)應(yīng)于可能的狀態(tài)轉(zhuǎn)換(路徑)序列。CTL公式由路徑量詞和時(shí)態(tài)算子組成。路徑量詞分為兩種:全稱路徑量詞A，表示“在網(wǎng)絡(luò)中的所有路徑”;存在路徑量詞E，表示“在網(wǎng)絡(luò)中存在某條路徑”，它們用于描述計(jì)算樹時(shí)序邏輯中的分支結(jié)構(gòu)。時(shí)態(tài)算子描述了計(jì)算樹中一條路徑上所有的屬性。CTL分為以下五種基本的時(shí)態(tài)算子:X時(shí)態(tài)算子表示屬性在路徑的下一個(gè)狀態(tài)為真;G時(shí)態(tài)算子表示屬性在路徑的每個(gè)狀態(tài)上都為真;F時(shí)態(tài)算子表示屬性在路徑的未來某一個(gè)狀態(tài)上為真;U時(shí)態(tài)算子表示在路徑的某一個(gè)狀態(tài)上它的第二個(gè)屬性為真并且在這個(gè)狀態(tài)之前的所有狀態(tài)上其第一個(gè)屬性都為真;R時(shí)態(tài)算子是U算子的邏輯對(duì)偶。CTL公式可以分為狀態(tài)公式φ和路徑公式 :

CTL邏輯公式在模型上的解釋如下:

M，s|=EXφ 當(dāng)且僅當(dāng)存在狀態(tài) si，si－1→si且滿足M，s|=φ。EX表示:“存在下一個(gè)狀態(tài)”。

M，s|=AGφ當(dāng)且僅當(dāng)對(duì)任一路徑s1→s2→s3→…，s1=s，并且滿足在該路徑上任一狀態(tài) si，M，si|=φ。表示從s開始的任何一條執(zhí)行路徑，該路徑上的任何一個(gè)狀態(tài)都滿足φ。

M，s|=EGφ當(dāng)且僅當(dāng)對(duì)任一路徑s1→s2→s3→…，s1=s，并且滿足在該路徑上任一狀態(tài) si，M，si|=φ。表示從s開始至少存在一條執(zhí)行路徑，該路徑上的任何一個(gè)狀態(tài)都滿足φ。

M，s|=AFφ當(dāng)且僅當(dāng)對(duì)任一路徑s1→s2→s3→…，s1=s，并且在該路徑上存在某個(gè)狀態(tài) si，M，si|=φ。表示從s開始的任何一條執(zhí)行路徑，該路徑上至少存在一個(gè)狀態(tài)都滿足φ。

M，s|=EFφ當(dāng)且僅當(dāng)對(duì)任一路徑s1→s2→s3→…，s1=s，并且在該路徑上存在某個(gè)狀態(tài) si，M，si|=φ。表示從s開始至少存在一條執(zhí)行路徑，該路徑上的至少存在一個(gè)狀態(tài)都滿足φ。

如圖2所示，我們用同步程序來研究胃腺癌核心信號(hào)轉(zhuǎn)導(dǎo)網(wǎng)絡(luò)并驗(yàn)證感興趣的性質(zhì)。計(jì)算建模和形式化驗(yàn)證可以幫助更好地了解癌細(xì)胞中多種信號(hào)轉(zhuǎn)導(dǎo)通路的相互作用。在本文中，我們應(yīng)用符號(hào)模型檢測(cè)器NuSMV來研究胃腺癌細(xì)胞模型中的許多重要的時(shí)序邏輯性質(zhì)，這些性質(zhì)已經(jīng)通過體外或體內(nèi)實(shí)驗(yàn)得到了驗(yàn)證，我們還提出了幾個(gè)可以通過未來實(shí)驗(yàn)進(jìn)行測(cè)試的屬性。

下面給出胃腺癌核心信號(hào)通路網(wǎng)絡(luò)模型的一部分 NuSMV代碼作為說明，如圖 2所示。在NuSMV模型檢測(cè)器中，關(guān)鍵字VAR用于聲明變量;ASSIGN用于定義模型的初始狀態(tài)(init)和狀態(tài)轉(zhuǎn)換(next)。CTL屬性的驗(yàn)證使用“SPEC”語句進(jìn)行編碼。

5 形式化分析與驗(yàn)證

胃腺癌的發(fā)生發(fā)展涉及多種蛋白和信號(hào)轉(zhuǎn)導(dǎo)通路的異常表達(dá)，研究蛋白和信號(hào)通路的變化如何影響胃腺癌細(xì)胞的命運(yùn)及發(fā)生發(fā)展意義重大。研究發(fā)現(xiàn)一些表達(dá)異常的基因可以作為新的潛在靶點(diǎn)用于胃腺癌的治療，近年來針對(duì)各種基因的靶向治療取得一定的療效，許多治療胃腺癌的靶向治療藥物陸續(xù)應(yīng)用于臨床。我們使用模型檢測(cè)器中的同步方式對(duì)圖1中的信號(hào)轉(zhuǎn)導(dǎo)通路和蛋白進(jìn)行分析與驗(yàn)證，了解胃腺癌的發(fā)生發(fā)展機(jī)制。在胃腺癌信號(hào)通路的研究中，我們期望在特定的條件下(比如基因敲除、關(guān)鍵癌蛋白功能喪失、藥物干預(yù)等)預(yù)測(cè)癌細(xì)胞的發(fā)生發(fā)展，鑒定出胃腺癌發(fā)生發(fā)展中起重要作用的關(guān)鍵蛋白和關(guān)鍵信號(hào)通路。

性質(zhì)1AF(!Antisurvival)。

性質(zhì)2AF(Prosurvival)。

性質(zhì)3AF(!Antisurvival＆Prosurvival)。

性質(zhì)1和性質(zhì)2被驗(yàn)證為“True”，表示胃腺癌細(xì)胞最終會(huì)達(dá)到“增殖”的狀態(tài)，而不一定要經(jīng)歷“凋亡”，因?yàn)榘┘?xì)胞的擴(kuò)散是必然的。性質(zhì)3被驗(yàn)證為“False”，表明胃腺癌細(xì)胞最終不能到達(dá)一個(gè)沒有凋亡而增殖活躍的狀態(tài)。

性質(zhì)4AG{(PI3K=1)→EF(P53=0＆Prosurvival)}。

性質(zhì)5AG{(AKT=1)→EF(P53=0＆Prosurvival)}。

性質(zhì)6AG{(betacatenin=1)→EF(P53=0＆Prosurvival)}。

性質(zhì)4～性質(zhì)6被驗(yàn)證為“True”，表明若蛋白PI3K、Ras、AKT變異或者過度表達(dá)，其下游信號(hào)成分將在所有路徑上被連續(xù)激活并抑制重要的腫瘤抑制劑 P53的表達(dá)，最終導(dǎo)致癌細(xì)胞的增殖。PI3K通路在調(diào)節(jié)細(xì)胞的各種功能中起著重要的作用，已經(jīng)成為抗癌藥物研究的一個(gè)重要靶點(diǎn)。當(dāng)AKT過度表達(dá)后，能夠磷酸化抑癌基因P21以及促凋亡基因Bad、Caspse-9等，從而阻止凋亡和促進(jìn)上皮細(xì)胞的存活［18］。betacatenin作為一種多功能胞漿蛋白，我國(guó)葉國(guó)剛等［19］的研究顯示，betacatenin在進(jìn)展期胃癌組織中的異常表達(dá)率比正常胃組織高，betacatenin在正常胃組織和胃癌組織中的表達(dá)具有顯著性差異。曾有報(bào)道［20］，在胃癌患者中，大約有8% ～26%的患者有betacatenin基因突變，該基因突變后產(chǎn)生不完整的betacatenin，由于其不能被降解，遂進(jìn)入胞核內(nèi)與Tcf/Lef結(jié)合，形成異二聚體，持續(xù)激活c-myc等靶基因，使其進(jìn)行非正常轉(zhuǎn)錄并過度表達(dá)，從而導(dǎo)致腫瘤的發(fā)生。這些性質(zhì)表明，即使某些途徑被某些單基因靶向療法阻斷，不同信號(hào)傳導(dǎo)途徑之間的串?dāng)_也可能是胃腺癌細(xì)胞存活的原因。

性質(zhì)7AG{(NFκB=1)→EF(P53=0＆Prosurvival)}。

NFκB是抗癌藥物研究的一個(gè)重要作用靶點(diǎn)，因?yàn)樗诖龠M(jìn)癌細(xì)胞生長(zhǎng)以及抵抗凋亡的過程中起著非常重要的作用。胃腺癌組織中NFκB的表達(dá)低分化顯著高于高/中分化組織，表明NFκB參與胃癌的生長(zhǎng)和分化。性質(zhì)7被驗(yàn)證為“True”，表明在對(duì)NFκB的研究中發(fā)現(xiàn)它的過度表達(dá)可以促進(jìn)細(xì)胞的增殖，抑制細(xì)胞的凋亡。蘇曉娟等［21］研究表明，NFκB的異常表達(dá)可能是胃癌形成的早期分子事件，其表達(dá)水平對(duì)評(píng)價(jià)胃癌的惡性程度及預(yù)后可能有一定的參考價(jià)值。

性質(zhì)8AG{(P53=1→ AF(MDM2=1)＆(MDM2=1→AF(P53=0)))}。

性質(zhì)8被檢測(cè)為“True”，表明P53的激活促進(jìn)了MDM2的表達(dá)，形成MDM2的依賴負(fù)反饋調(diào)節(jié)機(jī)制［22］，P53正向調(diào)節(jié) MDM2促進(jìn)其表達(dá)，MDM2負(fù)向調(diào)節(jié)P53抑制其表達(dá)［23］。其調(diào)節(jié)過程為:P53誘導(dǎo)激活MDM2，MDM2與 P53結(jié)合后形成P53-MDM2復(fù)合物，將P53由細(xì)胞核轉(zhuǎn)運(yùn)到細(xì)胞漿中，降解P53，從而阻止了依賴于P53的凋亡發(fā)生。

性質(zhì) 9PI3K=1→AG{(NFκB≥1→AF(NFκB=0)) ＆ (NFκB=0→AF(NFκB≥1))}。

性質(zhì)9被驗(yàn)證為“True”，表明有無外部刺激都會(huì)發(fā)生NFκB的振蕩。對(duì)于某些特定的信號(hào)通路實(shí)驗(yàn)研究發(fā)現(xiàn)，外部刺激可能誘發(fā)信號(hào)振蕩，引起生物學(xué)家的關(guān)注［24］。

性質(zhì)10(MEK=0＆ERK=0)|(PI3K=0＆ AKT=0)→AF(FOXO=1＆Antisurvival)。

性質(zhì)10被驗(yàn)證為“True”，表明通過磷酸化失活的促凋亡轉(zhuǎn)錄因子FOXO被聯(lián)合的MEK和ERK或PI3K和AKT抑制相互協(xié)同作用激活，驗(yàn)證結(jié)果與文獻(xiàn)［7］實(shí)驗(yàn)結(jié)果一致。FOXO被稱為腫瘤抑制劑，激活的FOXO轉(zhuǎn)錄因子可能對(duì)胃腺癌、心血管疾病和癌癥的治療有重要意義。

性質(zhì)11AG{((TAK1=0＆PI3K=0)|(TAK1=0＆AKT=0))→AF(FOXO=1＆Antisurvival)}。

性質(zhì)12AG{((TAK1=0＆PI3K=0)|(TAK1=0＆ AKT=0))→AF(ERK=1)}。

性質(zhì)13NLK=1→AF(FOXO=0＆!Antisurvival)。

性質(zhì)11和性質(zhì)12被驗(yàn)證為“True”，表明當(dāng)TAK1和PI3K或者TAK1和AKT被聯(lián)合抑制后，F(xiàn)OXO被激活并促進(jìn)癌細(xì)胞凋亡，但是TAK1和PI3K或者TAK1和AKT的協(xié)同機(jī)制尚不清楚，驗(yàn)證結(jié)果與文獻(xiàn)［25］實(shí)驗(yàn)結(jié)果一致。驗(yàn)證結(jié)果表明，聯(lián)合抑制TAK1和PI3K或者TAK1和AKT后，ERK仍處于激活或者過度表達(dá)狀態(tài)，這可能表明MEK/ERK不參與TAK1的下游抑制效應(yīng)。性質(zhì)13同樣被驗(yàn)證為“True”，表明激酶NLK(Nemo激酶)是一種候選基因，可能潛在地作為TAK1和PI3K/AKT信號(hào)轉(zhuǎn)導(dǎo)的串?dāng)_點(diǎn)，因?yàn)橐延袑?shí)驗(yàn)驗(yàn)證其作用于TAK1的下游［26］，并介導(dǎo)FOXO的抑制性磷酸化［27］。

6 結(jié)束語

我們通過對(duì)胃腺癌信號(hào)轉(zhuǎn)導(dǎo)網(wǎng)絡(luò)的離散值模型研究信號(hào)通路或者蛋白的表達(dá)如何影響細(xì)胞的命運(yùn)，與基于傳統(tǒng)建模方法隨機(jī)模擬［13，14］、布爾網(wǎng)絡(luò)［15］、隨機(jī)微分方程［16］相比，應(yīng)用形式化分析同步建模方法更具有靈活性。通過對(duì)一些時(shí)序邏輯公式的驗(yàn)證對(duì)信號(hào)通路進(jìn)行形式化研究，可以讓我們更清晰地了解胃腺癌發(fā)生發(fā)展機(jī)制，為靶向治療提供意見。文中鑒定了幾種關(guān)鍵蛋白，包括PI3K、AKT、NFκB、NLK、P53、TAK1、betacatenin 等蛋白激活或者過度表達(dá)如何影響細(xì)胞命運(yùn)。同時(shí)也解釋了單基因靶向治療的缺陷，由于不同信號(hào)通路間存在串?dāng)_現(xiàn)象，即使抑制某些關(guān)鍵蛋白的表達(dá)，但也并不能阻止胃腺癌細(xì)胞的增殖分化。實(shí)驗(yàn)還證明了在胃腺癌細(xì)胞信號(hào)轉(zhuǎn)導(dǎo)通路中同樣存在NFκB和P53-MDM2的振蕩屬性。在未來的工作中將繼續(xù)探索更全面和更具有代表性的胃腺癌信號(hào)轉(zhuǎn)導(dǎo)網(wǎng)絡(luò)，全面了解胃腺癌信號(hào)轉(zhuǎn)導(dǎo)網(wǎng)絡(luò)及其串?dāng)_，有助于研究人員開發(fā)更有效的多靶標(biāo)治療藥物。通過和最新研究成果結(jié)合進(jìn)一步改進(jìn)模型，更好地模擬真實(shí)的胃腺癌信號(hào)網(wǎng)絡(luò)的動(dòng)態(tài)變化。