计算机工程与科学
計算機工程與科學
계산궤공정여과학
Computer Engineering and Science
2015年
11期
2162-2168
,共7页
并发系统%广义可能性决策过程%广义可能性计算树逻辑%模型检测
併髮繫統%廣義可能性決策過程%廣義可能性計算樹邏輯%模型檢測
병발계통%엄의가능성결책과정%엄의가능성계산수라집%모형검측
concurrent systems%generalized possibilistic decision process%generalized possibilistic computation tree logic (GPCTL)%model checking
模型检测作为一种形式化验证技术,已被广泛应用于各种并发系统的正确性验证.针对具有非确定性选择和广义可能性分布的并发系统,引入广义可能性决策过程作为此类系统的模型;给出描述其性质的规范语言广义可能性计算树逻辑的概念;研究此类系统的广义可能性计算树逻辑模型检测问题.结论表明,其模型检测算法的时间复杂度也为多项式时间.所获得的结果扩大了广义可能性测度在模型检测中的应用范围.
模型檢測作為一種形式化驗證技術,已被廣汎應用于各種併髮繫統的正確性驗證.針對具有非確定性選擇和廣義可能性分佈的併髮繫統,引入廣義可能性決策過程作為此類繫統的模型;給齣描述其性質的規範語言廣義可能性計算樹邏輯的概唸;研究此類繫統的廣義可能性計算樹邏輯模型檢測問題.結論錶明,其模型檢測算法的時間複雜度也為多項式時間.所穫得的結果擴大瞭廣義可能性測度在模型檢測中的應用範圍.
모형검측작위일충형식화험증기술,이피엄범응용우각충병발계통적정학성험증.침대구유비학정성선택화엄의가능성분포적병발계통,인입엄의가능성결책과정작위차류계통적모형;급출묘술기성질적규범어언엄의가능성계산수라집적개념;연구차류계통적엄의가능성계산수라집모형검측문제.결론표명,기모형검측산법적시간복잡도야위다항식시간.소획득적결과확대료엄의가능성측도재모형검측중적응용범위.
