雷紅軒,彭家寅,劉 熠

(1.內(nèi)江師范學(xué)院數(shù)學(xué)與信息科學(xué)學(xué)院,四川內(nèi)江 641112; 2.四川省高等學(xué)校數(shù)值仿真重點實驗室,四川內(nèi)江 641112)

幾類非確定型量子程序的終止驗證

雷紅軒1,2,彭家寅1,2,劉 熠1,2

(1.內(nèi)江師范學(xué)院數(shù)學(xué)與信息科學(xué)學(xué)院,四川內(nèi)江 641112; 2.四川省高等學(xué)校數(shù)值仿真重點實驗室,四川內(nèi)江 641112)

程序驗證是保證程序正確性的關(guān)鍵技術(shù).由于經(jīng)典世界和量子世界的本質(zhì)不同,經(jīng)典程序驗證的技術(shù)和工具不能直接應(yīng)用到量子系統(tǒng).而量子程序設(shè)計語言是描述量子系統(tǒng)的一種新的形式化模型,量子程序的驗證問題就顯得更為迫切和必要.本文首先討論了量子通訊中常用的比特翻轉(zhuǎn)、相位翻轉(zhuǎn)、去極化、幅值阻尼、相位阻尼等信道作為特殊的非確定型量子程序從計算基態(tài)開始運行時的可達集合和終止集合等程序驗證問題.其次,把上述五種量子程序兩兩組合組成非確定型量子程序,根據(jù)這五種量子程序的可達集合之相似點,最終合并成三種非確定型量子程序,重點討論了這三種非確定型量子程序從計算基態(tài)開始運行時的終止和發(fā)散等程序驗證問題.研究表明:這三種非確定型量子程序從計算基態(tài)0開始運行時都是終止的;而從計算基態(tài)1開始運行時:比特翻轉(zhuǎn)信道和去極化信道組成的非確定型量子程序的終止和發(fā)散與分別刻畫它們的兩個參數(shù)有關(guān);比特翻轉(zhuǎn)信道和相位翻轉(zhuǎn)信道組成的非確定型量子程序的終止和發(fā)散只與刻畫比特翻轉(zhuǎn)信道的參數(shù)有關(guān);幅值阻尼信道和相位阻尼信道組成的非確定型量子程序是發(fā)散的,其發(fā)散條件與刻畫量子信道的兩個參數(shù)都沒有關(guān)系.本文的結(jié)果可以為量子信息安全中量子通訊協(xié)議的驗證提供理論和技術(shù)支持.

量子通訊;量子程序;程序驗證;信息安全

1 引言

Shor[1]關(guān)于大數(shù)的質(zhì)因子分解算法以及Grover[2]關(guān)于數(shù)據(jù)庫搜索算法的相繼出現(xiàn),顯示出量子計算在某些計算領(lǐng)域比經(jīng)典計算更有效[3].當(dāng)前,量子算法還處在較低水平的量子線路的探索階段.正如Abramsky[4]所說的,高水平的概念化的方法對量子系統(tǒng)的設(shè)計、編程、推理是很必要的.正如此,在過去的20多年中,多種量子程序語言被先后定義和提出.比如,Knill[5]最先提出了設(shè)計量子程序語言,?mer[6]第一次給出了真正的量子程序語言并對其進行了計算仿真,Selinger[7]指出一個量子程序由超算子描述.正確性是程序的最重要的屬性之一.長期以來,如何保證程序的正確性、提高軟件的可信度一直是計算機科學(xué)界高度關(guān)注的一個重要問題,也是推動計算機科學(xué)發(fā)展的主要動力之一.由于量子通訊協(xié)議可以由量子程序表示,所以量子程序的驗證問題就顯得更為迫切和必要.

