有限精度时间自动机的可达性检测

• 作者: 刘春明 唐稚松 徐雨波 晏荣杰 李广元
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 有限精度时间自动机 符号化方法 模型检测 可达性
• 年，卷（期）: 2006,（1）
• 所属期刊栏目: 理论计算机科学
• 页码范围: 1-10
• 页数: 10页
• 分类号: TP301
• 字数: 10727字
• 语种: 中文

摘要

为了缓解状态空间爆炸问题,减小模型检测过程中生成的状态空间,加快模型检测速度,引入有限精度时间自动机(finite precision timed automata,简称FPTA)作为实时系统的形式模型,并提出了一种数据结构SDS(series ofdelay sequence)符号化表示状态空间中的状态集.FPTA只记录时钟变量的整数值及时钟变化的先后次序,从而减小生成的状态空间.在一定的时间约束下,Alur与Dill提出的时间自动机的可达性检测可简化为FPTA的可达性检测.举例描述了状态空间的生成过程和表示方法.最后,列出部分初步的实验结果,分析了SDS的特点及不足.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李广元		3	81	3.0	3.0