999精品在线视频,手机成人午夜在线视频,久久不卡国产精品无码,中日无码在线观看,成人av手机在线观看,日韩精品亚洲一区中文字幕,亚洲av无码人妻,四虎国产在线观看 ?

帶空移動的加權有限自動機量化等價及其轉換

2016-09-08 10:38:40
計算機應用與軟件 2016年8期
關鍵詞:定義

汪 國 武

(安徽工程大學計算機與信息學院 安徽 蕪湖 241000) (安徽工程大學計算機應用技術重點實驗室 安徽 蕪湖 241000)

?

帶空移動的加權有限自動機量化等價及其轉換

汪 國 武

(安徽工程大學計算機與信息學院安徽 蕪湖 241000) (安徽工程大學計算機應用技術重點實驗室安徽 蕪湖 241000)

在經典的有限自動機理論中,帶空移動的有限自動機與不帶空移動的有限自動機是等價的。取值于實數的加權有限自動機是自動機的一種推廣模型,它給經典自動機的每個轉換賦一個取值于實數的權值,這些權值表示執行轉換的代價。為了研究帶空移動的加權有限自動機與不帶空移動的加權有限自動機是否具有等價性這一問題,提出量化等價的概念,并研究如何將一個帶空移動的加權有限自動機轉換為一個與之量化等價的不帶空移動的加權有限自動機。研究結果表明:這兩者是量化等價的。

量化等價不確定的有限狀態自動機加權自動機形式化驗證

0 引 言

在計算機科學中,有限狀態自動機[1,2]是自動機理論的研究對象,廣泛地被應用于神經網絡、模式識別、密碼算法、形式化分析與驗證等領域中。關于有限狀態自動機,一個有趣的結論是:帶空移動和不帶空移動的自動機具有等價性,即如果一個正則語言能被一個帶空移動的自動機接受,那么該語言可被一個不帶空移動的自動機接受。

經典的有限自動機是一種對系統進行定性的建模方法,它明確規定了所建模的系統所具有的性質和不具有的性質。為了對計算機系統的量化信息進行建模,研究者提出了很多能描述量化信息的自動機模型[3-7],模糊自動機[8,9]是其中一個比較有代表性意義的自動機的推廣模型。文獻[10]討論了帶空移動的模糊自動機和模糊自動機等價的充分必要條件;文獻[11]證明了帶空移動的不確定性模糊自動機和不確定性模糊自動機具有等價性。

取值于實數的加權有限自動機[12-15]是自動機的另一種推廣模型,該模型已經被用于嵌入式系統的設計和驗證[16,17]。取值于實數的加權有限自動機的基本特點是:通過給經典自動機的每個轉換賦一個取值于實數的權值,這些權值表示執行轉換的代價,如花費的時間或消耗的資源,或者表示為成功執行的幾率等。對取值于實數的加權有限自動機的研究已經取得較大的進展, 但前文提到的結論:帶空移動和不帶空移動的自動機具有等價性,到目前為止還沒有在加權有限自動機這種模型上進行研究。

本文首先提出帶空移動的加權有限自動機;接著為了描述帶空移動的加權有限自動機和不帶空移動的加權有限自動機的等價性,我們提出量化等價的概念;然后在量化等價的基礎上,研究和探討如何將一個帶空移動的加權有限自動機轉換為一個與之量化等價的不帶空移動的加權有限自動機。

1 帶空移動的加權有限自動機

首先介紹加權有限狀態自動機、帶空移動的加權有限狀態自動機及其識別的語言和量化語言等,然后引入量化等價的概念。

設Q是一個集合,記P(Q)為Q的冪集。后文R+表示非負實數集。

定義1一個加權有限(狀態)自動機[14]WFA(weighted finite automaton)M是一個8元組:

M=(Q,Σ,δ,qI,F,γ,i,f)

其中:

(1) Q:非空有窮狀態集合。對于任意q∈Q,稱q是M的一個狀態。

(2) Σ:輸入有限字母表。

(3) δ:δ?Q×Σ×Q是一個轉換關系。

(4) qI:qI∈Q是一個初始狀態。

(5) F:F?Q是終止狀態集合,對于任意q∈F,稱q為M的終止狀態。

