朱維軍,周清雷,李永亮

(鄭州大學(xué)信息工程學(xué)院,河南鄭州 450001)

?

以DNA為載體的線性時序邏輯模型檢測

朱維軍,周清雷,李永亮

(鄭州大學(xué)信息工程學(xué)院,河南鄭州 450001)

線性時序邏輯模型檢測被廣泛應(yīng)用于處理器設(shè)計與驗證、網(wǎng)絡(luò)協(xié)議驗證、安全協(xié)議驗證等領(lǐng)域.然而到目前為止,該技術(shù)只能在電子計算的平臺上實現(xiàn).為了以脫氧核糖核酸(Deoxyribo Nucleic Acid,DNA)為載體對線性時序邏輯(Linear Temporal Logic,LTL)實施模型檢測,給出了使用粘貼自動機實現(xiàn)Until算子模型檢測的方法.首先,使用粘貼自動機對Until公式的有窮狀態(tài)自動機(Finite State Automata,FSA)模型進行編碼;然后,將系統(tǒng)模型轉(zhuǎn)換為粘貼自動機的輸入字符串;最后,用粘貼自動機驗證系統(tǒng)是否滿足公式.仿真實驗結(jié)果證實,新方法可實現(xiàn)對LTL邏輯時序算子的檢測.

模型檢測;脫氧核糖核酸;線性時序邏輯;粘貼自動機

1　引言

模型檢測由圖靈獎得主Clarke教授等人提出[1].它是一種能夠自動驗證系統(tǒng)是否滿足給定性質(zhì)的形式化核心方法與技術(shù),被廣泛地應(yīng)用于硬件驗證[2]、網(wǎng)絡(luò)協(xié)議驗證、安全協(xié)議驗證[3]等領(lǐng)域.在時序邏輯模型檢測中,線性時序邏輯[4](Linear Temporal Logic,LTL)、計算樹邏輯[5](Computation Tree Logic,CTL)分別被用來描述系統(tǒng)需滿足的線性時序性質(zhì)和分支時序性質(zhì),有窮狀態(tài)自動機(Finite State Automata,FSA)則被用來為系統(tǒng)建模,模型檢測算法自動檢測模型是否滿足需求性質(zhì).

脫氧核糖核酸(Deoxyribo Nucleic Acid,DNA)計算以DNA分子為載體,以生物酶和生物操作作為信息處理工具,是一種與電子計算不同的計算模型.1994年,圖靈獎得主Adleman教授發(fā)表在《Science》上的一篇文章用DNA實驗求解了一個小規(guī)模的哈密頓路徑問題[6],被認為是DNA計算領(lǐng)域的開創(chuàng)性工作.由于DNA分子在實驗操作上相對容易,分子機構(gòu)上便于信息處理,DNA計算得到快速發(fā)展.學(xué)者們提出了諸如過濾模型[7]、粘貼自動機[8]等等DNA計算模型,并用這些模型成功解決了一系列NP難題:中國郵遞員問題和0-1規(guī)劃問題的DNA算法[9,10]、圖的最大團問題和最小覆蓋問題的DNA算法[11,12]、圖著色問題的DNA算法[13].特別是,許進教授等人用并行DNA計算模型解決了61個頂點的3著色問題[14].最新的一系列研究[15～17]更是涉及到了納米器件與DNA自組裝.

在經(jīng)典計算中的模型檢測,狀態(tài)空間與效率始終是困擾研究人員的難題.DNA計算具有強大的并行處理能力,可為模型檢測效率提升提供新的思路.2006年,圖靈獎得主Emerson教授提出了一種用DNA分子進行CTL模型檢測的思路與構(gòu)想,給出了CTL公式EFp的DNA模型檢測方法[18].這是使用DNA計算實現(xiàn)模型檢測的一個嘗試.然而,該方法不能對一般CTL公式實施檢測,更不能對LTL公式進行檢測.為此,我們研究以DNA分子為載體的LTL模型檢測方法.

2　線性時序邏輯與FSA

2.1線性時序邏輯

LTL邏輯的一階部分不可判定,因此我們只需研究其命題部分(Propositional LTL,PLTL).

定義1設(shè)AP是原子命題集合,如果φ和ψ是PLTL公式,那么,p∈AP、┑φ、φ∨ψ、φ?ψ都是PLTL公式.

