基于重写逻辑的Maude工具建模和分析哺乳动物信号通路的研究

144理论计算机科学电子笔记71（2003）网址：http://www.elsevier.nl/locate/entcs/volume71.html18页路径逻辑：生物网络Steven Eker、Merrill Knapp、Keith Laderoute、Patrick Lincoln和Carolyn Talcott计算机科学实验室，SRI国际，门洛帕克，CA 94025，美国。摘要在本文中，我们描述了使用基于重写逻辑的Maude工具来建模和分析哺乳动物信号通路。我们讨论了基本的生物学概念和事件的表示，并描述了使用新的搜索和模型检查功能的Maude 2.0分析建模的网络。我们还讨论了使用Maude符号生物学实验的思想为形式化方法，特别是重写基于逻辑的形式化方法开辟了一个令人兴奋的新世界。关键词：Maude，可执行模型，生物通路，形式化分析，元建模1介绍在本文中，我们描述了使用基于重写逻辑的Maude工具[7，6]来建模和分析哺乳动物信号通路。关于这项工作的初步报告见[16]。在这里，我们更详细地介绍了Maude模型，并描述了使用Maude 2.0 [6]的新搜索和模型检查功能来分析建模网络。我们还讨论了使用Maude这对于管理复杂的模型非常重要。对于生物学家来说，建立和使用莫德信号通路模型的自然性和相对容易性符号生物学实验的思想为形式化方法，特别是重写基于逻辑的形式化方法，开辟了一个充满挑战的新世界生物信号通路。基因组序列信息的巨大增长与全球基因表达分析的技术进步相结合，2003年由Else vier Science B.V. 操作访问根据C CB Y-NC-N D许可证进行。埃克和阿里145生物学和生物医学研究[43]。然而，现在产生的大量实验数据和相关分析迫切需要将这些信息整合到细胞过程的理论模型哺乳动物信号传导过程的研究，细胞检测，转换，并从其环境中的细胞内目标，如基因组的信息内部传输的分子途径虽然信号通路是复杂的，但从当代研究中已经出现了基本概念，表明它们可以通过计算方法进行分析。例如，大多数信号通路涉及多蛋白质复合物或模块在空间和时间上的分层组装，这些复合物或模块根据逻辑规则调节信息流[22，28]。此外，这些通路嵌入具有刺激、抑制、合作和其他连接的网络中，以确保信号在特定细胞或组织中得到适当的解释[18，36]。蜂窝信令网络建模。已经提出了用于细胞信号网络的计算分析的各种模型，包括结合速率和/或浓度信息来模拟对特定刺激的响应的方法[27，44，2]。或者，使用微分方程对由信号传导途径靶标（基因）组成的网络进行建模，以表示靶标及其途径组分的浓度变化（综述见[42]）。这里的目标包括预测转录信号测序，基因表达和调控机制的理解，包括反馈和多稳态开关。模型用于检验关于实验上未知的元素的假设。C.斯坦福大学的汤姆林小组使用控制理论的技术来分析控制信号过程的反应动力学，并确定可能的平衡状态[19]。他们能够模拟中等大小的阵列的细胞使用固定参数的开关阈值，并确定可能的平衡状态和阈值之间的分析relations为一个和两个细胞系统。另一种方法是将抽象技术应用于代谢反应的混合系统模型[30]。这给出了有限状态模型，然后进行模型检查。在[34]中，生物决策电路（具有反馈机制的电路）使用电路元件的混合逻辑/动力学模型进行建模。INRIA的HELIX项目开发了GNA（遗传网络分析器）工具，用于遗传调控网络的建模和模拟[10]。通过给出蛋白质浓度和反应速率的上限和下限来指定模型。该工具计算一个定性状态转换图，从中可以读取可能的定性行为。工作B。Palsson（UCSD）及其同事使用基于约束的通量平衡技术对基因组规模的代谢途径进行建模[12，37，9]。一个长期的目标是指定代谢表型，将表达的一个或-埃克和阿里146在不同的环境条件下。基本的想法是从代谢网络-其节点是建模系统的代谢物的图，并且其箭头表示这些代谢物之间的通量（箭头可以从外部开始或结束）。该图变成一个系统的符号微分方程使用变量的速率数据是未知的。为已知或预测的关系添加对变量的约束（目前的监管还没有建立模型。）线性规划技术（基于通量的分析）用于确定解决方案状态的空间，并找到相对于目标（如生长或副产物分泌）的最佳解决方案。这些结果说明了细胞不能做什么，并给出了它可能做什么的可能性--这些假设将在实验室实验中得到检验。许多为硬件或软件分析设计的工具已被应用于生物学问题[31]。有趣的是，对比目标：在软件/硬件系统的情况下，目标通常是设计，算法，实现的验证或验证;而在生物系统的情况下，工具用于假设生成和测试系统的模型，通常只有部分已知。为数字设计的静态时序分析而开发的pathetry工具[32]已用于通过枚举它们之间的所有路径来确定将靶与源断开连接的蛋白质家族该工具不适用于具有反馈（循环）的网络。 贝叶斯网络已被用于从大量基因表达阵列数据中找到统计依赖性[41]。SPICE硬件模拟器BioSpice的模拟器正在开发中，用于生物网络的数值模拟[1]。 π演算已用于表示和正向模拟小信号通路[38]。使用SRI的Karp小组[25，24，26]以及KEGG [23]和WIT [35]小组开发的工具，已经在测序的基因组中对数百种代谢途径进行了计算预测PathoLogic程序[26]使用AI技术通过模拟来预测实验已知的通路。该工具集还包括一个用于在EcoCyc数据库中动画生物途径的工具[39]。使用基于信号通路或网络的动力学测量的计算机模型进行模拟对于实现对信号转导的生物化学然而，这种模型的发展信号分子的细胞规模群体的随机性质提供了额外的复杂性[31，33]。此外，需要新的计算方法来克服模拟和分析这种详细模型的复杂性[17]。我们的方法侧重于开发代谢和信号传导过程的高度抽象的定性模型，这些模型可用作强大工具（如正式方法社区开发的工具）分析的基础，以研究广泛的问题。埃克和阿里1472符号系统生物学中的可执行模型Maude案例研究与EcoCyc工作[25]和其他初步案例研究[30，14]一起将正式建模技术应用于细胞路径，是发展符号系统生物学新科学的第一步。这门新的科学可以为生物学家提供新的能力，通过电动工具，使生物实体之间的关系产生新的推论这些工具将有助于我们理解复杂的生物系统，并加速研究，以测试有关其在体内运作的假设。在我们的方法中，重写规则描述了局部变化时，可能会发生的一个实例的左手边的规则存在于一个建模系统。重写逻辑允许在给定模型指定的基本更改的情况下对可能的复杂更改进行推理这些复杂的变化可以是同时发生的;也就是说，隔室的不同部分可以同时且独立地发生变化。此外，改变可以是多步骤的，允许对系统的可能的未来状态进行推理。因此，在非常合理的假设下，重写理论可以在Maude中执行以根据符号模型描述随时间的生物信号传导过程，并且可以被形式化地分析以推理从初始状态可达到的状态的属性。给定诸如上述的可执行模型，给定的初始状态是一个图，其节点是可达状态，其边是连接它们的规则。然后，通过图的路径对应于系统可以进化的可能方式执行策略从这些可能的路径中挑选出一条特定的在这样的模型中，可以执行多种计算，包括：静态分析、前向模拟、前向搜索、后向搜索、显式状态模型检查和Meta分析。静态分析允许检查模型的结构，并理解元素是如何相关和组织的（排序结构）。静态分析还提供了一种检查不一致或格式错误的声明以及查找丢失信息的方法正向模拟使用内置策略从给定的初始状态运行模型，或者运行固定数量的步骤，或者直到不再应用重写。这是非常快的，非常有用的初步探索。前向搜索是对给定初始状态下通过转换图的所有路径的宽度优先搜索它将从给定的初始状态中找到所有可能的结果搜索也可以被限制为找到满足给定属性的可能有限数量的状态反向搜索将模型反向运行对于满足某些约束的模型例如，它可以用于查找特定检查点的所有可能的前兆。显式状态模型检查扩展了可以调查的属性集合。搜索只涉及单个状态的属性。模型检查还考虑路径的属性例如，我们可以问：“如果我们到达一个状态，埃克和阿里148满足P的状态，那么我们之后总是会达到满足Q的状态吗？Meta分析允许我们对模型本身进行推理。模型的基本特征可以抽象成相关模型的族，使我们能够处理反应的不确定性。从已知反应的基本集合开始，可以探索反应集合的不同实例化例如，我们可以搜索在给定初始状态下给定路径属性为真的模型。此外，规则本身可以被抽象成规则族，每个规则族对应于例如特定类型的反应，诸如激活、抑制或转导。3信令路径模型BP在本节中，我们描述了哺乳动物细胞中主要受体介导途径的Maude模型BP（BioPathways）[20]，重点关注以表皮生长因子受体（EGFR）为中心的部分。英国石油公司正式反应数据精心策划的文献专家生物学家。目前，BP包括650多种蛋白质和500多种描述可能反应步骤的规则。在3.1小节中，我们描述了相关的生物学概念如何被表示为（隶属）方程理论。在3.2小节中，我们描述了使用重写规则来表示不同类型的信令事件在3.3小节中，我们给出了一些针对两种不同初始状态的例子分析首先，我们将考虑一个小的例子，对应于一个信号网络的一部分，涉及通过磷酸化调节新的蛋白激酶Cε（PKCe）这里可达状态的数量很小，人们可以详细地检查路径图第二个例子涉及更大的EGF信号网络。这里的可达状态是大的（39992）和探索的模型选择性搜索和模型检查不同的初始配置。在3.4小节中，我们讨论了反射和元建模的使用。3.1生物种类和成分感兴趣的两种基本类型是蛋白质和化学（非生物实体，如钙离子Ca++）。我们引入了一个sortThing来收集各种基本排序，从而形成更复杂的组件这些排序及其特定成员的示例由以下声明：分类蛋白质化学物质蛋白质化学物质Ops EGFR EGF PIP3 Pdk1 PKCe：-> Protein.操作Ca++：->化学。关键字op和ops用于将运算符从域排序列表声明为范围排序。在上面的两个示例中，域排序列表为空，表示声明的运算符是常量。因此，EGFR、EGF、PIP3、Pdk1和PKCe被认为是这类蛋白质的常数。需要细胞生物学的几个重要概念来模拟信号，埃克和阿里149naling网络。它们包括蛋白质修饰、蛋白质缔合和细胞区室化。蛋白质修饰。BP包括蛋白质修饰的全面代数。这里我们只展示了与后面的例子相关的一小部分。排序Modification ModSet。subsort修改ModSet。ops GDP GTP act deact：-> Modification.opnone：-> ModSet。op _ _：ModSet ModSet -> ModSet [aslogid：none].op [_-_]：Protein ModSet -> Protein [right id：none].有常数GDP，GTP，act和deact的排序修改，这是抽象类的修改与类似的效果，至于信令。ModSet是修改的多集排序，由单例（由子排序声明表示）和多集联合（由子排序表示）形成。none是空的修改集。使用操作符[_-_]将修饰集应用于蛋白质。例如，[EGFR-act]代表EGFR的活化形式。蛋白质协会。信号蛋白通常结合形成功能复合物[29]。这一重要现象在代数上由以下声明表示：复杂排序。subsort复杂的东西。op _：_：Thing Thing -> Complex [复杂]。因此，每个蛋白质或其他东西都是单元素复合物，两个这样的复合物可以通过“：”运算符关联复合物也被认为是物。一个例子是抑制复合物：（IqGap1：（E钙粘蛋白：b连环蛋白））描述了IqGap1隔离E钙粘蛋白和b连环蛋白，使它们不能参与其他反应。蛋白质区室化。在真核细胞（具有细胞核的细胞）中，蛋白质和其他分子以复杂的混合物存在，这些混合物被划分[22]。这些区室化的混合物（在此称为汤）由以下表述代数地表示对Soup Enclosure MemType进行排序。Subsort Thing Soup.opempty：-> Soup.op _ _：Soup Soup -> Soup [aspherid：empty].操作CMNM：-> MemType。联系我们|_{_}}：MemType Soup Soup -> Enclosure。埃克和阿里150=>一个外壳 有一个膜部分和一个内部，每个部分都有自己的组成汤。MemType用于指定特定的膜类型，例如细胞膜（CM）或核膜（NM）。从形式上讲，一碗汤是由多种东西组成的。多集并运算模拟了一些亚细胞区室的假定流体或动态性质，其中分子存在于汤中的顺序并不重要。术语{CM| cm：汤PIP 3 [Pdk 1- act]{cyto：汤PKCe}}代表在细胞膜中含有化学物质PIP 3和活化蛋白[Pdk 1- act]以及在细胞质（细胞内部）中含有蛋白PKCe的细胞符号cm：Soup是一个动态声明的变量，名为cm，排序为Soup。变量cm：Soup和cyto：Soup代表剩余的单元内容。最后，我们声明了一个作为顶级汤的sortDish，以及一个用于进行计算机实验的容器。整理盘子。OP PD：汤->菜。3.2生化事件为了模拟生物化学事件，如信号传导过程，我们使用重写理论的动态部分，重写规则，来表达涉及单个或多个亚细胞区室的生物化学过程或反应。例如，下面的文字描述了EGFR信号通路激活的第一步，EGF与EGFR的结合[40]“激活的Erk1被迅速转移到细胞核，在那里它被功能性地隔离，并可以调节包括转录因子在内在Maude语法中，此信令过程由以下重写规则描述：rl[410.Erk1/2.to.nuc]：{CM |cm：汤{cyto：汤[Erk 1-act]{NM |nm：汤{nuc：汤}{CM |cm：汤{cyto：汤{NM| nm：Soup {nuc：Soup [Erk1 -act]}。rl【438.Erk.act.Elk】：[？Erk1/2 - act] Elk1 => [？Erk 1/2 - act] [Elk 1- act]。规则410描述了激活的Erk1从细胞质到细胞核的易位。规则438描述了通过激活的Erk1激活Elk1（转录因子）。请注意，BP中的规则标签由一个数字和一个简短的描述组成，这允许仅使用规则标签对反应路径进行有意义的描述。我们通常只使用数字来引用规则。我们还采用了一种惯例，即符号以？带有sort的变量是否通过省略？（在模块中的某个地方声明）。所以呢？Erk 1/2是Erk 1/2的一个变体（包含Erk 1和Erk 2的蛋白质的一个亚类）。作为另一个例子，以下规则代表实验结果[3]，即在PIP3存在下，活化的Pdk 1从细胞质募集PKCe埃克和阿里151=>我们的优势并激活细胞膜rl[757.PIP3.Pdk1.act.PKCe]{CM| cm：汤PIP 3 [Pdk 1- act]{cyto：汤PKCe}}CM| cm：Soup PIP3 [Pdk1 - act][PKCe - act] cyto：Soup[metadata“cite = 21961415”].规则声明还可以包含附加信息，包括元数据属性。元数据属性允许规则使用任意信息进行注释，这些信息被核心重写引擎忽略，但可供满足级别操作使用。在上述规则中，元数据“cite = 21961415”给出了MedLine数据库引文的唯一标识符，作为该规则的理由生物网络规则的其他元数据包括反应速率或浓度数据、其他形式的文献引用、数据库链接和置信度评级。图1.显示了一个表示部分的蛋白激酶C网络，我们已经modeled，使用的生物网络符号之一，连同一些相应的莫德规则。箭头在反应物状态之前和之后连接。未使用的规则启用元素由垂直于箭头的线指示从图中我们看到PIP2和PIP3之间存在一个平衡（由它们之间的一对箭头表示）。这种均衡由一对规则（643，107）表示。此外，我们（从一对垂直箭头）看到，PKCe（至少）有两种激活方式（规则757和758）。 第758章变数？nPKC：nPKC的范围涵盖了包含PKCe和少量相关蛋白质的蛋白质亚类。3.3计算BP现在我们举几个例子来说明BP的用法3.3.1PKC分析我们首先考虑PKC网络，并对初始状态进行了分析Q14的定义如下。op q14：-> Dish.等式q14 =PD（Ca++{CM| PIP2 [PI3Ka - act] [PLCb 1- act] [Pten -act]{Erk1 Pdk1 PKCa PKCe}}）。首先，我们简单地根据两种不同的内置策略进行重写，分别由命令rewrite和frewrite调用。rewrite命令调用Maude默认策略，这是一种自顶向下的重写策略。使用此策略，我们有：重写问题14。结果菜肴：PD（{CM| Ca++ DAG IP3 [PI3Ka - act] [PLCb 1- act] [Pten -act]{Erk1 Pdk1 [PKCa - act] [PKCe -act]{NM|空{empty}）命令frewrite调用Maude的位置公平重写策略。我们-埃克和阿里152{PTEN*107PDK1PIP2 PIP364310884PI3K*PLC*PKCe758757Akt109{CA++}IP3 DAGPDK 1*cPKCcPKC*PKCe*Akt*314ERKErk*七五四;四一零等等rl [643.PI3KI.mets.PIP2.to.PIP3]：PIP2 [？PI3KI：PI3KI - act] => PIP3 [？PI3KI：PI3KI -act]。rl [107.Pten.pp.PIP3.to.PIP2]：PIP3 [Pten-act] => PIP2 [Pten-act]。rl [84.PLC.act.PIP2.Ca]：=>{CM| cm：汤（Ca++ DAG IP 3）[？PLC：PLC - act]{cyto：Soup}}.rl [758.DAG.act.nPKC]：Ca++{CM|PIP 2 cm：汤[？PLC：PLC-act]{ cyto：Soup}}=>{CM |DAG cm：汤{cyto：汤[？nPKC：nPKC-act]}}。{CM |DAG cm：汤{cyto：汤？nPKC：nPKC}}图1.一、PKC调控网络。蛋白质后的根据这一战略，我们有：Frewrite Q14.结果菜肴：PD（CM| Ca++ DAG IP3 [PI3Ka - act] [PLCb 1-act][Pten- act] [Pdk1 -act]{Erk1 [PKCa - act] [PKCe -act]{NM|空{empty}）注意，使用位置公平重写策略，Pdk1被激活并被招募到细胞膜，而使用自上而下策略，它在细胞质中保持未激活。这两次执行已经表明，从q14开始有多种可能的结果。我们可以使用搜索命令找到所有可能的结果搜索q14 =>！D：盘子。这构建了PKC调节网络的整个路径图，从初始状态q14开始，并报告了三个最终状态，编号为6，20和23。国家6是埃克和阿里153{{64384S0758S1107314S2108S3S4107314758757S5S6S7643107643S8754B84410S9S1084758S11314S12S13410S14314S15S16314 758643S1784S18410S19S20754BS21314S22410S23图二. PKCe路径图使用重写获得的结果，状态20是使用重写获得的结果。在状态23（如下所示），Erk1已被激活并从细胞质易位到细胞核。解决方案3（状态23）D：盘-->PD（CM| Ca++ DAG IP3 [PI3Ka - act] [PLCb1 - act] [Pten -act][Pdk1 - act][PKCe -act]{[PKCa-act]{NM|空{[Erk 1-act]}）图2.显示了q14（S0）的全路径图的结构。在重复的“交换菱形”中的一些规则标签请注意，该图基本上分为三个部分，每个部分对应一个解决方案。然而，从图形分析的角度来看，由这对规则（107，643）表示的均衡增加了一些复杂性。3.3.2EGF-EGFR网络我们对EGF-EGFR网络的分析从状态q1开始，op q1：-> Dish.等式q1 = PD（EGF CM| EGFR Pak1 PIP2 nWasp [H-Ras -GDP]Akt1 Gab1 Grb2 Gsk3 Eps8 Erk1 Mek1Mekk1 Mekk4 Mkk4 Mkk3 Mlk2 Jnk1p38a p70s6k Pdk1 PI3Ka PKCb1Raf1 Rsk1 Shc Sos [Cdc42 -GDP]{NM|空{cJun cFos}）。假设我们想知道一个激活了cJun和cFos的状态是否是可达的。进一步假设我们想知道如果PI3Ka从q1中移除会发生什么（称之为q1x）。Maude模型检查器[13，15]可以用来找到一个{埃克和阿里154|相反的例子断言，这样的状态是永远无法到达的。与Maude模型检验器的接口包含在MODEL-检验器模块中。这个模块定义了基于排序属性的LTL（线性时态逻辑）公式的语法。介绍了一种排序状态和满足关系，以及LTL公式.要使用模型检查器，用户定义特定的状态和命题，并公理化对这些状态和命题的满意度。LTL语义将满足从命题提升到任意LTL公式。在我们的BP实验中，状态是碟形的，因此碟形被声明为状态的一个子类。cJun和cFos被激活的碟满足的命题prop1定义如下。subsort Dish State .op prop 1：-> Prop .eq PD（输出：汤{CM|cm：汤{细胞：汤{NM|nm：汤{nuc：Soup [cJun-act][cFos-act]}）|= prop1 = true。公式prop> prop 1表示prop1永远不成立。执行命令红色Q1| = 10<> prop1.导致反例对于模型检查器的这种用途，通过定义eq findPath（S：State，P：Prop）= getPath（P：Prop，S：State| P<：Prop）。其中，getPath将Maude返回的反例抽象为一个规则标签列表，后跟满足给定命题的状态。如果我们执行findPath（q1，prop1）和findPath（q1x，prop1），我们会发现，事实上，在这两种情况下，都找到了cJun和cFos都被激活的状态然而，当PI3Ka存在时，Akt1和Eps8都被激活，但当其被去除时则不被激活。(For详情见附录中的图43.4Meta分析存在与信令网络（和许多其它系统）的可执行模型相关联的各种元数据。这包括证明或限定规则的信息和关于规则的评级信息。还有排序信息，例如“激活规则应在易位规则之前应用”。存在特定事件类的规则应该遵循的模式，并且可以使用“生物类型检查”来确保满足这些模式和模型结构上的其他约束。此外，随着系统模型的增长，一致性检查变得更加重要，并且能够回答诸如“所有规则标签是什么”之类的简单问题是非常有用的。或利用Maude的反射能力，埃克和阿里155很容易将这种元数据形式化，并使用它来进一步控制实验或回答问题并进行各种荟萃分析。作为一个例子，我们列出了如何回答有关申报蛋白质的问题. BP Meta模型扩展了Maude META-LEVEL模块[5]，该模块提供了模块和 重 写 的 元 表 示 。 对 于 有 关 常 量 的 问 题 ， 定 义 了 一 个 运 算 符constSetBySort，它接受一个（元表示的）模块和一个排序，并返回一组引用的标识符，这些标识符命名了给定模块中具有给定排序的例如，假设BP命名BP模型的元表示（这可以使用Full Maude 2.0[11]生成），减少constSetBySort（BP，'Protein）会操作符constSetBySort从模块中选 择 一 组 操 作 声 明 ， 并 使 用 辅 助 函 数 constSetBySortX 和constBySortX检查每个声明，以查看操作是否是常量，如果是，则声明的 排 序 是 否 小 于 或 等 于 模 块 排 序 偏 序 中 的 给 定 排 序 定 义 关 键 操 作constBySortX的运算符声明和等式如下所示。op constSetBySort：Module Sort -> QidSet.op constSetBySortX：OpDeclSet SortSet -> QidSet。opconstBySortX：OpDecl SortSet -> QidSet。...eq constBySortX（（op q：Qid：tl：TypeList -> t：Type[atts：AttrSet].），ss：SortSet）= if（（tl：TypeList == nil）and member（t：Type，ss：SortSet））then q：Qid没有其他的。constBySortX的应用程序通过模式匹配、提取操作名称、q：Qid、参数类型列表tl：TypeList、结果类型t：Type和任何属性来析构操作符声明。还有许多更有用的问题可以使用类似的技术来回答，例如除了能够询问关于模型结构和内容的问题之外，我们的生物学家还希望以比Maude规则语法更直观的形式可视化规则和路径段。在文学作品中，被称为尽管这些图片具有暗示性，但它们隐含了许多信息，它们可能是模糊的，并且有许多不同的描绘方式给定的反应或事件（OO设计符号的阴影）。已经有一些关于我们已经定义了一个卡通数据类型的BP元模型作为一个正式的基础可视化。正式漫画包含规则的所有信息，给出了关于细胞结构的一些假设，它们消除了与可视化无关的占位符等信息，并明确了其他信息，如生物信息，埃克和阿里156PIP3Pdk 1*PKCePIP3Pdk 1 *PKCePIP3 Pdk 1*PKCePKCe*757.PIP3.Pdk1*.act.PKCePIP3Pdk1* PKCe*PKCe*（一）（二）（三）图3.第三章。PKCe规则可视化的三种方法各种各样。规则的相关元素是它的标签和左侧和右侧的非占位符每一项在漫画中都以其印刷体名称、生物分类、在规则汤中的位置以及修改状态的抽象来表示因此，BP元模型中的卡通是以下形式的术语：ctoon（ruleid：Qid，lhs：ItemSet，rhs：ItemSet）其中项是以下形式item（pname：String，bsort：BioSort，loc：Location，a：Activation）定义了一个元操作rs2cts来将规则映射到卡通。将rs2cts应用于规则757.PIP3.Pdk1.act.PKCe（参见第3.2小节），生成卡通：ctoon（'757.PIP3.Pdk1.act.PKCe，（item（“PIP3”，Protein，membrane（item（“PIP3”，Protein，membrane图3.4显示了三种可能的可视化，可以从这个正式的卡通自动生成。视图（1）是图3.2中给出的规则的表示。这是一个常见的信令网络表示，显示了什么被改变了，还有什么必须存在。View（2）是一个受计算机过程网络的Petri网形式主义启发的可视化。它在一个框中显示规则标签，反应前所需的单元格内容由指向框的箭头指示因此，反馈回路显示了未改变的元素（催化剂）。视图（3）示出了添加关于反应元件在单元中位于何处的信息之前和之后的单元状态的表示。双线代表细胞膜，椭圆形的内侧代表细胞质。位置信息可以很容易地添加到（2）中的图片中。根据规则生成不同可视化的能力对于埃克和阿里157原因很多，包括：作为理解信号流或路径中的化学过程的辅助;以及作为规则正确地捕获关于反应的已知数据的附加检查。尽管它们具有“卡通”的外观，但是4结论和今后的工作我们已经描述了Maude中的生物信号网络的表示，并展示了如何将这样的模型用于各种计算机实验和高级形式的符号分析。像这样的可执行模型为生物学家提供了新的计算能力。它们的预测能力可用于生成通过其他手段测试的假设和设计实验。它们也是形式化建模广泛应用的起点虽然BP模型已经相当先进，但还有更多的数据要添加，还有更多的工作要做，以改进和扩展分析和元建模能力。一个重要的问题是开发方法来简化和抽象特定类别的问题的信令路径模型，以便能够扩展到更大的系统的分析和回答更复杂的问题。致谢。 我们要感谢匿名推荐人的帮助建议。我们也感谢其他过去和现在的成员的途径逻辑组-Jose 'Meseguer、John Bashkin、Kemal Somnez、Harry Bratt和Rasika Kumar-在模型和视觉表现的开发过程中进行了许多富有成效的讨论。引用[1] A. P. 阿金实验室http：//genomics.lbl.gov/genomics.lbl.gov/[2] A. R. Asthagiri和D. A.劳芬伯格丝裂原活化蛋白激酶（mapk）通路模型中反馈效应对信号动力学影响的计算研究。生物技术进展，17：227[3] V. Cenni，H. D？pple r，E. Sonnen b u r g，N. Maraldi，A. C. N e wton，和A.托克河。磷酸化对新型蛋白激酶Cε的调控 Biochem J. ，363：537[4] M. Cl av el，F. 杜伦，S。 E k e r，P. Lincoln，N. Marti-Oliet和J. 梅斯盖河在Maude中进行金属evel计算。In C. Kirchner和H. Kirchner，编辑，第二届重写逻辑 及其 应用 国际 研讨 会， WRLAElsevier ， 1998年 。http://www.elsevier。nl/locate/entcs/volume15.html。埃克和阿里158[5] M. Cl av el，F. 杜伦，S。 E k e r，P. Lincoln，N. Marti-Oliet，J. Mes e gue r和J.克萨达Maude作为元语言。In C.Kirchner和H.Kirchner，编辑，第二届重写逻辑及其应用国际研讨会，WRLAElsevier，1998年。 http://www.elsevier。nl/locate/entcs/volume15.html。[6] M. Cl av el，F. 杜伦，S。 E k e r，P. Lincoln，N. Marti-Oliet，J. Mes e gue r和J.克萨达迈向莫德2.0在第三届重写逻辑及其应用国际研讨会（WRLA爱思唯尔，2000年。http：//www.elsevier.nl/locate/entcs/volume36.html的网站。[7] M. Cl av el，F. 杜伦，S。 E k e r，P. Lincoln，N. Mar t's-Oliet，J. Mes e gue r和J. 克萨达关于Maude的教程。http://maude.csl.sri.com，2000年3月[8] D. L. Cook，J.F. Farley和S.J. 塔普斯科特一种用于描述、归档和分析复杂生物系 统 功 能 模 型 的 可 视 化 语 言 的 基 础 Genome Biology ， 2 （ 4 ） ， 2001.http://genomebiology.com/2001/2/4/research/www.example.com[9] M. W.隐蔽和B。O.帕尔森大肠杆菌基于限制的代谢模型中的转录调控。生物化学杂志，2002年。出版中。[10] H. de Jong，J. Geiselmann，C. Hernanedez和M.页. Genetic Network Analyzer：一种定性模拟基因调控网络的工具技术报告RR 4262，INRIA罗纳-阿尔卑斯，2001年9月。[11] P. 杜兰完整的Maude 2.0 alpha发行说明，2002年。[12] J. S.爱德华兹，M.隐蔽，B. O.帕尔森微生物代谢模型：通量平衡方法。环境微生物学，4（3）：133[13] S.艾克Maude 2.0 alpha发行说明，2002年。[14] S. Eker，P.Karp，P.D. Lincoln和P.罗梅罗从臭虫到BDD：饮食计划E.杆菌正在进行的工作草案。[15] S. Eker，J.Meseguer和A.Sridharanarayanan。Maude LTL模型检查器。本卷，2002年。[16] S. Eker，M. Knapp，K. Laderoute，P. Lincoln，J. Meseguer，and K.桑梅兹Pathway logic：生物信号的符号分析。太平洋生物计算研讨会，第400-412页。世界科学，2002年1月。[17] D. Endy和R.布伦特模拟细胞行为。Nature，409：391[18] D. Fambrough，K. McClure，A. Kazlauskas和E. S.着陆器由生长因子受体激活的不同信号通路诱导广泛重叠的基因组，而不是独立的基因组。Cell，97：727埃克和阿里159[19] R. Ghosh和C.汤姆林。通过Delta-Notch信号传导的侧抑制：分段仿射混合模型。In M.D. Di Benedetto和A.Sangiovanni-Vincentelli，编辑，混合系统：计算和控制HSCCSpringer，2001年。[20] A. Gschwind，E. Zwick，N. Prenzel，M. Leserer和A.乌尔里希细胞通讯网络：表皮生长因子受体反式激活作为受体间信号传递的范例。Oncogene，20：1594[21] M. Hucka，A. Finney，H. Sauro和H.博卢里系统生物学标记语言，2001。http://www.cds.caltech.edu/erato/sbml/docs/index.html。[22] J. D. Jordan，E. Landau和R.艾扬格信号网络：细胞多任务的起源。Cell，103：193[23] M. Kanehisa，S. Goto，S. Kawashima和A.中谷基因组网络上的KEGG数据库。核酸研究，30：42[24] P·卡普Biocyc网站，2002年。biocyc.org网站。[25] P. D. 卡普路径数据库：计算符号理论的案例研究Science，第2040-2042页[26] P. D. 卡普，S。Paley和P.罗梅罗路径工具软件，2002年。出版中。[27] K. W. 科恩控制哺乳动物G1/S细胞周期相变的分子网络组件的功能能力Oncogene，16：1065[28] K. W. 科恩哺乳动物细胞周期控制和DNA修复系统的分子相互作用图分子生物学细胞，10：2703[29] W.科奇有意义的关系：通过蛋白质相互作用调节Ras/Raf/MEK/ERK通路。Biochem J. ，351：289[30] P. Lincoln和A.蒂瓦里三角形切口侧抑制机制稳定性分析的自动化技术，2002。正在筹备中。[31] L. 阿乐用于电子和蜂窝信号网络的软件Science STKE，PE 11，2002.[32] L. 洛 克 湖 Eiden 和 M. 戴 霍 夫 - 布 兰 尼 根 探 路 者 ， 2002 年 。 得intramural.nimh.nih.gov/lcmr/smn/special_projects.html 余弦值.[33] H. H. McAdams 和A. 阿金 太吵 了！在 纳摩 尔尺度 上的 遗传调 控。 TrendsGenet，15：65[34] H. H. McAdams和L.夏皮罗遗传网络的电路模拟。Science，269：650[35] R. Overbeek，N.拉森湾D. Pusch，M. 小塞尔科夫N. 克尔皮德斯，M. Fonstein，N. Maltsev和E.塞尔科夫WIT：用于高通量基因组序列分析和代谢重建的集成系统。核酸研究，28：123埃克和阿里160[36] T. Pawso