电子学报2011，Vol.39Issue(3)：489-493,5.
实时模型检测中基于驻留环的精确加速
Exact Acceleration of Real-Time Model Checking Based on Parking Cycle
摘要
Abstract
Different time scales are often found between control systems and their environments. When these systems are modeled as timed automata, such difference can lead to fragmentation of the symbolic state space in the process of applying symbolic model checking techniques to the validation of them. Exact acceleration addresses the fragmentation problem without any side-effect to the reachability properties of the system under consideration. To address the fragmentation problems s caused by the acceleratable cycles,this paper introduces an exact acceleration technique based on parking cycle. The length of the parking cycle is constant,wifthout dependency on the window of fthe accelerartable cycles,and so makes fthe constructed acceleration simpler,the process of the exact acceleration faster, and both the time cost and the space cost of exact acceleration can be greatly reduced.关键词
模型检测/时间自动机/可加速环/精确加速/驻留环Key words
model checking/tired automata/acceleratabie cycle/exact acceleration/parking cycle分类
信息技术与安全科学引用本文复制引用
尹传龙,庄雷,王从银..实时模型检测中基于驻留环的精确加速[J].电子学报,2011,39(3):489-493,5.基金项目
河南省重大科技攻关(No.092101210104) （No.092101210104）
郑州市产学研专项(No.085SCXY00015) （No.085SCXY00015）