定義2一個PLTL模型是一個三元組M=(S,R,L),其中:

(1)S是非空有窮狀態(tài)集,s∈S是狀態(tài);

(2)R:S→S,R(s)是狀態(tài)s的唯一后繼狀態(tài);

(3)L:S→2AP,L(s)是在狀態(tài)s中成立的原子命題的集合.

定義3滿足關(guān)系╞定義如下:

(1)s|=p當(dāng)且僅當(dāng)p∈L(s);

(2)s|=┑φ當(dāng)且僅當(dāng)┑(s|=φ);

(3)s|=φ∨ψ當(dāng)且僅當(dāng)(s|=φ)∨(s|=ψ);

(4)s|=φ?ψ當(dāng)且僅當(dāng) ?j≥0.Rj(s)|=ψ∧(?0≤k

2.2FSA

定義4一個FSAA是一個五元組(Σ,Q,T,q0,F),其中:

(1)Σ是一個有窮非空字母表;

(2)Q是一個有窮非空狀態(tài)集;

(3) 轉(zhuǎn)移函數(shù)T:Q×Σ→R(Q);

(4)q0∈Q是起始狀態(tài);

(5)F?Q是接受狀態(tài)集.

定義5設(shè)w=y1,…,ym是定義在Σ上的字符串,如果存在Q中狀態(tài)序列r0,r1,…,rm滿足:

(1)r0=q0

(2)ri+1∈T(ri,yi+1),i=0,1,…,m-1

(3)rm∈F

則稱w是被A接受的文字.

定義6A識別的語言是被A接受的文字的集合.

3　粘貼自動機

粘貼自動機[8]是一種實現(xiàn)FSA的DNA計算模型,給定輸入字符串的DNA鏈,粘貼自動機模型能夠判斷字符串是否被自動機接受.

3.1FSA和輸入字符串的編碼方式

假設(shè)M=(Σ,S,T,s0,F)是一個FSA,字母表Σ中的任意一個字符a都可以用單鏈DNA編碼為C(a).

(1)Σ上的輸入字符串w=a1,…,an用一個DNA單鏈編碼:5′I1X0…XmC(a1)…X0…XmC(an)X0…XmI23′,其中,I1是啟動區(qū)序列,X0…Xm是間隔序列,用來間隔字符ai的編碼C(ai),I2是終止區(qū)序列.

3.2計算過程

粘貼自動機模型的計算過程分為3步:

第一步:數(shù)據(jù)預(yù)處理

(1) 合成輸入字符串和自動機的編碼鏈.

(2) 將所有的DNA鏈放到試管T中,使互補鏈充分結(jié)合.

(3) 在試管中T加入DNA連接酶,得到(部分)雙鏈DNA分子.

第二步:計算

經(jīng)過第一步的數(shù)據(jù)處理,如果輸入字符串被自動機接受,那么試管T中應(yīng)該是以啟動區(qū)開始以終止區(qū)結(jié)束的完全雙鏈的DNA分子;否則,試管T中的DNA不是完全雙鏈,要么終止區(qū)是部分雙鏈,要么啟動區(qū)和終止區(qū)中的某部分是部分雙鏈的.根據(jù)上述情況,可以向試管T中加入Mung Bean核酶,降解其中的單鏈DNA片段,保留完全雙鏈的DNA分子.

第三步:輸出結(jié)果

向試管T中加入Mung Bean核酶后,可以利用電泳技術(shù)分離不同長度的DNA分子,如果存在兩種或者兩種以上的不同的DNA分子質(zhì)量,說明在加入核酶前,試管T中存在部分雙鏈的DNA分子,輸入字符串不被自動機接受;否則,在加入核酶前,T中全部是完全雙鏈DNA分子,輸入字符串是被自動機接受的.

4　用粘貼自動機實現(xiàn)PLTL模型檢測

4.1將PLTL公式轉(zhuǎn)換為FSA

PLTL的基本核心公式如下:

p?q

(1)

圖1是式(1)的FSA模型.按照粘貼自動機模型中FSA的編碼方式編碼圖1中的自動機,將編碼好的DNA單鏈放到試管R中.

4.2生成系統(tǒng)模型的符合粘貼自動機的輸入字符串格式的運行

首先,我們用圖2所示的單鏈DNA對系統(tǒng)的狀態(tài)進行編碼.其中:X0…Xm是粘貼自動機中的間隔序列,為滿足粘貼自動機輸入字符串的格式而增加;L(s)是狀態(tài)標(biāo)簽函數(shù);Y用來調(diào)節(jié)編碼,使每個狀態(tài)編碼的長度為相等的偶數(shù),并且保證狀態(tài)和狀態(tài)編碼之間一一對應(yīng).

在狀態(tài)編碼的基礎(chǔ)上,我們可以使用算法1生成系統(tǒng)自動機模型中以開始狀態(tài)為始點以終止?fàn)顟B(tài)為終點的所有路徑.算法描述如下.

