%0 Journal Article
%T 实时模型检测中基于驻留环的精确加速
%A 尹传龙
%A 庄雷
%A 王从银
%J 电子学报
%P 489-493
%D 2011
%X 在控制系统和外界环境之间经常会出现时间度量差距.对这些系统用时间自动机建模,并运用符号模型检测技术进行验证时,会引起符号状态空间的片段问题.精确加速技术在不改变系统可达性的前提下解决了片段问题.针对可加速环引起的片段问题,本文提出一种基于驻留环实现精确加速的方法.驻留环的长度固定,不依赖于可加速环的窗口,因而构造的自动机模型更简单,能提高精确加速的速度,并能够降低精确加速的时间和空间开销.
%K 模型检测
%K 时间自动机
%K 可加速环
%K 精确加速
%K 驻留环
%U http://www.ejournal.org.cn/CN/abstract/abstract1983.shtml