基于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的振荡属性。在未来的工作中将继续探索更全面和更具有代表性的胃腺癌信号转导网络，全面了解胃腺癌信号转导网络及其串扰，有助于研究人员开发更有效的多靶标治疗药物。通过和最新研究成果结合进一步改进模型，更好地模拟真实的胃腺癌信号网络的动态变化。