(6) γ:δ→R+是一個加權函數。如果轉換(q,a,q′)∈δ,相應的權函數為γ(δ(q,a,q′)),表示M在狀態q讀入字母a后到達狀態q′時,需要的代價為γ(δ(q,a,q′))。

(7) i:qI→R+是初態權函數,初始狀態qI的權值為i(qI)。

(8) f:F→R+是終態權函數,如果對于任意q∈F,則終態q的權值為f(q)。

我們常用q′∈δ(q,a)表示(q,a,q′)∈δ。另外,我們記δ(q,a)={q′:(q,a,q′)∈δ}。為了符號簡便,后文γ(δ(q,a,q′))記為γ(q,a,q′)。類似地,我們也將γ(δ(q,a))簡寫為γ(q,a),γ(q,a)={q′/γ(q,a,q′):q′∈δ(q,a)}是一個權函數的集合,其元素表示為q′/γ(q,a,q′),目的是清楚地表明權函數值γ(q,a,q′)對應轉換到達的目標狀態為q′。

加權有限自動機與經典的有限自動機的區別是:加權有限自動機對每個轉換定義了相應的轉換代價,稱為權函數。此外,對于每個初始狀態和接受狀態也都定義了權值。

為了定義加權有限自動機的接受語言,將δ擴充為δ?P(Q)×Σ×P(Q),對于P?Q,a∈Σ,定義:

進一步將δ擴充為δ?Q×Σ*×P(Q),對于任意q∈Q,w∈Σ*,a∈Σ,作如下定義:

δ(q,ε)={q}

定義2設M=(Q,Σ,δ,qI,F,γ,i,f)是一個WFA。M所接受(識別)的語言L(M)定義為:

L(M)={x:x∈Σ*且δ(qI,x)∩F≠?}

不難看出,加權自動機的接受語言的定義與經典的自動機接受語言定義類似,然而加權自動機不僅能描述所識別的字符串,而且還能給出每個識別字符串的權重。

同樣地,我們也對權函數γ進行相應的擴展, 對于任意q∈Q,w∈Σ*,a∈Σ,定義:

γ(δ(q,ε,q))=0

(1)

γ(δ(q,wa,q′))=min{γ(δ(q,w,p))+

γ(δ(p,a,q′)):p∈δ(q,w)}

(2)

其中,式(2)表示:所有從狀態q出發先處理w后到達某一狀態,然后經由該狀態識別a到達狀態q′的運行過程的權值之和組成的集合的最小元素值。

定義3設M=(Q,Σ,δ,qI,F,γ,i,f)是一個WFA,x∈L(M)。x被M接受的權值定義為:

W(M,x)=i(qI)+min{γ(δ(qI,x,qf))+f(qf):qf∈(δ(qI,x)∩F)}

下面我們用例子去闡述以上的定義。

例1如圖1所示,一個WFAM=({q0,q1,q2,q3},{a,b,c,d},δ,q0,{q3},γ,i,f),其中轉換關系δ表示如下:

δ(q0,a)={q0,q1,q2}δ(q0,b)={q1,q2}δ(q0,c)={q2}

δ(q0,d)={q3}δ(q1,b)={q1,q2}δ(q1,c)={q2}

δ(q1,d)={q3}δ(q2,c)={q2}δ(q2,d)={q3}

相應的權函數γ表示如下:

γ(q0,a)={q0/7,q1/8,q2/11}γ(q0,b)={q1/9,q2/11}

γ(q0,c)={q2/11}γ(q0,d)={q3/13}

γ(q1,b)={q1/8,q2/10}γ(q1,c)={q2/11}

γ(q1,d)={q3/12}γ(q2,c)={q2/9}γ(q2,d)={q3/10}

初始狀態的權值:i(q0)=2,終態權函數:f(q3)=1。

顯然,acd∈L(M),因為δ(q0,acd)∩F={q3}≠?。據此,我們有:

γ(q0,acd,q3)=min{γ(q0,ac,q2)+γ(q2,d,q3)}

=min{min{(γ(q0,a,q2)+γ(q2,c,q2)),

(γ(q0,a,q1)+γ(q1,c,q2))}+10}

=min{min{(11+9),(8+11)}+10}

