桂林电子科技大学学报
桂林電子科技大學學報
계림전자과기대학학보
JOURNAL OF GUILIN UNIVERSITY OF ELECTRONIC TECHNOLOGY
2013年
4期
300-304
,共5页
状态爆炸%可达性%自动机%符号
狀態爆炸%可達性%自動機%符號
상태폭작%가체성%자동궤%부호
state explosion%reachability%automata technology%symbol
为了缓解模型检测并发程序中出现的状态爆炸问题,将并发程序建模成异步动态下推网络,同时将异步动态下推网络转化为异步下推网络,在异步下推网络下提出一种基于自动机的符号可达算法.该算法能避免精确搜索每一个状态空间,有效地缓解了状态爆炸.
為瞭緩解模型檢測併髮程序中齣現的狀態爆炸問題,將併髮程序建模成異步動態下推網絡,同時將異步動態下推網絡轉化為異步下推網絡,在異步下推網絡下提齣一種基于自動機的符號可達算法.該算法能避免精確搜索每一箇狀態空間,有效地緩解瞭狀態爆炸.
위료완해모형검측병발정서중출현적상태폭작문제,장병발정서건모성이보동태하추망락,동시장이보동태하추망락전화위이보하추망락,재이보하추망락하제출일충기우자동궤적부호가체산법.해산법능피면정학수색매일개상태공간,유효지완해료상태폭작.
