基于CTL模型檢測的胃腺癌核心路徑形式化驗證*

王亞鵬，雷麗暉

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

1 引言

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

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

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

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

2 信號轉導通路

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

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

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

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

核因子 κB NFκB(Nuclear Factor κB) 通路:NFκB作為重要的調控因子，參與細胞增殖、細胞凋亡等過程的調節。研究發現，現在多種人類癌癥細胞株中NFκB呈過度表達狀態，NFκB通過調控多種靶基因(如 COX-2、MMPS、Bcl-2、Ras、c-myc等，這些基因都含有與NFκB結合的位點)的表達，從而促進腫瘤的發生發展及轉移。NFκB也是抗癌藥物研究的一個重要靶點，因為其在促進癌細胞生長和抑制細胞凋亡的過程中起著非常重要的作用。研究發現，NFκB在胃癌組織中的表達明顯高于周邊正常組織［10］。

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

3 胃腺癌離散值模型

胃腺癌信號通路的作用機制非常復雜，涉及大量的基因突變、信號轉導通路和蛋白的表達異常。我們應用胃腺癌信號轉導網絡的離散值模型定性研究信號轉導通路異常或者蛋白突變導致過度表達情況下對胃腺癌發生發展的影響，從而可以根據胃腺癌發病機理找到治療胃腺癌潛在的靶點。

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

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

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

只有抑制子的節點狀態(更新)傳遞函數為:

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

只有激活子的節點狀態(更新)傳遞函數為:

圖1所示的胃腺癌信號轉導網絡，由77個節點組成，其中包含兩個輸出節點。可能的狀態數為277≈1．5 × 1023。傳統的隨機模擬［13，14］、布爾網絡［15］、隨機微分方程［16］不能有效模擬大型網絡，我們采用符號化模型檢測的方法來分析此模型。在模型中信號轉導通路之間交叉調控，我們的目的是識別和發現一些信號通路和關鍵蛋白，分析調控血管生成和細胞增殖的旁分泌信號通路，找到治療胃腺癌潛在的靶點。

4 模型檢測

4．1 模型檢測簡介

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

(1)抽象出系統的數學模型;

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

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

我們用Kripke結構表示模型檢測系統中有限狀態轉移系統，Kripke結構M用四元組表示:M=(S，S0，R，L)，其中，S 是可數且非空的狀態集合，S0表示初始狀態，R表示狀態遷移函數，L表示狀態的函數。給定一個Kripke結構(模型)M和一個時態邏輯公式φ，模型檢測器會自動、詳盡地搜索狀態空間來驗證模型M是否滿足邏輯公式φ。

4．2 計算樹時序邏輯

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

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

M，s|=EXφ 當且僅當存在狀態 si，si－1→si且滿足M，s|=φ。EX表示:“存在下一個狀態”。

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

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

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

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

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

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

5 形式化分析與驗證

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

性質1AF(!Antisurvival)。

性質2AF(Prosurvival)。

性質3AF(!Antisurvival＆Prosurvival)。

性質1和性質2被驗證為“True”，表示胃腺癌細胞最終會達到“增殖”的狀態，而不一定要經歷“凋亡”，因為癌細胞的擴散是必然的。性質3被驗證為“False”，表明胃腺癌細胞最終不能到達一個沒有凋亡而增殖活躍的狀態。

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

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

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

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

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

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

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

性質8被檢測為“True”，表明P53的激活促進了MDM2的表達，形成MDM2的依賴負反饋調節機制［22］，P53正向調節 MDM2促進其表達，MDM2負向調節P53抑制其表達［23］。其調節過程為:P53誘導激活MDM2，MDM2與 P53結合后形成P53-MDM2復合物，將P53由細胞核轉運到細胞漿中，降解P53，從而阻止了依賴于P53的凋亡發生。

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

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

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

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

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

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

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

性質11和性質12被驗證為“True”，表明當TAK1和PI3K或者TAK1和AKT被聯合抑制后，FOXO被激活并促進癌細胞凋亡，但是TAK1和PI3K或者TAK1和AKT的協同機制尚不清楚，驗證結果與文獻［25］實驗結果一致。驗證結果表明，聯合抑制TAK1和PI3K或者TAK1和AKT后，ERK仍處于激活或者過度表達狀態，這可能表明MEK/ERK不參與TAK1的下游抑制效應。性質13同樣被驗證為“True”，表明激酶NLK(Nemo激酶)是一種候選基因，可能潛在地作為TAK1和PI3K/AKT信號轉導的串擾點，因為已有實驗驗證其作用于TAK1的下游［26］，并介導FOXO的抑制性磷酸化［27］。

6 結束語

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