%0 Journal Article
%T 有限精度时间自动机的可达性检测
%A 晏荣杰？
%A 李广元？
%A 徐雨波？
%A 刘春明？
%A 唐稚松？
%J 软件学报
%P 1-10
%D 2006
%X 为了缓解状态空间爆炸问题,减小模型检测过程中生成的状态空间,加快模型检测速度,引入有限精度时间自动机(finiteprecisiontimedautomata,简称fpta)作为实时系统的形式模型,并提出了一种数据结构sds(seriesofdelaysequence)符号化表示状态空间中的状态集.fpta只记录时钟变量的整数值及时钟变化的先后次序,从而减小生成的状态空间.在一定的时间约束下,alur与dill提出的时间自动机的可达性检测可简化为fpta的可达性检测.举例描述了状态空间的生成过程和表示方法.最后,列出部分初步的实验结果,分析了sds的特点及不足.
%K 有限精度时间自动机
%K 符号化方法
%K 模型检测
%K 可达性
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=20060101&flag=1