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

Truly Bitstate-Hashing for SCC-Based Emptiness Checking Algorithms

作　　者：晏荣杰[1] 张文亮[1] 唐稚松[1] 

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

出　　处：《计算机学报》2008年第6期979-988,共10页Chinese Journal of Computers

基　　金：国家“九七三”重点基础研究发展规划项目基金(2002cb312200);国家自然科学基金(60273025,60223005,60421001)资助~~

摘　　要：对Couvreur提出的基于强连通图的空性检测算法进行改进,使基于嵌套的深度优先搜索与基于强连通图搜索算法的优势结合起来,在对基于迁移的扩展(具有多个可接受条件)Büchi自动机进行空性检测过程中,使用一个布尔变量标识一个状态,不仅节省了内存消耗,而且一般情况下的性能明显优于已有的算法,最坏情况等同于Couvreur的算法.同时反例寻找过程等同于基于强连通图的检测算法.The paper proposes an improvement for SCC-based emptiness checking algorithms, which combines the advantages of SCC-based and nested depth first search for finding a cycle meeting all sets of acceptance conditions. The new algorithm uses the method of bitstate-hashing during emptiness checking for transition based generalized Büchi automata, and the performance outperforms that of Couvreur＇s. Meanwhile, the performance for finding a counterexample is the same as that of SCC-based ones.

关 键 词：空性检测 基于迁移的扩展Büchi自动机 可接受条件 

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