算法1系統(tǒng)模型自動機的運行路徑生成算法

Input:公式(1)的自動機模型M

Output:表達M所有路徑的所有DNA分子

BEGIN

第1步:對于每個狀態(tài)s,向試管T中加入s的編碼;對于每條邊e,向試管T中加入e的編碼.經(jīng)過退火和連接反應(yīng),生成系統(tǒng)的FSA模型中的隨機路徑.

第2步:對試管T執(zhí)行提取前綴操作,使試管T中只含有以開始狀態(tài)為起點的路徑.

第3步:對試管T執(zhí)行提取后綴操作,使試管T中只含有以終止?fàn)顟B(tài)為終點的路徑.

第5步:通過親和純化技術(shù),過濾出試管T中所有包含I1和I2序列的單鏈DNA分子.

END

其中,第5步除去第4步中多余的DNA分子,得到滿足粘貼自動機輸入字符串格式要求的單鏈DNA分子,每條單鏈DNA對應(yīng)系統(tǒng)的一個運行.

4.3用粘貼自動機驗證系統(tǒng)是否滿足PLTL公式

4.1節(jié)獲得表征式(1)模型的單鏈DNA分子;4.2節(jié)的算法則得到了表征系統(tǒng)模型的單鏈DNA分子.在此基礎(chǔ)上,我們通過讓上述兩類單鏈DNA分子充分地進行生化反應(yīng),即可檢測系統(tǒng)是否滿足式(1).檢測方法如算法2所示.需要補充說明的是,我們可以證明:要驗證一個系統(tǒng)是否滿足式(1),只需驗證系統(tǒng)的長度小于|V|*2|V|-1+|E|的所有運行是否滿足式(1).篇幅所限,不再給出詳細證明過程.

算法2公式(1)的DNA模型檢測算法

Input:4.1節(jié)的試管R,即式(1)對應(yīng)的粘貼自動機的編碼;算法1獲得的試管T,即系統(tǒng)的所有運行

Output:系統(tǒng)模型是否滿足公式

BEGIN

第1步:用長度分離操作提出試管T中長度小于|V|*2|V|-1+|E|的單鏈DNA.

第2步:合并試管R到T,在T中加入DNA連接酶,使互補鏈充分反應(yīng).

第3步:充分反應(yīng)后,在試管T中加入MungBean核酶,降解所有單鏈DNA.

第4步:對T執(zhí)行分離操作,得到試管T1和T2,T1中是含有啟動區(qū)的DNA鏈,T2中則是不含的.

第5步:檢測T2.若T2中有DNA鏈,則它不含啟動區(qū),它是第2步中的部分雙鏈DNA分子被第3步中的核酶切開后的產(chǎn)物,第2步含有部分雙鏈DNA分子,系統(tǒng)有不滿足式(1)的運行.否則,執(zhí)行下一步.

第6步:對T1執(zhí)行分離操作,得到試管R1和R2,R1中是含有終止區(qū)的DNA鏈,R2中則是不含的.

第7步:檢測R2,如果R2中有DNA鏈,那么它只含有啟動區(qū)而不含有終止區(qū),它是第2步中的部分雙鏈DNA分子被第3步中的MungBean核酶切開后的產(chǎn)物.第2步含有部分雙鏈DNA分子,說明系統(tǒng)有不滿足式(1)的運行.否則,系統(tǒng)的所有運行都被粘貼自動機接受,系統(tǒng)滿足式(1).

END

