王亞鵬，雷麗暉

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

1 引言

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

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

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

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

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

近年來對胃腺癌關(guān)鍵蛋白和信號轉(zhuǎn)導(dǎo)通路的研究取得很大的進展，Suh等［2］發(fā)現(xiàn)叉頭轉(zhuǎn)錄因子P3(FOX3)影響了Hippo信號通路，他認(rèn)為FOXP3的低表達(dá)水平促進了癌細(xì)胞的發(fā)生發(fā)展，其與Hippo信號通路的核心激酶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信號通路抑制胃腺癌的進展。王欣等［6］認(rèn)為Smad1能夠抑制胃腺癌細(xì)胞的增殖和遷移，作用機制與Akt信號通路有關(guān)。

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

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

PI3k/Akt/mTOR通路:PI3k/Akt/mTOR信號通路作為細(xì)胞內(nèi)重要信號轉(zhuǎn)導(dǎo)通路之一，通過影響其下游多種分子的活化狀態(tài)，在生物體內(nèi)發(fā)揮著促進細(xì)胞增殖和抑制細(xì)胞凋亡的關(guān)鍵作用，它的過度表達(dá)與多種腫瘤的發(fā)生和發(fā)展密切相關(guān)。由于PI3K通路在調(diào)節(jié)細(xì)胞的各種功能中起著非常重要的作用，已經(jīng)成為抗癌藥物研究的一個重要靶點。目前代表性藥物是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é)合的位點)的表達(dá)，從而促進腫瘤的發(fā)生發(fā)展及轉(zhuǎn)移。NFκB也是抗癌藥物研究的一個重要靶點，因為其在促進癌細(xì)胞生長和抑制細(xì)胞凋亡的過程中起著非常重要的作用。研究發(fā)現(xiàn)，NFκB在胃癌組織中的表達(dá)明顯高于周邊正常組織［10］。

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

3 胃腺癌離散值模型

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

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

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

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

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

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

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

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

4 模型檢測

4．1 模型檢測簡介

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

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

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

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

我們用Kripke結(jié)構(gòu)表示模型檢測系統(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ù)。給定一個Kripke結(jié)構(gòu)(模型)M和一個時態(tài)邏輯公式φ，模型檢測器會自動、詳盡地搜索狀態(tài)空間來驗證模型M是否滿足邏輯公式φ。

4．2 計算樹時序邏輯

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

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

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

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

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

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

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

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

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

5 形式化分析與驗證

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

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

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

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

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

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

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

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

性質(zhì)8被檢測為“True”，表明P53的激活促進了MDM2的表達(dá)，形成MDM2的依賴負(fù)反饋調(diào)節(jié)機制［22］，P53正向調(diào)節(jié) MDM2促進其表達(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)運到細(xì)胞漿中，降解P53，從而阻止了依賴于P53的凋亡發(fā)生。

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

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

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

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

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

6 結(jié)束語

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