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

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

本文編號：2520739