本文關(guān)鍵詞：基于DNA計算的CTL模型檢測方法研究

  更多相關(guān)文章： 模型檢測 計算樹邏輯 DNA 計算

【摘要】：模型檢測由圖靈獎得主Clarke教授等人提出,是一種能夠自動驗證系統(tǒng)是否滿足指定性質(zhì)的技術(shù),并且在系統(tǒng)不滿足性質(zhì)時提供反例,被廣泛地應(yīng)用于硬件驗證、網(wǎng)絡(luò)協(xié)議驗證、安全協(xié)議驗證、軟件驗證等領(lǐng)域,取得了令人矚目的成果。另一方面,作為一種新的計算載體,DNA具有很高的信息存儲密度和強(qiáng)大的并行處理能力,DNA計算為突破經(jīng)典模型檢測算法的效率限制提供了新的思路。2006年,著名的計算機(jī)科學(xué)家、圖靈獎得主Ernest Allen Emerson首次把分子生物計算應(yīng)用到模型檢測領(lǐng)域,提出了一種用DNA分子對計算樹邏輯(Computation Tree Logic,CTL)公式進(jìn)行檢測的方法。但是,Emerson教授只給出了一種CTL公式EFp的DNA檢測算法,目前尚無其它基于DNA計算的CTL邏輯公式的檢測算法,更沒有DNA計算方法可以對全部的CTL邏輯公式進(jìn)行檢測。這是本文研究和要解決的問題。Emerson教授的方法存在一些不足之處:一,CTL公式EFp的DNA檢測算法使用了DNA限制性內(nèi)切酶和DNA連接酶,酶切反應(yīng)和連接反應(yīng)在同一生化環(huán)境中進(jìn)行,對生化反應(yīng)的環(huán)境要求苛刻,可靠性較低;二,當(dāng)系統(tǒng)模型不滿足公式EFp時,算法不能提供反例;三,只給出了一種CTL公式的檢測方法,能夠檢測的公式類型單一。針對上述三個問題,首先,用帶標(biāo)簽的有限狀態(tài)自動機(jī)對系統(tǒng)建立模型;其次,探索合適的編碼方式,用DNA分子編碼系統(tǒng)模型;再次,經(jīng)過研究和分析,把對系統(tǒng)模型的驗證問題規(guī)約為對長度在閾值范圍之內(nèi)的運行的驗證問題;然后,通過調(diào)用DNA分子的7種基本操作,給出了生成長度在閾值范圍之內(nèi)的運行的算法;最后,給出了4種CTL公式的DNA檢測算法。對于公式EFp,新算法的反應(yīng)試管中只含有一種核酸酶—DNA連接酶,對反應(yīng)環(huán)境要求較低,可靠性較高;并且,當(dāng)系統(tǒng)模型不滿足公式時,新方法能給出反例;此外,新方法給出了另外三種公式的檢測算法,能夠檢測的公式類型更多。新方法有效地彌補(bǔ)了Emerson方法中的不足。
【關(guān)鍵詞】：模型檢測 計算樹邏輯 DNA 計算
【學(xué)位授予單位】：鄭州大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2015
【分類號】：TP38
【目錄】：

• 摘要4-5
• ABSTRACT5-9
• 1 緒論9-24
• 1.1 研究背景與現(xiàn)狀9-21
• 1.1.1 系統(tǒng)有效性證明9-11
• 1.1.2 模型檢測11-17
• 1.1.3 DNA計算17-21
• 1.1.4 模型檢測與DNA計算的關(guān)系21
• 1.2 當(dāng)前存在的問題21-22
• 1.3 論文組織結(jié)構(gòu)22-24
• 2 預(yù)備知識24-43
• 2.1 帶標(biāo)簽的有限狀態(tài)自動機(jī)24-26
• 2.2 CTL邏輯的語法和語義26-29
• 2.3 用CTL邏輯公式描述性質(zhì)29
• 2.4 DNA基礎(chǔ)知識29-34
• 2.4.1 DNA分子結(jié)構(gòu)29-30
• 2.4.2 DNA操作技術(shù)30-34
• 2.5 DNA計算模型34-42
• 2.5.1 Adleman的首次實驗34-37
• 2.5.2 分子模型檢測37-40
• 2.5.3 粘貼系統(tǒng)40-41
• 2.5.4 粘貼自動機(jī)41-42
• 2.6 本章小結(jié)42-43
• 3 四種CTL公式的DNA檢測算法43-51
• 3.1 與公式EGp、AGp、EFp和AFp相關(guān)的定理43-45
• 3.2 公式EGp、AGp、EFp和AFp的DNA檢測算法45-49
• 3.2.1 生成集合X中的所有運行45-47
• 3.2.2 CTL公式EGp模型檢測的DNA方法47-48
• 3.2.3 CTL公式AGp模型檢測的DNA方法48
• 3.2.4 CTL公式EFp模型檢測的DNA方法48-49
• 3.2.5 CTL公式AFp模型檢測的DNA方法49
• 3.3 算法時間復(fù)雜度分析49-50
• 3.4 本章小結(jié)50-51
• 4 仿真實驗51-57
• 4.1 實驗環(huán)境與方法51-53
• 4.2 實驗結(jié)果53-56
• 4.3 本章小結(jié)56-57
• 5 總結(jié)與展望57-58
• 5.1 總結(jié)57
• 5.2 展望57-58
• 參考文獻(xiàn)58-63
• 個人簡歷、在學(xué)期間參加的科研項目及發(fā)表的論文63-64
• 致謝64-65

【參考文獻(xiàn)】

中國期刊全文數(shù)據(jù)庫 前5條

1 吳帆;李肯立;;基于自組裝的N皇后問題DNA計算算法[J];電子學(xué)報;2013年11期

2 蒲飛;張文輝;;結(jié)合搜索空間劃分和抽象進(jìn)行LTL模型檢測[J];中國科學(xué)(E輯:信息科學(xué));2007年12期

3 徐亮;陳偉;徐艷艷;張文輝;;Improved Bounded Model Checking for the Universal Fragment of CTL[J];Journal of Computer Science & Technology;2009年01期

4 李肯立;羅興;吳帆;周旭;黃鑫;;基于自組裝模型的最大團(tuán)問題DNA計算算法[J];計算機(jī)研究與發(fā)展;2013年03期

5 葛志磊;樊春海;YAN Hao;;DNA納米自組裝的研究進(jìn)展及應(yīng)用[J];科學(xué)通報;2014年02期

，

本文編號：527764