式(1)對應(yīng)的自動機接受的運行會產(chǎn)生完全雙鏈DNA分子,它既含有啟動區(qū)又含有終止區(qū),不會被MungBean核酶切開;而不被自動機接受的運行會產(chǎn)生部分雙鏈DNA分子,將被MungBean核酶切開,切后的產(chǎn)物要么只含有啟動區(qū),要么只含有終止區(qū).算法2就是根據(jù)這個事實檢測的.

4.4復(fù)雜度分析

算法2有兩個輸入:系統(tǒng)模型的符合粘貼自動機輸入字符串格式的運行;式(1)對應(yīng)的粘貼自動機模型.

假設(shè)系統(tǒng)模型有x個狀態(tài)、y條邊,算法1生成系統(tǒng)模型的符合粘貼自動機輸入字符串格式的運行.第1步要合成所有狀態(tài)和邊的編碼,此步共需執(zhí)行x+y個操作步驟;第2、3、5步,每步均需執(zhí)行1個操作步驟;第4步需執(zhí)行2個操作步驟,(分別為加入兩個DNA分子).因此,生成系統(tǒng)模型的符合粘貼自動機輸入字符串格式的運行的時間復(fù)雜度是O(x+y)+O(3)+O(2)=O(x+y).

假設(shè)有限狀態(tài)自動機M有m個狀態(tài)、n條邊,在建立其對應(yīng)的粘貼自動機模型的過程中,合成所有狀態(tài)和邊的編碼共需m+n個操作步驟,而式(1)對應(yīng)的自動機中,m=3、n=6,因此,建立式(1)對應(yīng)的粘貼自動機模型共需執(zhí)行9個操作步驟.

最后,在用粘貼自動機模型驗證系統(tǒng)運行是否滿足式(1)的算法2中,這7步中的每一步都需要執(zhí)行1個操作步驟.綜上所述,算法2的時間復(fù)雜度是O(x+y)+O(9)+O(7)=O(x+y).

表1給出了新算法與相關(guān)方法的復(fù)雜度比較.

表1　時序邏輯模型檢測的DNA方法的檢測效率之比較

5　仿真實驗

我們在Win7操作系統(tǒng)上,用VB語言編寫實驗程序以實現(xiàn)算法.新方法涉及的所有分子生物元操作,均已在現(xiàn)有的DNA計算相關(guān)工作中被使用,這些元操作的有效性也已被前人工作中的真實分子生物實驗所證實.因此,本文采用仿真實驗代替真實生物實驗,獲得的結(jié)果是可信的.

表2和表3給出了實驗的編碼方式.在此基礎(chǔ)上,我們實施了兩個仿真實驗.

表2　輸入字符串的編碼規(guī)則(即系統(tǒng)的運行,按照粘貼自動機輸入字符串的編碼方式編碼)

表3　式(1)對應(yīng)的自動機(按照粘貼自動機的編碼方式編碼)

實驗1系統(tǒng)模型如圖3,|V|=3,|E|=3,要驗證的系統(tǒng)運行的最大長度是15.由圖3可知:在狀態(tài)0,p和q同時滿足;由表2最后一行可知,p對應(yīng)的編碼是GG,q對應(yīng)的編碼是TT;因此狀態(tài)0對應(yīng)的編碼是GG/TT,其中斜線表示“或”,即不同的DNA分子可在p和q任選其一.依次類推,狀態(tài)1對應(yīng)的編碼是GG,狀態(tài)2對應(yīng)的編碼是TT.表4是系統(tǒng)模型長度不超過15的所有7個運行.算法2讓表3中單鏈DNA分子與表4中的單鏈DNA分子進行充分的生化反應(yīng),得到的雙鏈DNA分子如表5所示,即為系統(tǒng)運行7條路徑的檢測結(jié)果.由表5可見,所有路徑都是完整的雙鏈DNA分子,這表明所有運行均滿足p?q,因此系統(tǒng)滿足p?q.

表4　實驗1的系統(tǒng)運行

路徑路徑的DNA編碼或者路徑經(jīng)過的頂點順序1號路徑的編碼ATATCAAGCTACGG/TTCAAGCTACGGCAAGCTACTTCAAGCTACCGCG1號路徑的頂點順序0,1,22號路徑的編碼ATATCAAGCTAC(GG/TTCAAGCTACGGCAAGCTAC)2TTCAAGCTACCGCG2號路徑的頂點順序0,1,0,1,2k號路徑的編碼ATATCAAGCTAC(GG/TTCAAGCTACGGCAAGCTAC)kTTCAAGCTACCGCGk號路徑的頂點順序(0,1)k,27號路徑的編碼ATATCAAGCTAC(GG/TTCAAGCTACGGCAAGCTAC)7TTCAAGCTACCGCG7號路徑的頂點順序0,1,0,1,0,1,0,1,0,1,0,1,0,1,2

