摘要
稠密时间自动机被广泛应用于实时系统自动验证.然而其在补操作下不封闭,因而导致多种线性实时性质不可验证.离散时间自动机虽不存在此问题,但该模型表达能力偏弱.因此,提出了一种时间自动机时钟离散化算法,结合时钟物理约束因素,证明了新方法可有效解决上述问题.
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.
出处
《郑州大学学报(理学版)》
CAS
北大核心
2011年第3期70-72,共3页
Journal of Zhengzhou University:Natural Science Edition
基金
国家(863)高技术研究发展计划项目
编号2007AA010408
国家自然科学基金青年基金资助项目
编号61003079
60901078
河南省重大科技攻关计划项目
编号092101210104
关键词
时间自动机
模型检测
物理时钟
离散化
timed automata
model checking
physical clocks
discretization