生物系统的并发约束过程演算：建模、验证与分析 - 理论计算机科学电子笔记117-137

理论计算机科学电子笔记171（2007）117-137www.elsevier.com/locate/entcs分析生物系统的尤利亚和我一起去，乔戈A。 P'ereza，CamiloRueda a和FrankD. 瓦伦西亚b队a哥伦比亚卡利哈韦里亚纳庞蒂菲西亚大学计算机科学与工程系bCNRS和LIX、E′colePolytechnique、Palaiseau、France摘要在本文中，我们提出了我们的第一种方法来建模和验证生物系统使用ntcc，并发约束过程演算。我们认为ntcc中的部分信息结构可以为这类系统提供一种合适的语言。我们还说明了ntcc如何为生物系统的分析提供一个统一的框架，因为它们可以使用微积分关键词：过程演算，生物系统验证，部分信息，并发约束编程（CCP）1介绍部分信息在描述生物系统时自然出现。 在对这些系统建模时，可以区分两种主要的部分信息：定量和行为。虽然部分定量信息通常涉及关于系统状态的不完整信息（例如，变量可以取的可能值的集合），部分行为信息指的是与交互行为相关联的不确定性（例如，两个系统相互作用的未知相对 找到表达这些类型的精确方法 部分信息的分析有助于更好地理解生物系统中常见的复杂模式行为。部分信息是并发约束编程（CCP）[19]的一个核心特征，CCP是一种完善的并发形式主义在CCP中，过程通过告知和询问表示为约束的部分信息（例如，x42）。CCP最吸引人和最显著的特点可能是它将传统的过程演算操作视图与声明性视图相1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.05.012118J. 古铁雷斯等人理论计算机科学电子笔记171（2007）117基于逻辑。换句话说，过程项可以同时被视为计算代理和逻辑公式。这种结合使CCP能够从大量的过程演算和逻辑技术中受益。由于这些原因，CCP可以成为描述和推理生物系统的方便框架。在本文中，我们提出了ntcc[14]，一个基于CCP的时间进程演算，作为一种适合分析生物系统的语言。在ntcc中，上述类型的部分信息被自然地捕获。一方面，部分定量信息被约束系统的概念所捕获，约束系统是一种在约束上提供连贯性和定义（逻辑）推理能力的结构由于约束系统是ntcc的参数，通过选择适当的约束系统，可以在不同的详细程度上说明几种条件。这在描述定量信息时可能特别有用。例如，我们可以考虑在微分方程上的约束系统与在整数或实区间上的其他约束系统相互作用。另一方面，部分行为信息由ntcc中可用的非确定性和异步运算符表示。这些算子在离散时间内的相互作用NTCC允许明确地描述和推理许多生物现象发生时间的不确定性。此外，ntcc提供了推理技术来证明给定的过程P满足给定的性质F。事实上，微积分运算出一个线性-时间的规范逻辑及其相应的证明系统，在这个系统中可以正式地进行可达性分析。可达性分析是生物学背景下的核心。例如，考虑细菌转录：它可以被看作是一个可达性分析问题，其中人们想知道在给定的基因调控网络中是否有可能的基因表达。我们将利用这些特点，将生物系统建模为过程，将其属性建模为线性-时间公式，所有这些都在一个框架中。也就是说，ntcc为生物系统提供了一种与强大的推理技术紧密相关的描述语言。使用ntcc来研究生物系统的另一个优势在于，可以将这个理论框架转化为软件工具。事实上，AVISPA研究小组1（作者是其中的成员）最近建立了一个原型工具[2，3]，它允许描述表达为ntcc过程的生物系统，并允许观察它们随时间的行为。本文的主要贡献是将ntcc作为研究涉及部分信息的生物系统的统一框架，并展示其结构如何自然地捕获许多生物现象。更具体地说，我们建议使用约束系统来表示部分定量信息，并将部分行为信息建模为非确定性和异步过程。我们将钠-钾泵[20]，一种在真核细胞中促进主动转运的机制，作为我们方法适用性的一个令人信服的例子。事实上，我们将使用推理系统来给出一个1网址：http://avispa.puj.edu.coJ. 古铁雷斯等人理论计算机科学电子笔记171（2007）117119在不可预测的恶意代理存在的情况下，泵发生一般故障的证据。相关工作近年来，一些过程演算，如π演算[17，18]，BioAmbients [16]，Brane演算[7]，Beta binders [15]和κ演算[8]，作为生物学的描述语言已经被研究。然而，这种其他基于约束的演算已经在生物学背景下进行了研究。例如，在[5，10，4]中，hcc演算[11]被用于研究动态系统。然而，由于hcc不提供非确定性/异步操作符，表示部分行为信息变得困难。只有在这样的作品之一（[5]）中，hcc的逻辑性质被利用，使用模型检查方法对生物系统进行但是，没有使用证据系统或类似程序。其他涉及在生物学背景下使用逻辑的作品是[1]和[6]。一方面，[1]提出使用混合自动机来建模和分析生物系统的行为Simpathica [13]等支持工具 另一方面，在[6]中，提出了一种用于描述生物系统的基于规则的语言推理技术包括三个独立的语义结构（每一个都有相关的逻辑），它们的使用取决于所需的详细程度。我们相信，通过在系统描述中适当地使用约束系统，在保持相同的统一框架的情况下，在多个细节层次上的分析是可能的。本文件接下来描述ntcc过程演算：上面给出的直觉，关于使用ntcc对生物系统进行建模和验证，得到了彻底的解释。第3节总结了关于NTCC过程的规范和验证的主要结果。它们将在第4节中使用，其中介绍了钠钾泵。在这一节中，我们提出了这样一个系统的ntcc模型，以及验证这个模型的非平凡属性，使用上述推理系统。第5节结束。2ntcc作为描述生物系统在这一节中，我们将介绍ntcc过程演算，并通过实例展示它如何成为一种用于建模生物现象的适当语言。为了空间的缘故，本文省略了一些形式上的细节;[14]中给出了对ntcc让我们从ntcc中反应式计算的直观描述开始。在ntcc中，时间在概念上被划分为离散的时间间隔（或时间单位）。在一个特定的时间单位中，进程P从环境中得到一个输入（一个表示为约束的信息项）c，它以这个输入作为初始120J. 古铁雷斯等人理论计算机科学电子笔记171（2007）117存储，并且当它到达其静止点时，它将结果存储d输出到环境。静止点确定剩余过程Q，其然后在下一时间单元中执行。信息不会自动从一个时间单位转移到下一个时间单位在CCP中，一个基本概念是约束系统。直观地说，约束系统提供了一个签名，可以从中构造约束，以及一个指定它们之间相互依赖关系的蕴涵关系。更正式地说，一个约束系统是一个对（，Δ），其中是函数和谓词符号的签名，Δ是关于的可判定理论。给定一个约束系统（λ，Δ），设（λ，V，S）是它的底层一阶语言，其中V是变量x，y，.的集合。. ，S是逻辑符号的集合，其中，约束c、d、. 是这个一阶语言的公式。 我们说c在Δ中包含d，记为c| = d，i cd在所有Δ模型中均为真。出于操作原因，我们将要求|=可以决定。Hint，C表示底层约束系统中的约束集。一个广为人知的约束系统是FD [12]。在FD中，变量被假设在有限域上变化，除了等式之外，我们可能有谓词将变量的可能值限制在某个有限集合中。更正式地说，FD[n]（n> 0）是约束系统，其中n由常数符号0，. ，n − 1以及等式=，而Δ由方程理论的公理x = x，x = y <$y = x，x = y<$y = z<$x = z，和v =w <$false给出，对于每两个不同的常数v，w ∈ <$。 直觉FD[n]提供了一种在有限值域{0，.，n-1}，在这些值上语法相等。2.1工艺流程过程P、Q、. 从底层约束系统中的约束c∈ C和变量x∈ V通过以下方式构建：ΣP，Q，. * =告诉（c）|当ci做Pi时|PQ | local x in Pi∈I|除非c下一个P |unless c next P|！|! P下面我们提供一些关于ntcc过程行为的直觉。包含和查询（部分）信息进程tell（c）是表示部分信息的最简单操作，它在当前存储中包含一个约束c，从而使其在相同的时间间隔内可用于其他进程。在生物学背景下，告诉操作允许表示至少两种部分信息陈述：所谓的基本规则和状态定义状态。第一个条件精确地陈述了在生物系统的生命过程中适用的某些条件。这里有明显的优势。另一个生物学上的结石是，J. 古铁雷斯等人理论计算机科学电子笔记171（2007）117121这些条件可以通过利用可用的（可能不完整的）知识来表示。例2.1设过程M=tell（l pHinl<$2时，则为（u=u−k1）。非确定性选择非决定论是一种很有价值的方法，它表示从同一初始状态开始的几种可能的作用过程，而不提供关于如何选择其中一种过程的 在ntcc中，非确定性行为是通过当c做P时的一般化过程：一个保护选择求和Σi∈I，当ci做Pi时，其中I是索引的有限集合，表示一个过程，在当前时间间隔，必须非确定性地选择Pj（j∈I）之一其对应的约束条件cj由存储所包含。所选择的替代品，如果有的话，排除其他的。如果没有选择，则求和Σ被排除在外我们使用i∈IPi作为“盲选”过程的缩写Σi∈I 当Pi为真时。我们使用skip作为空求和的缩写而在生物学背景下，谨慎选择和部分信息的结合122J. 古铁雷斯等人理论计算机科学电子笔记171（2007）117表示一种适当的机制，以形式化系统交互中固有的不可预测性。在这个意义上，非确定性是明确表示部分行为信息的一种方式。下面的例子说明了这些想法。例2.2下面的过程P是一个生物系统的抽象模型：在一定量的ATP存在下（即，能量），系统释放酶;在存在一些ATP并且一些电化学梯度的条件适当的情况下，它发出正信号：当ATP> 0时，说明（releaseEnzyme = 1）P=+当ATP> 0时，则elecGradient = 1 do tell（emitSignal = 1）。P的演化取决于当前存储中的信息。最简单的情况是（空）存储为true：P不能添加任何进一步的信息。在存储d =（ATP ≥ 50）中，P导致存储变为d（releaseEnzyme= 1），因为在第一个替代方案中，（ATP ≥ 50）|=（ATP> 0），并且第二备选方案的保护不需要从d。有趣的情况是当P中的两个保护都被启用时;如存储e=（ATP>0 ） （ elecGradient = 1 ） 。 根 据 选 择 执 行 哪 个 进 程 ， 最 终 存 储 可 以 是 e（releaseEnzyme = 1）或e（emitSignal = 1）。基于部分信息，P构成了不可预测行为的简洁表示。通信过程P→Q表示P和Q的平行合成。在一个时间单位P中和Q并发地操作查询信息。我们使用i∈IPi，其中I是索引的有限集合，来表示所有Pi的平行合成。例2.3假设过程P如例2.2和下面的过程阿Q：当releaseEnzyme = 1时，do tell（promoteReaction = 1）Q=+当emitSignal = 1时，执行tell（promoteReaction = 0）。非正式地说，一旦检测到酶的存在，Q就促进反应发生，如果特定的信号过程被激活，Q就反对这种反应。存储e=（ATP> 0）（elecGradient = 1）中的并行合成PQ由于P中的选择保证了releaseEnzime = 1或emitSignal = 1的存在，因此进程PQ将导致存储变为e（releaseEnzyme = 1）（promoteReaction = 1）或e（emitSignal = 1）（promoteReaction = 0）。J. 古铁雷斯等人理论计算机科学电子笔记171（2007）117123我本地信息在ntcc中，就像在大多数进程演算中一样，有一个构造来限制进程之间可以相互作用的接口，从而允许对本地行为进行P中局部x形式的过程的行为类似于P，除了由P产生的关于x的所有信息只能被P看到，而由其他过程产生的关于x的信息不能被P看到。除了这类算子的传统精神之外，在部分信息的上下文中，局部信息可以在系统分析中代表有价值的帮助当执行复杂系统的整体分析时，局部变量可以帮助例2.4考虑一个复杂系统（例如，单元）由进程C表示。假设C的定义涉及一组变量X ={x1，x2，.，xn}，其表示感兴趣的一些特征。通过这种方式，在C的“独立”分析中，X中的变量将给出其随时间推移现在假设我们感兴趣的是一个由大量相同细胞相互作用组成的过程TT = C1...100米在这种情况下，由于分析的焦点已经从局部水平（单个细胞）移动到全局水平（组织），因此有必要从每个Xi（与Ci相关）中不参与相互作用的那些变量引起的行为中抽象出来，正在被模仿。 令Xi<$X<$={x<$，x<$，.，x∈}是包含这些的集合i12n“irrelevant” variables因此，每个小区Ci可以更好地表示为Cii= localxi，xi，.，x∈Ci3，过程T∈= C1∈C. Cm12N代表细胞请注意，每个单元格的内部结构通过这种隐藏保持不变。此外，从操作的角度来看，需要这样的隐藏来保持从P观察到的值的一致性：由于每个Ci可以为每个xi分配不同的值，因此可能会出现不一致。从这个例子中，可以观察到隐藏和部分信息概念的相互作用如何允许在不同的细节层次上分析系统。基本计时行为ntcc提供了两个基本的时间操作符：next（P）和unlesscnext（P）。 让我们分别分析一下。next（P）表示在下一个时间间隔中P的激活。因此，next（P）的移动是P的单位延迟。 next（P）也可以被认为是表示随时间的动态行为的最简单方式这在ntcc中是基本的，因为信息不会自动地从一个时间间隔传输到下一个时间间隔。在next（P）的基础上，很容易想到2注意，Xi不应该包含与Xi相同的变量，因为这表示每个单元格都是相互隔离的。3表示法localx1，. ..，xninP将进程localx1in（localx2in（... . （localxninP）.. . ））.124J. 古铁雷斯等人理论计算机科学电子笔记171（2007）117在更复杂的延迟结构中：我们使用nextn（P）作为下一个（下一个（. next（P））.. . ）），其中next重复n次。在部分信息的背景下，能够对信息的缺失进行推理是重要和必要的。虽然有时可以预测系统的某些可能的未来状态，但通常强烈需要表达意外行为。在这种情况下，unlesscnextP形式的进程可能会派上用场：只有当c不能从当前存储中推断出来时，P因此，它们等待一个时间单元以等待一条信息C出现，如果没有出现，则它们在下一个时间间隔中触发活动。为了说明这一点，考虑下面的例子。例2.5过程R=whenadoP1+whenbdoP2+whencdoP3对一个系统的三种可能演化的预测进行建模（即，P1、P2和P3）。请注意，由于它们可能只是部分理解的复杂行为的 一 小 部 分 ， 因 此 没 有 包 括 大 量 的 不 确 定 性 。 定 义 一 个 过 程 R=Runless（a<$b<$c）nextS将确保在发生不同于a、b或c的刺激的情况下，系统中的一致默认状态（这里由S表示）将被保留。遵循这种建模风格的定义不仅允许更完整的模型，而且还允许以安全的方式利用部分信息计数的优势。异步*运算符允许通过时间间隔来表示异步行为过程*P表示P的激活的任意长但有限的延迟。例如，过程D=*tell（enzymeReleased = 1）可以表示环境中特定酶的最终存在，但不提供何时实际发生这种事情的上限因此，这种异步行为构成了部分行为信息的另一个实例：除了关于作为系统状态的一部分的变量的部分信息（并且由上面讨论的运算符表示）之外，*运算符允许表示关于执行过程的时间单元的部分信息。当描述以未知相对速度相互作用的（生物）过程时，这是特别有趣的。例如，一个过程D→S（D的定义如上所述）可以代表系统S（可能需要酶的存在）和确保这种酶到达的过程之间相互作用的一个可解释的ntcc中异步行为的部分信息精神通过以下派生运算符得到加强，表示有界可能性：*[n，m] P = nextn（P）+nextn+1（P）+···+nextm−1（P）+nextm（P）。因此，该运算符表示额外的时间（部分）信息量J. 古铁雷斯等人理论计算机科学电子笔记171（2007）117125这是因为它确保P将在自然值[n，m]的封闭区间内的时间单位内的某个点被激活。与原始操作符一样，没有关于何时会发生这种受限制的可能性的额外信息。持久行为在某种程度上，与异步行为强制执行的最终行为相反，持久（或无限）行为用于表达在系统的每个可能状态下都有效的条件。复制操作员！P表示P<$next（P）<$next2（P）<$。. ，即P的无限多个副本，但一次一个。因此，持久性行为是一种适当的方式，可以强制执行说明相关系统基本规则的条件。说明这种行为的过程是DJ=！tell（enzymeReleased = 1），酶相关信号的持久版本。DJ简单地表示在未来的每个时间单元中，它所涉及的约束都是可用的。持久性行为也可以理解为一种机制，允许从静态描述或条件（仅在系统的一个状态下有效）移动到始终有效的动态与异步情况一样，可以派生持久化操作符的有界版本：！[n，m]P = nextn（P）<$nextn+1（P）<$··<$nextm−1（P）<$nextm（P）.该运算符表示P在区间[n，m]中的所有时间单元内始终有效的事实。作为它的最终对应物，当关于P的（持久）执行的某些附加信息可用时，这个派生运算符（称为有界不变性）可能会派上用场。2.2操作语义上述ntcc过程的直观行为是通过结构操作语义（SOS）来形式化的，该结构操作语义（SOS）考虑了形式为存储的过程-存储配置之间的转换，其中存储被表示为约束。SOS的跃迁由关系−→和=给出。它们在附录A中正式定义。直觉上，内部转换P，d− →PJ，dJ应该读作的（c、d）可观测跃迁P =R应读作一个时间单位到R并输出d可观察到的跃迁是从内部跃迁的终止序列中获得的。现在让我们考虑一个无限序列的可观察的转变（或运行）P=P1（第1条，第1条）=P2（第2条规则）=第3（第3条规则）..................... 这个序列可以解释为一个系统P与环境之间的交互在时间单位i，环境提供刺激si，Pi产生ri作为响应。如果α= s1.s2.s3...和αJ= r1.r2.r3.. . ，则上述相互作用表示为P（α，αJ）=ω。126J. 古铁雷斯等人理论计算机科学电子笔记171（2007）117或者，如果α=真ω，我们可以将运行解释为P中的并行组件之间的相互作用，而没有外部环境的影响（即，每个组件都是其他组件的环境的一部分）。在这种情况下，α被称为空输入序列，αJ被认为是P中这种相互作用的定时观测。我们可以说过程P的最强后置条件，记为sp（P），表示P可能输出的所有无限序列的集合。更精确地，sp（P）={αJ| for some α : P（α，αJ）===ω}。3NTCC过程的规范和验证在本节中，我们总结了一些结果，关于线性时序逻辑（LTL）相关的ntcc。这个特殊的LTL表达了约束序列的性质，我们将其称为CLTL。一个健全的，部分完整的证明系统，这种逻辑也被描述。这个逻辑的更多细节（包括可判定性结果）可以在[14，21]中找到。CLTL和ntcc之间强关系的重要性在于，除了上述操作语义学所诱导的观察方法之外，还可以采用基于逻辑的方法来验证生物系统的属性。也就是说，NTCC过程的模拟（即，它的定时观测）可以通过基本性质的证明（以时间公式表示）来补充我们首先给出LTL公式的语法，然后用CLTL语义解释它们。公式F、G、. 从底层约束系统中的约束c∈ C和变量x∈ V通过以下方式构建：F，G， .. . . ：=c|trstecue|法尔斯泰切|FstecG|FstecG|stecF|PastecxF|F|QF|◇F约束C（即，约束系统中的一阶公式）表示状态公式。 虚线符号表示通常的（时间）布尔值，存在算子在CLTL中，这些操作符并不总是与约束系统中的操作符一致，因此需要使用点表示法。符号、Q和如果不是下一个，总是会发生的。 我们用FstecG来做RstecFstecG。下面我们给公式一个CLTL语义。我们首先介绍一些符号和x-变量的概念。直觉上，d是ci的x-变体，它们除了关于x的信息之外是相同的。 更正式地说，给定序列α=c1.c2、我们用xα来表示序列xc1<$xc2. . 我们将使用α（i）表示a的第i个元素。定义3.1[x-变量]约束d是cixc =xd的x-变量。类似地，αJ是α i <$$>xα =<$xαJ的X -变式.定义3.2[CLTL语义学]我们说α满足（或者说它是一个模型J. 古铁雷斯等人理论计算机科学电子笔记171（2007）117127的）CLTL中的F，写作α| = CLTLF，iα，1 |= CLTLF，其中：阿罗阿岛|= CLTLtrstecue eα，i|= CLTLfalst e c s e阿罗阿岛|=CLTLciα（i）|=c阿罗阿岛|=CLTL<$stecFiα，i|=CLTLF阿罗阿岛|=CLTLFLLia，i|=CLTLFanddα，i|=CLTLG阿罗阿岛|=CLTLFLLia，i|=CLTLForα，i|=CLTLG阿罗阿岛|=CLTLFiα，i+1|=CLTLF阿罗阿岛|=CLTLQF iforallj≥iα，j|=CLTLF阿罗阿岛|=CLTLFihe e isaj≥is uchatα，j|=CLTLF阿罗阿岛|=CLTLstecxF ite re isanx-variantαJofαs uchatαJ，i|=CLTLF.定义[F]]={α |α |= CLTLF}。 F是CLTLvalid i [F]]= Cω，且CLTL satisablei [F]].过程验证。因图利山口|= CLTLF i表示P在任意环境的输入下可能输出的每个序列都满足F。定义3.3我们说过程P满足F，记为P| = CLTLF，isp（P）[[F]].例3.4假设R =*tell（c），F=c。则R| = CLTLF，因为在R输出的每个序列中，必须 有 一 个 e ， 从 而 产 生 c 。P = tell （ c ） +tell （ d ） |=CLTLcdandP|=CLTLcasstecdaseveryyeutoutbyPentailseithercord. 注意，how-everr，thatQ=tell（cd）|=CLTLcdbutQ|=C LTL（cstecd）ingeral，sinceQ可以输出一个e，它肯定包含c d，但仍然不包含c和d-取c=（x=42）， d=（x/=42）和e=cd。 因此， C语言的istingu是PfromQ。为了推理形式P的陈述|= CLTLF，ntcc配备了一个证明（或推理）系统，用于形式PF的断言。该系统如表1所示。我们说PFi，断言PF在表1的系统中有一个证明。断言PF旨在成为P的“对应物”|= F，因为P<$F应该近似于P| = CLTLF尽可能接近（理想情况下，它们应该相等）。[ 14 ]中的以下命题说明了以下两个命题之间的对应关系：|=和。我们说一个过程P是局部独立的，如果P中每个非一元和的守卫不包含局部变量。命题3.5（合理性）如果P≠F，则P| = F.此外，（完备性）如果P是局部独立的，并且P| = F则P<$F。因此，证明系统是健全的，也是完整的局部独立的过程-这代表了大量的家庭的ntcc过程。值得注意的是，我们引人注目的例子实际上是局部独立的。最后，下面的引理将在推导中有用（更多细节见[14]引理3.6对于每个过程P，1.Putrstecue e，2.P/Niffalstecs e，3.PAPQAPAPB和D4。PAstecB.128J. 古铁雷斯等人理论计算机科学电子笔记171（2007）117LTELLtell（c）LSUMi∈IPiAiPi∈I当ci做Pi时，_^i∈I（ci）非专利技术˙i∈I斯泰奇一世LPARPAQ BPQAstecBLUNLPAPALREP！PQA下一页 PcAPA吕宋localxinPP2PstecxALSTARPAPLNEXT 下一页（P）PALCONSPAPB如果一个人表1NTCC过程（线性-时间）性质的一个证明系统4NTCC中的一个生物系统分析在本节中，我们展示了使用我们的方法来建模和验证生物系统，使用钠钾泵作为案例研究。我们首先给出了一个简短的生物学描述的系统，并提出了一个NTCC模型表示其行为。随后，我们使用ntcc推理技术验证了该模型的一个非平凡性质。4.1生物学描述离子泵是连接膜两侧的天然通道。这些泵的功能是在称为运输的过程中移动离子穿过膜。根据所需能量的来源，运输可以是被动的或主动的。在被动转运中，离子遵循电化学梯度自由移动穿过当离子在梯度方向上移动时由于在主动转运中离子逆着梯度方向移动，细胞必须提供能量（通常以ATP的形式）来完成这种移动。特别地，钠-钾泵[20]（SP泵）是用于在动物真核细胞中主动转运离子的系统。它将细胞内的钠离子与细胞外的钾离子进行交换。该泵由两种蛋白质组成，称为α和β亚基。 泵的目的是保持细胞内的钠浓度低于外部。这种浓度差异产生电化学梯度，导致钠离子向细胞质被动转运。如果泵不能很好地工作，则梯度变得弱于运输，从而阻碍所需物质进入细胞。SP泵的泵送过程可以分为六个阶段。开始时，在细胞内存在对钠离子具有高亲和力的泵构象（1）。这种构象促进了三个钠离子与泵的结合然后，α亚基被ATP水解磷酸化（2），在细胞质中留下残留的ADP分子这种化学反应提供了J. 古铁雷斯等人理论计算机科学电子笔记171（2007）117129泵送过程所需的能量。一旦发生这种情况，泵构象发生变化，然后钠离子可以离开细胞（3）。在这一点上，存在对细胞外的钾离子具有高亲和力的泵构象（4）。 这导致两个钾离子与泵结合。因此，α亚基被去磷酸化（5），泵构象恢复到初始状态。此时钾离子可以进入细胞（6）。泵送过程总是通过调节电池中钠的浓度来进行。与这种主动转运运动平行的是被动转运运动，其允许钾和钠离子逆着主动转运的方向移动。这种互补运动由细胞中存在的电化学梯度引起。4.2SP泵的NTCC在这里，我们提出了一个NTCC模型的SP泵。我们使用非确定性和异步行为来建模关于某些组件的时间响应的部分行为信息在进入模型的详细其详细的定义可以在[14]中找到递归定义可以对形式q（x）d=efPq的递归定义进行编码;其中，等式是p_r_c_n_m和p_q_call_s_o_n_y_c_n_d，并且调用必须在“下一个”的范围内此外，我们可以依靠编程语言中关于过程调用的通常直觉。单元格使用基本的ntcc语法，可以提供单元格，这是指定和分析可变和持久数据结构的基础。一个单元格可以被认为是一个包含一个值的结构，如果测试，它会产生这个值。单元格在时间单位内保持其值，直到它被修改。我们使用符号x：v和x：=v分别表示初始化和赋值为v的单元格x。此外，我们将使用符号x：=x+z作为赋值x：=xJ+z的缩写，其中xJ是前一个时间单位中单元格x的值，z是固定值。运算x：=x-z可以类似地编码我们现在开始描述代表SP泵的ntcc模型，如图1和图2所示。让我们首先描述其建模的主要原则该模型假设了整数的有限域上的约束系统，考虑了三个相互作用的地方：细胞内部和外部，以及离子在进入或离开细胞之前停留的中间位置（即，泵）。该模型涉及一系列持久变量（建模为细胞），存储有关泵送过程的有用量。然后，将泵的输出和输入操作建模为对代表细胞内外离子数量的变量的修改特别地，变量N aO、N aI、KO和KI分别表示置于电池此外，还需要一定量的各种离子130J. 古铁雷斯等人理论计算机科学电子笔记171（2007）117用于电池的正确功能。这样的量由N IDEAL和KIDEAL表示。最后，该模型包括捕获泵的其他细节的附加变量：OPump表示泵的方向（细胞内部或外部），Alpha表示alpha亚基的当前结合，Pump表示泵的当前内容。这三个变量将被实例化为可以用整数编码的常量：例如，Alpha的可能值是P，free和null（注意常量的特殊字体样式）。最后，整数变量ATP和ADP分别表示细胞内ATP和ADP的 存在 。图1和图2中的模型反映了SP泵中主动和被动转运的互补性质，表示为ActiveTrans和PassiveTrans过程，其被整合为NaKPump过程。从这个过程中，然后可以假设泵所处的某种环境这就是流程系统背后的直觉。我们现在开始更详细地解释这些过程背后的思想。主动转运相ProcessActiveT rans集成了前面描述的六个阶段的子流程;这些流程相互调用。一些过程（即，NaPhase1、NaPhase2和KPhase1）包括对它们自身的可能递归调用。这是为了表示尽管给出了进化所需的所有条件，系统仍然停留在某些阶段的可能性。也就是说，我们试图模拟“可逆”阶段，一种由非确定性选择表示的行为。结果，这些阶段可能被执行多次，因此在至少一个时间单元中延迟系统执行发生这种延迟是因为系统等待泵的特定位置处存在某些物质。事实上，这些物质可以获得，但不在所需的地方。这种非确定性和异步行为可能代表组件结合的其他条件，例如与泵组件发生（化学）反应的元件之间的类似地，非确定性行为也可以表示某种故障。例如，在相NaPhase2中，磷酸盐可能无法与α亚基结合，这将导致系统故障，这可以从泵随时间的演变中直接观察到被动运输阶段过程PassiveTrans定义了两个子过程：一个用于钠离子的进入，另一个用于钾离子的输出。值得注意的是，在这些子过程的建模中，我们正在考虑离子运动真正发生的实际时间的部分行为信息，其由有界异步算子表示。J. 古铁雷斯等人理论计算机科学电子笔记171（2007）117131NaPhase1d=efwhen（NaI>NaIDEALKIDEAL）Pump=EmptyOPump=Indo（下一个（NaI：=NaI− 3<$P ump：=NaItell（unchangedK= 1）<$NaP相2）+下一个（NaP hase1-tell（unchangedK= 1）-tell（unchangedNa= 1）NaPhase2d=efwhenenPump=NaAlpha=freeATP>0do（下一个（OP ump：=OutAlpha：=PADP：= 1tell（unchangedK= 1）tell（unchangedNa= 1）NaP相3）+下一个（NaP相2Δtell（未改变K= 1）Δtell（未改变Na= 1）NaPhase3d=efwhenPump=NaOPump=Outdo下一个（NaO：=NaO+3 P泵：=空泵告诉（未改变K= 1）KP相 1）KPhase1d=efhenPump=EmptyOPump=Outdo（next（P ump：=K<$KO：=KO−2<$tell（unchangedNa= 1）<$KP hase2）+next（KP hase1tell（unchangedK= 1）tell（unchangedNa= 1）KPhase2d=efwhenenAlpha=PPump=Kdo下一个（OP ump：=InADP：=0Alpha：=freetell（unchangedK= 1）tell（unchangedNa= 1）KP阶段 3）KPhase3d=efwhenPump=KOPump=Indo下一个（KI：=KI+2P泵：=空泵告诉（未改变Na= 1）NaP相1）defActiveT rans=NaP相 1图1.钠-钾泵的ntcc模型（1/2）附加过程将上述过程整合为NakPump过程是简单的。存在附加的过程（即，控制），其控制泵的全局行为w.r.t.离子量的平衡;在离子之一的量达到平衡的情况下，建立一般系统故障（表示为死亡= 1）。与其他过程一样，该控制过程的结构使得可以包括附加特征。处理开始，其接收一组六个参数（表示为σ1. （6）是自我解释的。我们的模型的一个显着特点是，它可以从实验中提取的实际定量值参数化。在我们的模型中，离子浓度取决于使其更准确的参数;涉及其他生物组分的更详细的模型（例如，控制被动传输的动力学的电化学梯度和与离子和泵之间的物理接触有关的力的大小）将需要包括更复杂的数值参数。在这个意义上，考虑实数上的约束系统不仅允许包括更复杂的条件，而且还允许在不同的细节水平上执行分析。132J. 古铁雷斯等人理论计算机科学电子笔记171（2007）117defPassiveNad=efunlessNaO=NaI 下（下一个5（P assiveNa））[0，5]（除非未更改Na= 1下（NaI：=NaI+3<$NaO：=NaO− 3）<$当Na= 1do（NaI：=NaI+ 3<$NaO：=NaO− 3））时，P assiveK=除非KO=KInext（下一页5（P））[0，5]（除非下一个未更改K = 1（KI：=KI− 2<$KO：=KO+ 2）<$当K= 1do（KI：=KI−2<$KO：=KO+2））时，PassiveTransd=ef PassiveNa PassiveKControld=ef！（其中NaI=NaOdtell（等式Na=1））当KI=KO时，告诉（等式K= 1）当equilNa = 1 equilK = 1M时，！（tell（1）Start（σ1.. . 6）d=ef！（tell（ATP>0）tell（NaIDEAL=σ5）tell（KIDEAL=σ6））ADP：0α：空闲泵：输入泵：空泵NaI：σ1<$NaO：σ2<$KI：σ3<$KO：σ4NaKPumpd=eflocalNaI， NaO，KI，KO，Alpha，ADP， Pump，O Pumpin开始（σ1. 6）主动式被动式控制def系统=NaKP泵环境图2.钠钾泵的ntcc模型（2/2）4.3生物模型的性质证明：基于逻辑的方法在本节中，我们将给出一个非平凡的生物学例子来说明ntcc的推理能力。特别地，该示例涉及SP泵上的抑制过程这种抑制可能代表药物和疾病：为了防止循环问题，某些药物诱导泵的部分抑制，以增加心脏收缩的强度另一方面，某些物质可能会对泵造成完全抑制过程，从而导致细胞死亡抑制过程的例子也使我们能够利用所提出的模型的灵活性。我们将假设泵周围环境中存在（恶意）药物。这种药物的目的是控制α亚基，从而防止磷酸盐诱导泵的构象变化。 反过来，这种阻碍会导致完全抑制 由泵强制执行的主动传输机制。我们在模型中通过指定环境过程来表达这一点，如下所示：Environmentd=ef毒品（