表5　實驗1的系統(tǒng)運行的檢測結(jié)果

實驗2系統(tǒng)模型如圖4,|V|=3,|E|=4,要驗證的系統(tǒng)運行的最大長度是16.由圖4可知:狀態(tài)0對應(yīng)的編碼是GG/TT,狀態(tài)1對應(yīng)的編碼是GT,狀態(tài)2對應(yīng)的編碼是TT.表6是系統(tǒng)模型長度不超過16的所有29個運行.算法2讓表3中的單鏈DNA分子與表6中的單鏈DNA分子進行充分的生化反應(yīng),得到的雙鏈DNA分子如表7所示,即為系統(tǒng)運行29條路徑的檢測結(jié)果.

由表7可見,存在一部分路徑不是完全的雙鏈DNA分子,說明這些路徑不滿足p?q.因此系統(tǒng)不滿足p?q.

表6　實驗2的系統(tǒng)運行

表7　實驗2的系統(tǒng)運行的檢測結(jié)果

續(xù)表

實驗1和實驗2分別針對系統(tǒng)滿足公式和系統(tǒng)不滿足公式這兩種情況進行仿真檢測.把有關(guān)這些實驗所獲結(jié)果的表格(表4、表5、表6和表7)綜合起來,我們可以看出:無論系統(tǒng)模型是否滿足式(1),該式都可以使用DNA分子來實現(xiàn)模型檢測;特別是,當(dāng)系統(tǒng)不滿足式(1)時,新算法可以給出反例,以具體指出是系統(tǒng)中的哪些路徑不滿足公式,正如表7中的單號路徑所示.

進一步地,我們把有關(guān)新方法的上述實驗結(jié)果與相關(guān)方法進行比較,結(jié)果如表8所示.從表中不難看出:文獻[18]給出的是針對CTL公式的DNA模型檢測方法;而本文給出的是針對LTL公式的DNA模型檢測方法.由于Until是LTL公式的核心算子,Final與Always等其它時序算子表達的公式均可轉(zhuǎn)化為Until算子表達的公式,因此,時序算子加原子命題組成的LTL公式就可以在DNA分子上實施模型檢測.這是新算法相對于文獻[18]中方法的比較優(yōu)勢.

表8　時序邏輯模型檢測的DNA方法的檢測能力之比較

6　結(jié)論

本文的主要成果是算法2.使用該算法即可在DNA計算框架內(nèi)實現(xiàn)LTL邏輯的核心算子模型檢測.這是本文工作的貢獻.一方面,基于DNA計算的方法可利用其巨大的天然的并行計算優(yōu)勢緩解LTL模型檢測當(dāng)前面臨的狀態(tài)空間爆炸這一瓶頸,這是新算法在計算機科學(xué)中的潛在應(yīng)用價值.另一方面,在細胞內(nèi)進行的LTL模型檢測計算,將使得對腫瘤分子標(biāo)志發(fā)展過程的動態(tài)識別與動態(tài)地自動調(diào)整藥物用法與用量成為可能,進而有望為人類疾病的分子診療提供更好的自治智能方法,這是新方法在分子生物學(xué)與醫(yī)學(xué)中的潛在應(yīng)用價值.

[1]CLARKE E.Model Checking[M].Massachusetts:MIT Press,1999.

[2]BAMAT J,BAUCH P,BRIM L,et al.Designing fast LTL model checking algorithms for many-core GPUs[J].Journal of Parallel and Distributed Computing,2012,72(9):1083-1097.

[3]CARBONE R.LTL model-checking for security protocols[J].AI Communications,2011,24(3):281-283.

[4]GOTZHEIN R.Temporal logic and applications-a tutorial[J].Computer Networks and ISDN Systems,1992,24(3):203-218.

[5]BENARI M,PNUELI A,MANNA Z.The temporal logic of branching time[J].Acta Informatica,1983,20(3):207-226.