同時,一些量子過程代數(shù)也被先后提出,如Gay和Nagarajan[8]提出了CQP代數(shù),Feng等[9]提出了qCCS代數(shù),這些代數(shù)系統(tǒng)為量子通訊和非確定型程序建立了良好的模型.最近,Li[10]等作者定義了一個語言獨立的非確定型量子程序的模型,Yu[11]等作者提出了并發(fā)量子程序的概念和模型.在這些模型中,量子程序是由有限個量子隊列組成的,這些量子隊列是由狀態(tài)空間上的量子Markov鏈描述.本文在上述工作和作者已有成果的基礎(chǔ)上,首先討論量子通訊中常用的比特翻轉(zhuǎn)、相位翻轉(zhuǎn)、去極化、幅值阻尼、相位阻尼等信道作為特殊的非確定型量子程序—確定型量子程序,從計算基態(tài)開始運行時的可達集合、終止集合、發(fā)散集合等情況.其次按照可達集合重點討論這五種信道按照一定的組合方式組成的三種非確定型量子程序從計算基態(tài)開始運行時的終止和發(fā)散情況,進一步為量子程序和量子協(xié)議的驗證提供理論和技術(shù)支持.

2 基本概念

定義1[10]設(shè)H是一個有限維Hilbert空間,它也是量子程序的狀態(tài)空間.一個非確定型量子程序是二元組P=({εi|i=1,…,m},{M0,M1}),其中

(1)εi是H上的超算子,i=1,…,m;

(2){M0,M1}是H上的測量算子.

一個非確定型量子程序的一個計算是隨機地選取m個超算子中的一個組成的有限或無限的計算序列,在整個計算過程中,測量算子{M0,M1}作用在每一步上,以決定程序是終止還是繼續(xù)運行.這里選取“yes-no”測量,當(dāng)測量結(jié)果為0時，程序終止，此時程序狀態(tài)進入一個終止空間；否則，當(dāng)測量結(jié)果為1時，程序?qū)⑦M入下一步，繼續(xù)完成保跡的超算子ε.

程序P的執(zhí)行表定義為集合

S={1,2,…,m}∞={s1s2…sk…|sk∈{1,2,…,m},k≥0}

(1)

程序P的有限執(zhí)行表定義為集合

(2)

為方便起見,用θ表示空串.對任意的s=s1…sk∈Sfin,用|s|表示s的長度.對每一個|s|≤n,s(≤n)表示s的頭部s1s2,…,sn,也寫s=s1s2…∈S的頭部為

s(≤n)=s1s2…sn∈Sfin

(3)

和尾部為

s(>n)=sn+1sn+2…∈S

(4)

為了簡單表示,用Ti表示如下的超算子

(5)

其中,ρ∈D(H).進而,對任意的s=s1s2,…,sn∈Sfin,寫

Ts=Tsn°…°Ts2°Ts1

(6)

特別地,Tθ(ρ)=ρ.設(shè)ρ∈D(H)為輸入態(tài),程序P按照執(zhí)行表s=s1s2,…,∈S執(zhí)行,在n步后程序的狀態(tài)為Ts(≤n)(ρ).

定義2[10]設(shè)非確定型量子程序的輸入態(tài)為ρ,對任意一有限執(zhí)行表s∈Sfin,定義程序P在s內(nèi)終止的概率為

(7)

如果程序按照s=s1s2…執(zhí)行,則程序在不超過n步終止的概率為ts(≤n)(ρ).進而,程序在有限步終止的概率為

(8)

顯然,tr(ρ)≥ts(ρ),且tr(ρ)-ts(ρ)是程序在狀態(tài)ρ運行執(zhí)行表s時發(fā)散的概率.

對一個非確定型量子程序P,沿著任意一個執(zhí)行表s∈S的執(zhí)行都是可能的.因此,下面給出在所有可能的執(zhí)行路徑上程序終止概率的定義如下:

定義3[10]從狀態(tài)ρ開始運行的非確定型量子程序P的終止概率定義為t(ρ)=inf{ts(ρ)|s∈S}.

定義4[10](1)開始于狀態(tài)ρ的非確定型量子程序P的可達集合定義為R(ρ)={Ts(ρ)|s∈Sfin}.

(2)對任意的ρ∈D(H),如果t(ρ)=tr(ρ),則稱ρ是程序P的終止?fàn)顟B(tài),簡稱為終態(tài).用T表示程序P的所有終態(tài)的集合,即T={ρ∈D(H)|t(ρ)=tr(ρ)}.

