Bio-PEPA模型的基于质量守恒的静态分析方法

可在www.sciencedirect.com在线获取理论计算机科学电子笔记296（2013）107-126www.elsevier.com/locate/entcsBio-PEPA质量分析的守恒性艾伦·克拉克1简体中文CH Waddington Building，Kings Buildings，爱丁堡，苏格兰斯蒂芬·吉尔摩2爱丁堡大学信息学院10 Crichton Street，爱丁堡，苏格兰Maria Luisa Guerriero3系统生物学爱尔兰，康威研究所大学学院都柏林，贝尔菲尔德，都柏林4，爱尔兰。简·希尔斯顿4爱丁堡大学信息学院10 Crichton Street，爱丁堡，苏格兰摘要基于质量守恒的概念，对Bio-PEPA模型进行了静态分析。不遵守质量守恒定律可能表明模型描述中存在错误。在这里，我们专注于使用不变量分析来识别模型中的潜在错误。我们扩展的基本技术，考虑开放的模型，其中有可能自动忽略一些原因的大规模生产或消费，不太可能是错误的。 我们的方法是一种改进不变量分析的直接应用，因为它不依赖于对模型的深入理解和对应该具有守恒质量的组件集合的先验期望。 我们证明了使用我们的技术对一个已发表的模型从文献中，并解释我们的分析如何可以用来发现潜在的问题，在模型描述。当然，并非所有不能保持质量的模型都是令人敬畏的。然而，这是一种重要的模型验证方法，可以在模型本身评估之前应用-因为分析不依赖于精确的动力学，它可以在模型开发过程的早期进行，在模型完全参数化之前。关键词：生物PEPA1电子邮件：A.D. ed.ac.uk2电子邮件：Stephen. ed.ac.uk3电子邮件：Maria. ucd.ie4电子邮件：Jane. ed.ac.uk1571-0661 © 2013 Elsevier B. V.在CC BY-NC-ND许可下开放访问。http://dx.doi.org/10.1016/j.entcs.2013.07.008108A. Clark等人理论计算机科学电子笔记296（2013）1071介绍随着系统生物学建模方法的复杂化，以及实验技术收集更多关于生物功能的数据，构建的模型变得越来越复杂。使用高级建模语言（例如过程代数）而不是低级数学（例如普通微分方程）的优点之一在于，该语言促进自动化技术以支持建模者构建忠实于其意图的模型即她目前对生物机制的理解。本文关注的是一种特殊的静态分析的动态生物模型，旨在发现问题和错误的模型描述尽早在模型开发过程中，特别是在模型模拟产生分析结果。我们的分析关注的是模型中的质量守恒和使用不变生成来识别模型中可能违反质量守恒原理的物种或反应的定义。我们只对自动分析程序感兴趣，这些程序可以在没有人为干预的情况下应用，并在实践中以可接受的效率自动化。然后，这些程序可以应用于模型开发过程中产生的生物模型的每个版本我们以前[9]考虑过使用静态和动态分析相结合的方法来验证Bio-PEPA模型。在本文中，我们扩展了静态分析的剧目。分析的一个重要组成部分是在模型中生成化学物质的不变量的能力，这些不变量识别出在整个模拟过程中总量保持不变诸如此类的不变量可以使用傅里叶-莫茨金消除程序[12]从模型中的化学计量信息计算这是一个数值线性代数的程序，它对化学计量矩阵进行运算，以计算物种不变量和反应不变量。众所周知，傅立叶-莫茨金程序在最坏情况下具有双指数运行时间，但对于小型或中型模型，我们总是发现算法的运行时间在实践中是可以接受的。1.1相对于最新技术水平许多从事生物模型静态分析的研究人员一直在生成不变量并通过肉眼检查这些不变量。因此，尽管不变量的计算是自动的，但建模者直到现在还面临着决定已计算的不变量是否是该模型的预期不变量集的问题。如果这些匹配，那么建模者就确信模型已经按照预期构建。如果它们不匹配，则表明在构建模型时发生了错误目前这种常见做法的困难是，知道哪种不动产-A. Clark等人理论计算机科学电子笔记296（2013）107109蚂蚁通常需要强大的数学推理技能和深入的生物领域知识的结合，这使得决定计算的不变量是否暗示模型中的错误成为一项重要的任务。除此之外，标准的不变量分析并不那么容易解释开放生物系统的模型，在这些模型中，物质通过源流入模型，并通过汇再次流出。然而，这些模型是完全合法的，因此我们希望我们的分析也适用于这些模型。本文的创新之处在于(i) 将依赖于人类专业知识和技能的应用的不变评估问题转换为可以完全自动化以给出是或否答案的决策问题;以及(ii) 设计了一个程序，将不变量分析应用于开放生物系统的模型，该模型将问题限定为可以完全被物种不变量覆盖的封闭模型本文中的讨论集中在过程代数Bio-PEPA [7]中编写的模型上，该过程代数旨在特别适用于模拟生物系统，如信号通路。然而，所述的大部分内容适用于其他类型的建模范例，特别是可以转换为SBML模型的模型。事实上，由于这是一个定性分析，我们只需要化学计量矩阵的知识。2相关工作不变量生成和分析经常应用于Petri网建模[19]，也适用于生物过程模型[15，14]。不变量可以用于一系列分析目的（参见[2]的调查），包括指导大型模型的模块化分解[13]。不变量生成的大多数实现需要模型5的完整化学计量描述，并且使用Fourier-Motzkin过程从该描述向前工作以生成一组不变量。相比之下，Traviando跟踪分析工具[17]包含一种新的基于时间的算法，可以从离散随机模拟生成的跟踪中推断出一组不变量由Peter Kemper执行的傅立叶- Motzkin消除程序包含在Bio-PEPAEclipse插件的Bio-PEPA工具套件中[6]。我们在这里使用的是一种高级语言，它给了我们一个可以考虑的优势，即能够在模型的不同视图之间切换，以及在动态分析的不同状态之间切换。后者已经被证明是有价值的，在检测以前未知的问题与生物模型的分析[4]。为了发现误差而直接使用ODE模型的论文似乎相对较少，并且当这样做时-5在Petri网术语中，关联矩阵。110A. Clark等人理论计算机科学电子笔记296（2013）107|真矩阵描述了这种错误所施加的子空间。这里所需要的大多数方法对大多数生物学家来说都是相对陌生的，并且不是自动化的。与此相反，我们有自动化的方法，涉及到众所周知的概念保守的部分，熟悉的生物建模。3Bio-PEPA语言Bio-PEPA [7]是一种用于生物化学系统建模和分析的随机过程代数我们在这里简要概述了该语言的主要特征。关于其语法和语义的详细介绍，请参见[7]。在生物化学系统的Bio-PEPA模型中，每个分子种类（即蛋白质、基因、mRNA）由过程表示。系统在给定时间的状态由分子种类的当前量给出，并且生化反应发生的结果是所涉及种类的可用量的变化。过程通过共享的动作名称相互作用，动作名称代表反应并指定它们在反应中的作用（反应物、产物、催化剂、抑制剂等）。和它们的化学计量系数。反应发生的结果是根据化学计量6减少反应物的量并增加产物的量。Bio-PEPA中的物种数量可以是浓度（连续语义）或分子计数（离散语义），因此允许基于微分方程的数值方法以及通过使用Gillespie算法的随机模拟或通过底层连续时间马尔可夫链的数值评估进行的随机分析对于每个生物化学物种，建模者指定物种参与的反应集以及物种在每个反应中的作用。每个反应都与一个动力学定律相关联，该定律规定了该反应的发生率。形式上，Bio-PEPA系统的主要组成部分是物种组成部分，描述每个物种的行为，以及模型组成部分，指定所有相互作用和物种的初始数量Bio-PEPA组件的语法由下式给出：S：：=（α，κ）opS|S + S |C，OP = ↓|↑ | ⊕ |G|ⓈP：：=PDP S（x）我其中S是物种组分，P是模型组分。 在prefix term （α，κ）opS，κ是反应α中物质S的化学计量系数，fix combinator具体而言，↓表示反应物，↑表示产物，g表示抑制剂，g表示通用改性剂。符号αop 在物种S的定义中，S是（α，κ）opS[6]相对于反应的物质的化学计量表示该反应产生或消耗了多少该物质的分子。在Bio-PEPA中，每当发生反应时，语义自动调整物种的定量变量以反映化学计量A. Clark等人理论计算机科学电子笔记296（2013）107111def当k= 1时。运算符“+”表示可能的动作之间的选择，常数C由等式C d = ef S定义。过程PDQ表示组件P和Q之间的同步;集合I确定I上的活动其中操作数被强制同步， 表示同步所有常见的动作类型。在一个n≠tS（x）的模型中，参数x∈N表示S分子的初始数量。除了物种和模型组件之外，Bio-PEPA系统还包括动力学速率、参数以及（如果需要）位置、事件和物种的其他辅助复数有时用冒号表示，如E：S，但冒号只是名称中的一个字母，而不是运算符。在这里，我们使用下面的简单示例来说明基本概念。在Bio-PEPA中，由酶E催化的将底物分子Sin转化为产物分子P的反应S-E→P被建模为S=r1↓defP=r1↑defE=r1其中R1是与反应相关的名称。r1的动力学定律由米氏动力学r=kcat·E·S1KM+Skcat和KM是反应动力学常数。这表示S、P和E都参与了事件的发生反应r1的结果，而r1发生的结果是减少了总的酶E的作用是加速反应，但其量是不确定的。Bio-PEPA Eclipse插件[11]是用于Bio-PEPA模型开发和分析的软件框架。除了通过随机模拟进行动态时间序列分析和求解微分方程外，Bio-PEPA Eclipse插件还使建模人员能够执行静态分析-例如识别下文所述的不变量、源和汇。 有关Bio-PEPA语言和工具功能及其导入/导出格式的更多信息，请参见[3，6，11]。Bio-PEPA软件工具可从http://www.biopepa.org/获得。4不变量在本节中，我们将回顾关于Bio-PEPA模型的不变量的定义以及计算整个模型的不变量集的过程模型的不变量集通常在模型构建期间计算，以帮助模型验证。有两种计算不变量;状态112A. Clark等人理论计算机科学电子笔记296（2013）107Rdefdef不变量和反应不变量。一个状态不变量涉及模型中的一组组件或物种。在模拟过程中的任何时候，可以将状态不变量的分量的总体相加，结果总是相同的。考虑以下简单模型，左边是反应语法，右边是Bio-PEPA语法E+S−→ESE=r↓+rm↑+p↑ES−r−m→E+SpS=r↓+rm↑defES−→E+PES=r↑+rm↓+p↓defP=p↑在这个模型中，只有两个状态不变量：E+ES和S+ES+P。要看到这一点，请考虑象征性地结合生物PEPA对物种E的定义物种ES每一个↑反应的出现都与其相应的↓反应相匹配。当S、ES和P的定义结合起来时，情况也是如此。 相反，量E+S不是该模型的不变量，我们可以看到，当物种E和S的定义结合起来时，因为物种E的Bio-PEPA定义中的p↑项与S定义中相应的p↓项不匹配。更一般地说，一个状态不变量可以有一组系数，例如我们可以说（1×O2）+（2×O）是一个状态不变量。系数也可以是负的。我们可以知道，在一个模型中，A−B是不变的，其中物种A而B类只会一起反应不变量是一组反应，使得从模型可能达到的任何状态X，如果反应不变量中的每个反应中的一个被激发， 然后模型返回到X。在上面的示例模型中，只有一个反应不变量：r+rm，如下所示，E+ S−→rES−r−m→ E+ S。在状态不变量的情况下，反应不变量可以包括一组系数，使得一些反应可能需要多次触发以使模型返回到原始状态。请注意，反应以何种顺序进行并不重要。不包括在不变量中的反应可以穿插在不变量的反应中，在这种情况下，对模型状态的影响将与只发生穿插反应的情况相同，因此我们不会返回到原始状态，除非穿插反应本身形成反应不变量5不变量、源和汇在本节中，我们将详细介绍模型中组分和反应不变量与源和汇的关系一个模型可以同时具有源和汇。A. Clark等人理论计算机科学电子笔记296（2013）107113defdef为了便于阅读，我们将源和汇统称为抽头。分接头可以是基于组分的或基于反应的。一个组分源至少被一个反应消耗相反，组分汇是至少由一个反应产生但从未被任何反应消耗的组分Bio-PEPA的语法使得组件的识别taptrivial;一个分量是一个源，如果它的定义包含至少一个↓运算符，没有↑运算符，尽管它可能包含，g或。相反，汇分量的定义至少包含一个↑运算符，而不包含↓运算符。以下Bio-PEPA的片段强调了这一点。来源=a↓+b↓+c↓水槽=a↑+bg+c↑反应抽头的定义类似。也就是说，反应源是没有反应物但具有至少一种产物的反应简单地说，反应源产生一些东西，但不消耗任何东西，而反应汇消耗一些东西，但不产生任何东西。在Bio-PEPA语法中，虽然观察组分源和汇是微不足道的，但反应源和汇只能通过查看整个模型来但是Bio-PEPA软件提供了一个显示反应的模型的概要视图，在这个视图中，识别源反应或汇反应是微不足道的。在任何情况下，大纲视图都会列出所有组分和反应源和汇。下面的代码片段显示了两个反应，其中一个是源，另一个是汇。源反应：−→P1+P2汇反应：R1+R2−→5.1水龙头标记边界在构建模型时，建模者必须选择要包括物理系统的哪些特征。包含在其中的真实系统的组件称为模型组件。那些被排除在外的被称为外部组件或统称为外部环境。就其性质而言，模型在程度和范围上是有限的。外部组件基本上是模型中没有提到的所有内容。对于一个有用的模型，我们希望在物理系统中，外部组件对模型组件的影响可以忽略不计，或者这种影响可以忽略不计。这导致了模型组件和外部组件之间的边界，在这里，我们希望论证模型中的抽头代表了这种边界。(Note我们并不是说这样的边界只由模型中的抽头表示。 反应汇形成模型组件之间的自然边界，外部环境。这是因为从模型A的角度来看，114A. Clark等人理论计算机科学电子笔记296（2013）107反应槽正在从系统中移除质量。实际上，质量并没有减少到零，但它减少到的物种是一个外部组件，因此没有在模型中提到。对于反应源当然也是如此。质量不是从无到有产生的，而是由模型中没有提到的外部组件产生的。5.2不变量a由抽头任何一个改变组分抽头的反应都不能涉及任何反应不变量。其原因很简单：如果一个组分P是一个源，那么任何改变P的反应r都必须减少P的粒子数，因为不存在增加组分源的粒子数的反应在反应r激发之前，组分P的初始布居数永远不能通过模型中其他反应的任何组合来恢复因此，反应r不能参与任何反应不变量。同样的道理也适用于组件汇。然而，分量抽头可以涉及分量不变量。反应抽头可以是反应不变量的一部分，但是被列为反应抽头的反应物或产物的组分不能形成组分不变量的一部分。当我们考虑反应源r时，推理是相当简单的。 如果r修改了P的人口，它必须增加人口P，因为r是反应源。作为一个源，r不能减少任何其他组分的布居。其结果是，任何假定的不变量，其中涉及P也将有其值增加了一个触发r，因此将不会是一个不变量。类似的推理适用于r是汇反应的情况。然而，正如分量抽头可以涉及分量不变量，反应抽头可以涉及反应不变量/循环，如在：源反应：−→P汇反应：P−→5.3去除反应和组分在建模时，有时需要从模型的描述中删除一个组件或一个反应。这样做可以看到它对模型评估的影响。移除可以手动完成，或者可以在建模软件中自动完成。在本节中，我们简要描述了从Bio-PEPA模型中移除组件和反应，然后如何影响不变量。去除一个反应很简单：简单地删除动力学定律并通过从组件定义中删除相应的反应行为来更新任何组件描述。下面显示了一个名为am的反应的移除。移除前的模型位于左侧;移除后的模型位于右侧。A. Clark等人理论计算机科学电子笔记296（2013）107115defdefdefdefdefdefdefdefE=a↓+am↑+b↑S=a↓+am↑ES=a↑+am↓+b↓P=b↑E=a↓+b↑S=a↓ES=a↑+b↓P=b↑如果我们去掉一个物种参与的唯一反应，那么这个物种就变成了一个常数，等于它的初始种群。删除一个组件只涉及删除该组件的定义。在Bio-PEPA中，这自动涉及更新涉及删除的组分的任何反应的反应描述。这就提出了一个问题，即应该对涉及删除的组分的布居的动力学定律做些什么。在大多数情况下，它可以安全地从动力学定律中删除。由于我们的主要分析是无比率分析，因此对这一问题的进一步处理超出了本文的范围。当我们从模型中删除一个反应时，计算出的不变量集会发生什么第一个观察结果是，通过从模型中删除一个反应，我们不能使一个分量不变量无效：任何先前形成分量不变量的分量组(If我们从一个模型中去掉所有的反应，那么所有的成分都有恒定的种群。）上面的例子说明了这一点，我们可以看到，在左手和右手模型中，组件不变量是相同的-E+ES和S+ES+P-。我们的第二个观察是，通过移除一个反应，我们可以创建更多的组分不变量，如果我们移除一个违反不变量性质的反应，并且没有其他违反候选不变量性质的反应反应不变量被反应不变量内的任何反应的去除所破坏，但不被反应不变量内的任何反应的去除所干扰。当一个组件从模型中移除时，计算出的不变量集会发生什么变化？如果被移除的组件是组件不变量的一部分，那么自然地，该不变量可以被无效。然而，组分的去除不会破坏任何不涉及它的组分不变量，也不会破坏任何反应不变量。然而，它可能导致不变量分析将先前的单个（反应或组分）不变量报告为两个或更多个不变量。这是因为分析过程报告了最小不变量的集合，尽管不变量不会因移除组件而失效，但它可能不再是最小不变量。6质量守恒我们已经讨论了模型的不变量和作为模型的源和汇的抽头。我们还讨论了从模型中去除组分或反应对不在本节中，我们结合116A. Clark等人理论计算机科学电子笔记296（2013）107这些概念，以检查模型的一致性。在对模型进行了不变量分析之后，我们可以检查质量是否守恒，因为模型中的每个组件都应该被至少一个不变量覆盖。然后，我们可以通过将模型中的所有分量不变量求和来获得覆盖整个模型的单个不变量。这为我们提供了一个方便的静态分析一致性检查的各种生物模型。这种检查总是适用的：不变量总是可以求和，因为两个常数的和是一个常数。然而，由于它们的有限范围，在生物模型中，质量往往不守恒。发生这种情况是因为质量损失或从外部组件获得，而这些组件不在模型范围内。发生这种情况的一种简单方式是进行生产或降解反应，其产生或去除一个或多个模型组件的质量这些反应表现为源反应和汇反应，并且是模型中质量似乎不守恒的原因正如我们之前所观察到的，从模型中删除反应并不会使任何组分不变量无效。我们利用这一点，从模型中删除所有的抽头反应，即所有的源和汇反应。一旦我们做到了这一点，我们就从模型中去掉了任何可以生产或消费质量的明显手段。在去除抽头反应的模型上执行不变分析应该会给我们总的不变覆盖。也就是说，结果模型中的所有组件都应该被至少一个不变量覆盖。如果不是这种情况，则意味着质量是在模型内部产生或消耗的6.1分析步骤本节总结了使用质量守恒分析在模型中检测、查找和修复锯齿的步骤。• 运行不变式检查。软件会自动忽略所有的敲击反应并计算出一组不变量。如果某个不变量未覆盖模型中的所有组件，则会发出警告，表明模型不守恒质量。此外，建模者被示出未被任何不变式覆盖的模型组件的集合。• 对模型中的每个反应重新运行一次不变式检查。每个分析忽略模型中的所有抽头反应加上一个非抽头反应。每个分析给出一组不被任何分量不变量覆盖的分量所有这些集合都等于（或子集）的物种，不包括任何不变量时，没有非抽头反应被忽略。这需要对模型中的每个反应运行不变分析这在实践中是可以容忍的;在我们的案例研究中，在传统的台式计算机上分析模型所需的时间不到一秒钟。• 这提供了可能导致损失的可疑反应列表 或者模型中的大规模生产。 仔细看看这份清单， 两个相似的反应。它们的成分应该是相似的A. Clark等人理论计算机科学电子笔记296（2013）107117参与者和通过忽略这两个反应中的任何一个而产生的未覆盖组件的集合中可以在忽略所有抽头反应加上这样的对中的两个反应的同时执行不变量检查。仔细检查任何反应（或反应对），其去除导致分析确定质量守恒。• 如果发现反应定义错误，则更新模型描述以修正反应并重新运行质量守恒分析。在Bio- PEPA中，修改反应包括修改组分定义，以添加或删除作为反应反应物或产物的组分。如果模型足够先进，以至于反应的速率定律已经被写出来，那么现在是更新与修改后的反应相关的速率定律的好时机。Bio-PEPA软件可以再次帮助这一点，因为当速率定律表达式不包含对反应物的引用或包含对非反应物的引用时会这一点在[10]中有更充分的讨论7为例在本节中，我们提供了一个案例研究来说明我们的技术。 考试- Ple模型已经使用我们以前的不变量分析技术进行了分析[9，10]。 我们更新了这里的案例研究，包括我们在质量守恒分析中发现模型中特定的锯齿的方法，特别是这种分析如何引导我们找到模型中的错误部分我们的方法直接从微分方程的正式文本工作，不需要额外的图形表示或其他补充的非正式设计。当然，我们建议使用高级语言，如进程代数或Petri网，并从这些语言中生成微分方程，但许多从业者都是从ODE模型开始的。我们在案例研究中考虑的模型在[5]中被呈现为一系列普通的微分方程，我们首先必须将其手动转换为Bio-PEPA模型。这一步代表了模型中另一个潜在的干扰源，我们希望在进行任何定量分析之前检测到这一点。逻辑示意图变量名从ODE中保留。这些与图1中的（生物学）有意义的名称有关。Bio-PEPA软件计算的模型轮廓见图2。这包括两个额外的反应r20alt和r29alt，它们代表了[10]中报告的早期模型验证的可能改进。这里的目的是代表在评估模型结果之前发现模型误差所使用的方法。7.1初始不变量分析我们最初的不变量分析可能会提供一些线索，这个模型的准确性不变量分析的结果给出了6个分量不变量和11个未被任何不变量覆盖的分量，如图所示3 .第三章。118A. Clark等人理论计算机科学电子笔记296（2013）107M1 TNFαM2 TNFR 1M3TNFα/TNFR1M4 TRADDM5TNFα/TNFR1/TRADDM6 TRAF2M7TNFα/TNFR1/TRADD/TRAF2M8 IKKM9TNFα/TNFR1/TRADD/TRAF2/IKKM10 RIP1M11TNFα/TNFR1/TRADD/TRAF2/RIP1M12 TNFα/TNFR1/TRADD/TRAF2/RIP1/IKKM13 IKKαM14 Iκ B/NF-κBM15 Iκ B/NF-κB/IKKκ BM16 Iκ B-PM17 NF-κBM18 RIP1/Caspase-8M20 RIP1cFADDM22 Caspase-8M23 TNFα/TNFR1/TRADD/FADDM24 TNFα/TNFR1/TRADD/FADD/Caspase-8M25 Caspase-8M26 Caspase-8β/E表达载体M27 E转向架M28 DNA片段化M29 E载体M31 c-IAP/c-IAPFig. 1. 模型中的ODE变量名和生物变量名有未被发现的物种这一事实可能会让我们感到担忧，但我们注意，其中一些是普通的预期，例如，组分M 31参与汇反应：r 29 alt，M 31−→，组分M 5参与汇反应：r 20，M5 −→。我们不能指望这两个组成部分中的任何一个包含在任何状态不变量中。然而，当我们重复这个分析时，选择忽略所有的敲击反应，我们发现同一组不变量和同一组由任何不变量所揭示的成分。这消除了未覆盖的组件是由在模型组件和外部环境之间的边界处大量生产或消耗换句话说，我们的模型在模型组件中产生或消耗质量虽然我们需要对模型和不变定律有相当深入的理解，才能预测模型中预期的不变量集，但我们只需要相对较浅的理解，就能知道我们期望模型分量保持质量守恒7.2成分还原分析在本节中，我们通过迭代地重新分析模型的不变覆盖率，同时连续删除每个反应，缩小了在我们的系统中检测到的质量不守恒的原因我们对每一个非敲击反应重新分析一次。在每次运行中，忽略所有抽头反应加上一个其他非抽头反应。我们称之为“简化分析”，因为模型小于整个原始模型。它是合成的，因为我们每次只做一个反应我们将使用L来表示未覆盖物种的原始集合。 表1示出了当为了以下目的而依次忽略每个反应时相对于L不变量检查。表中前三行的结果告诉我们，这些反应并不是导致质量不守恒的独立原因 这使我们的搜索范围从最初的31个非轻拍反应缩小到A. Clark等人理论计算机科学电子笔记296（2013）10711931种M1初始分子数= 30r1， M1 + M2→ M3r2， M3→M1 + M2M2初始分子数= 15r1， M1 + M2→ M3r13， M12→M2 +M4+M6+ M10 + M13r2， M3→M1 + M2r24，M 24→M 2+M 4+M 6+M 10 +M 21 +M 25M28初始分子数= 0（is-sink）r28，M 27→M28M 29初始分子数= 10r 25，M 25+M 29→M 26r 26，M26→M 25 +M 29r 29，M29→M 30r30，M 30→M 29 +M31M 5初始分子数= 0r20，M 5→r21，M 23→M 5+M 21r3， M3 + M4→M5r4， M5→M3 +M4r5， M5 + M10→M11r6， M11→M5 +M10r7， M5 + M6→M7r8， M7→M5 + M633例反应r19，M 17→M 31r2，M 3→M 1+M 2r20，M 5→r20alt，M 21→M 23r21，M 23→M 5+M 21r22，M 22 +M 23→M24r 23，M 24→M 22+M 23r24，M 24→M 2+M 4+M 6+M 10 +M21 +M 25r25，M 25 +M 29→M26r 26，M 26→M 25+M 29r 27，M 26→M22 +M 27r 28，M27→M 28r29，M 29→M 30r29alt，M 31→...19反应省略4水槽M16M19M20M282沉行动r20，M 5→r29alt，M 31→...26种遗漏图二.从TNFα介导的NF-κB信号转导途径的Bio-PEPA模型推断的大纲视图的压缩空间版本。 在[10]中报告的早期模型验证过程中，已将r20alt和r29alt反应添加到 Bio-PEPA模型状态不变量：(i)M21 +M 23 +M 24(ii)M12 +M 13 +M 15 +M 8+M 9(i)M14 +M 15 +M 16(iv)M18 +M 22 +M 24 +M 25 +M 26（v）M26 +M 27 +M 28 +M 29 +M30(vi)M10 +M 11 +M 12 +M 18 +M 22 +M 24 +M 26 +M 29 +M 30未覆盖的物种：• {M1，M 17，M 19，M 2，M 20，M 3，M 31，M 4，M 5，M 6，M 7}120A. Clark等人理论计算机科学电子笔记296（2013）107图三.用Bio-PEPA Eclipse Plug-in计算TNFα介导的NF-κB信号转导通路A. Clark等人理论计算机科学电子笔记296（2013）107121忽略的反应未覆盖组件集r1... R 17Lr 25... 第二十八条，Lr20， r22， r23，r29alt， r31Lr18， r24L− {M19，M 20，M 6，M 7}R19L− {M17}r20alt{M17，M 31}R21L− {M1，M 3，M 5，M7}r29， r30L− {M17，M 31}表1该表显示了忽略每个反应对任何不变量未覆盖的组分集的影响。只有反应r18， r24， r19， r20alt， r21，r29和r30的去除才有效果。七个反应这些反应是：r18：M18−→M 19 +M 20 +M 22r24：M24−→M 2+M 4+M 6+M 10 +M 21 +M 25r19：M17−→M 31r20备选：M21−→M 23r21：M23−→M 5+M 21r29：M29−→M 30r30：M30−→M 29 +M 31表1中的一个有趣之处在于，有两行由一对反应组成，即：{r18，r 24}和{r29，r30}。去除这两个反应中的任何一个都可以“第一对似乎无关，然而，检查第二对，我们看到一个简单的环，它产生了质量。反应r29消耗M29生成M30，反应r30在生成原始M29和额外的M31时消耗M30。 这似乎是模型中的一个定理，要么反应r29也应该消耗M31，要么反应r30不应该产生M31。 当然，为了真正确定这条定律，人们必须首先充分理解模型的意图。 然而在这种情况下 我们可以重写这两个反应，给出所涉及的组分它们的描述性生物学名称。r29：E矢量−→E矢量-IAPr30：E介电常数-IAP−→ E介电常数+c-IAP从这两个反应中，我们谨慎地选择修改反应r29以消耗c-IAP。122A. Clark等人理论计算机科学电子笔记296（2013）107忽略的反应未覆盖组件集r1... R 17Mr19... R 20Mr22， r23Mr26， r31Mr18， r24M− {M6，M 7，M 19，M20}R21M− {M1，M 3，M 5，M7}r20alt{}表2该表显示了忽略每个反应对一组组分的影响，这些组分未被具有反应r29的校正版本的模型的任何不变量只有消除反应R18、 R24、 R21和R20alt具有任何效应。做了这个修正之后，我们重新分析了模型，仍然没有被保存下来。这符合我们的预期，因为我们已经纠正了组件M31的生产。然而，在最初的模型M31只参与自己的生产。因此，存在其他未覆盖组件的事实不可能是由该单个组件的生产引起的。因此，我们再次执行这些步骤，并找到与表1相似的表。表2显示了原始表的更新版本，用反应r29的校正版本对模型进行时间另外M=L− {M 17，M 31}。表2中最重要的兴趣点是反应r20alt的结果。移除r20alt意味着不变量分析计算出质量在模型中是这强烈暗示r20alt或相关反应。然而，一个单一的反应本身是不可能出错的，只有三个其他的反应改变了未被覆盖的组分的集合。我们先看r21，因为它似乎与r20alt关系最密切，而且r18和r24似乎是一对。两个反应r20alt和r21是：r20备选：M21−→M23r 21：M23−→M 5+M21和前面一样，我们已经确定了一个简单的循环：如果r20alt和r21都触发一次，模型将返回到相同的原始状态，但计数增加了M5。再一次的修正是，要么r20alt应该有M5作为反应物，要么r21不应该有M5作为产物。和以前一样，我们不能武断地说哪一个应该是这个模型的最佳修正，而是重写反应，A. Clark等人理论计算机科学电子笔记296（2013）107123M17M1M31M5M17M1M31M5TNF α原始2015TNFa校正r29201510 105 500TNFa校正的r20 alt2015TNFa两次校正201510 105 500图四、 四个模型的时间序列分析：（a）原始模型，（b）修正R29后的模型(c)修正了R20的模型;以及（d）修正了两个双方差的模型。 显然，从（d）中可以得出的生物学见解与从（d）中可以得出的见解是完全不同的。(a)与原始组件名称的关系给了我们一些指示：r20alt：FADD −→ TNFα/TNFR1/TRADD/FADDr21：TNFα/TNFR1/TRADD/FADD−→ TNFα/TNFR1/TRADD + FADDM5（TNFα/TNFR 1/TRADD）可能作为反应物r20alt缺失。在我们的模型中解决了这个问题后，我们重新分析了模型，正如预期的那样，分析返回了质量在我们的新模型中守恒7.3结果图4描述了TNFα介导的NF-κB信号转导途径模型的四个版本的时间序列分析结果。第一个版本是在我们开始任何质量守恒分析之前的第二个版本有一个反应r29的更新版本，它被引入来修复我们检测到的第一个反应。第三个版本根据我们发现的第二个平衡定律修正了原始模型，因此更新了反应r20alt。第四和最后一个版本更新M17M1M31M5M17M1M31M510203040506000 10203040 5060（一）（b）第（1）款10203040506000 102030405060（c）第（1）款（d）其他事项124A. Clark等人理论计算机科学电子笔记296（2013）107两个反应R29和R20交替表示内部保持质量的模型为了清楚起见，并不是模型中的所有物种都被绘制出来。有趣的结果是物种M5的种群发展。在前两个版本中，在粒子数最初下降后，M5被错误地排除在反应r20alt的反应物列表之外，这两个版本都恢复了，并稳定在超过10的平衡值。然而，当反应被固定为包括M5作为反应物时，M5的群体在稳定到小于5的平衡值之前只有短暂的恢复尝试。修正我们对反应R29的影响不太明显。8限制在本节中，我们将讨论我们的方法的局限性。没有静态分析可以检测模型中的所有锯齿，我们也不希望在这里这样做。此外，如果分析产生太多误报，任何警告模型中可能错误的静态分析几乎都变得当这种情况发生时，建模者很可能开始忽略分析结果。在本节中，我们讨论了可能存在误报的一些原因，我们认为这些并不会减损我们方法的一般实用性我们的质量守恒分析最明显的困难是，如果模型本身不被期望保持质量。当模型的规模高于分子水平时，例如细胞或甚至生物体水平，这是可能的。当使用生物学模型来测量人口水平与出生率和死亡率时，会出现合理的块，例如[8]中考虑了Bio-PEPA中的流行病学模型。在这些情况下，另一个例子是在细胞水平，其中单个细胞的生长和分裂成两个子细胞（胞质分裂）被建模。我们的分析依赖于将所有反应的集合划分为两组的过程;抽头和非抽头反应。这允许我们忽略从模型范围之外将质量引入模型组件的反应，或者将质量从模型中丢弃到外部环境中。反过来，这使我们能够专注于完全在模型范围内的反应，以确定质量是否守恒。如果反应相对于模型组分被正确地写下，那么我们的划分是保守的，在这个意义上，非抽头反应不会被错误地归因为抽头反应（尽管抽头反应可能被识别为非抽头反应）。这是正确的关系，因为抽头反应在分析中被忽略，所以我们最好保守地忽略太少而不是太多的反应。此外，可以明确忽略反应，如在组成还原分析步骤中所做的那样，参见第7.2节。A. Clark等人理论计算机科学电子笔记296（2013）1071259结论本文讨论了生物模型的静态分析方法，特别是确定所讨论的模型是否符合质量守恒定律。我们仔细地定义了真实系统中处于模型范围内的部分和不处于模型范围内的部分之间的边界。我们预计，质量可能会从模型组件损失到外部环境中，或者由模型组件从外部环境中获得。我们忽略导致这种损失或增益的反应，以确定完全在模型中描述行为的反应是否保持质量。如果我们确定模型不能保持质量守恒，那么我们就去寻找引起它的反应。这涉及质量守恒分析的组成应用，对于模型范围内的每个反应。对于每个反应，我们比较了质量守恒分析的结果，有和没有该反应。这可以大大缩小对模型中错误反应的搜索范围。我们认为，我们的分析有几个优点。这是一种定性分析，这意味着可以在开发的所有阶段对模型进行分析，特别是在确定甚至估计参数此外，我们的分析是相当便宜的，虽然正如我们以前注意到的[10]，在最坏的情况下，使用的不变分析可以是指数的，实践表明，这很少发生。不变量检查可以在典型的台式计算机上有效地执行，对于涉及40多个反应的模型来说，这是即时的。守恒分析检查可以自动执行，而无需了解模型。一旦确定存在故障，甚至可以在不详细了解模型性质的情况下进行查找。为了修复错误而实际修改模型当然需要了解建模者的意图然而，我们希望在这里指出的一点是，不变量分析和质量守恒的一般期望很好地结合在一起，形成了对模型的自