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

• 作者: 张文辉 易锦
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 模型检测 Büchi自动机 LTL(linear temporal logic)公式 TGBA(transition-based generalized Büchi automaton)
• 年，卷（期）: 2006,（4）
• 所属期刊栏目: 理论计算机科学
• 页码范围: 720-728
• 页数: 9页
• 分类号: TP301
• 字数: 9607字
• 语种: 中文

摘要

目前的模型检测方法中,有一种方法是基于自动机来实现的.具体做法是:将抽象出的系统模型用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自动机的求交运算,减少了需要复制的状态个数,使转换后的自动机具有较少的状态.测试的结果表明:对随机产生的公式,新算法相对于以往的算法有明显的优势.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张文辉		5	22	3.0	4.0