(3)對任意的ρ∈D(H),如果對某些s∈S,有ts(ρ)=0,則稱ρ是P的發(fā)散態(tài).用D表示程序P的所有發(fā)散態(tài)的集合,即D={ρ∈D(H)|ts(ρ)=0,對某些s∈S}.

等式t(ρ)=tr(ρ)被叫做非確定型量子程序P的終止條件.這個條件是說,只要程序P從狀態(tài)ρ開始,則它一定會在有限步內(nèi)終止且終止概率為1.

下面分別用I,X,Y,Z表示單位矩陣、Pauli-X矩陣、Pauli-Y矩陣、Pauli-Z矩陣.H2=span{|0〉,|1〉},M0=|0〉〈0|,M1=|1〉〈1|.

3 常用信道組成的確定型量子程序的可達集合和終態(tài)

為便于閱讀,用Ei,i=1,…,5和εi,i=1,…,5分別表示比特翻轉(zhuǎn)、相位翻轉(zhuǎn)、去極化、幅值阻尼、相位阻尼等信道的運算元和Kraus算子和表示(超算子).

3.1 比特翻轉(zhuǎn)信道組成的確定型量子程序的可達集合和終態(tài)

經(jīng)計算P從計算基態(tài)|0〉或|1〉運行時的可達集合分別為R(|0〉〈0|)={|0〉〈0|,|1〉〈1|}和R(|1〉〈1|)={|0〉〈0|,|1〉〈1|},而|0〉,|1〉∈T,D=?.

3.2 相位翻轉(zhuǎn)信道組成的確定型量子程序的可達集合和終態(tài)

3.3 去極化信道組成的非確定型量子程序的可達集合和終態(tài)

經(jīng)計算P從計算基態(tài)|0〉或|1〉運行時的可達集合均為R(|0〉〈0|)=R(|1〉〈1|)={|0〉〈0|,|1〉〈1|},而|0〉,|1〉∈T,D=?.

3.4 幅值阻尼信道組成的確定型量子程序的可達集合和終態(tài)

3.5 相位阻尼信道組成的確定型量子程序的可達集合和終態(tài)

綜上，在單量子比特空間H2中,五種確定型量子程序從計算基態(tài)|0〉或|1〉開始運行時有如下結(jié)論:

(1)比特翻轉(zhuǎn)信道K1和去極化信道K3從{|0〉,|1〉}開始運行時的可達集合相同,即R(|0〉〈0|)=R(|1〉〈1|)={|0〉〈0|,|1〉〈1|},而|0〉,|1〉∈T,D=?.

(2)相位翻轉(zhuǎn)信道K2、幅值阻尼信道K4、相位阻尼信道K5從|0〉開始運行時的可達集合均為R(|0〉〈0|)={|0〉〈0|},且|0〉∈T;而從|1〉開始運行時的可達集合均為R(|1〉〈1|)={|1〉〈1|}且|1〉∈D,此時D≠?.

4 幾種常用量子信道組成的非確定型量子程序

由上一節(jié)的分析,下面我們根據(jù)這五種確定型量子程序的可達集合之相似點選取幾種特殊的組合討論這五種量子信道兩兩組合組成的非確定型量子程序從計算基態(tài){|0〉,|1〉}開始運行時的終止和發(fā)散情況，即:

(1)比特翻轉(zhuǎn)信道K1和去極化信道K3組成的非確定型量子程序;

(2)比特翻轉(zhuǎn)信道K1和相位翻轉(zhuǎn)信道K2組成的非確定型量子程序;

(3)幅值阻尼信道K4和相位阻尼信道K5組成的非確定型量子程序.

4.1 比特翻轉(zhuǎn)信道和去極化信道組成的非確定型量子程序

比特翻轉(zhuǎn)信道和去極化信道組成的非確定型量子程序為

P=({K1,K3},{M0,M1})

(9)

4.1.1K1執(zhí)行m次后K3執(zhí)行n次

(a)當(dāng)ρ=|0〉〈0|時:Ts1(≤m)s3(≤n)(ρ)=0,t(ρ)=1,ρ∈T.即,非確定型量子程序P按執(zhí)行表s=s1(≤m)s3(≤n)從初態(tài)|0〉〈0|運行時是終止的.

