构建度量区时序逻辑的时间自动机

作     者：王勤思 WANG Qin-si

作者机构：中国科学院软件研究所计算机科学重点实验室北京100190 中国科学院研究生院北京100049 

基　　金：国家自然科学基金项目(60673051 60736017 60873260) 

出 版 物：《计算机工程与设计》 (Computer Engineering and Design)

年 卷 期：2011年第32卷第2期

页      码：568-571,575页

摘      要：在实时系统的形式验证中,为了直接验证带有明显时间约束的性质,选用了一种被广泛接受的(线性时间)实时时序逻辑——度量区时序逻辑来描述待验证的性质;提出了基于迁移的扩展时间B chi自动机;构建了度量区时序逻辑的基于迁移的扩展时间B chi自动机。这样扩展了已有实时系统模型检测工具的性质规范语言的表达能力,使其能直接处理和验证带有明显时间约束的性质。实现的工具表明,该算法有效且可行,并且显著地减少了结果自动机节点和迁移的数量,从而降低了结果自动机的大小,有利于进一步的模型检测过程。

主 题 词：模型检测 实时时序逻辑 度量区时序逻辑 基于迁移的扩展时间Buchi自动机 Tableau方法 

学科分类：08[工学] 081202[081202] 0812[工学-测绘类] 

D　O　I：10.16208/j.issn1000-7024.2011.02.035

馆 藏 号：203218739...