摘要：在控制系统和外界环境之间经常会出现时间度量差距.对这些系统用时间自动机建模,并运用符号模型检测技术进行验证时,会引起符号状态空间的片段问题.精确加速技术在不改变系统可达性的前提下解决了片段问题.针对可加速环引起的片段问题,本文提出一种基于驻留环实现精确加速的方法.驻留环的长度固定,不依赖于可加速环的窗口,因而构造的自动机模型更简单,能提高精确加速的速度,并能够降低精确加速的时间和空间开销.

关键词：模型检测 时间自动机 可加速环 精确加速 驻留环 

单位：郑州大学信息工程学院; 河南郑州450052; 吉首大学数学与计算机科学学院; 湖南吉首416000