=min{19+10}=29

根據定義3,我們可以得到:

W(M,acd)=i(q0)+min{γ(q0,acd,q3)+f(q3)}

=2+min{29+1}

=32

所以,acd被M接受的權值為32。

現在我們引入另一種加權有限自動機模型,帶空移動的加權有限狀態自動機,如圖1所示。

圖1 不帶ε移動的WFA

定義4一個帶空移動的加權有限自動機ε-WFA(weighted finite automata with ε-moves)M′是一個8元組:

M′=(Q,Σ,δ,qI,F,γ,i,f)

其中,Q,Σ,qI,F,γ,i,f的意義與定義1相同,所不同的是轉換關系δ?Q×(Σ∪{ε})×Q。也就是說,對于q∈Q,允許q做一個空移動(ε移動)而到達其他的狀態。

類似地,下面我們將δ擴充為δ*?Q×Σ*×Q,對于P?Q,q∈Q,w∈Σ*,a∈Σ,定義:

ε-closure(q)={p:狀態q經若干個ε可達p}

(3)

δ*(q,ε)=ε-closure(q)

(4)

(5)

δ*(q,wa)=δ*(δ(δ*(q,w),a),ε)

(6)

其中,式(6)表示:從狀態q出發先處理w后到達某一狀態,然后經由該狀態識別a到達的狀態集合。特別地,當w=ε時,我們有:δ*(q,a)=δ*(δ(δ*(q,ε),a),ε)。

定義5設M′=(Q,Σ,δ,qI,F,γ,i,f)是ε-WFA,則M′所識別的語言:

L(M′)={x:x∈Σ*且δ*(qI,x)∩F≠?}

同樣地,我們也對ε-WFA的權函數γ擴展為γ*:δ*→R+, 對于任意q∈Q,w∈Σ*,a∈Σ,定義:

γ*(δ*(q,a,p))=min{γ(δ(q,a,p)):(q,a,p)∈δ*}

(7)

γ*(δ*(q,wa,q′))=min{γ*(δ*(q,wp))+

γ*(δ*(p,a,q′)):p∈δ*(q,w)}

(8)

其中,式(8)表示:從狀態q出發先處理w后到達某一狀態,然后經由該狀態識別a到達狀態q′的運行過程的權值之和,包含了計算空字符ε的權值。相同的字符串有多個權值,取最小值。

例2如圖2所示,M′是一個ε-WFA,求γ*(δ*(q0,bd,q3))值。

圖2 帶ε移動的WFA

由于:

δ*(q0,b)=δ*(δ(δ*(q0,ε),b),ε)

=δ*(δ({q0,q1,q2},b),ε)

=δ*({q1},ε)={q1,q2}

所以:

γ*(δ*(q0,b,q1))=min{γ(δ(q0,b,q1))}

=min{γ(q0,ε,q1)+γ(q1,b,q1)}

=min{1+8}=9

同理可得,γ*(δ*(q1,d,q3))=12,γ*(δ*(q0,b,q2))=11,γ*(δ*(q2,d,q3))=10。

因此:

γ*(δ*(q0,bd,q3))=min{(γ*(δ*(q0,b,q1))+γ*(δ*(q1,

d,q3))),(γ*(δ*(q0,b,q2))+

γ*(δ*(q2,d,q3)))}

=min{(9+12),(11+10)}=21

定義6設M′=(Q,Σ,δ,qI,F,γ,i,f)是一個ε-WFA,x∈L(M′)。x被M′接受的權值為:

W(M′,x)=i(qI)+min{γ*(δ*(qI,x,qf))+f(qf):

qf∈(δ*(qI,x)∩F)}

例3如圖2所示,M′是一個ε-WFA,顯然有:bd∈L(M′),因為δ*(q0,bd)∩F={q3}≠?,根據定義6,我們可知:

W(M′,bd)=i(q0)+min{γ*(δ*(q0,bd,q3))+f(q3)}

=2+min{21+1}

=24

因此,bd被M′接受的權值為24。

以下我們給出一個判斷兩個加權自動機是否等價的標準:

定義7設任意兩個WFAM和M′,如果有L(M)=L(M′)且當x∈L(M)時有W(M,x)=W(M′,x),那么就稱M和M′量化等價。