ts1(≤m)s3(≤n)(ρ)=

對終止概率t(ρ)的討論如下:

(1)當(dāng)p1=1,p3=0時:

ts1(≤m)s3(≤n)(ρ)=0

即ρ=|1〉〈1|∈D.

(2)當(dāng)p1=0時:

ts1(≤m)s3(≤n)(ρ)=1

即ρ=|1〉〈1|∈T.

(3)p1=1,p3≠0時:

(4)p1≠1,p3≠0時:

即當(dāng)m→∞,或n→∞,或m,n→∞時,t(ρ)=1.

(5)p1≠1,p3=1時:

即當(dāng)m→∞,或n→∞,或m,n→∞時,t(ρ)=1.

(6)0

即當(dāng)m→∞,或n→∞,或m,n→∞時,t(ρ)=1.

(7)當(dāng)p1≠1,p3=0時:

命題1 比特翻轉(zhuǎn)信道(K1)和去極化信道(K3)組成的非確定型量子程序P按執(zhí)行表s=s1(≤m)s3(≤n)運行時,有下列結(jié)論:

(1)當(dāng)初態(tài)為|0〉〈0|時是終止的;

(2)當(dāng)初態(tài)為|1〉〈1|,且當(dāng)p1=1,p3=0時,ts(ρ)=0,即程序從狀態(tài)|1〉〈1|開始運行時是發(fā)散的;否則,ts(ρ)=1,即程序從狀態(tài)|1〉〈1|開始運行時是終止的.

4.1.2K3執(zhí)行m次后K1執(zhí)行n次

(a)當(dāng)ρ=|0〉〈0|時:

Ts3(≤m)s1(≤n)(ρ)=0,t(ρ)=1,ρ∈T

即,非確定型量子程序P按執(zhí)行表s=s3(≤m)s1(≤n)從初態(tài)|0〉〈0|運行時是終止的.

(b)當(dāng)ρ=|1〉〈1|時:

則

ts3(≤m)s1(≤n)(ρ)=

對終止概率t(ρ)的討論如下:

(1)當(dāng)p1=1,p3=0時:

ts3(≤m)s1(≤n)(ρ)=0

即ρ=|1〉〈1|∈D.

(2)當(dāng)p1=0,p3≠0時:

ts3(≤m)s1(≤n)(ρ)=1

即ρ=|1〉〈1|∈T.

(3)當(dāng)p1=0,p3=1時:

ts3(≤m)s1(≤n)(ρ)=1,t(ρ)=1.

(4)當(dāng)p1=1,p3≠0時:

(5)當(dāng)p1≠1,p3=1時：

ts3(≤m)s1(≤n)(ρ)=1,t(ρ)=1.

(6)當(dāng)p1=0,p3=0時:

ts3(≤m)s1(≤n)(ρ)=1,t(ρ)=1.

(7)當(dāng)0

即當(dāng)m→∞,或n→∞,或m,n→∞時,t(ρ)=1.

命題2 比特翻轉(zhuǎn)信道(K1)和去極化信道(K3)組成的非確定型量子程序P按執(zhí)行表s=s3(≤m)s1(≤n)運行時,有下列結(jié)論:

(1)當(dāng)初態(tài)為|0〉〈0|時是終止的;

(2)當(dāng)初態(tài)為|1〉〈1|,且當(dāng)p1=1,p3=0時,ts(ρ)=0,即程序從狀態(tài)|1〉〈1|開始運行時是發(fā)散的;否則,ts(ρ)=1,即程序從狀態(tài)|1〉〈1|開始運行時是終止的.

4.1.3K1執(zhí)行1次后K3執(zhí)行1次如此反復(fù)

(a)當(dāng)ρ=|0〉〈0|時:Ts1s3s1s3…(ρ)=0,t(ρ)=1,ρ∈T.即,非確定型量子程序P按執(zhí)行表s=s1s3s1s3…從初態(tài)|0〉〈0|運行時是終止的.

(b)初態(tài)ρ=|1〉〈1|:

