计算机工程与科学
計算機工程與科學
계산궤공정여과학
Computer Engineering and Science
2015年
10期
1884-1889
,共6页
三值逻辑%模型检测%扩展的不完全Kripke结构
三值邏輯%模型檢測%擴展的不完全Kripke結構
삼치라집%모형검측%확전적불완전Kripke결구
three-valued logic%model checking%extensional partial Kripke structure
多值模型检测是解决形式化验证中状态爆炸问题的一种重要方法,三值模型检测是多值模型检测的基础,其中如何检验不确定状态的真值是一难点.针对不确定状态检验,提出了一种模型检测方法,首先对不完全Kripke结构PKS进行了扩展,然后在扩展后的模型上给出了检测不确定状态真值的方法,最后给出了基于扩展不完全Kripke结构的三值逻辑模型检测算法.与已有的三值逻辑模型检测算法相比,该算法降低了算法复杂度,完善了对于不确定或不一致信息的处理,从而增强了三值逻辑模型检测的实用性.
多值模型檢測是解決形式化驗證中狀態爆炸問題的一種重要方法,三值模型檢測是多值模型檢測的基礎,其中如何檢驗不確定狀態的真值是一難點.針對不確定狀態檢驗,提齣瞭一種模型檢測方法,首先對不完全Kripke結構PKS進行瞭擴展,然後在擴展後的模型上給齣瞭檢測不確定狀態真值的方法,最後給齣瞭基于擴展不完全Kripke結構的三值邏輯模型檢測算法.與已有的三值邏輯模型檢測算法相比,該算法降低瞭算法複雜度,完善瞭對于不確定或不一緻信息的處理,從而增彊瞭三值邏輯模型檢測的實用性.
다치모형검측시해결형식화험증중상태폭작문제적일충중요방법,삼치모형검측시다치모형검측적기출,기중여하검험불학정상태적진치시일난점.침대불학정상태검험,제출료일충모형검측방법,수선대불완전Kripke결구PKS진행료확전,연후재확전후적모형상급출료검측불학정상태진치적방법,최후급출료기우확전불완전Kripke결구적삼치라집모형검측산법.여이유적삼치라집모형검측산법상비,해산법강저료산법복잡도,완선료대우불학정혹불일치신식적처리,종이증강료삼치라집모형검측적실용성.