2 量化等價

在經典有限自動機理論中,對于任意一個帶空移動的有限自動機,可以構造一個等價的不帶空移動的有限自動機,使得兩者識別的語言相同。那么,對于加權自動機是否也有類似的結論。也就是說,對于任意一個ε-WFAA,是否存在一個與之量化等價的WFAB是下文將研究解決的問題。

為了解決這個問題,我們來探討WFAB的構造過程。我們注意到,ε-WFAA和WFAB的區別在于前者允許有空移動,而對于一個語言的句子來說,除非ε單獨作為一個句子,否則空移動ε不會影響句子本身。所以,考慮將A在識別句子過程中遇到類似于ε*aε*(a的前后各有若干個ε,a∈Σ)的字符串時,在B中用一個輸入字符為a的非空轉換替換。此外,如果ε-WFA的語言中包含句子ε,則將B的初始狀態同時也設為終態,讓B也可以識別句子ε,這樣可保證L(A)=L(B)成立。另一方面,在構造B時,使得B中的輸入字符a的權值等于A中串ε*aε*的權值之和,那么也可以保證W(A,x)=W(B,x)成立。也就是說,由于W(A,x)表示x在其運行路徑上的所有轉換的權值之和,如果構造WFAB,滿足使B的每一次轉換的輸入字符a(a≠ε)及其權函數γ的值都與A相同,那么必有L(A)=L(B)且W(A,x)=W(B,x)成立。

命題1設A=(Q,Σ,δA,qI,FA,γA,i,fA)是一個ε-WFA。我們構造一個WFAB=(Q,Σ,δB,qI,FB,γB,i,fB)如下:

(1) 對于A中的Q,Σ,qI,i在B中保持不變。

(3) 終態集FB:如果ε∈L(A),FB=FA∪{qI},否則FB=FA。

(4) 終態權函數fB:如果ε∈L(A)時,fB(qI)=W(A,ε)-i(qI),否則,對于所有q∈FA,使fB(q)=fA(q)。

那么,對于A和B有以下結論成立:

(1) L(A)=L(B);

(2) 對于任意x∈L(A),有W(A,x)=W(B,x)。

證明對于結論1的證明,參見文獻[3]。下面證明結論2成立。為此,我們需要先證明以下的結論1和結論2成立。

首先我們用數學歸納法證明結論1成立。

2) 假定|x|=n時,上式成立。當|x|=n+1時,不妨設x=wa,這里|w|=n,a∈Σ,則有:

構造步驟(2)

歸納假設

=δB(qI,wa)

因此當|x|=n+1時,結論1成立。

接下來,我們也用數學歸納法證明結論2成立。

γB(δB(qI,x,p))=γB(δB(qI,wa,p))

=min{γB(δB(qI,w,q′))+γB(δB(q′,a,p)):

q′∈δB(qI,w)}

=min{γB(δB(qI,w,q′))+γB(δB(q′,a,p)):

結論1

歸納假設

構造步驟(2)

由1)、2)可得,結論2成立。

現在我們可以證明:對于任意x∈L(A),有W(A,x)=W(B,x)成立。同樣用數學歸納法證明。

1) 當|x|=0時,即當x=ε的情況:

W(B,ε)=i(qI)+γ(δ(qI,ε,qI))+f(qI)

=i(qI)+f(qI)

=i(qI)+W(A,ε)-i(qI)

構造步聚(4)

=W(A,ε)

所以,當ε∈L(A)時,結論W(A,ε)=W(B,ε)成立。

2) 當|x|≥1時,即當x≠ε的情況:

=i(qI)+min{γB(δB(qI,x,p))+fA(p):p∈

結論2

=i(qI)+min{γB(δB(qI,x,p))+fA(p):p∈

(δB(qI,x)∩FA)}

結論1

=i(qI)+min{γB(δB(qI,x,p))+fA(p):p∈

(δB(qI,x)∩FB)}

步驟(3)

=i(qI)+min{γB(δB(qI,x,p))+fB(p):p∈

(δB(qI,x)∩FB)}

步驟(4)

=W(B,x)

定義3

所以,對于?x∈L(A)(x≠ε),有W(A,x)=W(B,x)成立。

綜合1)和2)得到:?x∈L(A),W(A,x)=W(B,x)成立。

