發(fā)布時(shí)間：2019-07-29 20:32

【摘要】：隨著量子計(jì)算、量子信息以及量子物理技術(shù)不斷進(jìn)展,形式化驗(yàn)證量子系統(tǒng)的重要性已經(jīng)日益凸顯.由于物理環(huán)境的干擾和系統(tǒng)復(fù)雜性,在設(shè)計(jì)和實(shí)現(xiàn)量子系統(tǒng)的時(shí)候不可避免的會(huì)出現(xiàn)缺陷和錯(cuò)誤,因此保證量子系統(tǒng)的正確性、安全性和可靠性就至關(guān)重要了.而形式化驗(yàn)證是解決這些問題的關(guān)鍵技術(shù),已經(jīng)被應(yīng)用于驗(yàn)證量子通信的安全性和量子程序的正確性.不管是量子模擬計(jì)算還是量子并行計(jì)算,原理上都是利用量子相干性.然而,真實(shí)的量子系統(tǒng)具有開放性,并不是一個(gè)孤立系統(tǒng).事實(shí)上,它會(huì)與外部環(huán)境發(fā)生相互耦合,造成量子相干性很難得到保持,從而出現(xiàn)量子相干性的衰減.這就是所謂的消相干.因此,相比封閉量子系統(tǒng)來說,更有必要對(duì)開放量子系統(tǒng)的形式化驗(yàn)證做一定的研究.形式化驗(yàn)證包括三種類型:等價(jià)性檢測、模型檢測和定理證明.其中,模型檢測是目前較為成功的一種形式化驗(yàn)證方法,在學(xué)術(shù)界和工業(yè)界都得到廣泛關(guān)注和應(yīng)用.由于量子系統(tǒng)與經(jīng)典系統(tǒng)存在根本性差異,這就意味著經(jīng)典模型檢測技術(shù)不能直接推廣到量子系統(tǒng)中,所以開放量子系統(tǒng)的模型檢測是一項(xiàng)富有挑戰(zhàn)性的工作.本論文主要圍繞建立一個(gè)開放量子系統(tǒng)的邏輯語言、量子遷移系統(tǒng)線性時(shí)間屬性的檢測、量子馬爾可夫鏈的檢測和廣義量子Loop程序終止的驗(yàn)證等幾個(gè)方面進(jìn)行研究.文章的具體工作有以下幾個(gè)方面:(1)開放量子系統(tǒng)的量子邏輯研究:從語構(gòu)和語義角度構(gòu)建一套適合于刻畫開放量子系統(tǒng)的邏輯,稱為量子算子邏輯.作為公理化系統(tǒng),證明量子算子邏輯具有可靠性和完備性.作為可滿足性系統(tǒng),討論量子算子邏輯的可滿足性問題.研究表明:對(duì)于量子算子邏輯公式的可滿足性,存在有限模型結(jié)構(gòu).給定一個(gè)模型結(jié)構(gòu),提出量子算子邏輯的公式可滿足的檢測算法.作為量子算子邏輯的應(yīng)用,邏輯刻畫了貝爾態(tài)的糾纏性以及推理BB84協(xié)議的安全性.該內(nèi)容見第三章.(2)開放量子遷移系統(tǒng)的模型檢測:基于量子算子邏輯,定義開放量子遷移系統(tǒng),用于描述量子系統(tǒng)的演化.由于量子系統(tǒng)具有無窮多個(gè)量子態(tài),這不利于提出有效搜索算法,為了避免這樣的問題,引入一個(gè)有窮抽象量子狀態(tài)的概念.針對(duì)開放量子遷移系統(tǒng),提出量子線性時(shí)間屬性,包括量子安全性、量子不變性、量子活性和量子持續(xù)性等.分別針對(duì)量子不變性和量子安全性給出檢測算法,重點(diǎn)提出基于自動(dòng)機(jī)的量子正則安全性的檢測技術(shù).作為應(yīng)用,驗(yàn)證開放量子行走的目標(biāo)頂點(diǎn)的可達(dá)性.該內(nèi)容見第四章.(3)量子馬爾可夫鏈的模型檢測:基于量子算子邏輯,引入一類新型量子馬爾可夫鏈,定義量子線性時(shí)間屬性,并分析量子馬爾可夫鏈的可達(dá)性.分別針對(duì)測量一次、測量多次情形,提出基于自動(dòng)機(jī)的量子正則安全性的檢測技術(shù).該內(nèi)容見第五章.(4)廣義量子Loop程序終止驗(yàn)證:利用量子馬爾可夫鏈對(duì)廣義量子Loop程序進(jìn)行建模.通過引入以一定概率在第n步終止和可終止兩種定義,解決現(xiàn)有終止定義在表達(dá)力方面存在的問題.分析終止問題的歸約和終狀態(tài)的可達(dá)性,提出程序終止的驗(yàn)證方法.針對(duì)單量子比特系統(tǒng)、多量子比特系統(tǒng)、復(fù)合量子系統(tǒng)、嵌套量子系統(tǒng),給出廣義量子Loop程序終止的概率和終狀態(tài)的顯式計(jì)算表達(dá)式.最后,證明廣義量子Loop程序終止的充分必要條件.該內(nèi)容見第六章。
【圖文】：

邐邋＜５逡逑圖４．２邋（ＪＴＳ和１ＱＦＡ－ＣＭ的乘積系統(tǒng)逡逑根據(jù)定理４．３．２，可將可滿足性問題轉(zhuǎn)換為量子不變性Ｓ曰［＆Ｋ］在乘逡逑積系統(tǒng)中是否是可滿足的，即驗(yàn)證逡逑９了５邋＠l鈴澹保藉澹媯В睿觶╨粒義隙雜詬夢侍飪桑子盟惴ǎ玻孔硬槐湫緣哪Ｐ圖觳猓┙星蠼猓搜櫓さ膩義峽陜閾�，只袠q悸淺嘶刺ǎ粒穡┲械牡詼齜至浚校饈怯捎誆淮嬖諞桓齔嘶村義希叮卞義，

本文編號(hào)：2520739