一种时间自动机时钟离散化算法

摘要

稠密时间自动机被广泛应用于实时系统自动验证.然而其在补操作下不封闭,因而导致多种线性实时性质不可验证.离散时间自动机虽不存在此问题,但该模型表达能力偏弱.因此,提出了一种时间自动机时钟离散化算法,结合时钟物理约束因素,证明了新方法可有效解决上述问题.%Some linear real-time properties can not be verified automatically because dense timed automata are not closed under complement operation. Discrete timed automata can be used to model checking discrete regular properties, but the express power of them is weak. A novel procedure was given to construct discrete timed automata from their dense time version. For physical factors of clock constrain, the new algorithm was used to solve the problem above efficiently.