基于dna计算的线性时序逻辑模型检测方法-朱维军.pdf

《基于dna计算的线性时序逻辑模型检测方法-朱维军.pdf》由会员分享，可在线阅读，更多相关《基于dna计算的线性时序逻辑模型检测方法-朱维军.pdf（20页珍藏版）》请在淘文阁 - 分享文档赚钱的网站上搜索。

1、第39卷第12期 计 算 机 学 报 v0139 No122016年12月 CHINESE JOURNAL OF COMPUTERS Dec2016基于DNA计算的线性时序逻辑模型检测方法朱维军” 周清雷 张钦宪2(郑州大学信息工程学院郑州450001)2(郑州大学基础医学院郑州450001)摘要该文研究基于脱氧核糖核酸(Deoxyribonucleic Acid，DNA)计算的线性时序逻辑(Linear Temporal Logic，LTL)模型检测问题为此，该文给出了使用粘贴自动机实现urL模型检测的方法首先，使用3-5型单链DNA分子对LTL公式的有穷状态自动机(Finite State

2、 Automata，FSA)模型进行编码，从而获得实现公式的粘贴自动机；其次，使用5，-3型单链DNA分子对系统模型进行编码，从而获得粘贴自动机的输入字符串；最后，对表征粘贴自动机的DNA单链分子和表征输入字符串的DNA单链分子实施一系列生化反应，即可判定系统是否满足公式分子生物学仿真实验结果表明：给出的DNA编码序列能达到999的碱基配对正确率，且新方法成功地对所有4种LTL基本公式与5种LTL常见公式实施了检测；与之对照，已有的方法只能有效检测1种LTL基本公式与0种LTL常见公式在此基础上，对本实验给出的DNA编码方案直接作位数扩展即可拥有对任意给定LTL一般公式的(理论)检测能力关键词

3、模型检测；脱氧核糖核酸；线性时序逻辑；粘贴自动机；有穷状态自动机；DNA计算中图法分类号TP301；TP384 DOI号1011897SPJ1016201602578A LTL Model Checking Approach Based on DNA ComputingZHU Wei-Junl ZHOU QingLei” ZHANG QinXian2”(School of Information Engineering，Zhengzhou University，Zhengzhou 450001)”(School of Basic Medical Sciences，Zhengzhou Unive

4、rsity，Zhengzhou 450001)Abstract This paper investigates the Linear Temporal Logic(LTL)model checking problemunder the circumstance of Deoxyribonucleic Acid(DNA)computingTo address this problem，we presented a method for checking LTL formulas via some sticker automataFirstly。3一5singlestranded DNA mole

5、cules are applied to encoding a Finite State Automaton(FSA)modelfor the given LTL formulaSO that a sticker automata which iS a DNA model of the formula canbe obtainedSecondly，the given system model is encoded by 5一3singlestranded DNAmolecules，by which the input strings of sticker automata can be gen

6、eratedFinally，a series ofbiochemical reactions are implemented on the singlestranded DNA molecules characterizingsticker automata or input strings。in order tO determine whether the system meets the formula ornotThe experimental results show that the generated DNA coding sequences achieve in 999by ac

7、curacy for base pairingFurthermore，the proposed method successfully checks four kinds ofbasic LTL formulas and five kinds of popular LTL formulaswhereas the existing methods canonly check one kind of basic LTL formula and none popular LTL formula，as shown in theexperimentsBy extending more bits on p

8、resented DNA encoding scheme，the proposed methodcan check any given LTL formulas theoreticallyKeywords model checking； deoxyribonucleic acid；linear temporal logic； sticker automata；finite state automata；DNA computing收稿13期：20150416；在线出版13期：2015一IIi0本课题得到国家自然科学基金(61250007，U1204608，U1304606，61373043，61

9、572444)、中国博士后科学基金(2012M511588，2015M572120)和河南省高等学校青年骨干教师资助计划(2014GGJS一001)资助朱堆军，男，1976年生，博士，副教授，中国计算机学会(CEF)高级会员，主要研究方向为DNA计算、形式化方法E-mail：zhuweijun76163corn周清，男。1962年生，博士，教授，博士生导师，中国计算机学会(CCF)理事，主要研究领域为DNA计算、形式化方法、信息安全张钦宪，男。1953年生，教授，博士生导师，主要研究领域为DNA计算、分子生物学万方数据12期 朱维军等：基于DNA计算的线性时序逻辑模型检测方法 25791 引

