摘要：基于自动机理论模型检测的一个关键算法是判断有穷状态系统是否满足属性的判空检测．对标准Bachi自动机作判空检测，容易引起状态爆炸．本文以TGBA为研究对象，提出基于启发式SCCs的广义Btichi自动机判空检测算法．该算法在on-the-fly算法的基础上结合启发式深度优先搜索和SCCs检测算法，能较快地判断TGBA的非空性．通过正确性证明、复杂性分析和实验验证了该算法的正确可行性．在TGBA非空的情况下，该算法的时空性能比已有算法更优．

关键词：模型检测 buchi自动机 判空检测 

单位：同济大学电子与信息工程学院; 上海201804