###
DOI:
Journal of Software:2006.17(1):1-10

有限精度时间自动机的可达性检测
晏荣杰,李广元,徐雨波,刘春明,唐稚松
(中国科学院 软件研究所 计算机科学重点实验室,北京 100080;中国科学院 研究生院,北京 100049)
Reachability Checking of Finite Precision Timed Automata
Yan RJ,Li GY,Xu YB,Liu CM,Tang ZS
()
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 4032   Download 3195
Received:April 28, 2004    Revised:July 11, 2005
> 中文摘要: 为了缓解状态空间爆炸问题,减小模型检测过程中生成的状态空间,加快模型检测速度,引入有限精度时间自动机(finite precision timed automata,简称FPTA)作为实时系统的形式模型,并提出了一种数据结构SDS(series of delay sequence)符号化表示状态空间中的状态集.FPTA只记录时钟变量的整数值及时钟变化的先后次序,从而减小生成的状态空间.在一定的时间约束下,Alur与Dill提出的时间自动机的可达性检测可简化为FPTA的可达性检测.举例描述了状态空间的生成过程和表示方法.最后,列出部分初步的实验结果,分析了SDS的特点及不足.
Abstract:To relieve the state space explosion problem, and accelerate the speed of model checking, this paper introduces the concept of finite precision timed automata (FPTAs) and proposes a data structure to represent its symbolic states. FPTAs only record the integer values of clock variables together with the order of their most recent resets to reduce the state space. The constraints under which the reachability checking of a timed automaton can be reduced to that of the corresponding FPTA are provided, and then an algorithm for reachability analysis is presented. Finally, the paper presents some preliminary experimental results, and analyzes the advantages and disadvantages of the new data structure.
文章编号:     中图分类号:    文献标志码:
基金项目:the National Natural Science Foundation of China under Grant Nos.60273025, 60223005, 60421001 (国家自然科学基金); the National Grand Fundamental Research 973 Program of China under Grant No.2002cb312200 (国家重点基础研究发展规划(973)) the National Natural Science Foundation of China under Grant Nos.60273025, 60223005, 60421001 (国家自然科学基金); the National Grand Fundamental Research 973 Program of China under Grant No.2002cb312200 (国家重点基础研究发展规划(973))
Foundation items:
Reference text:

晏荣杰,李广元,徐雨波,刘春明,唐稚松.有限精度时间自动机的可达性检测.软件学报,2006,17(1):1-10

Yan RJ,Li GY,Xu YB,Liu CM,Tang ZS.Reachability Checking of Finite Precision Timed Automata.Journal of Software,2006,17(1):1-10