DNA加法的形式化验证和模型构建

理论计算机科学电子笔记171（2007）209-222www.elsevier.com/locate/entcsDNA加成的κ模型Xian Xu，1，2Xiaoju Dong3 和玉溪富3号基础知识上海交通大学中国上海市华山路1954号（200030）中国摘要DNA计算是近年来的研究热点。使用理论进行形式化和验证（π演算，生物环境，κ演算等）在计算机科学中，由于它可以在一定程度上帮助证明和预测各种生物过程而引起人们的注意。结合这两个方面，方法可用于验证DNA计算中的算法，包括基本的算术运算，如果它们被包括在DNA芯片中的话。本文首先介绍了一种新设计的DNA二进制加法算法，该算法在DNA计算机处理器中构成一个单元，然后用κ-演算（一种非常适合描述蛋白质相互作用的形式化方法）对该算法进行了形式化，从一定意义上证明了该算法的正确性，并给出了一个合理的例子。最后，对所描述的模型进行了讨论，并提出了一些可能的改进方向。保留字：DNA计算，加法，建模，κ演算，生物计算1介绍自从Adleman [ 1 ]利用DNA为了实现DNA计算机，研究人员利用DNA行为的基本特性和原则。计算机的基础结构是设计和实现的，在这个过程中，最基本的步骤是实现ALU（算术逻辑单元），包括初步的数学，1国家自然科学基金（60225012）、国家杰出青年科学基金（03DZ14025）、国家自然科学基金（60473006）、MSRA、博士点研究基金（20010248033）资助。2 电子邮件地址：xuxian@sjtu.edu.cn3邮箱：xjdong，yxfu @ sjtu. edu. cn1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.05.018210X. Xu等人/理论计算机科学电子笔记171（2007）209加、减、乘、除等运算，下面介绍一种用DNA实现加法运算的新方法在DNA的算法之下是生物分子计算的机制，DNA自组装。它是实现各种DNA应用的基础驱动程序。Eric Winfree和他的同事们对这个问题进行了大量的研究，[17，18]是他们的一些结果。另一方面，计算机科学也有助于生物分子实验和分析的发展。虽然生物学是一门以实验为基础的学科，其特点是观察、分析、总结、猜想和假设，但它大多是一种基于近似和推测的工作，并不完全是基于严格的数学。因此，提供一种强大的方法来描述和分析生物现象的各种结果，如信号转导和基因调控，逐渐显示出其重要性。由于与计算机科学的密切联系，生物学特别是分子生物学利用各种形式化方法来帮助建模和验证实验和命题的正确性过程代数和其他类似的理论，由于其内在的可表达性，适用于建模不同种类的生物分子过程。这些方法包括π-演算[15 ，16]、随机π-演算 [9 ，11 ，13]、bioambient [6，14]、brane-calculi [5]、P-系统[10]、κ-演算[7]等，它们能够有效地描述某种生物过程，形成一个针对特定过程的方法网络，研究者可以根据自己的需要从中此外，与方法对应的工具部分可用于执行描述和模拟生物过程，例如BioSPI [3]，从而跟踪程序并验证结果。事实上，生物分子学科与计算机科学研究的两个方面并没有泾渭分明，而是被互利所模糊。例如，DNA计算中的高度并行性的优点使其在帮助解决诸如NPC问题之类的难题方面具有效率，并且计算机科学中的理论，特别是那些基于计算机自动化的数学理论可以用于促进对各种生物过程的分析和理解，特别是在分子水平上，其主要形式是用形式化方法对生物过程进行建模，以验证和预测某些性质或事件。这两个方面实际上在几个方面相互作用，促使两者在总体上进一步发展。下面我们尝试做一些与上面描述的场景相关的事情。由于BioX实验室[12]提出了一种新的DNA加法算法，因此我们尝试使用Vincent Danos [7]的微积分κ对该算法进行建模。下面，我们将首先让读者熟悉两个方面，即算法和κ演算。然后对模型进行了讨论，给出了描述效果和结论。X. Xu等人/理论计算机科学电子笔记171（2007）2092112κ演算κ，或正式分子生物学[7]，是一种正式的方法，旨在表征不同种类的蛋白质之间的相互作用。与π演算、bioambient等形式化方法相比，它的特点是可以用交互的方式描述不同种类蛋白质的行为，如蛋白质上某类结构域的连接和断开，并且可以用结构化的、简洁的方式描述相互作用网络。下面我们简要介绍一下语法和语义，让读者熟悉这个方法。2.1语法下面给出κ的语法S：= 0 |A（ρ）|S，S|（x）（S）κ的基本元素是溶液，用S表示，它可以被看作是一个蛋白质系统，包括反应的候选物。解决方案可以是以下之一：• 0（空溶液）。 意思是没有。• A（ρ）（蛋白质）。这意味着一个界面为ρ的蛋白质。界面包含蛋白质结构域位点的信息，即蛋白质的反应能力，蛋白质可能有一组位点，每个位点有两种状态：隐藏和可见。前者意味着它被保持不被看到，后者意味着该网站可以到达。如果某个站点可见，则可能通过特定通道（称为边连接，其名称从名称集中选择）进行连接E包括x，y，z···，则称该位点是束缚的，否则为自由的。用A、B、C···表示蛋白质，用ρ、σ···来表示接口。此外，委员会认为，蛋白质的位点按自然数（N）排序，总数目蛋白质A的位点数定义为s（A）。实际上，接口是从N到E的（部分）映射，其中h表示隐藏，v表示可见。为了方便起见，例如，A（s（A）= 3）的一个界面ρ被定义为{（1，h），（2，x），（3，v）}，可以表示为ρ= 1 + 2x + 3，其中符号的对应关系很容易找到。• S，S（组）。这意味着解决方案的组合可能是蛋白质之间由许多边缘连接。• （x）（S）（新）。这意味着在两个蛋白质之间创建一个边缘x。而x被称为在S中有界，通过它可以精确地定义解的自由名和有界名，类似于π-演算。我们省略了它。例如，解可以采取以下形式（A和B通过边x为它们之间的互动而创建）：定义x x yS=（x）（A（1 + 2+ 3），C（1+ 2 + 3）），B（1 + 2）212X. Xu等人/理论计算机科学电子笔记171（2007）2092.2语义κ 的 语 义 是 通 过 演 化 关 系 定 义 的 ， 在 [ 7 ] 中 称 为 增 长 关 系 ， 在proteerfacesofproteins中。 它是如此的明亮（表1）。 not_excluded_e不是一个名称序列，它应该被设计为避免捕获绑定的名称。在表1中的关系中，接口可以从隐藏（状态）切换到可见（状态），反之亦然，可以被分配用于连接的边名称，并且可以从较小的接口形成较大的增长。然后，表2定义了增长关系，CREATE：x∈x<$xx≤HV-100：xx≤n（ρ）=xJ Jxρ≤σxρ≤σ反射：xρ≤ρSUM：表1xρ+ρJ≤σ+σJ界面演化解决方案在表2中的关系中，溶液可以根据其中蛋白质的界面，关于组成（GROUP）和生成（SYNTH）反应而演变。无：x≤0GROUP：S≤Txρ≤σσ是A上的一个参数xS，A（ρ）≤T，A（σ）S≤Tfn（σ）<$x<$σisan（impartial）interfacenASYNTH：xS≤T，A（ρ）表2解决方案演变根据两个表（1，2），可以定义反应粗略地说，如果x∈S≤T，则新的w是yS−→（x∈）T是一个单偶核。所谓单调，我们是指反应不还原蛋白质。同样在[7]中，需要更多的条件来确保井的动态。读者可参考[7] 为他们此外，在实际的生物系统中，接口可能需要重命名和扩展，上面定义的反应需要扩展，但这似乎并不复杂，对我们的工作也没有什么影响，所以我们省略了它。以下面的例子为例，其中A，B上的两个可见点2，3分别可以反应形成一个名为x的连接（边）。实际上，该反应可以由表1和2中给出的关系式获得，因此其他种类的反应可以类似地进行获得。A（1 + 2），B（1+2+ 3）−→（x）（A（1 + 2x），B（1+2+3x））X. Xu等人/理论计算机科学电子笔记171（2007）2092133另一种DNA加法算法甚至在使用DNA的内置计算能力来解决科学问题之前，科学家们就已经尝试用DNA进行最近，BioX实验室的研究人员设计了一种新的DNA二进制数加法算法，希望将其应用于更大的项目中，以构建真正的DNA计算机。与以往的算法相比，该算法简单、高效。在我们的模型到来之前，我们将在下面介绍它。3.1该算法虽然其基本思想类似于其他一些算法，但这里的算法是针对构建DNA驱动装置的效率，因此它必须节省更多的时间而不是空间。一般来说，它是使用蛮力，也就是说，准备所有可能的结果在位计算和组合他们得到一个最终的结果。从理论上看，时间效率是令人满意的，在生物步骤中呈线性。所需的DNA寡核苷酸的数量也与两个数的最大位数成线性关系。为 了 描 述 这 个 算 法 ， 假 设 两 个 二 进 制 数 相 加 的 长 度 为 n ， 记 为A=An−1An−2···A2A1A0和B=Bn−1Bn−2···B2B1B0。对于每个比特，我们将加法过程分解为两个阶段。考虑第iJ位（0≤i≤n− 1），• 将Ai加到来自最后一个低位加法的进位位，记为Ci，并得到部分位结果Hi;• 将Hi与Bi相加，得到第iJ位与其进位到下一高位的和按照这个规则，我们可以预先写出第i个J位上所有可能的位加法，对第一个和最后一个位要特别注意。它们在表3中给出。在表3中的⑴和（ii）中，Hi=Ai+Ci。Si-1没有任何作用，只是记录最后一个低位的和，以区分相同的进位位，更重要的是，帮助组织根据表3中的（iii）和（iv）中的结果（Ci+1，Si）的互补场景，因为后两者必须在其尾部附加加法结果（想象DNA串）。所以实际上Hi仅仅是由Ai和Ci决定的。 顺便说一下，我们使用2是为了方便，事实上它可以是任何符号，除了那些在表中使用的符号。在表3的（iii）和（iv）中，Hi与Bi相加，并且我们得到第iJ位和进位位Ci+1到下一高位的相加结果注意必须保持Si，从而导致在（i）和（ii）中设计Si−1还要注意，当i= 0时，H0=A0+C0，由于C0= 0，我们只需要保持A0对H0，这将在实验中反映出来。此外，委员会认为，4 例如，互补和连接步骤214X. Xu等人/理论计算机科学电子笔记171（2007）209Ci Si−1 Hi000010101111Ci Si−1 Hi001011102112(i)：Ai= 0（ii）：Ai= 1Hi Ci+1 SI000101210Hi Ci+1 SI001110211(iii) ：Bi= 0J表3(iv) ：Bi= 1第i位的DNA加成：Hi=Ai+Ci和Ci+1，Si来自Hi+Bi当i=n− 1时，Hn−1和Bn−1相加，得到Sn−1和一个进位，记为Cn。因此，整个加法结果是Cn Sn−1Sn−2···S2S1S0，去掉最左边的0。3.2实验从表3中，如果我们将表中的每一行视为具有两个相应粘性末端（由表3中的每个表中的双垂直线分开）的ssDNA（单链DNA）分子，则实际上可以暗示加法算法是沃森-克里克互补和连接的连续过程，从H0链，终止于Cn，Sn−1链。这个过程很容易理解和实现，因为算法已经屏蔽了编码中的困难部分也就是使用暴力手段。编码太大，无法在此显示，请参阅[12]以获取整个编码表。有两件事需要注意。 一个是因为C0=0H0不可能是2，那么B0的表的最下面一行可以被丢弃。 另一个是为了提取包括整个计算过程（也是添加结果）的结果dsDNA（双链DNA），使用PCR（聚合酶链式反应），因此必须以某种方式将引物添加到链上一个简单方法是将左引物连接到H0，右引物连接到Sn−1。计算开始于将两个二进制数的每一位的所有编码ssDNA放入具有连接酶的反应环境中，然后计算（自组装）自动开始时机成熟时，用PCR提取结果dsDNA，并尝试对每个Si（0≤i≤n− 1）和Cn进行测序。实际上这个实验在操作上要复杂得多，因为它在-X. Xu等人/理论计算机科学电子笔记171（2007）209215在体外环境中涉及许多技术，每种技术都可能导致错误率，例如在连接和读出期间，这在[12]中进行了这使得算法难以扩大规模。另一个挑战是计算过程是连续的，也就是说，几乎不可能通过两次二进制加法来将三个数字相加，并且实验的复杂性使得第一次计算遗漏了与另一次计算不兼容的结果。这些缺点使得这里描述的DNA加法算法离DNA计算机的应用有点远（实际上其他算法也面临类似的挑战）。更多的实验细节，包括在“湿”环境中的错误处理与其他算法的简要比较可以在[12]中找到。4DNA加成的κ现在我们将开始用κ来建模DNA加法算法。首先阐述了模型的总体思路，然后定义了模型的要素，即典型的蛋白质和反应规则，最后对模型进行了描述。4.1基本思路了解加法算法中的反应过程，我们可以将该过程视为DNA互补和连接的链式反应。一旦给出了两个二进制数，就决定了编码，表3中的每一行都表示为ssDNA。更具体地说，计算循环具有（i）或（ii）中的Hi和（iii）或（iv）中的Hi之间的连接，以及Ci+1上的类似连接，Si（Ci，Si−1）。 其中的一些内在机制是，直到最后一次连接完成后，可以进行下一次连接，并且连接的选择是唯一的。因此，我们可以用κ来描述这个过程。 表中的行（或ssDNA3可以被描述为κ蛋白（有点不安，但只是把它看作是一个抽象的元素），每个都有两个位置，一个对应于Hi，另一个对应于Ci+1，Si（Ci，Si−1），即表3中每个表中由双竖线分开的两个部分，我们将这两个位置称为左一和右一。而且对于每个蛋白质，左边的位点最初是可见的，但右边的位点最初是隐藏的。然后计算进行多个步骤，每个步骤的操作如下：蛋白质的左侧位点连接到最后一个蛋白质的右侧位点的某个边缘，从而启用（或激活）右侧位点（将其切换为可见），然后继续类似的过程。很容易看出，表3中的（i）或（ii）中的H0最初应设置为 而两种引物的状态变化可以作为指示剂到计算结束时，可以从蛋白质的连接产物中提取相加结果。216X. Xu等人/理论计算机科学电子笔记171（2007）209我我我我我我我A00（c0s0+h0）我A01（c0s1+h0）我A02（c1s0+h1）我A10（c0s0+h1）我A11（c0s1+h1）我A12（C1S0+H2）我B00（h0+c0s0）我B01（h1+c0s1）我B02（h2+c1s0）我B10（h0+c0s1）我B11（h1+c1s0）我B12（H2+C1S1）我4.2定义在这里，我们给出了蛋白质的形式定义和反应规则，用于建模的DNA添加算法。4.2.1蛋白这里的蛋白质是指κ中的抽象元素，而不是生物学意义上的具体元素如前所述，我们将表3中的每一行抽象为一个蛋白质，它有两个位点，每个位点对应一个ssDNA粘性末端。为了保持一致性，我们根据表中的信息定义蛋白质，表3. 对于表3中的（i），定义A0j对于行j（j=0，1，2，3），其中0表示A i= 0（i = 0，1，2，···，n − 1）。类似地，我们分别在表3的（ii）、（iii）和（iv）中定义行j的A1j、行j的B0j和行j的B1j我我对于每一种蛋白质，它的界面定义在两个基于他们所获取的价值。例如，蛋白质A00具有界面（c0s0+h0），这意味着在这种情况下，从最后一个低位开始的进位位是0，最后一个低位的和是0，并且该位的部分和是0。 现场h0最初是隐藏的，正如上面的建模思想中所提到的。类似地，其余蛋白质蛋白质的定义见表4。(i)：A0j㈡：A1j(iii) ：B0j表4(iv) ：B1j表3中每行的蛋白质定义现在我们考虑第一个和最后一个。我们将取消A0j的定义1j0和A0（j=0，1，2，3），当然保持其余部分不变。我们定义它们，作为A0（PrimerL+h0）和A1（PrimerL+h1），其中PrimerL表示左0 0引物指示计算的开始，它是隐藏的，直到连接X. Xu等人/理论计算机科学电子笔记171（2007）209217n开始. 为了得到一个平滑的结尾，我们定义了另外四种蛋白质BEnd00（c0s0+n引物R）、BEnd01（c0s1+引物R）、BEnd10（c1s0+引物R）、BEnd11（c1s1+引物R）n n nPrimerR），其中，例如，BEnd01（c0s1+ PrimerR）意味着最后一位上的和是1，并且它不携带任何到下一个更高的位，并且PrimerR被隐藏直到计算结束，以控制整个计算的停止。此外，由于位A0的简化，也可以对位B0做类似的事情。由于表3中（iii）和（iv）中的最后一行不可能达到B0，因此我们可以在我们的模型中消除相应的蛋白质，即蛋白质B02和B12。0 04.2.2规则我们将规则分为几组，下面将对每组进行解释。• Activation.考虑每种蛋白质的两个位点。左侧站点的连接将激活右侧站点，并将其切换为可见，以便将来连接。我们将举一些例子。例如，下面的两个规则属于该组。注意x是一条边，在其他例子中也是A00（c0sx+h0）−→A00（c0sx+h0）我0我0B00（hx+c0s0）−→B00（hx+c0s0）我0我0• 连接.蛋白质的右侧位点被激活后，它可以与左侧位点上的特定蛋白质反应，形成另一种连接。这继续进行加法的步骤。例如，下面的两个规则属于该组。A00（c0sx+h0），B00（h0+c0s0）−→（y）（A00（c0sx+hy），B00（hy+c0s0））我0我0我0B00 （hx+c0s0），A00（c0s0+h0）−→（y）（B00（hx+c0sy），A00（c0sy+h0））i−1 0 ii−100我0• 开始和结束。添加的开始和结束需要特殊处理。如前所述，PrimerL和PrimerR用于处理这两种情况。例如，下面列出了该组中的两个规则。A0（PrimerL+h0），B00（h0+c0s0）−→0 0（y）（A0（PrimerL+hy），B00（hy+c0s0））0 0 0 0BEnd00（c0s0+PrimerR），B00（hx+c0s0）−→n n−1 0（y）（BEnd00（c0sy+PrimerR），B00（hx+c0sy））n0n−1 004.3模型由于完整的模型比较大，我们只给出了其中的一些典型样本进行说明。整个模型在本文的附录中给出（可在网站上获得[2]）。在这里我们继续描述模型的仿真过程，然后给出一个加法计算的例子为了方便起见，我们假设提供了仿真模拟可以分为几个步骤。设两个二进制数相加为A=An−1An−2···A2A1A0，B=Bn−1Bn−2···B2B1B0。218X. Xu等人/理论计算机科学电子笔记171（2007）209n0011A1（PrimerL+h1），0A00（c0s0+h0），A01（c0s1+h0），A02（c1s0+h1），A03（c1s1+h1），1111A10（c0s0+h1），A11（c0s1+h1），A12（c1s0+h2），A13（c1s1+h2，2222A10（c0s0+h1），A11（c0s1+h1），A12（c1s0+h2），A13（c1s1+h2），3333然后(i) 在模拟系统中输入A和B的编码，即所有相关的例如，如果Ai= 1（i=0， 1···，n− 2，n− 1），则将蛋白质A1j（j= 0， 1， 2， 3）放置，Bi（i= 0， 1···，n− 2，n− 1）也是如此与此同时，i0 1pq如果A0= 0，则输入A0，如果A0= 1，则输入A0，以及BEndn（p，q=0，1）。(ii) 将系统规则设置为上面给出的规则。(iii) 运行系统。(iv) 当蛋白质BEnd pq（p，q=0，1）之一上的位点PrimerR变为可见时，计算结束。现在从PrimerR到PrimerL，读出路径上蛋白质序列上所有不同的c i s j位点，并将它们的下标j串起来以获得相加的结果。可以很容易地验证模拟过程是正确的，并产生与[12]中描述的DNA添加算法相关的预期结果。在某种程度上，这可以在下面的计算示例中显示目前还不知道是否存在一些有效的工具，但据说是由一些研究人员设计和实现的，然而，在适当的仿真工具可用之前，似乎还有很长的4.3.1加法计算的一个例子为了直观起见，我们给出了一个DNA加法的计算例子。取两个长度为4的二进制数（n= 4）。例如，A= 1101，B = 0110，其中B的最左边的0被添加以获得一致性。现在我们可以得到这两个数字中的位的编码对于A，溶液（系统）中相应的蛋白质如表5所示。对于B，溶液中相应的蛋白质如表6所示。表5A的模拟计算的运行如下所示（图1）。为了简洁起见，我们简单地展示了主要的反应路线。点表示不参与当前步骤的其他蛋白质。注意yi（i= 1，2，3，···）是边名，蛋白质的排列无关紧要。现在是时候对代表结果的蛋白质进行测序了。我们可以找到这些蛋白质，其位点指示结果，如下所示c1sy8c1sy6c0sy4c0sy2X. Xu等人/理论计算机科学电子笔记171（2007）209219B00（h0+c0s0），B01（h1+c0s1），B02（h2+c1s0），000B10（h0+c0s1），B11（h1+c1s0），B12（h2+c1s1），111B10（h0+c0s1），B11（h1+c1s0），B12（h2+c1s1），222B00（h0+c0s0），B01（h1+c0s1），B02（h2+c1s0），333BEnd00（c0s0+PrimerR），BEnd01（c0s1+PrimerR），44BEnd10（c1s0+PrimerR）、BEnd11（c1s1+PrimerR）44表6B两个二进制数的和可以通过从左到右将下划线的位串起来得到因此，这个例子成功地表明，我们设计的模型是合理的。5讨论在这里，我们给出了一些想法，在本文中所描述的工作首先，我们没有选择κ作为描述方法，而是考虑了Bioambients，因为它也能够描述分子相互作用。但最终选择κ是因为它在描述中的高效率蛋白质分子之间的相互作用。κ命名蛋白质定义的名称，包括它们的位点，由于它们在ssDNA名称中的大量和复杂性而例如Ci和Hi。我们试图遵守表3的惯例，但事实证明这是灾难性的，因为下标和上标的复杂集合变得一团糟。更糟糕的是，加法结果很难从结束解（蛋白质串）中解脱出来。在此基础上，对本文所提出的地名进行了设计它不仅记录了表3中各表的行号，以明确其在计算过程中的临时状态，而且保留了计算过程中所有必要的部分结果（Ci，Si，Hi），使加法结果的提取更加容易。蛮力方法该算法的一个缺点是，如果模型大小是通过其中的蛋白质和规则的数量来测量的话，那么它的规模太大假设加法算法是如果不进行修改以放弃蛮力方法，似乎该模型不太可能大大缩小所以我们把这个模型看作是一个紧凑型的220X. Xu等人/理论计算机科学电子笔记171（2007）209A1（引物L+h1），B0 1（h1+c0s1），····0 0→（y1）（A1（PrimerL+hy1），B01（hy1+c0s1），）0 1 0 1→（y1）（A1（PrimerL+hy1），B01（hy1+c0s1），）0 1 0 1→（y1）（B01（hy1+c0s1），A01（c0s1+h0），）01 1→（y1y2）（B01（hy1+c0sy2），A01（c0sy2+h0）， ）01 1 1 1→（y1y2）（A01（c0sy2+h0），B10（h0+c0s1），）1 1 1→（y1y2y3）（A01（c0sy2+hy3），B10（hy3+c0s1），）11010→（y1y2y3）（B10（hy3+c0s1），A11（c0s1+h1）， ）10 2→（y1y2y3y4）（B10（hy3+c0sy4），A11（c0sy4+h1），）10121→（y1y2y3y4）（A11（c0sy4+h1），B11（h1+c1s0），）2 1 2→（y1y2y3y4y5）（A11（c0sy 4+hy5），B11（hy5+c1s0），）211 2 1→（y1y2y3y4y5）（B11（hy5+c1s0），A12（c1s0+h2），）2 1 3→（y1y2y3y4y5y6）（B11（hy5+c1sy6），A12（c1sy6+h2）， ）210 3 0→（y1y2y3y4y5y6）（A12（c1sy6+h2），B02（h2+c1s0）， ）3 0 3→（y1y2y3y4y5y6y7）（A12（c1sy6+hy7），B02（hy7+c1s0），）302 3 2→（y1y2y3y4y5y6y7）（B02（hy7+c1s0），BEnd10（c1s0+PrimerR），············································································································ ）3 2 4→（y1y2y3y4y5y6y7y8）（B02（hy7+c1sy8），BEnd10（c1sy8+PrimerR），·············································································）3 2 0 4 0→（y1y2y3y4y5y6y7y8）（B02（hy7+c1sy8），BEnd10（c1sy8+P rimerR），）3 2 0 40Fig. 1. 一个加法计算的一个在K。至于加法算法，它的本质是蛮力5，这决定了在生物实验和形式化建模中实现的复杂性，但该算法确实是高效的，并且可以在生物步骤的线性时间内完成。这种用空间换取时间的方法在生物计算中很受欢迎。另一方面，如果我们计划降低模型的空间复杂度，我们可能不得不重新设计附加算法，牺牲一些时间以节省空间。这可以作为一个改进方向，即在模型中寻找时间和规模之间的可能平衡，同时充分利用巨大的并行性5与传统意义略有不同，这里我们指的是X. Xu等人/理论计算机科学电子笔记171（2007）209221DNA计算另一个改进的可能性是，形式化的建模方法可以更容易地使用和更强的描述某些类型的分子反应。虽然我们在这里使用κ，但这并不意味着不能选择其他方法。例如，Bioambients、P-系统甚至π-演算可能适合描述算法的某些方面，这是合理的。因此，能否利用不同方法的优点，设计一种新的适合于DNA计算的建模方法，将是一个值得考虑的问题κ本身的改进也是可能的，比如在解决方案定义中设计更高级别的对象抽象，例如将蛋白质复合物作为一个整体对象进行交互，以简化描述，但这可能需要在语法和语义上进行调整。就我们所知，与π-演算等方法相比，κ缺乏有用的编译器和执行器，这在一定程度上限制了它的应用。因此，开发一种有效的κ模拟工具变得越来越迫切。有了这样的工具，可以进行模型的第一步验证，该工具可以用于跟踪蛋白质相互作用，并为某些机制的证明找到可能的线索，或者对某些潜在功能进行可能的预测。6结论我们提出了一种新的算法来解决算术加法问题的DNA，以及一个正式的方法，κ，建模的协议。在此基础上，我们定义了一个用于DNA加法算法的κ模型，从蛋白质到反应规则，分为几个类别，并详细解释了原理，以及一些适当的例子。完整的模型可以在附录中找到，我们通过模型动力学中的一个例子来证明模型的正确性最后，我们对DNA加法算法和描述模型的优缺点进行了深入的讨论，并对两者的未来改进提出了此外，还阐述了对有效模拟工具的需求，强调了有效模拟工具在κ描述生物计算应用中的重要性。确认我们非常感谢李丹和桓龙就本文的主题进行了许多有益的讨论。我们也非常感谢匿名推荐人的建议。222X. Xu等人/理论计算机科学电子笔记171（2007）209引用[1] 阿德曼L.我...分子计算的解决方案到组合问题科学266（5187）：1021-1024，1994.[2] 计算机科学基础研究：http://basics.sjtu.edu.cn。[3] BioSPIProjeH ome page：http://www.wisdom.weizmann.ac.il/Bibiospi/。[4] Benenson，Y.，B.吉尔，U.本多尔河Adar和E.夏皮罗基因表达逻辑控制的自主分子计算机。Nature，429：423-429，2004.doi：10.1038/nature02551。[5] 卡尔代利湖膜演算。在2004年系统生物学计算方法（V.Danos，V.Schachter编辑）中，LNBI3082：257-278，2005，Springer-Verlag（柏林）。[6] 卡尔代利湖，和A. D.戈登移动环境。理论计算机科学，Cordination特刊（D。 L e Me'tayerEditor），Vol240（1）：177-213，June2000.[7] 达诺斯，五，和C.Laneve. 分子生物学. 理论计算机科学，特刊：计算系统生物学，325（1）：69-110，2004。[8] Guarnieri，F.，M. Fliss和C.班克罗夫特 使DNA增加。 Science，273（5272）：220-223，1996.[9] Kuttler，C.，J. Niehren和R.是的Pi演算中的基因调控：在λ开关处模拟协同性。计算系统生物学学报，BioConsur 2004年特刊，以及计算机科学讲义，生物信息学讲义，Springer Verlag，2005年。[10] Paun，Gh.. 请与我同呼吸。JournalofComputerandSystemSiences，61（1）：108-43 （2000年）图尔库中心为计算机Science-TUCS报告208,十一月 1998年，http://www.tucs.fi）上提供。[11]Priami，C.，A. Regev，W.Silverman和E.夏皮罗随机名字传递演算在分子过程表示和模拟中的应用。Information Processing Letters80：25-31，2001.[12] Qian，L.，中国地质大学，J. Zhao等人使用线性自组装的DNA添加。BioX实验室已提交。2005年[13] Regev，A.. 随机π-演算中分子路径的表示与模拟。在2001年第二届生化途径和遗传网络计算研讨会上发表。[14] Regev，A.，E.M. Panina，W.西尔弗曼湖Cardelli和E.夏皮罗BioAmbients-An Abstraction for BiologicalCombustion.理论计算机科学，325：141-167，2004。[15] Regev，A.，W. Silverman和E.夏皮罗用计算机过程代数表示生物分子过程：信号转导途径的π-演算程序。美国人工智能协会（http://www.aaai.org），2000年。[16] Regev，A.，W. Silverman和E.夏皮罗用Pi演算过程代数表示和模拟生化过程。Proceedings of the Paci ficSymposium of Bio-computing 2001（PSB2001），6：459-470，2001.[17]Winfree，E..DNA自组装计算NAE[18] Winfree，E.. “DNA的自组装”。 PhD Thesis. 加州理工学院，1998年6月。