[6]ADLEMAN L.Molecular computation of solutions to combinatorial problems[J].Science,1994,266(5187):1021-1023.

[7]ADLEMAN L.On constructing a molecular computer[J].Discrete Mathematics and Theoretical Computer Science,1995,27:1-21.

[8]ZIMMERMANN K,IGNATOVA Z,PEREZ M.DNA Computing Models[M].Berlin:Springer,2008.

[9]YIN Z X,ZHANG F Y,XU J.A Chinese postman problem based on DNA computing[J].Journal of Chemical Information and Computer Sciences,2002,2(42):222-224.

[10]YIN Z X,ZHANG F Y,XU J.The general form of 0-1 programming problem based on DNA computing[J].Biosystems,2003,70(1):73-79.

[11]PAN L Q,XU J,LIU Y C.A surface-based DNA algorithm for the maximal clique problem[J].Chinese Journal of Electronics,2002,11(4):469-471.

[12]PAN L Q,XU J.A surface-based DNA algorithm for the minimal vertex cover problem[J].Progress in Natural Science,2003,13(1):81-84.

[13]高琳,許進.圖的頂點著色問題的DNA算法[J].電子學(xué)報,2003,31(4):494-497.

GAO Lin,XU Jin.A DNA algorithm for graph vertex coloring problem[J].Acta Electronica Sinica,2003,31(4):494-497.(in Chinese)

[14]XU J,QIANG X L,ZHANG K,et al.A parallel type of DNA computing model for graph vertex coloring problem[A].2010 IEEE Fifth International Conference on Bio-inspired Computing:Theories and Applications[C].Changsha:IEEE Press,2010.231-235.

[15]YANG J,DONG C,DONG Y,et al.Logic Nanoparticle beacon triggered by the binding induced effect of multiple inputs[J].ACS Applied Material Interfaces,2014,6(16):14486-14492.

[16]ZHANG C,WU L,YANG J,et al.A molecular logical switch beacon controlled by thiolated DNA signals[J].Chemical Communications,2013,49:11308-11310.

[17]ZHANG C,MA J,YANG J.Nanoparticle aggregation logic computing controlled by DNA branch migration[J].Applied Physics Letters,2013,103(9):093-106.

[18]EMERSON E A,HAGER K D,KONIECZKA J H.Molecular model checking[J].International Journal of Foundations of Computer Science,2006,17(04):733-741.

朱維軍男,1976年生于河南鄭州,現(xiàn)為鄭州大學(xué)副教授.主要研究方向:DNA計算、形式化方法.

E-mail:zhuweijun76@163.com

周清雷男,1962年生于河南新鄉(xiāng),現(xiàn)為鄭州大學(xué)教授、博士生導(dǎo)師.主要研究方向:DNA計算、形式化方法.

E-mail:ieqlzhou@zzu.edu.cn

Conduct Linear Temporal Logic Model Checking via DNA Molecules

ZHU Wei-jun,ZHOU Qing-lei,LI Yong-liang

(SchoolofInformationEngineering,ZhengzhouUniversity,Zhengzhou,Henan450001,China)

The linear temporal logic (LTL) model checking is widely used in processor design and verification,network protocol verification and security protocol verification.Up to now,this technique can only be realized on the platform of electronic computer.In order to conduct LTL model checking under the circumstance of deoxyribo nucleic acid (DNA),we proposed a method to check the Until constructor via a sticker automaton.We encode a finite state automaton (FSA) which is a model of the formula Until,with a DNA sticker automaton.And we convert a model of a system into its paths,as the input strings of the sticker automaton.We verify whether the system satisfies the formula or not,by using the sticker automaton.In this way,the formula Until can be checked with the double strand DNA molecules.The simulation results show that the method can successfully check the basic temporal formulas.

model checking;deoxyribo nucleic acid;linear temporal logic;sticker automaton

2014-11-15;修回日期:2015-01-27;責(zé)任編輯:覃懷銀

國家自然科學(xué)基金(No.61250007,No.U1204608,No.U1304606,No.61572444);中國博士后科學(xué)基金(No.2012M511588,No.2015M572120);河南省高等學(xué)校青年骨干教師資助計劃項目(No.2014GGJS-001)

TP301;TP384

A

0372-2112 (2016)06-1265-07