计算机研究与发展
計算機研究與髮展
계산궤연구여발전
JOURNAL OF COMPUTER RESEARCH AND DEVELOPMENT
2002年
5期
607-611
,共5页
宋煌%庄雷%苏锦祥%周清雷
宋煌%莊雷%囌錦祥%週清雷
송황%장뢰%소금상%주청뢰
时间转换表%时间自动机%区域自动机%时间后继%区域可达
時間轉換錶%時間自動機%區域自動機%時間後繼%區域可達
시간전환표%시간자동궤%구역자동궤%시간후계%구역가체
用时间自动机验证一个有穷状态实时系统的正确性,可归结为判定两个时间正则语言的包含问题,亦可归结为判定两个时间正则语言的交是否为空的问题.在判定一个时间正则语言是否为空时,先要将时间自动机转化为无时间的区域自动机.Alur和Dill给出的构造区域自动机的算法,存在许多不可达或虽可达但无用的状态.通过对时钟约束进行分析,在求时钟区域和时间后继的过程中,不断地将一些不可达或无用状态筛掉,使构造出的区域自动机更为优化,改进了Alur等人给出的算法.
用時間自動機驗證一箇有窮狀態實時繫統的正確性,可歸結為判定兩箇時間正則語言的包含問題,亦可歸結為判定兩箇時間正則語言的交是否為空的問題.在判定一箇時間正則語言是否為空時,先要將時間自動機轉化為無時間的區域自動機.Alur和Dill給齣的構造區域自動機的算法,存在許多不可達或雖可達但無用的狀態.通過對時鐘約束進行分析,在求時鐘區域和時間後繼的過程中,不斷地將一些不可達或無用狀態篩掉,使構造齣的區域自動機更為優化,改進瞭Alur等人給齣的算法.
용시간자동궤험증일개유궁상태실시계통적정학성,가귀결위판정량개시간정칙어언적포함문제,역가귀결위판정량개시간정칙어언적교시부위공적문제.재판정일개시간정칙어언시부위공시,선요장시간자동궤전화위무시간적구역자동궤.Alur화Dill급출적구조구역자동궤적산법,존재허다불가체혹수가체단무용적상태.통과대시종약속진행분석,재구시종구역화시간후계적과정중,불단지장일사불가체혹무용상태사도,사구조출적구역자동궤경위우화,개진료Alur등인급출적산법.