Ts(≤2n)(ρ)=

ts(≤2n)(ρ)=

類似于命題1和命題2的討論,有如下各結(jié)論.

命題3 比特翻轉(zhuǎn)信道(K1)和去極化信道(K3)組成的非確定型量子程序P按執(zhí)行表s=s1s3s1s3…運行時,有下列結(jié)論:

(1)當(dāng)初態(tài)為|0〉〈0|時是終止的;

(2)當(dāng)初態(tài)為|1〉〈1|,且當(dāng)p1=1,p3=0時,ts(ρ)=0,即程序從狀態(tài)|1〉〈1|開始運行時是發(fā)散的;否則,ts(ρ)=1,即程序從狀態(tài)|1〉〈1|開始運行時是終止的.

4.1.4K3執(zhí)行1次后K1執(zhí)行1次如此反復(fù)

(a)當(dāng)ρ=|0〉〈0|時:Ts3s1s3s1…(ρ)=0,t(ρ)=1,ρ∈T.即,非確定型量子程序P按執(zhí)行表s=s3s1s3s1…從初態(tài)|0〉〈0|運行時是終止的.

(b)初態(tài)ρ=|1〉〈1|:

Ts(≤2n)(ρ)=

ts(≤2n)(ρ)=

命題4 由比特翻轉(zhuǎn)信道(K1)和去極化信道(K3)組成的非確定型量子程序P按執(zhí)行表s=s3s1s3s1…運行時,有下列結(jié)論:

(1)當(dāng)初態(tài)為|0〉〈0|時是終止的;

(2)當(dāng)初態(tài)為|1〉〈1|,且當(dāng)p1=1,p3=0時,ts(ρ)=0,即程序從狀態(tài)|1〉〈1|開始運行時是發(fā)散的;否則,ts(ρ)=1,即程序從狀態(tài)|1〉〈1|開始運行時是終止的.

綜上可得如下定理:

定理1 設(shè)P是由比特翻轉(zhuǎn)信道(K1)和去極化信道(K3)組成的非確定型量子程序,則P按任意的執(zhí)行表s運行時,有如下結(jié)論:

(1)當(dāng)初態(tài)為|0〉〈0|時是終止的;

(2)當(dāng)初態(tài)為|1〉〈1|,且當(dāng)p1=1,p3=0時,t(ρ)=0,即程序從狀態(tài)|1〉〈1|開始運行時是發(fā)散的;否則,當(dāng)p1≠1或p3≠0時,t(ρ)=1,即程序從狀態(tài)|1〉〈1|開始運行時是終止的.

4.2 比特翻轉(zhuǎn)信道和相位翻轉(zhuǎn)信道組成的非確定型量子程序

比特翻轉(zhuǎn)信道和相位翻轉(zhuǎn)信道組成的非確定型量子程序為

P=({K1,K2},{M0,M1})

(10)

4.2.1K1執(zhí)行m次后K2執(zhí)行n次

(a)當(dāng)初態(tài)ρ=|0〉〈0|時:Ts1(≤m)s2(≤n)(ρ)=0,t(ρ)=1,ρ∈T.即,非確定型量子程序P按執(zhí)行表s=s1(≤m)s2(≤n)從初態(tài)|0〉〈0|運行時是終止的.

命題5 非確定型量子程序P按執(zhí)行表s=s1(≤m)s2(≤n)運行時,有下列結(jié)論:

(1)當(dāng)初態(tài)為|0〉〈0|時是終止的;

(2)當(dāng)初態(tài)為|1〉〈1|,且當(dāng)p1=0時,ts(ρ)=1,即程序從狀態(tài)|1〉〈1|運行時是終止的;否則,當(dāng)p1=1時,ts(ρ)=0,即程序從狀態(tài)|1〉〈1|運行時是發(fā)散的.

4.2.2K2執(zhí)行m次后K1執(zhí)行n次

(a)當(dāng)初態(tài)ρ=|0〉〈0|時:Ts2(≤m)s1(≤n)(ρ)=0,t(ρ)=1,ρ∈T.即,非確定型量子程序P按執(zhí)行表s=s2(≤m)s1(≤n)從初態(tài)|0〉〈0|運行時是終止的.