根據以上結論,我們得到本文一個主要結論 。

定理1任意一個ε-WFA總存在一個與之量化等價的WFA。

表1 ε-WFA A中的δ*和γ*

3 算 法

前文介紹了如何將ε-WFA轉換成與之量化等價的WFA,下面探討轉換的算法實現。根據構造過程可知,構造WFA的主要任務是構造步驟(2):對于ε-WFA中所有的(q,a)∈Q×Σ,計算出δ*(q,a)=δ*(δ(δ*(q,ε),a),ε)和相應的γ*(δ*(q,a))值。據此,設計出相應的轉換算法,如算法1所示:

算法1ε-WFA2WFA算法

輸入:ε-WFAA=(Q,Σ,δ,qI,F,γ,i,f)

輸出:WFAB=(Q,Σ,δ′,qI,F′,γ′,i,f′)

1:F′=F;f′=f;δ′=?;

2:γ′=?;

3:forall{q∈Q}

4:forall{a∈Σ}

5:InitQueue(W);InitQueue(W′);

6:Enqueue(W,);

//添加初始項,使W≠?

7:while(W≠?)do

8:=Dequeue(W);

//這里α一定為ε

9:ifδ(q2,ε)≠?then

10:forall{q3∈δ(q2,ε)}

11:v=v+γ(q2,ε,q3);

12:Enqueue(W,);

13:ifq3∈Fthen

14:F′=F∪{qI};f′(qI)=v-i(qI);

15:else//δ(q2,ε)=?,即q2后不含空移動

16:Enqueue(W′,);

17://此時,W′中存放的元素,q2∈δ*(q,ε)

18:while(W′≠?)do

19:=Dequeue(W′);

20:ifα=ε&δ(q2,a)≠?then

21:forallq3∈δ(q2,a)

22:δ′=δ′∪{δ(q,a,q3)};v1=v1+γ(q2,a,q3);

23:γ′=γ′∪{v1=γ(q,a,q3)};

24:Enqueue(W,);

25://此時,W中存放元素,q2∈δ(δ*(q,ε),a)

26:while(W≠?)do

27:=Dequeue(W);

28:ifδ(q2,ε)≠?then

29:forall{q3∈δ(q2,ε)}

30:v=v+γ(q2,ε,q3);Enqueue(W,);

31:δ′=δ′∪{δ(q,a,q3)};γ′=γ′∪{v=γ(q,a,q3)};

我們輪流使用2個工作隊列W和W′,隊列的每一個元素中存放轉換函數及相應的權值,任一元素共有4個參數組成。其中前3個參數表示轉換函數(q,α,q2)∈δ,第4個參數為轉換的權值v=γ(q,α,q2),這里q,q2∈Q,α∈(Σ∪{ε})。

算法的第5行對隊列W和W′作初始化,第6行給W添加一個特殊元素,使得其后的循環條件W≠?成立。

算法的第7-16行,主要利用隊列W由q求算δ*(q,ε),存入W′。重復從隊列W中取出每一個元素(第8行):如果該元素(轉換)的后繼轉換仍為帶空移動的轉換時(第9行),則將后繼入隊(第12行),在此過程中,若到達了終態(第13行)則將qI置為終態并設定終態權值(第14行),這段代碼對應構造過程的步驟(3)和(4);否則,意味著完成了δ*(q,ε)計算,則將元素轉移到W′中保存(第15、16行),循環結束后W′中存放的元素為:,滿足q2∈δ*(q,ε)。

算法的第18-24行,從W′中取出所有元素即轉換δ*(q,ε)(第19行),求算δ(δ*(q,ε),a),存入隊列W中。

算法的第25-31行,從W中取出所有元素即轉換δ(δ*(q,ε),a)(第27行),求算δ*(δ(δ*(q,ε),a),ε),結果存入隊列W中。

整個算法圍繞求算δ*(q,a)=δ*(δ(δ*(q,ε),a),ε)和γ*(δ*(q,a))之值,在這個過程中完成對F′、f′、δ′、γ′的構造。

