基于SCC空性检测中状态空间的缩减方法

作者：晏荣杰; 张文亮; 唐稚松

来源：计算机学报, 2008, (06): 979-988.

• 空性检测
• 基于迁移的扩展Büchi自动机
• 可接受条件 emptiness checking
• transition-based generalized Büchi automaton
• acceptance conditions

对Couvreur提出的基于强连通图的空性检测算法进行改进,使基于嵌套的深度优先搜索与基于强连通图搜索算法的优势结合起来,在对基于迁移的扩展(具有多个可接受条件)Büchi自动机进行空性检测过程中,使用一个布尔变量标识一个状态,不仅节省了内存消耗,而且一般情况下的性能明显优于已有的算法,最坏情况等同于Couvreur的算法.同时反例寻找过程等同于基于强连通图的检测算法.

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