10、言模型检测由图灵奖得主Clarke教授等人1提出，是一种能够自动验证系统是否满足给定性质的共性技术目前已被广泛地应用于处理器设计验证2、网络协议验证、安全协议验证3、软件规范验证H1等领域，并被美国国家航空航天局以及Intel、IBM、摩托罗拉等信息技术领军企业使用模型检测的一般原理是：在模型检测系统中，有穷状态自动机建立系统模型，通过时序逻辑公式描述系统需满足的性质若有穷状态机满足相应的逻辑公式，则其满足性质；否则，不满足图灵奖得主Pnueli教授开创性地引入计算机科学的线性时序逻辑563与图灵奖得主Clarke教授提出的计算树逻辑口(Computation Tree Logic，CTL)，

11、是目前在计算机工业界使用的两大主流时序逻辑，分别被用来描述系统的线性时序性质和分支时序性质生物计算机以生物分子作为信息存储的载体，以生物酶和生物操作作为计算工具，是一种与传统的电子计算机不同的计算机模型1994年，图灵奖得主Adleman教授81在Science)上发表的一篇文章用DNA实验求解了一个小规模的汉密尔顿路径问题，被公认是DNA计算领域的开创性工作由于DNA分子天然的巨大并行计算优势，一系列DNA计算模型和方法被提出用于解决复杂计算问题，例如：Lipton9在Science)上发表文章给出命题公式可满足性问题的DNA解法；Ouyang等人1叩在Science)上发表文章给出最大团问

12、题的DNA解法；Shapiro等人1妇在Nature上发表文章给出两状态两字符自动机问题的DNA解法等此外，过滤模型12、粘贴系统”、长度一编码型自动机模型14、粘贴自动机模型15、DNA图灵机模型1 6|、非枚举型DNA计算模型17、巨磁电阻型DNA计算模型1盯、DNA分子逻辑计算模型19、纳米分子逻辑计算模型2叩等多种DNA计算模型相继被构建，各种非自治算法或自组装方法也被提出用于解决诸如最大卧2、图顶点着色172 2|、可满足性m、N皇后231、最大匹配2 4|、最小顶点覆盖2 5、最小集合覆盖与最小精确覆盖2 6|、子集和、Ramsey数283等若干非确定多项式(Non-determi

13、nistic Polynomial，NP)问题一方面，试管生化反应、纳米器件与分子自组装可被用于求解计算机科学问题821|另一方面，由于拥有良好的信息处理机制与巨大的并行性，因此活细胞也可被用于执行计算许进教授等人32以合成生物学中广泛使用的生物砖为材料，以大肠杆菌Escherichia coli为宿主细胞，以DNA重组酶Hin为计算工具，构建了一个解决可满足性问题的细胞计算模型该模型中，每个细胞可独立生成并判定可满足性问题的一个解，数以亿计的细胞检查数以亿计的可能解，显示了细胞计算的巨大潜力文献33则使用大肠杆菌细胞构建一个条件学习系统，在“学习”信号的帮助下可识别“坏人”信号，这是构建人工

14、分子生物智能系统的一个有益尝试计算机与其他计算工具的一个关键区别在于通用性许进教授3胡为通用DNA计算机找到了一种称之为“探针机”的数学模型，并将存储系统、运算系统、检测系统与控制系统集合为一个整体，逐步形成一个真正意义上的通用DNA计算机“中州型DNA计算机眦“模型检测问题是与可满足性问题相关但又非常不同的又一个重要计算问题，在DNA计算的框架内寻求模型检测问题的解法始终是研究人员追求的目标直到2006年，图灵奖得主Emerson教授等人35提出了一种使用DNA分子对CTL基本公式EFp进行模型检测的方法对于LTL逻辑而言，其模型检测在经典计算中是一个PSPACE问题我们的前期研究找到了可对

15、LTL逻辑一个基本时序算子“until”实施检测的DNA方法3 6|对于更多的LTL基本时序公式，形式化验证工业实践中常见的LTL公式，乃至任意给定的LTL一般公式，如何在DNA计算框架内实施模型检测?这些问题仍悬而未决本文将对此进行研究2基础知识21线性时序逻辑LTL逻辑的一阶部分不可判定，因此我们只需研究其命题部分(Propositional LTL，PLTL) Mordechai BPrinciples of the spin model checkerwwwkipwredupleichon201415一bALPrinciplesSpinCheckerpdf，2008 Clarke EG