(b)當(dāng)初態(tài)ρ=|1〉〈1|:

命題6 非確定型量子程序P按執(zhí)行表s=s2(≤m)s1(≤n)運行時,有下列結(jié)論:

(1)當(dāng)初態(tài)為|0〉〈0|時是終止的;

(2)當(dāng)初態(tài)為|1〉〈1|,且當(dāng)p1=0時,ts(ρ)=1,即程序從狀態(tài)|1〉〈1|運行時是終止的;否則,當(dāng)p1=1時,ts(ρ)=0,即程序從狀態(tài)|1〉〈1|運行時是發(fā)散的.

4.2.3K1執(zhí)行1次后K2執(zhí)行1次如此反復(fù)

(a)當(dāng)初態(tài)ρ=|0〉〈0|時:Ts1s2s1s2…(ρ)=0,t(ρ)=1,ρ∈T.即,非確定型量子程序P按執(zhí)行表s=s2s1s2s1…從初態(tài)|0〉〈0|運行時是終止的.

(b)當(dāng)初態(tài)ρ=|1〉〈1|時:

命題7 非確定型量子程序P按執(zhí)行表s=s1s2s1s2…運行時,有下列結(jié)論:

(1)當(dāng)初態(tài)為|0〉〈0|時是終止的;

(2)當(dāng)初態(tài)為|1〉〈1|,同時當(dāng)p1=0時,ts(ρ)=1,即程序從狀態(tài)|1〉〈1|運行時是終止的;否則,當(dāng)p1=1時,ts(ρ)=0,即程序從狀態(tài)|1〉〈1|運行時是發(fā)散的.

4.2.4K2執(zhí)行1次后K1執(zhí)行1次如此反復(fù)

(a)當(dāng)初態(tài)ρ=|0〉〈0|時:Ts2s1s2s1…(ρ)=0,t(ρ)=1,ρ∈T.即,非確定型量子程序P按執(zhí)行表s=s2s1s2s1…從初態(tài)|0〉〈0|運行時是終止的.

(b)當(dāng)初態(tài)ρ=|1〉〈1|時:

命題8 非確定型量子程序P按執(zhí)行表s=s2s1s2s1…運行時,有下列結(jié)論:

(1)當(dāng)初態(tài)為|0〉〈0|時是終止的;

(2)當(dāng)初態(tài)為|1〉〈1|,且當(dāng)p1=0時,ts(ρ)=1,即程序從狀態(tài)|1〉〈1|運行時是終止的;否則,當(dāng)p1=1時,ts(ρ)=0,即程序從狀態(tài)|1〉〈1|運行時是發(fā)散的.

定理2 設(shè)P是由比特翻轉(zhuǎn)信道(K1)和相位翻轉(zhuǎn)信道(K2)組成的非確定型量子程序,則程序P按任意執(zhí)行表s運行時,有下列結(jié)論:

(1)當(dāng)初態(tài)為|0〉〈0|時是終止的;

(2)當(dāng)初態(tài)為|1〉〈1|,且當(dāng)p1=0時,t(ρ)=1,即程序從狀態(tài)|1〉〈1|運行時是終止的;否則,當(dāng)p1=1時,t(ρ)=0,即程序從狀態(tài)|1〉〈1|運行時是發(fā)散的;

(3)當(dāng)初態(tài)為|1〉〈1|時,程序P的終止和發(fā)散只與比特翻轉(zhuǎn)信道(K1)的參數(shù)p1有關(guān).

從上面的定理可以看到,比特翻轉(zhuǎn)信道(K1)和相位翻轉(zhuǎn)信道(K2)組成的非確定型量子程序P的終止和發(fā)散只與比特翻轉(zhuǎn)信道(K1)的參數(shù)p1有關(guān),與相位翻轉(zhuǎn)信道(K2)的參數(shù)p2沒有關(guān)系,這和比特翻轉(zhuǎn)信道(K1)單獨作為確定型量子程序時終止和發(fā)散的結(jié)論一致.