復雜度分析我們注意到算法主要是處理隊列中的元素,算法的復雜度主要由入隊的次數決定,即由語句Enqueue(W,)決定。該語句在算法中共出現4次,12行、16行、24行和30行。在不考慮外層循環(第3、4行)的情況下,第12行最多執行|Q|2次,因為滿足循環條件的狀態q3(第10行)最多有|Q|個,而且這些元素中的任意一個也可能有|Q|個帶空移動的轉換需要加入到隊列W中;第16行也最多執行|Q|2次,因為該行只是將W中所有元素轉移至W′中;第24行最多執行|Q|次,因為滿足循環條件的狀態q3(第21行)最多有|Q|個;第31行最多執行|Q|2次,原因同第12行。共執行3|Q|2+|Q|次,考慮外層循環,總共|Q|·|Σ|·(3|Q|2+|Q|)次。所以時間復雜度為O(|Q|3·|Σ|)。

4 結 語

本文針對加權自動機的等價性問題提出了量化等價的概念,研究和探討如何將一個帶空移動的加權有限自動機轉換為一個與之量化等價的不帶空移動的加權有限自動機,研究結果表明轉換前后兩者是量化等價的。

[1] Hopcroft J E,Ullman J D.Introduction to Automata Theory,Languages,and Computation[M].MA:Pearson Education India,1979.

[2] 蔣宗禮.形式語言與自動機理論[M].2版.北京:清華大學出版社,2007.

[3] 張晉津.轉換系統行為近似等價性的研究[D].南京航空航天大學,2010.

[4] 潘海玉.狀態轉化系統的格值量化驗證方法研究[D].上海:華東師范大學,2012.

[5] Pan H Y,Cao Y Z,Zhang M,et al.Simulation for lattice-valued doubly labeled transition systems[J].International Journal of Approximate Reasoning,2014,55(3):797-811.

[6] Pan H Y,Zhang M,Wu H Y,et al.Quantitative analysis of lattice-valued Kripke structures[J].Fundamenta Informaticae,2014,135(3):269-293.

[7] Pan H Y,Li Y M,Cao Y Z.Lattice-valued simulations for quantitative transition systems[J].International Journal of Approximate Reasoning,2015,56(2):28-42.

[8] 李永明.模糊系統分析[M].北京:科學出版社,2005.

[9] Li Y M.Finite automata theory with membership values in lattices[J].Information Sciences,2011,181(5):1003-1017.

[10] Li Z H,Li P,Li Y M.The relationships among several types of fuzzy automata[J].Information Sciences,2006,176(15):2208-2226.

[11] Cao Y Z,Yoshinori E.Nondeterministic fuzzy automata[J].Information Sciences,2012,191(15):86-97.

[12] Chatterjee K,Doyen L,Henzinge T.Quantitative languages[J].ACM Transactions on Computational Logic,2010,11(4):1-38.

[13] Chatterjee K,Doyen L,Henzinger T A.Expressiveness and closure properties for quantitative languages[J].Logical Methods in Computer Science,2010,6(3):199-208.

[14] Aminof B,Kupferman O,Lampert R.Rigorous approximated determinization of weighted automata[J].Theoretical Computer Science,2013,480(8):104-117.

[15] Boker U,Henzinger T.Exact and approximate determinization of discounted-sum automata[J].Logical Methods in Computer Science,2014,10(1):1-33.

[16] 黃明璋,李國強.基于模型檢測的并發程序分析綜述[J].計算機應用與軟件,2014,31(12):1-6,24.

[17] 袁志斌.Büchi自動機的優化綜述[J].計算機應用與軟件,2010,27(6):32-34,88.

QUANTITATIVE EQUIVALENCE OF WEIGHTED FINITE AUTOMATA WITH ε-MOVES AND ITS TRANSITION

Wang Guowu

(SchoolofComputerandInformation,AnhuiPolytechnicalUniversity,Wuhu241000,Anhui,China) (KeyLaboratoryofComputerApplicationTechnology,AnhuiPolytechnicUniversity,Wuhu241000,Anhui,China)

