基于雙格的多值模型精化關(guān)系及對稱化簡.pdf

1、模型檢測是一種自動驗證系統(tǒng)行為屬性的技術(shù)。傳統(tǒng)的模型檢測針對基于布爾邏輯建立的系統(tǒng)模型,要求對系統(tǒng)的所有行為給予確定的描述。然而,在軟件開發(fā)的許多階段,如在需求分析階段,由于用戶的要求不明確以及觀點的不一致,模型中可能包含不確定或不一致信息,傳統(tǒng)布爾模型無法滿足此要求,而多值模型更適合在此類情況下進行建模和分析。多值模型一般采用基于德摩根代數(shù)的多值邏輯來定義,是傳統(tǒng)布爾模型的擴展。與傳統(tǒng)模型檢測類似,多值模型檢測也存在狀態(tài)爆炸問題。精化

2、關(guān)系是采用抽象和對稱化簡等方法解決狀態(tài)爆炸問題的基礎(chǔ),用來刻畫系統(tǒng)的具體模型和約簡模型之間相對于時序邏輯所描述的行為屬性的保持關(guān)系。現(xiàn)有的針對多值模型的精化關(guān)系定義過強,適用范圍受到限制。因此,我們提出了一種新的更加通用的多值模型精化關(guān)系,并且以此為基礎(chǔ)研究了多值模型的對稱化簡方法。
　　我們以世界雙格作為理論基礎(chǔ),其中的邏輯值之間存在兩種序關(guān)系:真值序關(guān)系與信息序關(guān)系。任意一個德摩根代數(shù)均同構(gòu)于世界雙格的一個子格;同時,對行為屬

3、性的模型檢測可根據(jù)邏輯值的真值序關(guān)系定義,而模型檢測結(jié)果的精確度以及具體模型和約簡模型之間的屬性保持關(guān)系則可根據(jù)邏輯值的信息序關(guān)系定義。為此,我們首先定義了基于世界雙格的多值模型,以及時序邏輯μ演算所對應(yīng)的語義。然后,我們從兩個角度刻畫了新的多值模型的精化關(guān)系:(i)通過將多值模型分解為三值模型進行刻畫,(ii)直接針對多值模型的結(jié)構(gòu)進行刻畫;證明了這兩種刻畫等價,是具體模型與約簡模型滿足對μ演算公式的模型檢測保持信息序關(guān)系的充分必要條