4.3 幅值阻尼信道和相位阻尼信道組成的非確定型量子程序

幅值阻尼信道和相位阻尼信道組成的非確定型量子程序為

P=({K4,K5},{M0,M1})

(11)

分別選取執(zhí)行表s為s′=s4(≤m)s5(≤n),s″=s5(≤m)s4(≤n),s?=s4s5s4s5…,s″=s5s4s5s4…經(jīng)計算均有如下的結(jié)果:

(a)當(dāng)初態(tài)ρ=|0〉〈0|時:Ts(ρ)=0,t(ρ)=1,ρ∈T.即,非確定型量子程序P按執(zhí)行表s從初態(tài)|0〉〈0|運行時是終止的.

(b)當(dāng)初態(tài)ρ=|1〉〈1|時:

Ts(ρ)=(1-p4)l|1〉〈1|,t(ρ)=0,ρ∈D,

其中l(wèi)為幅值阻尼信道K4執(zhí)行的次數(shù).

定理3 設(shè)P是由幅值阻尼信道(K4)和相位阻尼信道(K5)組成的非確定型量子程序,則程序P按任意執(zhí)行表s運行時,有下列結(jié)論:

(1)當(dāng)初態(tài)為|0〉〈0|時是終止的;

(2)當(dāng)初態(tài)為|1〉〈1|,t(ρ)=0,即程序從狀態(tài)|1〉〈1|開始運行時是發(fā)散的.

5 結(jié)束語

終止條件是研究循環(huán)程序的一個非常重要但又極其困難的課題.事實上一般量子循環(huán)的終止是不可判定的.本文對幾類非確定型量子程序的終止和發(fā)散進行了詳細的討論，此研究對量子程序的設(shè)計和量子協(xié)議的設(shè)計都有很好的幫助和啟迪作用,但對非確定型量子程序的研究還有很多的理論和實驗需要完善和補充,例如對于五種常用量子信道兩兩組成的非確定型量子程序在別的測量算子,如M0=|+〉〈+|,M1=|-〉〈-|下的終止和發(fā)散情況,及H2空間中兩個以上常用量子信道組合組成的非確定型量子程序的終止發(fā)散的情況如何我們在另文中加以討論.

[1]P W Shor.Algorithms for quantum computation:discrete logarithms and factoring[A].Proc.35th Annual Symp.on Foundations of Computer Science[C].Los Alamitos,CA:IEEE Press,1994.124-134.

[2]L Grover.A fast quantum mechanical algorithm for database search[A].Proc 28th Annual ACM Symp on the Theory of Computing[C].New York:ACM Press,1996.212-219.

[3]M A Nielsen,I L C′huang.Quantum Computation and Quantum Information[M].Cambridge:Cambridge University Press,2000.

[4]S Abramsky.High-level methods for quantum computation and information[A].Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04)[C].USA:IEEE Computer Society,2004.410-414.

[5]E H Knill.Conventions for Quantum Pseudocode[R].USA:Los Alamos National Laboratory,1996.

[6]B?mer.A Procedural Formalism for Quantum Computing[D].Vienna:Department of Theoretical Physics,Technical University of Vienna,1998.

[7]P Selinger.Towards a quantum programming language[J].Mathematics Structures in Computer Science,2004,14(4):527-586.

[8]S J Gay,R Nagarajan.Communicating quantum processes,annual symposium on principles of programming languages[A].Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages[C].USA:Programming Language,2005.145-157.

[9]Y Feng,R Y Duan,M S Ying.Bisimulation for quantum processes[A].Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)[C].New York:ACM Press,2011.523-534.

[10]Y J Li,N K Yu,M S Ying.Termination of nodeterministic quantum programs[J].Acta Informatica,2014,51(1):1-24.

[11]N K Yu,M S Ying.Reachability and termination analysis of concurrent quantum programs[J].Lecture Notes in Computer Science,2012,7454:69-83.

[12]M S Ying,N K Yu,Y Feng,R Y Duan.Verification of quantum programs[J].Sci Comput Program,2013,78(9):1679-1700.