16、rand challenge problem：Model check concurrent softwarehttp：wwwcslsricomusersshankarVGC05Clarkeppt万方数据2580 计 算 机 学 报定义1 设AP是原子命题集合，如果9和妒是PLTL公式，那么，PAP、一9V妒、o外伊妒都是PLTL公式定义2 一个PLTL模型是一个三元组M一(S，R，L)，其中：(1)S是非空有穷状态集，sES是状态；(2)R：SS，R(s)是状态s的后继状态；(3)L：S一2AP，L(s)是在状态s中成立的原子命题的集合定义3 满足关系定义如下：(1)s户当且仅当pL(s)；(

17、2)s-19当且仅当、(s9)；(3)s9V驴当且仅当(s9)V(s妒)；(4)s9胗妒当且仅当jJoR(s)妒(VO志RI(s)9)，其中，Ro(s)一s，R。+1(s)一R(R。(s)；(5)s=09当且仅当R(s)9定义4 导出公式定义如下：(1)9全true胗9；(2)口9全一一9；(3)妒妒全一(-1PV、妒)；(4)9一妒全一9V仁并发程序验证的基本问题是活性(会不会死锁)、公平性(会不会死等)、安全性(会不会出错)，以及可达性，均为形式化验证实践中常见的需求性质，且与4个基本时序算子共同构成该逻辑中最具研究价值与实用价值的公式子集，如表1所示表1线性时序逻辑的基本时序公式与常用公

18、式上述9个公式的直观含义涉及命题或性质成立的如下时序关系从当前时刻开始，给定原子性质未来是否成立?9个公式的具体含义分别如下公式1原子性质P始终成立，直到原子性质q成立公式2原子性质P永远成立公式3原子性质P终将成立公式4下一时刻原子性质P成立公式5原子性质P永远不成立如果某程序满足公式5，则该程序运行永远不会进入某种不安全状态公式6含义同公式3如果某程序满足公式6，则该程序运行终将到达某种状态公式7在未来任意时刻，如果原子性质夕成立，那么此后原子性质q终将成立如果某程序满足公式7，则该程序运行不会出现死锁公式8如果从将来任意时刻开始，原子性质P均最终成立，那么从将来任意时刻开始，原子性质q均

19、最终成立如果某程序满足公式8，则该程序运行使用各种资源是“强公平”的公式9如果从将来某一时刻开始，原子性质P永远成立，那么从将来任意时刻开始，原子性质q均最终成立如果某程序满足公式9，则该程序运行使用各种资源是“弱公平”的图1则用(FSA)图的方式表达了9个公式的含义，其中FSA的定义参见22节22有穷状态自动机与模型检测定义5 一个FSA A是一个五元组(三，Q，T，qo，F)，其中：(1)三是一个有穷非空字母表(原子命题集)；(2)Q是一个有穷非空状态集；(3)转移函数(转移规则)T：Q三一R(Q)；(4)goEQ是起始状态；(5)FQ是接受状态集定义6 设叫一Y。，Y。是定义在三上的字符

20、串，如果存在Q中状态序列r。，r1“，k满足：(1)ro=口o；(2)n+1T(ri，Y件1)，i一0，1，m一1；(3)r辨F，则称叫是被A接受的文字定义7 A识别的语言被定义为A接受的文字的集合在本文中，系统建模使用的自动机均为带标签之FSA，其原子命题在状态而非边上被满足，例如万方数据12期 朱维军等：基于DNA计算的线性时序逻辑模型检测方法 2581(a)砩的公式FSA A。 (b)的公式FSA A(c)鸭的公式FSA A3 (d)R的公it2SA A鬯念(e)R的公式FsA A (f)R的公式FSA A6状态S。出发输入字母P即进入状态s。)、转移规则2(从状态s。出发输人字母q即进

21、入状态s。，)以及转移规则3(从状态踊出发输入字母P或q即进入状态乩)，而PPq、Pq、PqP则为此FSA的接受字集合中的3个接受字例2 图2示例了一个带标签之FSA在此例中，FSA存在3个状态，分别是0、1和2，其中，0是初始状态，2是终止状态；状态0满足原子命题P和q，状态1满足原子命题P，状态2满足原子命题q；FSA可从状态0转移至状态1，也可从状态1转移至状态0，还可从状态1转移至状态2从图中显而易见：012是FSA的一个接受运行经过的路径(状态序列)，PPq是该路径先后满足的一个原子命题序列；O-1一。一12是FSA的另一个接受运行经过的路径(状态序列)，PPPPq是此路径先后满足的