In classical finite automaton theory, the finite automaton with ε-moves and normal finite automaton are equivalent. The weighted finite automaton valued in real numbers is an extension model of automaton, it assigns one weight valued in real numbers to every transition of classical automaton, these weights denote the cost of transitions execution. To study whether the finite automaton with ε-moves and the normal finite automaton are equivalent, we introduce the concept of quantitative equivalence, and give a method of how to transform a weighted finite automaton with ε-moves to a normal weighted finite automaton in quantitative equivalence with the former. Study result shows that these two are quantitatively equivalent.

Quantitative equivalenceNondeterministic finite automataWeighted automataFormal verification

2015-01-23。國家自然科學基金項目(61300170);安徽省教育廳自然科學基金項目(KJ2013B020);安徽省優秀青年人才基金重點項目(2013SQRL034ZD)。汪國武,講師,主研領域:形式化分析與驗證。

TP301.1

A

10.3969/j.issn.1000-386x.2016.08.005

猜你喜歡
定義
以愛之名,定義成長
活用定義巧解統計概率解答題
例談橢圓的定義及其應用
題在書外 根在書中——圓錐曲線第三定義在教材和高考中的滲透
永遠不要用“起點”定義自己
海峽姐妹(2020年9期)2021-01-04 01:35:44
嚴昊:不定義終點 一直在路上
華人時刊(2020年13期)2020-09-25 08:21:32
定義“風格”
成功的定義
山東青年(2016年1期)2016-02-28 14:25:25
有壹手——重新定義快修連鎖
修辭學的重大定義
當代修辭學(2014年3期)2014-01-21 02:30:44
主站蜘蛛池模板: 久久精品这里只有国产中文精品| 国产在线观看一区精品| 日韩麻豆小视频| 国产在线91在线电影| 亚洲欧美另类日本| 中文成人无码国产亚洲| 在线国产综合一区二区三区| 国产在线欧美| av色爱 天堂网| 国产啪在线| 在线亚洲小视频| 91av成人日本不卡三区| 99久久精品国产麻豆婷婷| 免费人成视网站在线不卡| 欧美三级不卡在线观看视频| 国产在线观看91精品亚瑟| 99伊人精品| 中文字幕日韩欧美| 92精品国产自产在线观看| 亚洲熟女偷拍| 91福利在线观看视频| 伊人久综合| 国产视频一区二区在线观看 | 久久久久无码精品| 制服无码网站| 亚洲无码日韩一区| 亚洲国产欧美自拍| 日韩亚洲综合在线| 毛片手机在线看| 国产大全韩国亚洲一区二区三区| av在线无码浏览| 久久国产香蕉| 国产成人精品综合| 萌白酱国产一区二区| 亚洲侵犯无码网址在线观看| 美女一级毛片无遮挡内谢| 日韩精品一区二区三区中文无码| 无码中字出轨中文人妻中文中| 久久国语对白| 日本成人精品视频| 91九色国产在线| 欧美人与牲动交a欧美精品| 综合五月天网| 日本精品αv中文字幕| 91久久国产成人免费观看| 真实国产乱子伦视频| 四虎永久在线精品国产免费| 国产免费羞羞视频| 亚洲中久无码永久在线观看软件| 激情乱人伦| 国产久草视频| 亚洲Va中文字幕久久一区| 国产高清国内精品福利| 国产一区二区丝袜高跟鞋| 精品亚洲麻豆1区2区3区| 99re66精品视频在线观看| 手机永久AV在线播放| 精品伊人久久久久7777人| 啪啪永久免费av| 欧美综合中文字幕久久| 蜜桃臀无码内射一区二区三区| 日韩无码一二三区| 日韩精品免费一线在线观看| 在线观看91香蕉国产免费| 岛国精品一区免费视频在线观看| 国产无码高清视频不卡| 天天操精品| 欧美日韩中文字幕二区三区| 国产亚洲视频在线观看| 老司机午夜精品网站在线观看| 亚洲AV色香蕉一区二区| 亚洲一区二区三区国产精品| 国产无码网站在线观看| 人妖无码第一页| 乱人伦中文视频在线观看免费| 欧美日韩北条麻妃一区二区| 亚洲日本精品一区二区| 在线看免费无码av天堂的| 亚洲精品成人福利在线电影| 亚洲日韩欧美在线观看| 久久久久国产一级毛片高清板| 欧美 亚洲 日韩 国产|