计算机工程与设计
計算機工程與設計
계산궤공정여설계
COMPUTER ENGINEERING AND DESIGN
2013年
10期
3685-3689
,共5页
纪明宇%王海涛%陈志远%李艳梅
紀明宇%王海濤%陳誌遠%李豔梅
기명우%왕해도%진지원%리염매
形式化验证%模型检测%状态空间爆炸%决策图%对称约减%商模型
形式化驗證%模型檢測%狀態空間爆炸%決策圖%對稱約減%商模型
형식화험증%모형검측%상태공간폭작%결책도%대칭약감%상모형
formal verification%model checking%state space explosion%decision diagram%symmetry reduction%quotient model
针对复杂随机系统模型检测过程中的状态空间爆炸问题,提出一种用于支持迁移回报特征描述的概率模型对称约减方法.通过引入状态集等价关系唯一表示函数,约减了原模型中的状态集尺寸;通过加入回报特征描述,改进了传统的多终端二元决策图,用于表示概率回报模型中的迁移关系;基于迁移矩阵,提出了一种高效的对称约减算法,完成了迁移关系的约简.实验结果表明了该方法的可行性与有效性.
針對複雜隨機繫統模型檢測過程中的狀態空間爆炸問題,提齣一種用于支持遷移迴報特徵描述的概率模型對稱約減方法.通過引入狀態集等價關繫唯一錶示函數,約減瞭原模型中的狀態集呎吋;通過加入迴報特徵描述,改進瞭傳統的多終耑二元決策圖,用于錶示概率迴報模型中的遷移關繫;基于遷移矩陣,提齣瞭一種高效的對稱約減算法,完成瞭遷移關繫的約簡.實驗結果錶明瞭該方法的可行性與有效性.
침대복잡수궤계통모형검측과정중적상태공간폭작문제,제출일충용우지지천이회보특정묘술적개솔모형대칭약감방법.통과인입상태집등개관계유일표시함수,약감료원모형중적상태집척촌;통과가입회보특정묘술,개진료전통적다종단이원결책도,용우표시개솔회보모형중적천이관계;기우천이구진,제출료일충고효적대칭약감산법,완성료천이관계적약간.실험결과표명료해방법적가행성여유효성.
