5--協(xié)議驗(yàn)證技術(shù)-資料下載頁(yè)
2025-08-14 11:09本頁(yè)面
【正文】 T，那么就一定存在一個(gè)q∈ S， q→ q’∈ T，并且（ p’,q’）為強(qiáng)互擬關(guān)系； ⑵ 如果存在一個(gè) q’∈ S， q → q’∈ T，那么就一定存在一個(gè)p’∈ S， p → p’∈ T，并且（ p’,q’）為強(qiáng)互擬關(guān)系； 2 弱狀態(tài)互擬關(guān)系 ： 狀態(tài)轉(zhuǎn)換系統(tǒng) S,i,E,T 的兩個(gè)狀態(tài) p∈ S， q∈ S為弱互擬關(guān)系的充分必要條件是，對(duì)所有 e∈ E， e不為 I（內(nèi)部事件）； ⑴ 如果存在一個(gè) p’∈ S， p → p’∈ T，那么就一定存在一個(gè)q’∈ S， q → q’∈ T，并且（ p’,q’）為弱互擬關(guān)系； ⑵ 如果存在一個(gè) q’∈ S， q → q’∈ T，那么就一定存在一個(gè)p’∈ S， p → p’∈ T，并且（ p’,q’）為弱互擬關(guān)系； 第五章 協(xié)議驗(yàn)證技術(shù) ?15351333( 5 , 5 )( 3 , 3 )ccbb???????????????????????為 強(qiáng) 互 擬 關(guān) 系為 強(qiáng) 互 擬 關(guān) 系 所 以 ， (1,3) 為 強(qiáng) 互 擬 關(guān) 系154632cb圖 5 . 4 強(qiáng) 互 擬 關(guān) 系bcd第五章 協(xié)議驗(yàn)證技術(shù) 34243525( 4 , 4 )( 5 , 5 )( 2 , 3 )bbcc???????????????????????為 弱 互 擬 關(guān) 系為 弱 互 擬 關(guān) 系因 此 ， 為 弱 互 擬 關(guān) 系123 54aIbcI為 內(nèi) 部 事 件圖 5 . 5 弱 互 擬 關(guān) 系第五章 協(xié)議驗(yàn)證技術(shù) 圖 ，我們可以得出這樣的一個(gè)結(jié)論，即強(qiáng)互擬關(guān)系和弱互擬關(guān)系的差別在于后者忽略了內(nèi)部事件。兩個(gè)狀態(tài)為強(qiáng)互擬關(guān)系就一定為弱互擬關(guān)系，反之不然。一個(gè) FSM中所有強(qiáng)狀態(tài)互擬關(guān)系的集合為 FSM的強(qiáng)互擬關(guān)系 RS， RS是 S*S的一個(gè)子集。一個(gè) FSM中所有弱狀態(tài)互擬關(guān)系的集合為 FSM的弱互擬關(guān)系 RW， RW是 S*S的一個(gè)子集，并且 RW大于 RS。圖 FSM的 RW等于 RS，圖 的 RS=（（ 1,1） ,（ 2,2） ,（ 3,3） ,（ 4,4） ,（ 5,5）），而 RW=RS+（ 2,3）。 第五章 協(xié)議驗(yàn)證技術(shù) 互擬關(guān)系（特別是弱互擬關(guān)系）有兩種重要應(yīng)用，一是 FSM的簡(jiǎn)化，二是兩個(gè) FSM的等價(jià)性比較（即等價(jià)性分析）。 1 FSM的簡(jiǎn)化 如果（ p,q）為 S,i,E,T的一對(duì)弱狀態(tài)互擬關(guān)系，那么 p， q可合并成一個(gè)狀態(tài)， FSM得到簡(jiǎn)化。第 3章 FSM的簡(jiǎn)化方法四（隱藏內(nèi)部事件）時(shí)，我們已經(jīng)給出若干簡(jiǎn)化 FSM的例子（圖 ）。 第五章 協(xié)議驗(yàn)證技術(shù) FSM的等價(jià)比較 我們真正感興趣的是兩個(gè) FSM是否等價(jià)，兩個(gè) FSM的等價(jià)分強(qiáng)互擬等價(jià)（ strong bisimulation equivalence）和弱互擬等價(jià)（ weak bisimulation equivalence），它們分別可借助于FSM的強(qiáng)互擬關(guān)系和弱互擬關(guān)系來(lái)定義。 強(qiáng)互擬等價(jià)： 兩個(gè)相同 S1,i1,E1,T1和 S2,i2,E2,T2為強(qiáng)互擬等價(jià)的充分必要條件是： 1 2 S121 S= S S , R S * S 。2 ( i ,i ) Rs??（ ）（ ）將 Rs 換 成 Rw 就 是 弱 互 擬 等 價(jià) 的 定 義第五章 協(xié)議驗(yàn)證技術(shù) 上述定義（弱互擬等價(jià)為例）可解釋為：為了證明兩個(gè)系統(tǒng)是否弱互擬等價(jià)，我們只要將兩個(gè)系統(tǒng)和起來(lái)看作一個(gè)系統(tǒng)，找出復(fù)合系統(tǒng)的弱互擬關(guān)系 Rw，并且證明兩個(gè)初始狀態(tài)為弱狀態(tài)互擬關(guān)系就可以了。條件（ 2）有嵌套性，即如果 (i1,i2)為弱狀態(tài)互擬關(guān)系，那么它們的后繼狀態(tài)一定是弱狀態(tài)互擬關(guān)系（參見(jiàn)FSM的弱狀態(tài)互擬關(guān)系定義），同樣，它們的后繼狀態(tài)的后繼狀態(tài)一定是弱互擬關(guān)系 …… 因此兩個(gè)系統(tǒng)的所有狀態(tài)一定是彼此為弱互擬關(guān)系。根據(jù)這個(gè)原理，我們可以設(shè)計(jì)一個(gè)算法，建立一個(gè)自動(dòng)證明系統(tǒng)去證明兩個(gè) FSM是否等價(jià)。 第五章 協(xié)議驗(yàn)證技術(shù) 在許多文獻(xiàn)中，兩個(gè) FSM的強(qiáng)（弱）互擬等價(jià)也稱(chēng)之為強(qiáng)（弱）觀察等價(jià)（ strong/weak observation equivalence)。 圖 FSM是弱觀察等價(jià)的，它們的復(fù)合系統(tǒng)的弱互擬關(guān)系 Rw為： Rw＝{(.,(… )),(0,(0,.)),(0,(.,0)),(00,(0,0)),(1,(1,.)),(1,(.,1)),(11,(1,1)),(10,(1,0)),(01,(0,1))} 它們初始狀態(tài) (.,(.,.))是弱狀態(tài)互擬的，讀者可驗(yàn)證各對(duì)互擬狀態(tài)是否成立，案例來(lái)自 【 20】 。 第五章 協(xié)議驗(yàn)證技術(shù) b ! 1 a ? 0b ! 0a ? 1b ! 1b ! 1b ! 0b ! 00 100 0 1 1 11 0a ? 0 a ? 0 a ? 1 a ? 1o oa bb ! 1IIa ? 10 , 10 , 0 , 0, 1 1 , 1, , 01 , 1 , 0a ? 0a ? 0a ? 1a ? 1a ? 0b ! 0 b ! 0 b ! 0b ! 1 b ! 1o oa bFSM的弱觀察等價(jià) 第五章 協(xié)議驗(yàn)證技術(shù) 基于 CCS的觀察等價(jià)性分析 上節(jié)定義的觀察等價(jià)性可直接引入到 CCS表達(dá)式。 兩個(gè)系統(tǒng)的行為表達(dá)式 B1和 B2是強(qiáng)觀察等價(jià)的充分必要條件是它們對(duì)應(yīng)的狀態(tài)轉(zhuǎn)換系統(tǒng)是強(qiáng)觀察等價(jià)的，同樣，表達(dá)式 B1和 B2是弱觀察等價(jià)的充分必要條件是它們對(duì)應(yīng)的FSM是觀察等價(jià)的。 怎樣根據(jù) CCS表達(dá)式導(dǎo)出 FSM呢？ 第五章 協(xié)議驗(yàn)證技術(shù) 010 1 1 2.abCC S B a BB B B B???? ???1 2 2 3 0 1 20， ，一 個(gè) 表 達(dá) 式 總 能 寫(xiě) 成 遞 歸 形 式 ：B =b. B ,B =c. B ,.. ... . 這 里 B ,B ,B ,.. .就 是 FSM 的 狀 態(tài) 集 合 ， B 為 初 始 狀 態(tài) ； a,b,c,...為 事 件 的 集 合 ， ... 為 轉(zhuǎn) 換的 集 合 。 例 如 下 面 表 達(dá) 式 可 導(dǎo) 出 下 圖 所 示 的 FSMaBB 1 B 2C B 1C 1ab 1ddc. . . . ...B a b C c I d BC a d B???第五章 協(xié)議驗(yàn)證技術(shù) 觀察等價(jià)是 CCS和 LOTOS的理論基礎(chǔ)，它們所形成的代數(shù)變換規(guī)則有的基于強(qiáng)觀察等價(jià)性，有的基于弱觀察等價(jià)行。 CCS或 LOTOS表達(dá)式變換過(guò)程就是等價(jià)變換過(guò)程。第三章第 5節(jié)已給出了多個(gè) CCS表達(dá)式的實(shí)例，此處不再重復(fù)。
公司管理相關(guān)推薦
鄂ICP備17016276號(hào)-1