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

Constructing transition-based generalized timed Buhi automata for metric interval temporal logic

作　　者：王勤思[1,2] 

机构地区：[1]中国科学院软件研究所计算机科学重点实验室,北京100190 [2]中国科学院研究生院,北京100049

出　　处：《计算机工程与设计》2011年第2期568-571,575,共5页Computer Engineering and Design

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

摘　　要：在实时系统的形式验证中,为了直接验证带有明显时间约束的性质,选用了一种被广泛接受的(线性时间)实时时序逻辑——度量区时序逻辑来描述待验证的性质;提出了基于迁移的扩展时间B chi自动机;构建了度量区时序逻辑的基于迁移的扩展时间B chi自动机。这样扩展了已有实时系统模型检测工具的性质规范语言的表达能力,使其能直接处理和验证带有明显时间约束的性质。实现的工具表明,该算法有效且可行,并且显著地减少了结果自动机节点和迁移的数量,从而降低了结果自动机的大小,有利于进一步的模型检测过程。In order to model check real-time systems against properties with explicit timing constraints whieh cannot be expressed by any temporal logic directly, a widely accepted formalism - metric interval temporal logic-is used to describe the real-time properties to be checked. Then, a novel formalism of automaton - timed transition-based generalized B^chi automata - is promoted. Finally, the algorithm according to which the metric interval temporal logic formulae are translated to equal timed transition-based generalized Buchi automata is given. In this way, the existing model checkers for real-time systems are extended to be able to straightforwardly check pro- perties with explicit timing constraints. A tool is also implemented to prove the feasibility and validity of the proposed method, and show that the numbers of both locations and transitions of result automata are reduced significantly, which will benefit the whole proeess of model checking real-time systems.

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

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]