[13]雷紅軒,席政軍,李永明.廣義量子Loop程序的若干性質(zhì)[J].電子學(xué)報,2013,41(4):727-732. LEI Hong-xuan,XI Zheng-jun,LI Yong-ming.Some properties of genaralized quantum loop program[J].Acta Electronica Sinica,2013,41(4):727-732.(in Chinese)

[14]雷紅軒,席政軍,李永明.量子最弱自由前置條件的交換性及其性質(zhì)[J].軟件學(xué)報,2013,24(5):933-941. LEI Hong-xuan,XI Zheng-jun,LI Yong-ming.Commutativity of quantum weakest liberal precondition and its properties[J].Journal of Software,2013,24(5):933-941.(in Chinese)

[15]林運國，雷紅軒，李永明.量子馬爾可夫鏈安全性模型檢測[J].電子學(xué)報,2014,42(11):2191-2197.

LIN Yun-guo,LEI Hong-xuan,LI Yong-ming.Model checking of safety property over quantum markov chain[J].Acta Electronica Sinica,2014,42(11):2191-2197.(in Chinese)

雷紅軒 男,1967年出生于陜西洋縣,博士,教授,主要研究領(lǐng)域為自動機理論,量子程序驗證和量子模型檢測.

E-mail:hongxuan-lei@163.com

彭家寅 男，1962出生于四川資中縣，博士，教授，主要研究領(lǐng)域為量子信息處理.

E-mail:pengjiayin62226@163.com

劉 熠 男，1979年出生于四川儀隴縣，博士，副教授，主要研究領(lǐng)域為智能信息處理.

E-mail：liuyiyl@126.com

Termination Verification of Some Kinks Nondeterministic Quantum Programs

LEI Hong-xuan1,2，PENG Jia-yin1,2,LIU Yi1,2

(1.SchoolofMathematicsandInformationScienceofNeijiangNormalUniversity，Neijiang，Sichuan641112，China； 2.KeyLaboratoryofNumericalSimulationofSichuanProvince，Neijiang，Sichuan641112，China)

Program verification is the key technology to ensure the correctness of the program.However,due to essential differences of the classical and quantum world,classical program verification techniques and tools cannot be applied directly to the quantum system.Since quantum programming language is a new formal model of quantum system,the verification problem of quantum program is more urgent and necessary.We investigate the program verification for the reachable set and the terminating set of specific nondeterministic quantum program described respectively by bit flip channel,phase flip channel,depolarizing channel,amplitude damping channel and phase damping channel starting from computational basic states in quantum communication systems.Then,we combine pairwise the above five quantum programs into nondeterministic quantum programs,and merge these nondeterministic quantum programs into three nondeterministic quantum programs in terms of the similarities of the reachable set of five quantum programs,and discuss the problem for termination and divergence of these three nondeterministic quantum programs starting from computational basic states.The results shows that these three nondeterministic quantum programs starting from computational basic state 0 are terminated,while starting from computational basic state 1,the termination and the divergence of nondeterministic quantum program consisted by bit flip channel and depolarizing channel relates to the two parameters describing two quantum channels,the termination and the divergence of nondeterministic quantum program consisted by bit flip channel and phase flip channel relates to one parameter describing bit flip channel,and nondeterministic quantum program consisted by amplitude damping channel and phase damping channel is divergence without the two parameters describing quantum channel.And the results provide theoretical and technical support for verification of quantum communication protocol in quantum information security.

quantum communication;quantum programs;program verification;information security

2015-07-06;

2015-11-06；責(zé)任編輯：覃懷銀

四川省教育廳重點科研項目(No.14ZA0242);教育部數(shù)學(xué)與應(yīng)用數(shù)學(xué)專業(yè)綜合改革(No.ZG0464)；四川省數(shù)學(xué)與應(yīng)用數(shù)學(xué)專業(yè)綜合改革(No.01249)；四川省教育廳科研創(chuàng)新團隊基金(No.15TD0027);四川省應(yīng)用基礎(chǔ)研究計劃(No.2015JY0120)

TP301.6

A

0372-2112 (2016)12-2932-07

??學(xué)報URL:http://www.ejournal.org.cn

10.3969/j.issn.0372-2112.2016.12.017