###
DOI:
Journal of Software:2006.17(4):720-728

从基于迁移的扩展Büchi自动机到Büchi自动机
易锦,张文辉
(中国科学院,软件研究所,计算机科学重点实验室,北京,100080;中国科学院,研究生院,信息与工程学院,北京,100049)
Efficient Translation from Transition-Based Generalized Büchi Automata to Büchi Automata
YI Jin,ZHANG Wen-Hui
()
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 3102   Download 3250
Received:November 22, 2004    Revised:October 27, 2005
> 中文摘要: 目前的模型检测方法中,有一种方法是基于自动机来实现的.具体做法是:将抽象出的系统模型用Büchi自动机来表示,将需要验证的性质用LTL(linear temporal logic)公式来表达;然后将LTL公式取反后转化为Büchi自动机,并检查这两个自动机接受语言之间的包含关系.有一类LTL公式转化为Büchi自动机的算法是:在计算过程中,首先得到一个标注在迁移上的扩展Büchi自动机(transition-based generalized Büchi automaton,简称TGBA),然后把这种扩展Büchi自动机转换成非扩展的Büchi自动机.针对这类转换算法,根据Büchi自动机接受语言的特点,重新定义了基于迁移的扩展Büchi自动机的求交运算,减少了需要复制的状态个数,使转换后的自动机具有较少的状态.测试的结果表明:对随机产生的公式,新算法相对于以往的算法有明显的优势.
Abstract:The automata-theoretic approach is one of the state-of-the-art model-checking methods, which consists of the following steps: use a Büchi automaton to represent the abstract system model; use an LTL formula to express the properties to be verified; translate the negation of the LTL formula to a Büchi automaton and check whether the intersection of sentences accepted by the two automata is non-empty. One type of methods for translating LTL formulas to Büchi automata has one step for calculating transition-based generalized Büchi automata (TGBA) and another step for translating TGBA to Büchi automata. This paper redefines the product operation of TGBA according to the characteristics of the accepting language of Büchi automata. This leads to the reduction of the number of states that need to be copied and therefore smaller Büchi automata. The experimental results given at the end of this paper demonstrate the advantage of the approach based on test cases with randomly generated formulas.
文章编号:     中图分类号:    文献标志码:
基金项目:Supported by the National Natural Science Foundation of China under Grant Nos.60223005, 60373050, 60421001, 60573012 (国家自然科学基金); the National Grand Fundamental Research 973 Program of China under Grant No.2002cb312200 (国家重点基础研究发展规划(973)) Supported by the National Natural Science Foundation of China under Grant Nos.60223005, 60373050, 60421001, 60573012 (国家自然科学基金); the National Grand Fundamental Research 973 Program of China under Grant No.2002cb312200 (国家重点基础研究发展规划(973))
Foundation items:
Reference text:

易锦,张文辉.从基于迁移的扩展Büchi自动机到Büchi自动机.软件学报,2006,17(4):720-728

YI Jin,ZHANG Wen-Hui.Efficient Translation from Transition-Based Generalized Büchi Automata to Büchi Automata.Journal of Software,2006,17(4):720-728