计算机工程与应用
計算機工程與應用
계산궤공정여응용
COMPUTER ENGINEERING AND APPLICATIONS
2013年
22期
40-45
,共6页
陈娟娟%魏欧%黄志球%陈哲
陳娟娟%魏歐%黃誌毬%陳哲
진연연%위구%황지구%진철
多值模型检测%精化关系%对称化简
多值模型檢測%精化關繫%對稱化簡
다치모형검측%정화관계%대칭화간
multi-valued%model checking%refinement%symmetry reduction
多值模型是传统布尔模型的扩展。与布尔模型相比，多值模型更适合对包含不确定和不一致信息的软件系统进行建模。为了解决模型检测时的状态爆炸问题，研究了对基于双格的多值模型的对称化简方法。提出了一种新的多值模型的精化关系，证明其保持对μ演算公式的模型检测结果的正确性。定义多值模型的对称化简商结构，证明商结构与原模型之间存在互为精化的关系，因此对μ演算公式的模型检测在二者上可以得到相同的结果。
多值模型是傳統佈爾模型的擴展。與佈爾模型相比，多值模型更適閤對包含不確定和不一緻信息的軟件繫統進行建模。為瞭解決模型檢測時的狀態爆炸問題，研究瞭對基于雙格的多值模型的對稱化簡方法。提齣瞭一種新的多值模型的精化關繫，證明其保持對μ縯算公式的模型檢測結果的正確性。定義多值模型的對稱化簡商結構，證明商結構與原模型之間存在互為精化的關繫，因此對μ縯算公式的模型檢測在二者上可以得到相同的結果。
다치모형시전통포이모형적확전。여포이모형상비，다치모형경괄합대포함불학정화불일치신식적연건계통진행건모。위료해결모형검측시적상태폭작문제，연구료대기우쌍격적다치모형적대칭화간방법。제출료일충신적다치모형적정화관계，증명기보지대μ연산공식적모형검측결과적정학성。정의다치모형적대칭화간상결구，증명상결구여원모형지간존재호위정화적관계，인차대μ연산공식적모형검측재이자상가이득도상동적결과。
Multi-valued model is an extension of classical boolean model, which is appropriate for modeling software systems with incomplete and uncertain information. This paper investigates symmetry reduction over bilattice-based multi-valued models. A new refinement relation between the multi-valued models is proposed, which preserves modeling checking of μ-calculus . The symmetry-reduced quotient structure of a multi-valued model is defined, and it is showed that the quotient structure and the original model refines each other w.r.t. the refinement relation. This allows for the same model checking results of μ-calculus formulas over them.