22、一个原子命题序列依次类推，由于长度的不同，存在无穷多个类似路径，因而存在无穷多个原子命题序列(g)钙的公式飚A， (h)的公式FSA A(i)的公里t,2SA A9(j)9个公式FSA的并A1。图1公式对应的FSA图2；与之相反，公式的自动机模型均为不带标签之FSA，其原子命题在边上被满足，例如图1例1 图1(a)示例了一个不带标签之FSA在此例中，FSA存在2个状态(2个节点)，分别是和。，其中，s是初始状态，s。是终止状态此公式FSA有如下3个转移规则(3个边)：转移规则1(从FSA21节给出了LTL公式的定义，22节给出了系统模型FSA的定义，在此基础上，模型检测问题被定义为算法判定系统

23、模型FSA是否满足LTL公式LTL模型检测方法的原理如图3所示如果对于系统FSA的每一个接受运行(路径)经过的状态序列，存在一个它满足的原子命题序列，使得该原子图3基于经典计算的LTL模型检测算法原理万方数据2582 计 算 机 学 报命题序列组成的字符串是公式FSA的一个接受文字，那么，系统FSA满足公式反之也成立简而言之，模型检测结果为“yes”，当且仅当系统FSA的每一个路径都是公式FSA路径集合的一个元素例3 图2所示的系统FSA满足公式1，计算原理如下把图2中路径012对应的一个字符串PPq输入图1(a)所示的公式1的FSA，计算得知PPq是公式1的FSA接受的文字，即图2中路径01

24、2(ppq)是图1(a)中路径集合的一个元素(PPq也是公式1的FSA的一个路径)把图2中其他路径对应的字符串作为输入，也获得了同样的结果因此，图2的每一条(从0开始到2结束的)路径都是公式1的FSA路径集合的一个元素根据图3所示的算法原理，模型检测的结果为“yes”，即系统满足公式23粘贴自动机粘贴自动机37是一种实现FSA的DNA计算模型给定一个表征输入字符串(文字)的DNA链，给定一个FSA，粘贴自动机模型能够判断该字符串是否被FSA接受231 FSA和输入字符串的编码方式文献-37-给出了如下编码方式假设M一(三，S，T，S。，F)是一个FSA，字母表三中的任意一个字符a都可以用单链D

25、NA编码为C(口)(1)三上的输人字符串a。，a。由DNA单链分子编码：57工lXoX。C(口1)X。X。C(口。)XoX。I。3 7，其中，j。是启动区序列，X。X。是间隔序列，以间隔字符ai的编码C(口i)，J：是终止区序列(2)状态转移函数T(&，a)一s，被编码为37 X汁。X。C(口)X。Xi 57，其中，X表示核苷酸X的Watson-Crick补链，C(口)表示a的DNA序列的Watson-Crick补链(3)每个初态s的编码：37 J。X。X。57(4)每个终态Sj的编码：3 7 Xj+1X。工2 5232计算过程粘贴自动机模型的计算过程分为以下3步3 7|第1步数据预处理(1)

26、合成输入字符串和自动机的编码链(2)将所有的DNA链放到试管T中，退火使互补链充分杂交，碱基互补配对形成双链；在试管T中加入连接酶，得到(完全或部分)双链DNA分子第2步计算经过第1步的数据处理，如果输入字符串被自动机接受，那么试管T中是以启动区开始、以终止区结束的完全双链DNA分子；否则，试管T中的DNA分子不是完全双链原因在于，表达输入字符串的单链分子之部分片段被表达转移规则的单链分子配对成功，而其余部分片段则不存在表达转移规则的单链分子可与之配对故此，我们向试管T中加入Mung Bean核酶，降解其中的单链DNA片段，保留完全双链DNA分子，以完成本步第3步输出结果利用电泳技术分离不同长

27、度的DNA分子若存在多种长度DNA分子，则表明在加入核酶前试管T中存在部分双链DNA分子，这提示输入字符串不被自动机接受；否则，在加入核酶前，T中均为完全双链DNA分子，这提示输入字符串被自动机接受24 Mung Bean核酶及其应用于粘贴自动机S。核酸酶来源于米曲霉，可降解单链DNA或核糖核酸(Ribonucleic Acid，RNA)，是一种单链核酸酶，产生带5磷酸的单核苷酸或寡核苷酸双链，对双链DNA、双链RNA和DNARNA杂交体不敏感酶浓度大时可完全消化双链，中等浓度时可在切口或小缺口处切割双链Mung Bean核酶是来源于绿豆芽的核酸酶，将单链DNA降解为5端带磷酸基团的单核苷酸或

28、寡核苷酸双链DNA、双链RNA及DNARNA杂交体对此酶相对不敏感然而此酶大量使用时也能将双链核酸完全降解Mung Bean核酶的物理性质及催化性质与S。核酸酶相似，但Mung Bean核酶的作用比S，核酶更温和Mung Bean核酶用于使DNA突出端变为平端总之，上述两种核酶都可从单链DNA分子上逐个删除核苷酸，S，核酶有时也将单链DNA分子强行插入双链DNA，因此Mung Bean核酶更适合于粘贴自动机计算3 7。两种酶都可降解无法接受的输人字符串的单链片段，而被接受的输入字符串完全双链DNA分子在酶降解后仍保持完整无缺3 7|文献38使用Mung Bean核酶降解粘贴自动机单链片段，该文

29、以真实生化实验的方式正确计算出0、1两个二进制数之间的“逻辑与”、“逻辑或”的运算结果从而再次证实，使用Mung Bean核酶降解粘贴自动机单链片段，是生物学可实现的此外，该实验也得到了一些有关使用Mung Bean核酶降万方数据12期 朱维军等：基于DNA计算的线性时序逻辑模型检测方法 2583解粘贴自动机单链片段的如下技术要点3引：(1)掌握好酶量与反应时间酶量与反应时间过少则单链降解不完全，过多则可导致双链降解该实验给出的酶量是输入字符串分子量的27，反应时间是3小时8|(2)需注意DNA分子的呼吸作用，即双链分子以单双链转变的形式动态存在该作用可导致酶降解单链状态下互补分子，从而改变D

30、NA分子动态平衡条件，最终导致双链分子被降解该实验的对策是，不采用热失活方式终止酶切反应，加入蛋白变性剂失活Mung Bean核酶，同时在退火后先用T4连接酶将DNA分子的缺口补上，以稳定双链分子3引3基于粘贴自动机的模型检测方法31将9个LTL公式转换为FSA对于表1给出的LTL的9个基本公式或常用公式，分别构造它们的FSA模型，如图1中的前9个子图所示这些子图的并，如图1(j)所示按照粘贴自动机模型中FSA的编码方式编码图1(j)中的自动机将每一个实施编码后的DNA单链按如下规则选择放置：如果该单链是对自动机Ai中的某个节点或边实施的编码，则把该单链放置于试管R；中，其中i是从1到9之间的

31、自然数若LTL公式不属于上述9个公式，则对公式的FSA模型使用同样的方法实施编码后放人试管Ro32按照粘贴自动机的输入字符串格式生成系统的运行321状态编码状态用图4所示的单链DNA编码其中X。X。是粘贴自动机的间隔序列，为满足粘贴自动机输入字符串的格式而增加；L(s)是状态标签函数；y用于调节编码，使得每个状态编码的长度均为彼此相等的偶数，并且确保状态和状态编码之间一一对应5，| 圣：圣 l坐!I!旧图4状态的DNA编码322生成系统FSA的所有以开始状态为始点以终止状态为终点的路径算法1 系统模型自动机的运行路径生成算法3 6|输入：系统自动机的模型M输出：表达M所有路径的所有DNA分子B

32、EGIN第1步对于每个状态s，向试管T中加入s的编码；对于每条边。，向试管T中加入e的编码经过退火和连接反应，生成系统的FSA模型的随机路径第2步对试管丁执行提取前缀操作，使试管T中只含有以开始状态为起点的路径第3步对试管T执行提取后缀操作，使试管T中只含有以终止状态为终点的路径第4步在试管T中加入DNA分子了：譬和面Xio=X丽I z，其中Ii是启动区，Ho是初始状态编码的前半段，B是终止状态编码的后半段，x0X。是间隔序列，J：是终止区通过退火和连接反应，在单链DNA分子5 7端添加启动区，并且在单链DNA分子37端添加间隔区和终止区第5步使用亲和纯化技术，过滤出试管T中所有包含J，和I。

33、序列的单链DNA分子END其中，第5步除去第4步中多余的DNA分子，得到符合粘贴自动机输入字符串格式要求的单链DNA分子，每条单链DNA对应系统的一个运行33用粘贴自动机验证系统是否满足公式23节给出的粘贴自动机计算原理可概括如下：一些单链DNA分子(本文称之为I类分子)用于编码字符串，另一些单链DNA分子(本文称之为II类分子)用于编码FSA，上述两种单链分子充分杂交，如果形成完全双链分子，则字符串是FSA接受的文字；否则，即为不被接受的文字进一步地，我们可以把LTL模型检测问题规约为粘贴自动机的计算问题，规约原理如图5所示参见图5(e)执行算法1得到的所有I类分子即表征着系统FSA运行的所

34、有路径，即为将参与粘贴自动机计算的已编码的字符串，编码格式如图5(a)所示使用231节的编码方式(2)、(3)和(4)可以对给定的LTL公式的FSA模型设计出II类分子，编码格式如图5(b)所示把I类分子和II类分子作为粘贴自动机计算的两个输入，根据粘贴自动机计算原理(特别是DNA编码设计的两类分子之碱基配对关系)，两类分子杂交形成(或未形成)完全双链当且仅当系统运行(字符串)是(或不是)公式FSA的接受字，参见图5(c)和图5(d)根据图3所示的模型检测原理(特别是两个FSA的路径包含关系)，如果系统FSA的所有路径(字符串)均为此LTL公式FSA模型接受的文字，那么系统模型FSA满足LTL

35、公式，否则，不满足以上即为LTL模型检测的DNA算法的核心思想与基本原理它解释了该算法能够验证系统是否满足公式的原因算法描述如下万方数据2584 计 算 机 学 报 2016焦系统运行经 系统运行经启 间 过的第1个状 间 间 过的第n个状 间 终动 隔 态满足的原 隔 隔 态满足的原 隔 止区 区 子命题的 区 区 子命题的 区 区DNA编码 DlNA编码(a)表征系统FSA运行的DNA分子(I类分子)(b)表征公式FSA的3种DNA分子(II类分子)系统的一个长度为n的运行(DNA分子)公式FSA的 公式,FSA的转 公式FSA的转 公式FSA的初始状态 移规则(边 移规则(边)y 终止状

36、态(DNA分子)(DNA分子)(DNA分子)(DNA分子)(c)两类分子杂交之后形成完全双链(当系统某运行是公式FSA的接受字)系统的一个长度为tl的运行(DNA分子)公式FSA的 公式FsA的转 公式FSA的初始状态 移规则(边h 终止状态(DNA分子)(DNA分子)(DNA分子)(d)两类分子杂交之后形成不完全双链(当系统某运行不是公式FSA的接受字)l输出：“系统满足性质” l输出：“系统不满足性质”E据LTL模型检l l根据L1几模型目一般原理可知l l测一般原理司lBl中每个路径均为B。中路径l|B。中存在路径不是B2中路径串对应B1路径，1 f字符串对应B路径IpB，路径1 FSA

37、路径即B粘贴自动 所有字符串均为FSA的接受字扣I百笋时，、成完全双链? 嚣盆誉”l输入(作为字符串) 丫输入(作为FsA)I类DlNA分子集合(每l II类DNA分子集合(不同1一个DNA分子表征B】l 分子分别表征B2的初始状l的一个接受运行)l 态、终止状态与转移规则)l I输出 I实施DNA编码l算法1胁-I l公式FSAB：lf输入 f模型l系绁SAB。I LTL公刘lI建模 I描述系统 系统需满足的性质(e)算法流程图5基于DNA的LTL模型检测方法原理算法2LTL逻辑公式的DNA模型检测算法输入：31节的试管R一Ro，R，R9)，即LTL公式之粘贴自动机编码；算法1得到的试管T，

38、即系统的所有运行输出：系统模型是否满足公式BEGINZl，13，Z6：一】ylX 2_1+IEI如，ls：一Iyl14：一2l，18，z。：一lyI X21+IyI+IE如：一len(，)(IVI2|-1+JEI)IF待检测的公式为仍，其中i是从1到9之间的某个自然数，THEN第1步用长度分离操作提出试管T中长度小于l；的单链DNA第2步合并试管Ri到T，在T中加入DNA连接酶，使互补链充分杂交ELSE*待检测的为一般公式第1步用长度分离操作提出试管T中长度小于l。的单链DNA第2步合并试管R。到丁，在T中加入DNA连接酶，使互补链充分杂交ENDIF第3步在试管T中加入Mung Bean核酶，

39、降解所有单链DNA分子IF待检测的公式为识，其中i是从1到9之间的某个自然数，THEN第4步对所有的从1到厶之间的自然数j，使用凝胶电泳技术分离出长度为IxoX。C(口，)xo瓦C(q)Xokfz I幼的DNA分子，通过凝胶成像系统显示结果考察杂交反应前系统路径DNA分子浓度是否约等于反应后完全双链DNA分子浓度如果是，模型检测结果返回“Yes”否则，模型检测结果返回“No”，并使用sanger测序法生成一系列长度相差1个碱基的PCR产物混合物，根据不同长度片段的电泳速度不同，电泳技术直接读取DNA上的核苷酸顺序，比较不完全双链分子与转移规则编码，即可获得不满足公式的自动机路径ELSE*待检测

40、的为一般公式第4步对所有的从1到1。之间的自然数j，使用凝胶电泳技术分离出长度为I J-X。瓦C(口-)xo矗C(q)XoXmIz l幼的DNA分子，通过凝胶成像系统显示结果考察杂交反应前系统路径DNA分子浓度是否约等于反应后完全双链DNA分子浓度如果是，模型检测结果返回“Yes”否则，模型检测结果返回“No”，并使用sanger测序法生成一系列长度相差1个碱基的PCR产物混合物，根据不同长度片段的电泳速度不同，电泳技术直接读取DNA上的核苷酸顺序，比较不完全双链分子与转移规则编码，即可获得不满足公式的自动机路径ENDIFEND公式FSA接受运行可产生完全双链DNA分子，它既含启动区又含终止区

41、，无法被Mung Bean万方数据12期 朱维军等：基于DNA计算的线性时序逻辑模型检测方法 2585核酶切开而不被公式FSA接受的运行则产生部分双链DNA分子，将被Mung Bean核酶切开，切后的产物或者只含启动区，或者只含终止区算法2就是根据此现象获得检测结果读出检测结果需要使用凝胶电泳技术当接受运行经过J个原子命题时，分子编码为I-X0XmC(n，)XokC(口i)XoXmI：，其长度l L xo矗C(口1)XokC(口，)Co墨f2 II j1 I+I L I+(j+1)I X0溉I+I C(a。)1，而l L l，l L I，XoXml，lC(a。)I均为在编码设计阶段即被确定的常

42、数，因此在使用凝胶电泳技术时，DNA分子的长度可利用上式计算由于经过原子命题的数目不同，因此不同的接受运行都有其不同的长度单链分子、不同时包含启动区与终止区的双链分子并非接受运行，其长度均不符合上式计算结果因此可知，长度符合上式计算结果的双链分子与接受运行存在对应关系当所有运行(路径)均满足公式时，系统满足公式在真实的检测中，情况更加复杂DNA计算本质上是一种概率计算，真阳性的概率无法达到百分之百在本算法中如果特异性生化反应概率接近l，即可判定模型检测结果有效杂交后长度为J I，X。X。C(a1)X。X。C()XoX。12 I坳的分子浓度若约等于杂交前I类分子的浓度，则真阳性率接近于1其中，D

43、NA分子浓度的测定可使用分光光度法，通过分光光度计读取0I)260值，根据DNA浓度公式计算分子浓度当真阳性率远小于1时，系统不满足公式，模型检测算法需给出反例此时，并非所有路径分子均形成长度为I 11 XoX。C(n1)XoX。C(ni)X。X。J。I幼的完全双链分子，对部分双链分子，经Mung Bean核酶降解，获得字符串分子与部分转移规则分子的配对，如此配对在逻辑层面并非完全，但在分子层面则为双链分子片段使用sanger测序法可读出双链片段如下信息：何种字符串与何种转移规则实现了匹配，代表何种系统运行路径的字符串未能实现与转移规则的完全匹配使用电泳技术读出此字符串，即为算法给出的反例例4

44、 图2所示的系统FSA满足公式1，其DNA计算原理如图6所示图6(a)给出了1种DNA分子，被用于表征系统FSA的一个接受运行。一1-2，此运行经过的3个状态满足的原子命题序列可为PPq也可为qPq图6(c)给出了5种DNA分子，分别表征公式FSA的初始状态跏、终止状态如。、转移规则1、转移规则2以及转移规则3(3个转移规则的含义参见例1)如图6(d)所示，粘贴自动机编码框架内恰当的DNA编码设计可导致如下现象发生表征状态$00的1个分子、表征状态s吡的1个分子、表征转移规则1的2个分子、表征转移规则2的1个分子与表征系统运行。一1-2的1个分子通过碱基配对形成1个完全双链参见图6(d)，从左

45、往右观察此完全双链的上下两条单链，可见它们携带的信息均符合如下特征：从初始状态出发，到终止状态结束，中间经过的原子命题序列为PPq这意味着，系统运行。一12经过的字符串PPq是公式1的FSA的一个接受字同理可见，所有I类分子与所有II类分子均形成完全双链，因此可知，系统的所有接受运行都是公式1的FSA的接受字因此，可以获得如下模型检测结果：图2所示的系统FSA满足公式1(a)表征系统FsA一个运t?o一1-2的DNA分子0 1 0 1 2(b)表征系统FsA一个运行0101-2的DNA分子圜圜 l转移规l I转移规lJ则(边)IJ则(边)JI，II soD-q飞lI雕JDNA|篚JDNAll编

46、码|编码I(C)表征公式FSA的5种DNA分子系统的一个运行0一i-2(满足搠或咖)(DNA分子)公式FSA 公式FSA 公式FSA 公式FSA 公式FsA的初始 的转移规 的转移规 的转移规 的终止状态则，则声则1飞l 状态(DNA(DNA(DNA(DNA(DNA分子) 分子) 分子) 分子) 分子)(d)两类分子杂交之后形成完全双链图6一个模型检测例子：图2所示FSA满足公式134复杂度分析文献36给出了算法1，并指出其复杂度为O(x+y)，其中X和Y分别为自动机的节点数和边数算法2需要调用算法1作为前者的输入设算法2本身调用的基本操作包括基本生化操作、基本逻辑操作(基本电子操作)其中，基

47、本生化操作包括向试管中加入编码、退火、连接、提取前缀操作(使用探针杂交或PCR技术)、提取后缀操作(使用探针杂交或PCR技术)、亲和纯化、凝胶电泳、合并试管、添加酶、测序；基本逻辑操作包括赋值、按习爿目一问嗣圆一。戚凹一问嗣园一。腻倒一问硎园一。隔幽一问隔区一一启硎区一万方数据计 算 机 学 报给定式子计算数值算法2始于10个赋值语句，执行了10个基本逻辑操作第1步使用1次凝胶电泳技术以分离不同长度的分子第2步调用合并试管与添加酶各1次，计2个基本生化操作第3步添加酶1次第4步使用2次凝胶电泳技术和1次sanger测序综上，算法2需执行O(1)个基本操作，调用算法1作为输入需时O(z+y)，因此算法2共计执行O(z+y)个基本操作表2给出了新算法与相关方法的复杂度比较可见，与基于电子计算的经典方法相比，基于DNA计算的新方法把基本操作次数的数量级降为线性然而，生物操作所需时间既不统一也不固定，一些杂交反应甚至需要数小时才能达到平衡状态3 7|，这也是当前的DNA计算面临的共性问题之一两种机制的计算方法存在互补性表2时序逻辑模型检测的DNA方法的复杂度比较O(z+y)个基本操作O(z+了)个基本操作PSPACE个基本操作4仿真实验41实验所需的DNA编码设计本文算法在粘贴自动机通用模型上构建，因此必须满足粘贴自动机的编码设计规则，仅在规则框架内细化设计