从基于迁移的扩展Büchi自动机到Büchi自动机  

Efficient Translation from Transition-Based Generalized Büchi Automata to Büchi Automata

作　　者：易锦[1] 张文辉[1] 

机构地区：[1]中国科学院软件研究所计算机科学重点实验室

出　　处：《软件学报》2006年第4期720-728,共9页Journal of Software

基　　金：国家自然科学基金;国家重点基础研究发展规划(973)~~

摘　　要：目前的模型检测方法中,有一种方法是基于自动机来实现的.具体做法是:将抽象出的系统模型用Büchi自动机来表示,将需要验证的性质用LTL(lineartemporallogic)公式来表达;然后将LTL公式取反后转化为Büchi自动机,并检查这两个自动机接受语言之间的包含关系.有一类LTL公式转化为Büchi自动机的算法是:在计算过程中,首先得到一个标注在迁移上的扩展Büchi自动机(transition-basedgeneralizedBüchiautomaton,简称TGBA),然后把这种扩展Büchi自动机转换成非扩展的Büchi自动机.针对这类转换算法,根据Büchi自动机接受语言的特点,重新定义了基于迁移的扩展Büchi自动机的求交运算,减少了需要复制的状态个数,使转换后的自动机具有较少的状态.测试的结果表明:对随机产生的公式,新算法相对于以往的算法有明显的优势.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 translating LTL formulas to Büchi automata has one two automata is non-empty. One type of methods for 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.

关 键 词：模型检测 Büehi自动机 LTL 公式 TGBA 

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