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

作者：易锦; 张文辉

来源：软件学报, 2006, (04): 720-728.

• 模型检测
• Büchi自动机
• LTL(linear temporal logic)公式
• TGBA(transition-based generalized Büchiautomaton) model checking
• Büchi automata
• LTL (linear temporal logic)
• TGBA (transition-based generalized Büchi automaton)

目前的模型检测方法中,有一种方法是基于自动机来实现的.具体做法是:将抽象出的系统模型用Büchi自动机来表示,将需要验证的性质用LTL(lineartemporallogic)公式来表达;然后将LTL公式取反后转化为Büchi自动机,并检查这两个自动机接受语言之间的包含关系.有一类LTL公式转化为Büchi自动机的算法是:在计算过程中,首先得到一个标注在迁移上的扩展Büchi自动机(transition-basedgeneralizedBüchiautomaton,简称TGBA),然后把这种扩展Büchi自动机转换成非扩展的Büchi自动机.针对这类转换算法,根据Büchi自动机接受语言的特点...

• 单位
  中国科学院软件研究所; 中国科学院研究生院; 计算机科学国家重点实验室